theory Finalise_DR

lemma swap_for_delete_corres:
  "dcorres dc \<top> (valid_mdb and valid_idle and not_idle_thread (fst p)
                     and not_idle_thread (fst p') and valid_etcbs and (\<lambda>_. p \<noteq> p'))
      (swap_for_delete (transform_cslot_ptr p) (transform_cslot_ptr p'))
      (cap_swap_for_delete p p')" apply (rule corres_gen_asm2) apply (simp add: swap_for_delete_def cap_swap_for_delete_def when_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres[OF refl]])+ apply simp apply (rule swap_cap_corres) apply (wp get_cap_wp)+ apply simp apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs and (\<lambda>_. p \<noteq> p')) (swap_for_delete (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_swap_for_delete p p') proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs) (swap_for_delete (transform_cslot_ptr p) (transform_cslot_ptr p')) (cap_swap_for_delete p p') proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs) (do cap1 <- KHeap_D.get_cap (transform_cslot_ptr p);
cap2 <- KHeap_D.get_cap (transform_cslot_ptr p');
swap_cap cap1 (transform_cslot_ptr p) cap2 (transform_cslot_ptr p')
od) (do cap1 <- CSpaceAcc_A.get_cap p;
cap2 <- CSpaceAcc_A.get_cap p';
cap_swap cap1 p cap2 p'
od) proof (prove)
goal (3 subgoals):
 1. p \<noteq> p' \<Longrightarrow> dcorres dc ?Q2 ?Q'2 (do cap1 <- KHeap_D.get_cap (transform_cslot_ptr p);
cap2 <- KHeap_D.get_cap (transform_cslot_ptr p');
swap_cap cap1 (transform_cslot_ptr p) cap2 (transform_cslot_ptr p')
od) (do cap1 <- CSpaceAcc_A.get_cap p;
cap2 <- CSpaceAcc_A.get_cap p';
cap_swap cap1 p cap2 p'
od)
 2. \<And>s. \<lbrakk>p \<noteq> p'; True\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>p \<noteq> p'; (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (7 subgoals):
 1. \<And>cap1 cap1a cap2 cap2a. \<lbrakk>p \<noteq> p'; cap1 = transform_cap cap1a; cap2 = transform_cap cap2a\<rbrakk> \<Longrightarrow> dcorres dc (?R12 cap1 cap1a cap2) (?R'12 cap1 cap1a cap2a) (swap_cap cap1 (transform_cslot_ptr p) cap2 (transform_cslot_ptr p')) (cap_swap cap1a p cap2a p')
 2. \<And>cap1 cap1a. \<lbrakk>p \<noteq> p'; cap1 = transform_cap cap1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap1\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>?R12 cap1 cap1a\<rbrace>
 3. \<And>cap1 cap1a. \<lbrakk>p \<noteq> p'; cap1 = transform_cap cap1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 cap1a\<rbrace> CSpaceAcc_A.get_cap p' \<lbrace>?R'12 cap1 cap1a\<rbrace>
 4. p \<noteq> p' \<Longrightarrow> \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p) \<lbrace>\<lambda>cap1. (\<lambda>_. True) and ?Q15 cap1\<rbrace>
 5. p \<noteq> p' \<Longrightarrow> \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap p \<lbrace>\<lambda>cap1a. valid_idle and not_idle_thread (fst p') and valid_etcbs and ?Q'17 cap1a\<rbrace>
 6. \<And>s. \<lbrakk>p \<noteq> p'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. \<lbrakk>p \<noteq> p'; (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst p) and valid_etcbs and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>cap1 cap1a cap2 cap2a. \<lbrakk>p \<noteq> p'; cap1 = transform_cap cap1a; cap2 = transform_cap cap2a\<rbrakk> \<Longrightarrow> dcorres dc (?R12 (transform_cap cap1a) cap1a (transform_cap cap2a)) (?R'12 (transform_cap cap1a) cap1a cap2a) (swap_cap (transform_cap cap1a) (transform_cslot_ptr p) (transform_cap cap2a) (transform_cslot_ptr p')) (cap_swap cap1a p cap2a p')
 2. \<And>cap1 cap1a. \<lbrakk>p \<noteq> p'; cap1 = transform_cap cap1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap1\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>?R12 cap1 cap1a\<rbrace>
 3. \<And>cap1 cap1a. \<lbrakk>p \<noteq> p'; cap1 = transform_cap cap1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 cap1a\<rbrace> CSpaceAcc_A.get_cap p' \<lbrace>?R'12 cap1 cap1a\<rbrace>
 4. p \<noteq> p' \<Longrightarrow> \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p) \<lbrace>\<lambda>cap1. (\<lambda>_. True) and ?Q15 cap1\<rbrace>
 5. p \<noteq> p' \<Longrightarrow> \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap p \<lbrace>\<lambda>cap1a. valid_idle and not_idle_thread (fst p') and valid_etcbs and ?Q'17 cap1a\<rbrace>
 6. \<And>s. \<lbrakk>p \<noteq> p'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. \<lbrakk>p \<noteq> p'; (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst p) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>cap1 cap1a. \<lbrakk>p \<noteq> p'; cap1 = transform_cap cap1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap1\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p') \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>cap1 cap1a. \<lbrakk>p \<noteq> p'; cap1 = transform_cap cap1a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 cap1a\<rbrace> CSpaceAcc_A.get_cap p' \<lbrace>\<lambda>a. valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and valid_etcbs and K (p \<noteq> p') and not_idle_thread (fst p) and not_idle_thread (fst p')\<rbrace>
 3. p \<noteq> p' \<Longrightarrow> \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr p) \<lbrace>\<lambda>cap1. (\<lambda>_. True) and ?Q15 cap1\<rbrace>
 4. p \<noteq> p' \<Longrightarrow> \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap p \<lbrace>\<lambda>cap1a. valid_idle and not_idle_thread (fst p') and valid_etcbs and ?Q'17 cap1a\<rbrace>
 5. \<And>s. \<lbrakk>p \<noteq> p'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. \<lbrakk>p \<noteq> p'; (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst p) and valid_etcbs and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p \<noteq> p'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr p) s \<noteq> None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. opt_cap (transform_cslot_ptr p') a \<noteq> None \<longrightarrow> True)) s)) s
 2. \<And>s. \<lbrakk>p \<noteq> p'; (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst p) and valid_etcbs and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> (valid_idle and not_idle_thread (fst p') and valid_etcbs and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p' s \<longrightarrow> (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and valid_etcbs and K (p \<noteq> p') and not_idle_thread (fst p) and not_idle_thread (fst p')) s)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> p'; (valid_mdb and valid_idle and not_idle_thread (fst p) and not_idle_thread (fst p') and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst p) and valid_etcbs and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> (valid_idle and not_idle_thread (fst p') and valid_etcbs and (\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p' s \<longrightarrow> (valid_idle and valid_mdb and cte_wp_at (\<lambda>_. True) p and cte_wp_at (\<lambda>_. True) p' and valid_etcbs and K (p \<noteq> p') and not_idle_thread (fst p) and not_idle_thread (fst p')) s)) s)) s proof (prove)
goal:
No subgoals!