theory Finalise_DR

lemma descendants_of_eqv:
  assumes cte_at: "mdb_cte_at (swp (cte_wp_at P) s) (cdt s)"
    and cte_at_p: "cte_at p s"
  shows "KHeap_D.descendants_of (transform_cslot_ptr p) (transform s)
           = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s)" proof - note inj = transform_cdt_slot_inj_on_mdb_cte_at[OF cte_at] have P: "{(x, y). KHeap_D.is_cdt_parent (transform s) x y}
              = (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y))
                      ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}" apply (simp add: KHeap_D.is_cdt_parent_def CSpaceAcc_A.is_cdt_parent_def) apply (simp add: transform_def transform_cdt_def map_lift_over_eq_Some
                     inj) apply auto done have inj': "inj_on transform_cslot_ptr ({p} \<union> dom (cdt s) \<union> ran (cdt s))" using cte_at_p mdb_cte_atD[OF _ cte_at] apply - apply (rule transform_cdt_slot_inj_on_cte_at[where P=\<top> and s=s]) apply (fastforce simp: cte_wp_at_caps_of_state elim!: ranE) done show ?thesis apply (simp add: KHeap_D.descendants_of_def CSpaceAcc_A.descendants_of_def
                     KHeap_D.cdt_parent_rel_def CSpaceAcc_A.cdt_parent_rel_def) apply (simp add: P) apply (subst trancl_image) apply (rule subset_inj_on[OF inj]) apply (auto simp: KHeap_D.is_cdt_parent_def CSpaceAcc_A.is_cdt_parent_def)[1] apply safe apply (subst(asm) inj_on_eq_iff[OF inj'], simp_all) apply (drule DomainI[THEN eqset_imp_iff[OF trancl_domain, THEN iffD1]]) apply (auto simp: CSpaceAcc_A.is_cdt_parent_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. KHeap_D.descendants_of (transform_cslot_ptr p) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s) proof (state)
goal (1 subgoal):
 1. KHeap_D.descendants_of (transform_cslot_ptr p) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s) proof (state)
this:
inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s))

goal (1 subgoal):
 1. KHeap_D.descendants_of (transform_cslot_ptr p) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. {(x, y). KHeap_D.is_cdt_parent (transform s) x y} = (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y} proof (prove)
goal (1 subgoal):
 1. {(x, y). cdl_cdt (transform s) y = Some x} = (\<lambda>x. case x of (x, y) \<Rightarrow> (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). cdt s y = Some x} proof (prove)
goal (1 subgoal):
 1. {(x, y). \<exists>a b. y = transform_cslot_ptr (a, b) \<and> (\<exists>aa ba. x = transform_cslot_ptr (aa, ba) \<and> cdt s (a, b) = Some (aa, ba))} = (\<lambda>x. case x of (x, y) \<Rightarrow> (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). cdt s y = Some x} proof (prove)
goal:
No subgoals! proof (state)
this:
{(x, y). KHeap_D.is_cdt_parent (transform s) x y} = (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}

goal (1 subgoal):
 1. KHeap_D.descendants_of (transform_cslot_ptr p) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. inj_on transform_cslot_ptr ({p} \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
using this:
cte_wp_at (\<lambda>_. True) p s
cdt s ?c = Some ?p \<Longrightarrow> swp (cte_wp_at P) s ?p \<and> swp (cte_wp_at P) s ?c

goal (1 subgoal):
 1. inj_on transform_cslot_ptr ({p} \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<And>c p. cdt s c = Some p \<Longrightarrow> swp (cte_wp_at P) s p \<and> swp (cte_wp_at P) s c\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({p} \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; \<And>c p. cdt s c = Some p \<Longrightarrow> swp (cte_wp_at P) s p \<and> swp (cte_wp_at P) s c; x \<in> {p} \<union> dom (cdt s) \<union> ran (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s proof (prove)
goal:
No subgoals! proof (state)
this:
inj_on transform_cslot_ptr ({p} \<union> dom (cdt s) \<union> ran (cdt s))

goal (1 subgoal):
 1. KHeap_D.descendants_of (transform_cslot_ptr p) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. KHeap_D.descendants_of (transform_cslot_ptr p) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. {q. (transform_cslot_ptr p, q) \<in> {(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+} = transform_cslot_ptr ` {q. (p, q) \<in> {(p, c). CSpaceAcc_A.is_cdt_parent (cdt s) p c}\<^sup>+} proof (prove)
goal (1 subgoal):
 1. {q. (transform_cslot_ptr p, q) \<in> ((\<lambda>x. case x of (x, y) \<Rightarrow> (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y})\<^sup>+} = transform_cslot_ptr ` {q. (p, q) \<in> {(p, c). CSpaceAcc_A.is_cdt_parent (cdt s) p c}\<^sup>+} proof (prove)
goal (2 subgoals):
 1. \<And>q. inj_on transform_cslot_ptr (Domain {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y} \<union> Range {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y})
 2. {q. (transform_cslot_ptr p, q) \<in> (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+} = transform_cslot_ptr ` {q. (p, q) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+} proof (prove)
goal (2 subgoals):
 1. \<And>q. Domain {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y} \<union> Range {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y} \<subseteq> dom (cdt s) \<union> ran (cdt s)
 2. {q. (transform_cslot_ptr p, q) \<in> (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+} = transform_cslot_ptr ` {q. (p, q) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+} proof (prove)
goal (1 subgoal):
 1. {q. (transform_cslot_ptr p, q) \<in> (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+} = transform_cslot_ptr ` {q. (p, q) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>((aa, ba), ab, bb) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+; transform_cslot_ptr p = transform_cslot_ptr (aa, ba); (a, b) = transform_cslot_ptr (ab, bb)\<rbrakk> \<Longrightarrow> (a, b) \<in> transform_cslot_ptr ` {q. (p, q) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+}
 2. \<And>a b aa ba. \<lbrakk>(a, b) = transform_cslot_ptr (aa, ba); (p, aa, ba) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+\<rbrakk> \<Longrightarrow> (transform_cslot_ptr p, a, b) \<in> (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) = transform_cslot_ptr (ab, bb); ((aa, ba), ab, bb) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+\<rbrakk> \<Longrightarrow> (aa, ba) = p \<or> (aa, ba) \<in> dom (cdt s) \<or> (aa, ba) \<in> ran (cdt s)
 2. \<And>a b aa ba. \<lbrakk>(a, b) = transform_cslot_ptr (aa, ba); (p, aa, ba) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+\<rbrakk> \<Longrightarrow> (transform_cslot_ptr p, transform_cslot_ptr (aa, ba)) \<in> (\<lambda>x. case x of (x, y) \<Rightarrow> (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) = transform_cslot_ptr (ab, bb); (aa, ba) \<in> Domain {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<rbrakk> \<Longrightarrow> (aa, ba) = p \<or> (aa, ba) \<in> dom (cdt s) \<or> (aa, ba) \<in> ran (cdt s)
 2. \<And>a b aa ba. \<lbrakk>(a, b) = transform_cslot_ptr (aa, ba); (p, aa, ba) \<in> {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+\<rbrakk> \<Longrightarrow> (transform_cslot_ptr p, transform_cslot_ptr (aa, ba)) \<in> (\<lambda>x. case x of (x, y) \<Rightarrow> (transform_cslot_ptr x, transform_cslot_ptr y)) ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}\<^sup>+ proof (prove)
goal:
No subgoals! proof (state)
this:
KHeap_D.descendants_of (transform_cslot_ptr p) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s)

goal:
No subgoals!