theory Retype_R

lemma retype_pspace_relation:
  assumes  sr: "pspace_relation (kheap s) (ksPSpace s')"
      and  vs: "valid_pspace s" "valid_mdb s"
      and vs': "pspace_aligned' s'" "pspace_distinct' s'"
      and  pn: "pspace_no_overlap_range_cover ptr sz s"
      and pn': "pspace_no_overlap' ptr sz s'"
      and  ko: "makeObjectKO dev ty = Some ko"
      and cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n"
      and orr: "obj_relation_retype (default_object (APIType_map2 ty) dev us) ko"
      and num_r: "m = 2 ^ (obj_bits_api (APIType_map2 ty) us - objBitsKO ko) * n"
  shows
  "pspace_relation (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us))
                              (retype_addrs ptr (APIType_map2 ty) n us) (kheap s))
            (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))"
  (is "pspace_relation ?ps ?ps'") unfolding pspace_relation_def proof have not_unt: "ty \<noteq> Inr (APIObjectType ArchTypes_H.Untyped)" by (rule makeObjectKO_Untyped[OF ko]) have dom_not_ra:
    "\<forall>x \<in> dom (kheap s). x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us)" apply clarsimp apply (erule(1) pspace_no_overlapC[OF pn _ _ cover vs(1)]) done hence dom_Int_ra:
    "set (retype_addrs ptr (APIType_map2 ty) n us) \<inter> dom (kheap s) = {}" by auto note pdom = pspace_dom_upd [OF dom_Int_ra, where ko="default_object (APIType_map2 ty) dev us"] have pdom': "dom ?ps' = dom (ksPSpace s') \<union> set (new_cap_addrs m ptr ko)" by (clarsimp simp add: foldr_upd_app_if[folded data_map_insert_def]
                           dom_if_Some Un_commute
                split del: if_split) note not_unt = makeObjectKO_Untyped [OF ko] have "pspace_dom (kheap s) = dom (ksPSpace s')" using sr by (simp add: pspace_relation_def) thus "pspace_dom ?ps = dom ?ps'" apply (simp add: pdom pdom') apply (rule arg_cong[where f="\<lambda>T. S \<union> T" for S]) apply (rule obj_relation_retype_addrs_eq[OF not_unt num_r orr cover]) done have dom_same:
    "\<And>x v. kheap s x = Some v \<Longrightarrow> ?ps x = Some v" apply (frule bspec [OF dom_not_ra, OF domI]) apply (simp add: foldr_upd_app_if) done have cover':"range_cover ptr sz (objBitsKO ko) m" by (rule range_cover_rel[OF cover objBits_le_obj_bits_api[OF ko] num_r]) have dom_same':
    "\<And>x v. ksPSpace s' x = Some v \<Longrightarrow> ?ps' x = Some v" apply (clarsimp simp:foldr_upd_app_if[folded data_map_insert_def]) apply (drule domI[where m = "ksPSpace s'"]) apply (drule(1) IntI) apply (erule_tac A = "A \<inter> B" for A B in in_emptyE[rotated]) apply (rule disjoint_subset[OF new_cap_addrs_subset[OF cover']]) apply (clarsimp simp:ptr_add_def field_simps) apply (rule pspace_no_overlap_disjoint'[OF vs'(1) pn']) done show "\<forall>x \<in> dom ?ps. \<forall>(y, P) \<in> obj_relation_cuts (the (?ps x)) x.
                   P (the (?ps x)) (the (?ps' y))" using sr apply (clarsimp simp: pspace_relation_def) apply (simp add: foldr_upd_app_if split: if_split_asm) apply (clarsimp simp: foldr_upd_app_if[folded data_map_insert_def]) apply (rule conjI) apply (drule obj_relation_retype_cutsD [OF _ orr], clarsimp) apply (rule impI, erule notE) apply (simp add: obj_relation_retype_addrs_eq[OF not_unt num_r orr cover,symmetric]) apply (erule rev_bexI) apply (simp add: image_def) apply (erule rev_bexI, simp) apply (drule bspec, erule domI) apply clarsimp apply (drule(1) bspec, simp) apply (subgoal_tac "a \<in> pspace_dom (kheap s)") apply clarsimp apply (frule dom_same', simp) apply (simp(no_asm) add: pspace_dom_def) apply (rule rev_bexI, erule domI) apply (simp add: image_def) apply (erule rev_bexI, simp) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_relation (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (1 subgoal):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) \<and> (\<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y))) proof (state)
goal (2 subgoals):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped) proof (state)
this:
ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped)

