theory CNode_DR

lemma dcorres_ensure_empty:
  "dcorres (dc\<oplus>dc) \<top>  (valid_idle and not_idle_thread (fst slot) and valid_etcbs)
    (CSpace_D.ensure_empty (transform_cslot_ptr slot)) (ensure_empty slot)" apply (clarsimp simp: CSpace_D.ensure_empty_def ensure_empty_def liftE_bindE unlessE_whenE) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule get_cap_corres; simp) apply (rule corres_whenE) apply (simp add:transform_cap_def split:cap.splits arch_cap.splits) apply (rule dcorres_free_throw) by wpsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpace_D.ensure_empty (transform_cslot_ptr slot)) (CSpaceAcc_A.ensure_empty slot) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (valid_idle and not_idle_thread (fst slot) and valid_etcbs) (do cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
whenE (cap \<noteq> cdl_cap.NullCap) throw
od) (do cap <- CSpaceAcc_A.get_cap slot;
whenE (cap \<noteq> cap.NullCap) (throwError DeleteFirst)
od) proof (prove)
goal (3 subgoals):
 1. dcorres (dc \<oplus> dc) ?Q ?Q' (do cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
whenE (cap \<noteq> cdl_cap.NullCap) throw
od) (do cap <- CSpaceAcc_A.get_cap slot;
whenE (cap \<noteq> cap.NullCap) (throwError DeleteFirst)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. dcorres ?r'4 ?P4 ?P'4 (KHeap_D.get_cap (transform_cslot_ptr slot)) (CSpaceAcc_A.get_cap slot)
 2. \<And>cap capa. ?r'4 cap capa \<Longrightarrow> dcorres (dc \<oplus> dc) (?R4 cap) (?R'4 capa) (whenE (cap \<noteq> cdl_cap.NullCap) throw) (whenE (capa \<noteq> cap.NullCap) (throwError DeleteFirst))
 3. \<lbrace>?Q4\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. (valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dcorres (dc \<oplus> dc) (?R4 cap) (?R'4 capa) (whenE (cap \<noteq> cdl_cap.NullCap) throw) (whenE (capa \<noteq> cap.NullCap) (throwError DeleteFirst))
 2. \<lbrace>?Q4\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> (cap \<noteq> cdl_cap.NullCap) = (capa \<noteq> cap.NullCap)
 2. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dcorres (dc \<oplus> dc) (?P17 cap) (?P'19 capa) throw (throwError DeleteFirst)
 3. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dc () ()
 4. \<lbrace>?Q4\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>cap s. cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?P17 cap s\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. capa \<noteq> cap.NullCap \<longrightarrow> ?P'19 capa s\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dcorres (dc \<oplus> dc) (?P17 cap) (?P'19 capa) throw (throwError DeleteFirst)
 2. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dc () ()
 3. \<lbrace>?Q4\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>cap s. cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?P17 cap s\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. capa \<noteq> cap.NullCap \<longrightarrow> ?P'19 capa s\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. (valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>cap capa s. cap = transform_cap capa \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError DeleteFirst \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dc () ()
 3. \<lbrace>?Q4\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>cap s. cap \<noteq> cdl_cap.NullCap \<longrightarrow> ?P17 cap s\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>capa s. capa \<noteq> cap.NullCap \<longrightarrow> ?P'19 capa s\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. (valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'4) s