theory Finalise_DR

lemma dcorres_deleting_irq_handler:
  "dcorres dc \<top> (invs and valid_etcbs)
     (CSpace_D.deleting_irq_handler word)
     (CSpace_A.deleting_irq_handler word)" apply (simp add:CSpace_D.deleting_irq_handler_def CSpace_A.deleting_irq_handler_def) apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_get_irq_slot]) apply (simp, rule delete_cap_simple_corres,simp) apply (rule hoare_vcg_precond_imp [where Q="invs and valid_etcbs"]) including no_pre apply (wpsimp simp:get_irq_slot_def)+ apply (rule irq_node_image_not_idle) apply (simp add:invs_def valid_state_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (CSpace_D.deleting_irq_handler word) (CSpace_A.deleting_irq_handler word) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs) (gets (CSpace_D.get_irq_slot word) >>= delete_cap_simple) (KHeap_A.get_irq_slot word >>= cap_delete_one) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (gets (CSpace_D.get_irq_slot word) >>= delete_cap_simple) (KHeap_A.get_irq_slot word >>= cap_delete_one)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (invs and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>rv slot. rv = transform_cslot_ptr slot \<Longrightarrow> dcorres dc (?R4 rv) (?R'4 slot) (delete_cap_simple rv) (cap_delete_one slot)
 2. \<lbrace>?Q4\<rbrace> gets (CSpace_D.get_irq_slot word) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> KHeap_A.get_irq_slot word \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> KHeap_A.get_irq_slot word \<lbrace>\<lambda>a. invs and not_idle_thread (fst a) and valid_etcbs\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 3. \<And>s. (invs and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>invs and valid_etcbs\<rbrace> KHeap_A.get_irq_slot word \<lbrace>\<lambda>a. invs and not_idle_thread (fst a) and valid_etcbs\<rbrace>
 2. \<And>s. ?Q'4 s \<Longrightarrow> (invs and valid_etcbs) s
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. (invs and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>invs and valid_etcbs\<rbrace> KHeap_A.get_irq_slot word \<lbrace>\<lambda>a. invs and not_idle_thread (fst a) and valid_etcbs\<rbrace>
 2. \<And>s. ?Q'4 s \<Longrightarrow> (invs and valid_etcbs) s
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. (invs and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>invs s; valid_etcbs s\<rbrakk> \<Longrightarrow> not_idle_thread (interrupt_irq_node s word) s
 2. \<And>s. ?Q'4 s \<Longrightarrow> (invs and valid_etcbs) s
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. (invs and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>invs s; valid_etcbs s\<rbrakk> \<Longrightarrow> valid_idle s
 2. \<And>s. \<lbrakk>invs s; valid_etcbs s\<rbrakk> \<Longrightarrow> valid_irq_node s
 3. \<And>s. ?Q'4 s \<Longrightarrow> (invs and valid_etcbs) s
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal:
No subgoals!