theory Refine

lemma absKState_correct':
  "\<lbrakk>einvs s; invs' s'; (s,s') \<in> state_relation\<rbrakk>
   \<Longrightarrow> absKState s' = abs_state s" apply (intro state.equality, simp_all add: absKState_def abs_state_def) apply (rule absHeap_correct) apply (clarsimp simp: valid_state_def valid_pspace_def)+ apply (clarsimp dest!: state_relationD) apply (rule absCDT_correct) apply (clarsimp simp: valid_state_def valid_pspace_def
                                      valid_state'_def valid_pspace'_def)+ 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 (erule absArchState_correct) apply (rule absExst_correct, simp, assumption+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> 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 (14 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_distinct s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> valid_objs s
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s')
 6. \<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
 7. \<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
 8. \<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
 9. \<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
 10. \<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)
A total of 14 subgoals... 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 (15 subgoals):
 1. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_distinct s
 3. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 4. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 5. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> valid_objs s
 6. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> valid_mdb s
 7. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; invs' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s, s') \<in> state_relation
 8. \<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
 9. \<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
 10. \<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
A total of 15 subgoals... 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!