theory Finalise_DR

lemma cdl_cdt_parent_cte_at_lift:
  "\<lbrakk> mdb_cte_at (swp (cte_wp_at P) s) (cdt s) ; a \<in> KHeap_D.descendants_of p (transform s) \<rbrakk>
    \<Longrightarrow> (\<exists>slot. cte_at slot s \<and>  p = transform_cslot_ptr slot)" apply (simp add:KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def) apply (frule DomainI) apply (clarsimp simp:KHeap_D.is_cdt_parent_def) apply (simp add:transform_def transform_cdt_def) apply (clarsimp simp:transform_cdt_slot_inj_on_mdb_cte_at map_lift_over_eq_Some split:if_splits) apply (rule_tac x = ab in exI,rule_tac x = bb in exI) apply (drule(1) mdb_cte_atD) apply (clarsimp simp :cte_wp_at_cte_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); a \<in> KHeap_D.descendants_of p (transform s)\<rbrakk> \<Longrightarrow> \<exists>slot. cte_wp_at (\<lambda>_. True) slot s \<and> p = transform_cslot_ptr slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (p, a) \<in> {(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<and> p = transform_cslot_ptr (a, b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (p, a) \<in> {(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+; p \<in> Domain ({(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+)\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<and> p = transform_cslot_ptr (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (p, a) \<in> {(x, y). KHeap_D.is_cdt_parent (transform s) x y}\<^sup>+; cdl_cdt (transform s) (aa, b) = Some p\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<and> p = transform_cslot_ptr (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (p, a) \<in> {(x, y). KHeap_D.is_cdt_parent \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = map_lift_over transform_cslot_ptr (cdt s), cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> x y}\<^sup>+; map_lift_over transform_cslot_ptr (cdt s) (aa, b) = Some p\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<and> p = transform_cslot_ptr (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (transform_cslot_ptr (ab, bb), a) \<in> {(x, y). KHeap_D.is_cdt_parent \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = map_lift_over transform_cslot_ptr (cdt s), cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> x y}\<^sup>+; (aa, b) = transform_cslot_ptr (aaa, ba); cdt s (aaa, ba) = Some (ab, bb); p = transform_cslot_ptr (ab, bb)\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>_. True) (a, b) s \<and> transform_cslot_ptr (ab, bb) = transform_cslot_ptr (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (transform_cslot_ptr (ab, bb), a) \<in> {(x, y). KHeap_D.is_cdt_parent \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = map_lift_over transform_cslot_ptr (cdt s), cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> x y}\<^sup>+; (aa, b) = transform_cslot_ptr (aaa, ba); cdt s (aaa, ba) = Some (ab, bb); p = transform_cslot_ptr (ab, bb)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ab, bb) s \<and> transform_cslot_ptr (ab, bb) = transform_cslot_ptr (ab, bb) proof (prove)
goal (1 subgoal):
 1. \<And>aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (transform_cslot_ptr (ab, bb), a) \<in> {(x, y). KHeap_D.is_cdt_parent \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s, cdl_cdt = map_lift_over transform_cslot_ptr (cdt s), cdl_current_thread = transform_current_thread s, cdl_irq_node = interrupt_irq_node s, cdl_asid_table = transform_asid_table s, cdl_current_domain = cur_domain s\<rparr> x y}\<^sup>+; (aa, b) = transform_cslot_ptr (aaa, ba); p = transform_cslot_ptr (ab, bb); swp (cte_wp_at P) s (ab, bb) \<and> swp (cte_wp_at P) s (aaa, ba)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (ab, bb) s \<and> transform_cslot_ptr (ab, bb) = transform_cslot_ptr (ab, bb) proof (prove)
goal:
No subgoals!