theory Untyped_DR

lemma descendants_of_empty_lift :
  "\<lbrakk>cte_at slot' s; valid_mdb s\<rbrakk> \<Longrightarrow>
  (CSpaceAcc_A.descendants_of slot' (cdt s) = {})
   = (\<not> (\<exists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')))" apply (rule iffI) apply clarsimp apply (frule transform_cdt_dom_standard) apply (clarsimp simp:descendants_of_def) apply (thin_tac "(a,b) = P" for P) apply (drule(1) transform_cdt_some_rev) apply (clarsimp simp:valid_mdb_def) apply clarsimp apply (drule_tac x = a in spec,drule_tac x = b in spec) apply (subgoal_tac "cdt s \<Turnstile> slot' \<rightarrow> (a, b)") apply simp apply (rule r_into_trancl') apply (simp add:cdt_parent_rel_def is_cdt_parent_def) apply (rule ccontr) apply (clarsimp simp:descendants_of_def) apply (drule tranclD) apply clarsimp apply (drule_tac x = aa in spec,drule_tac x = "nat (bl_to_bin ba)" in spec) apply (frule descendants_of_cte_at[rotated]) apply (simp add:descendants_of_def) apply (rule r_into_trancl') apply simp apply (drule_tac slot = "(aa,ba)" in mdb_cte_transform_cdt_lift) apply (simp add:valid_mdb_def) apply (clarsimp simp:cdt_parent_rel_def is_cdt_parent_def transform_cslot_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s\<rbrakk> \<Longrightarrow> (CSpaceAcc_A.descendants_of slot' (cdt s) = {}) = (\<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; CSpaceAcc_A.descendants_of slot' (cdt s) = {}\<rbrakk> \<Longrightarrow> \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; CSpaceAcc_A.descendants_of slot' (cdt s) = {}; transform_cdt s (a, b) = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; CSpaceAcc_A.descendants_of slot' (cdt s) = {}; transform_cdt s (a, b) = Some (transform_cslot_ptr slot'); \<exists>slot. (a, b) = transform_cslot_ptr slot\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+; transform_cdt s (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr slot'); (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+; transform_cdt s (transform_cslot_ptr (aa, ba)) = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)
 2. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+; \<exists>slot_b. transform_cslot_ptr slot_b = transform_cslot_ptr (aa, ba) \<and> cdt s slot_b = Some slot'\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+; \<exists>slot_b. transform_cslot_ptr slot_b = transform_cslot_ptr (aa, ba) \<and> cdt s slot_b = Some slot'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>aa ba a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+; transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba); cdt s (a, b) = Some slot'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>aa ba a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba); cdt s (a, b) = Some slot'; (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (3 subgoals):
 1. \<And>aa ba a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba); cdt s (a, b) = Some slot'; (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+; cdt s \<Turnstile> slot' \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>aa ba a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba); cdt s (a, b) = Some slot'; (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+\<rbrakk> \<Longrightarrow> cdt s \<Turnstile> slot' \<rightarrow> (a, b)
 3. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>aa ba a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba); cdt s (a, b) = Some slot'; (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+\<rbrakk> \<Longrightarrow> cdt s \<Turnstile> slot' \<rightarrow> (a, b)
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>aa ba a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba); cdt s (a, b) = Some slot'; (slot', a, b) \<notin> (CSpaceAcc_A.cdt_parent_rel (cdt s))\<^sup>+\<rbrakk> \<Longrightarrow> cdt s \<Turnstile> slot' \<leadsto> (a, b)
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of slot' (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<nexists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot'); CSpaceAcc_A.descendants_of slot' (cdt s) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. transform_cdt s (a, b) \<noteq> Some (transform_cslot_ptr slot'); cdt s \<Turnstile> slot' \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. transform_cdt s (a, b) \<noteq> Some (transform_cslot_ptr slot'); \<exists>z. cdt s \<Turnstile> slot' \<leadsto> z \<and> cdt s \<Turnstile> z \<rightarrow>* (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; \<forall>a b. transform_cdt s (a, b) \<noteq> Some (transform_cslot_ptr slot'); cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> ?p47 a b aa ba \<in> CSpaceAcc_A.descendants_of (?x47 a b aa ba) (cdt s)
 2. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot'); cte_wp_at (\<lambda>_. True) (?p47 a b aa ba) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> cdt s \<Turnstile> ?x47 a b aa ba \<rightarrow> ?p47 a b aa ba
 2. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot'); cte_wp_at (\<lambda>_. True) (?p47 a b aa ba) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> cdt s \<Turnstile> ?x47 a b aa ba \<leadsto> ?p47 a b aa ba
 2. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot'); cte_wp_at (\<lambda>_. True) (?p47 a b aa ba) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot'); cte_wp_at (\<lambda>_. True) (aa, ba) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot')\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)
 2. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot'); transform_cdt s (transform_cslot_ptr (aa, ba)) = (case cdt s (aa, ba) of None \<Rightarrow> None | Some slot' \<Rightarrow> Some (transform_cslot_ptr slot'))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot' s; valid_mdb s; cdt s \<Turnstile> slot' \<leadsto> (aa, ba); cdt s \<Turnstile> (aa, ba) \<rightarrow>* (a, b); transform_cdt s (aa, nat (bl_to_bin ba)) \<noteq> Some (transform_cslot_ptr slot'); transform_cdt s (transform_cslot_ptr (aa, ba)) = (case cdt s (aa, ba) of None \<Rightarrow> None | Some slot' \<Rightarrow> Some (transform_cslot_ptr slot'))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!