theory Finalise_DR

lemma finite_descendants_if_from_transform:
  " mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s))" apply (case_tac "KHeap_D.descendants_of x (transform s) = {}") apply simp apply (drule ex_in_none_empty_set) apply clarsimp apply (frule(1) cdl_cdt_parent_cte_at_lift) apply clarsimp apply (frule(1) descendants_of_eqv) apply clarsimp apply (rule finite_imageI) apply (rule finite_subset) apply (rule descendants_in_cte_wp_set) apply simp apply (simp add:cte_wp_at_set_finite) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); KHeap_D.descendants_of x (transform s) = {}\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s))
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); KHeap_D.descendants_of x (transform s) \<noteq> {}\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); KHeap_D.descendants_of x (transform s) \<noteq> {}\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); \<exists>xa. xa \<in> KHeap_D.descendants_of x (transform s)\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (a, b) \<in> KHeap_D.descendants_of x (transform s)\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (a, b) \<in> KHeap_D.descendants_of x (transform s); \<exists>slot. cte_wp_at (\<lambda>_. True) slot s \<and> x = transform_cslot_ptr slot\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (a, b) \<in> KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); (a, b) \<in> KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba); KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> finite (KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba); KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s); (a, b) = transform_cslot_ptr (ab, bb); (ab, bb) \<in> CSpaceAcc_A.descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> finite (transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba); KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s); (a, b) = transform_cslot_ptr (ab, bb); (ab, bb) \<in> CSpaceAcc_A.descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> finite (CSpaceAcc_A.descendants_of (aa, ba) (cdt s)) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba); KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s); (a, b) = transform_cslot_ptr (ab, bb); (ab, bb) \<in> CSpaceAcc_A.descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> CSpaceAcc_A.descendants_of (aa, ba) (cdt s) \<subseteq> ?B19 a b aa ba ab bb
 2. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba); KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s); (a, b) = transform_cslot_ptr (ab, bb); (ab, bb) \<in> CSpaceAcc_A.descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> finite (?B19 a b aa ba ab bb) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba); KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s); (a, b) = transform_cslot_ptr (ab, bb); (ab, bb) \<in> CSpaceAcc_A.descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at (?P22 a b aa ba ab bb)) s) (cdt s)
 2. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba); KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s); (a, b) = transform_cslot_ptr (ab, bb); (ab, bb) \<in> CSpaceAcc_A.descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> finite {x. cte_wp_at (?P22 a b aa ba ab bb) x s} proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cte_wp_at (\<lambda>_. True) (aa, ba) s; x = transform_cslot_ptr (aa, ba); KHeap_D.descendants_of (transform_cslot_ptr (aa, ba)) (transform s) = transform_cslot_ptr ` CSpaceAcc_A.descendants_of (aa, ba) (cdt s); (a, b) = transform_cslot_ptr (ab, bb); (ab, bb) \<in> CSpaceAcc_A.descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> finite {x. cte_wp_at P x s} proof (prove)
goal:
No subgoals!