theory Retype_R

lemma retype_obj_at_disj':
  assumes vs: "pspace_aligned' s" "pspace_distinct' s"
     and  pn: "pspace_no_overlap' ptr sz s"
     and cover: "range_cover ptr sz (objBitsKO obj) n"
  shows
  "obj_at' P p (s \<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr obj)
                      (new_cap_addrs n ptr obj) (ksPSpace s)\<rparr>)
     = (obj_at' P p s \<or> p \<in> set (new_cap_addrs n ptr obj)
                         \<and> (\<exists>ko. projectKO_opt obj = Some ko \<and> P ko))" apply (simp add: retype_obj_at' [OF vs pn cover]) apply (safe, simp_all) apply (drule subsetD [OF new_cap_addrs_subset [OF cover]]) apply (insert pspace_no_overlap_disjoint' [OF vs(1) pn ]) apply (clarsimp simp: obj_at'_def) apply (rule_tac x1 = p in ccontr[OF in_empty_interE]) apply (simp add:ptr_add_def p_assoc_help domI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr obj) (new_cap_addrs n ptr obj) (ksPSpace s)\<rparr>) = (obj_at' P p s \<or> p \<in> set (new_cap_addrs n ptr obj) \<and> (\<exists>ko. projectKO_opt obj = Some ko \<and> P ko)) proof (prove)
goal (1 subgoal):
 1. p \<in> set (new_cap_addrs n ptr obj) \<longrightarrow> (\<exists>ko. projectKO_opt obj = Some ko \<and> P ko) = (obj_at' P p s \<or> (\<exists>ko. projectKO_opt obj = Some ko \<and> P ko)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (new_cap_addrs n ptr obj); obj_at' P p s\<rbrakk> \<Longrightarrow> \<exists>ko. projectKO_opt obj = Some ko \<and> P ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P p s; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}\<rbrakk> \<Longrightarrow> \<exists>ko. projectKO_opt obj = Some ko \<and> P ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P p s; p \<in> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> \<exists>ko. projectKO_opt obj = Some ko \<and> P ko proof (prove)
goal (1 subgoal):
 1. \<And>ko obja. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> p; p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obja, s)}; P obja; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>ko. projectKO_opt obj = Some ko \<and> P ko proof (prove)
goal (3 subgoals):
 1. \<And>ko obja. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> p; p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obja, s)}; P obja; ps_clear p (objBitsKO ko) s; \<nexists>ko. projectKO_opt obj = Some ko \<and> P ko\<rbrakk> \<Longrightarrow> ?A22 ko obja \<inter> ?B22 ko obja = {}
 2. \<And>ko obja. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> p; p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obja, s)}; P obja; ps_clear p (objBitsKO ko) s; \<nexists>ko. projectKO_opt obj = Some ko \<and> P ko\<rbrakk> \<Longrightarrow> p \<in> ?A22 ko obja
 3. \<And>ko obja. \<lbrakk>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s) = {}; ptr \<le> p; p \<le> ptr_add (ptr && ~~ mask sz) (2 ^ sz - Suc 0); ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obja, s)}; P obja; ps_clear p (objBitsKO ko) s; \<nexists>ko. projectKO_opt obj = Some ko \<and> P ko\<rbrakk> \<Longrightarrow> p \<in> ?B22 ko obja proof (prove)
goal:
No subgoals!