theory Refine

lemma absKState_correct:
assumes invs: "einvs (s :: det_ext state)" and invs': "invs' s'"
assumes rel: "(s,s') \<in> state_relation"
shows "absKState s' = abs_state s" using assms apply (intro state.equality, simp_all add: absKState_def abs_state_def) apply (rule absHeap_correct, clarsimp+) apply (clarsimp elim!: state_relationE) apply (rule absCDT_correct, clarsimp+) apply (rule absIsOriginalCap_correct, clarsimp+) apply (simp add: state_relation_def) apply (simp add: state_relation_def) apply (clarsimp simp:  user_mem_relation invs_def invs'_def) apply (simp add: state_relation_def) apply (rule absInterruptIRQNode_correct, simp add: state_relation_def) apply (rule absInterruptStates_correct, simp add: state_relation_def) apply (rule absArchState_correct, simp) apply (rule absExst_correct, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. absKState s' = abs_state s proof (prove)
using this:
einvs s
invs' s'
(s, s') \<in> state_relation

goal (1 subgoal):
 1. absKState s' = abs_state s proof (prove)
goal (10 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absHeap (gsUserPages s') (gsCNodes s') (ksPSpace s') = kheap s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksCurThread s' = cur_thread s
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksIdleThread s' = idle_thread s
 6. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> observable_memory (ksMachineState s') (user_mem' s') = observable_memory (machine_state s) (user_mem s)
 7. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 8. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 9. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 10. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (10 subgoals):
 1. \<lbrakk>invs' s'; (s, s') \<in> state_relation; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksCurThread s' = cur_thread s
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksIdleThread s' = idle_thread s
 6. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> observable_memory (ksMachineState s') (user_mem' s') = observable_memory (machine_state s) (user_mem s)
 7. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 8. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 9. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 10. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (9 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absCDT (cteMap (gsCNodes s')) (ctes_of s') = cdt s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksCurThread s' = cur_thread s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksIdleThread s' = idle_thread s
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> observable_memory (ksMachineState s') (user_mem' s') = observable_memory (machine_state s) (user_mem s)
 6. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 7. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 8. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 9. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (8 subgoals):
 1. \<lbrakk>invs' s'; (s, s') \<in> state_relation; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> absIsOriginalCap (cteMap (gsCNodes s')) (ksPSpace s') = is_original_cap s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksCurThread s' = cur_thread s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksIdleThread s' = idle_thread s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> observable_memory (ksMachineState s') (user_mem' s') = observable_memory (machine_state s) (user_mem s)
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 6. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 7. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 8. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>invs' s'; (s, s') \<in> state_relation; invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> ksCurThread s' = cur_thread s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksIdleThread s' = idle_thread s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> observable_memory (ksMachineState s') (user_mem' s') = observable_memory (machine_state s) (user_mem s)
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 6. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 7. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ksIdleThread s' = idle_thread s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> observable_memory (ksMachineState s') (user_mem' s') = observable_memory (machine_state s) (user_mem s)
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 6. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> observable_memory (ksMachineState s') (user_mem' s') = observable_memory (machine_state s) (user_mem s)
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_state s; valid_state' s'; cur_tcb' s'; cur_tcb s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> observable_memory (ksMachineState s') (user_mem s) = observable_memory (machine_state s) (user_mem s)
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptIRQNode (ksInterruptState s') = interrupt_irq_node s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absInterruptStates (ksInterruptState s') = interrupt_states s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absArchState (ksArchState s') = arch_state s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> absExst s' = exst s proof (prove)
goal:
No subgoals!