goal (2 subgoals):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (kheap s). x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>kheap s x = Some y; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>x\<in>dom (kheap s). x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us)

goal (2 subgoals):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
using this:
\<forall>x\<in>dom (kheap s). x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us)

goal (1 subgoal):
 1. set (retype_addrs ptr (APIType_map2 ty) n us) \<inter> dom (kheap s) = {} proof (state)
this:
set (retype_addrs ptr (APIType_map2 ty) n us) \<inter> dom (kheap s) = {}

goal (2 subgoals):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (state)
this:
pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = pspace_dom (kheap s) \<union> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x)

goal (2 subgoals):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) = dom (ksPSpace s') \<union> set (new_cap_addrs m ptr ko) proof (state)
this:
dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) = dom (ksPSpace s') \<union> set (new_cap_addrs m ptr ko)

goal (2 subgoals):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (state)
this:
ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped)

goal (2 subgoals):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. pspace_dom (kheap s) = dom (ksPSpace s') proof (prove)
using this:
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. pspace_dom (kheap s) = dom (ksPSpace s') proof (state)
this:
pspace_dom (kheap s) = dom (ksPSpace s')

goal (2 subgoals):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
using this:
pspace_dom (kheap s) = dom (ksPSpace s')

goal (1 subgoal):
 1. pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (1 subgoal):
 1. pspace_dom (kheap s) = dom (ksPSpace s') \<Longrightarrow> dom (ksPSpace s') \<union> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) = dom (ksPSpace s') \<union> set (new_cap_addrs m ptr ko) proof (prove)
goal (1 subgoal):
 1. pspace_dom (kheap s) = dom (ksPSpace s') \<Longrightarrow> (\<Union>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x) = set (new_cap_addrs m ptr ko) proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)) = dom (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))

goal (1 subgoal):
 1. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. kheap s x = Some v \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x = Some v proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>kheap s x = Some v; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x = Some v proof (prove)
goal:
No subgoals! proof (state)
this:
kheap s ?x = Some ?v \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) ?x = Some ?v

goal (1 subgoal):
 1. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO ko) m proof (state)
this:
range_cover ptr sz (objBitsKO ko) m

goal (1 subgoal):
 1. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. ksPSpace s' x = Some v \<Longrightarrow> foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') x = Some v proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>ksPSpace s' x = Some v; x \<in> set (new_cap_addrs m ptr ko)\<rbrakk> \<Longrightarrow> ko = v proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>x \<in> set (new_cap_addrs m ptr ko); x \<in> dom (ksPSpace s')\<rbrakk> \<Longrightarrow> ko = v proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>x \<in> dom (ksPSpace s'); x \<in> set (new_cap_addrs m ptr ko) \<inter> dom (ksPSpace s')\<rbrakk> \<Longrightarrow> ko = v proof (prove)
goal (1 subgoal):
 1. \<And>x v. x \<in> dom (ksPSpace s') \<Longrightarrow> set (new_cap_addrs m ptr ko) \<inter> dom (ksPSpace s') = {} proof (prove)
goal (1 subgoal):
 1. \<And>x v. x \<in> dom (ksPSpace s') \<Longrightarrow> {ptr..ptr_add (ptr && ~~ mask sz) (2 ^ sz - 1)} \<inter> dom (ksPSpace s') = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. ksPSpace s' x = Some y \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> dom (ksPSpace s') = {} proof (prove)
