theory Finalise_DR

lemma dcorres_revoke_cap_no_descendants:
  "slot' = transform_cslot_ptr slot \<Longrightarrow>
  dcorres dc \<top> (\<lambda>s. valid_mdb s \<and> cte_at slot s \<and>  CSpaceAcc_A.descendants_of slot (cdt s) = {})
    (revoke_cap_simple slot')
    (return x)" apply (rule dcorres_revoke_cap_simple_helper) apply (simp add:gets_def) apply (rule dcorres_absorb_get_l) apply (subgoal_tac "(KHeap_D.descendants_of slot' (transform s')) = {}") apply clarsimp apply (rule dcorres_absorb_get_l) apply clarsimp apply (clarsimp simp:descendants_of_eqv valid_mdb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot' = transform_cslot_ptr slot \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. valid_mdb s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> CSpaceAcc_A.descendants_of slot (cdt s) = {}) (revoke_cap_simple slot') (return x) proof (prove)
goal (1 subgoal):
 1. slot' = transform_cslot_ptr slot \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. valid_mdb s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> CSpaceAcc_A.descendants_of slot (cdt s) = {}) (do descendants <- gets $ KHeap_D.descendants_of slot';
assert (finite descendants);
non_null <- gets (\<lambda>s. {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> opt_cap slot s \<noteq> None});
non_null_descendants <- return (descendants \<inter> non_null);
if non_null_descendants \<noteq> {} then do a <- select non_null_descendants;
y <- delete_cap_simple a;
revoke_cap_simple slot'
od else return ()
od) (return x) proof (prove)
goal (1 subgoal):
 1. slot' = transform_cslot_ptr slot \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. valid_mdb s \<and> cte_wp_at (\<lambda>_. True) slot s \<and> CSpaceAcc_A.descendants_of slot (cdt s) = {}) (do s <- get;
y <- assert (finite (KHeap_D.descendants_of (transform_cslot_ptr slot) s));
sa <- get;
if KHeap_D.descendants_of (transform_cslot_ptr slot) s \<inter> {slot. opt_cap slot sa \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot sa = Some y)} \<noteq> {} then do a <- select (KHeap_D.descendants_of (transform_cslot_ptr slot) s \<inter> {slot. opt_cap slot sa \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot sa = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple slot'
od else return ()
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot' = transform_cslot_ptr slot; True; valid_mdb s' \<and> cte_wp_at (\<lambda>_. True) slot s' \<and> CSpaceAcc_A.descendants_of slot (cdt s') = {}\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')));
s <- get;
if KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)} \<noteq> {} then do a <- select (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple slot'
od else return ()
od) (return x) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>slot' = transform_cslot_ptr slot; True; valid_mdb s' \<and> cte_wp_at (\<lambda>_. True) slot s' \<and> CSpaceAcc_A.descendants_of slot (cdt s') = {}; KHeap_D.descendants_of slot' (transform s') = {}\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- assert (finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s')));
s <- get;
if KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)} \<noteq> {} then do a <- select (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') \<inter> {slot. opt_cap slot s \<noteq> Some cdl_cap.NullCap \<and> (\<exists>y. opt_cap slot s = Some y)});
y <- delete_cap_simple a;
revoke_cap_simple slot'
od else return ()
od) (return x)
 2. \<And>s'. \<lbrakk>slot' = transform_cslot_ptr slot; True; valid_mdb s' \<and> cte_wp_at (\<lambda>_. True) slot s' \<and> CSpaceAcc_A.descendants_of slot (cdt s') = {}\<rbrakk> \<Longrightarrow> KHeap_D.descendants_of slot' (transform s') = {} proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>slot' = transform_cslot_ptr slot; KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') = {}; valid_mdb s'; cte_wp_at (\<lambda>_. True) slot s'; CSpaceAcc_A.descendants_of slot (cdt s') = {}\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
return ()
od) (return x)
 2. \<And>s'. \<lbrakk>slot' = transform_cslot_ptr slot; True; valid_mdb s' \<and> cte_wp_at (\<lambda>_. True) slot s' \<and> CSpaceAcc_A.descendants_of slot (cdt s') = {}\<rbrakk> \<Longrightarrow> KHeap_D.descendants_of slot' (transform s') = {} proof (prove)
goal (2 subgoals):
 1. \<And>s' s'a. \<lbrakk>slot' = transform_cslot_ptr slot; KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s') = {}; valid_mdb s'; cte_wp_at (\<lambda>_. True) slot s'; CSpaceAcc_A.descendants_of slot (cdt s') = {}; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return ()) (return x)
 2. \<And>s'. \<lbrakk>slot' = transform_cslot_ptr slot; True; valid_mdb s' \<and> cte_wp_at (\<lambda>_. True) slot s' \<and> CSpaceAcc_A.descendants_of slot (cdt s') = {}\<rbrakk> \<Longrightarrow> KHeap_D.descendants_of slot' (transform s') = {} proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot' = transform_cslot_ptr slot; True; valid_mdb s' \<and> cte_wp_at (\<lambda>_. True) slot s' \<and> CSpaceAcc_A.descendants_of slot (cdt s') = {}\<rbrakk> \<Longrightarrow> KHeap_D.descendants_of slot' (transform s') = {} proof (prove)
goal:
No subgoals!