goal:
No subgoals! proof (state)
this:
ksPSpace s' ?x = Some ?v \<Longrightarrow> foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') ?x = Some ?v

goal (1 subgoal):
 1. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
using this:
pspace_relation (kheap s) (ksPSpace s')

goal (1 subgoal):
 1. \<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>(a, b) \<in> obj_relation_cuts y x; foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x = Some y; pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us); default_object (APIType_map2 ty) dev us = y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a))
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us)\<rbrakk> \<Longrightarrow> (a \<in> set (new_cap_addrs m ptr ko) \<longrightarrow> b (default_object (APIType_map2 ty) dev us) ko) \<and> (a \<notin> set (new_cap_addrs m ptr ko) \<longrightarrow> b (default_object (APIType_map2 ty) dev us) (the (ksPSpace s' a)))
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (3 subgoals):
 1. \<And>x a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us)\<rbrakk> \<Longrightarrow> a \<in> set (new_cap_addrs m ptr ko) \<longrightarrow> b (default_object (APIType_map2 ty) dev us) ko
 2. \<And>x a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us)\<rbrakk> \<Longrightarrow> a \<notin> set (new_cap_addrs m ptr ko) \<longrightarrow> b (default_object (APIType_map2 ty) dev us) (the (ksPSpace s' a))
 3. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us)\<rbrakk> \<Longrightarrow> a \<notin> set (new_cap_addrs m ptr ko) \<longrightarrow> b (default_object (APIType_map2 ty) dev us) (the (ksPSpace s' a))
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us)\<rbrakk> \<Longrightarrow> a \<in> set (new_cap_addrs m ptr ko)
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us)\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). a \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x\<rbrakk> \<Longrightarrow> \<exists>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. a = fst x
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); \<forall>x\<in>dom (kheap s). \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; \<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y))\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; \<forall>x\<in>obj_relation_cuts y x. case x of (ya, P) \<Rightarrow> P y (the (ksPSpace s' ya))\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y (the (ksPSpace s' a))\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y (the (ksPSpace s' a)); a \<in> pspace_dom (kheap s)\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a))
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y (the (ksPSpace s' a))\<rbrakk> \<Longrightarrow> a \<in> pspace_dom (kheap s) proof (prove)
goal (2 subgoals):
 1. \<And>x a b y ya. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y ya; ksPSpace s' a = Some ya\<rbrakk> \<Longrightarrow> b y (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') a))
 2. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y (the (ksPSpace s' a))\<rbrakk> \<Longrightarrow> a \<in> pspace_dom (kheap s) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y (the (ksPSpace s' a))\<rbrakk> \<Longrightarrow> a \<in> pspace_dom (kheap s) proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y (the (ksPSpace s' a))\<rbrakk> \<Longrightarrow> \<exists>x\<in>dom (kheap s). a \<in> fst ` obj_relation_cuts (the (kheap s x)) x proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y (the (ksPSpace s' a))\<rbrakk> \<Longrightarrow> a \<in> fst ` obj_relation_cuts (the (kheap s x)) x proof (prove)
goal (1 subgoal):
 1. \<And>x a b y. \<lbrakk>pspace_dom (kheap s) = dom (ksPSpace s'); (a, b) \<in> obj_relation_cuts y x; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); kheap s x = Some y; b y (the (ksPSpace s' a))\<rbrakk> \<Longrightarrow> \<exists>x\<in>obj_relation_cuts y x. a = fst x proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>x\<in>dom (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s)). \<forall>(y, P)\<in>obj_relation_cuts (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) x. P (the (foldr (\<lambda>p ps. ps(p \<mapsto> default_object (APIType_map2 ty) dev us)) (retype_addrs ptr (APIType_map2 ty) n us) (kheap s) x)) (the (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s') y))

goal:
No subgoals!