theory Retype_R

lemma retype_ekheap_relation:
  assumes  sr: "ekheap_relation (ekheap s) (ksPSpace s')"
      and  sr': "pspace_relation (kheap s) (ksPSpace s')"
      and  vs: "valid_pspace s" "valid_mdb s"
      and et: "valid_etcbs 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
  "ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain))
                              (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s))
            (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))"
  (is "ekheap_relation ?ps ?ps'") proof - have not_unt: "ty \<noteq> Inr (APIObjectType ArchTypes_H.Untyped)" by (rule makeObjectKO_Untyped[OF ko]) show ?thesis apply (case_tac "ty \<noteq> Inr (APIObjectType apiobject_type.TCBObject)") apply (insert ko) apply (cut_tac retype_pspace_relation[OF sr' vs vs' pn pn' ko cover orr num_r]) apply (simp add: foldr_upd_app_if' foldr_upd_app_if[folded data_map_insert_def]) apply (simp add: obj_relation_retype_addrs_eq[OF not_unt num_r orr cover,symmetric]) apply (insert sr) apply (clarsimp simp add: ekheap_relation_def
                      pspace_relation_def default_ext_def cong: if_cong
                      split: if_split_asm) subgoal by (clarsimp simp add: makeObjectKO_def APIType_map2_def cong: if_cong
                              split: sum.splits Structures_H.kernel_object.splits
                                     arch_kernel_object.splits ARM_H.object_type.splits apiobject_type.splits) apply (frule ekh_at_tcb_at[OF et]) apply (intro impI conjI) apply clarsimp apply (drule_tac x=a in bspec,force) apply (clarsimp simp add: other_obj_relation_def split: if_split_asm) apply (case_tac ko,simp_all) apply (clarsimp simp add: makeObjectKO_def cong: if_cong split: sum.splits Structures_H.kernel_object.splits
                                 arch_kernel_object.splits ARM_H.object_type.splits
                                 apiobject_type.splits if_split_asm) apply (drule_tac x=xa in bspec,simp) subgoal by force subgoal by force apply (simp add: foldr_upd_app_if' foldr_upd_app_if[folded data_map_insert_def]) apply (simp add: obj_relation_retype_addrs_eq[OF not_unt num_r orr cover,symmetric]) apply (clarsimp simp add: APIType_map2_def default_ext_def ekheap_relation_def
           default_object_def makeObjectKO_def etcb_rel_makeObject
           cong: if_cong
           split: if_split_asm) apply force done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (state)
goal (1 subgoal):
 1. ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) 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 (1 subgoal):
 1. ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (1 subgoal):
 1. ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (2 subgoals):
 1. ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; 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'))\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))
 2. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; pspace_relation (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) (\<lambda>x. if x \<in> set (new_cap_addrs m ptr ko) then Some ko else ksPSpace s' x)\<rbrakk> \<Longrightarrow> ekheap_relation (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then default_ext (APIType_map2 ty) default_domain else ekheap s x) (\<lambda>x. if x \<in> set (new_cap_addrs m ptr ko) then Some ko else ksPSpace s' x)
 2. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; pspace_relation (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x)\<rbrakk> \<Longrightarrow> ekheap_relation (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then default_ext (APIType_map2 ty) default_domain else ekheap s x) (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x)
 2. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; pspace_relation (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then default_ext (APIType_map2 ty) default_domain else ekheap s x) (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x)
 2. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (case APIType_map2 ty of Structures_A.apiobject_type.TCBObject \<Rightarrow> Some (default_etcb\<lparr>tcb_domain := default_domain\<rparr>) | _ \<Rightarrow> None) = Some y\<rbrakk> \<Longrightarrow> ((\<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb')) \<and> ((\<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'))
 2. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y\<rbrakk> \<Longrightarrow> ((\<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb')) \<and> ((\<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'))
 3. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x_ \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (case APIType_map2 ty of Structures_A.apiobject_type.TCBObject \<Rightarrow> Some (default_etcb\<lparr>tcb_domain := default_domain\<rparr>) | _ \<Rightarrow> None) = Some y_\<rbrakk> \<Longrightarrow> ((\<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x_ \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y_ tcb')) \<and> ((\<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x_ \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x_ = Some (KOTCB tcb') \<and> etcb_relation y_ tcb')) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y\<rbrakk> \<Longrightarrow> ((\<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb')) \<and> ((\<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'))
 2. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ((\<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb')) \<and> ((\<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa) \<longrightarrow> (\<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'))
 2. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb'
 2. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'
 3. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (3 subgoals):
 1. \<And>y xa a b tcb. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; a \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s a = Some y; xa \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa; kheap s a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb'
 2. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'
 3. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (3 subgoals):
 1. \<And>y xa a b tcb. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; a \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s a = Some y; xa \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa; kheap s a = Some (TCB tcb); (a \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) a. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (a \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>x\<in>obj_relation_cuts (the (kheap s a)) a. case x of (y, P) \<Rightarrow> P (the (kheap s a)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y))))\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb'
 2. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'
 3. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (4 subgoals):
 1. \<And>y xa b tcb x aa ba. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; aa \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s aa = Some y; xa \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (aa, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa; kheap s aa = Some (TCB tcb); case ko of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (aa, ba) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb'
 2. \<And>y xa a b tcb. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; a \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s a = Some y; xa \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa; kheap s a = Some (TCB tcb); \<forall>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). a \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; case the (ksPSpace s' a) of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb'
 3. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'
 4. \<lbrakk>\<not> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (4 subgoals):
 1. \<And>y xa b tcb x aa ba x6. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some (KOTCB x6); aa \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s aa = Some y; xa \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (aa, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa; kheap s aa = Some (TCB tcb); tcb_relation tcb x6; x \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (aa, ba) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; ko = KOTCB x6\<rbrakk> \<Longrightarrow> etcb_relation y x6
 2. \<And>y xa a b tcb. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; a \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s a = Some y; xa \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa; kheap s a = Some (TCB tcb); \<forall>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). a \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; case the (ksPSpace s' a) of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb'
 3. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'
 4. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) default_domain)) (retype_addrs ptr (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (3 subgoals):
 1. \<And>y xa a b tcb. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; a \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s a = Some y; xa \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa; kheap s a = Some (TCB tcb); \<forall>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). a \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x; case the (ksPSpace s' a) of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb'
 2. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'
 3. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) default_domain)) (retype_addrs ptr (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (3 subgoals):
 1. \<And>y xa a b tcb. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; a \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s a = Some y; xa \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (a, b) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa; kheap s a = Some (TCB tcb); case the (ksPSpace s' a) of KOTCB x \<Rightarrow> tcb_relation tcb x | _ \<Rightarrow> False; a \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y tcb'
 2. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'
 3. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) default_domain)) (retype_addrs ptr (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; a_ \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s a_ = Some y_; xa_ \<in> set (retype_addrs ptr (APIType_map2 ty) n us); (a_, b_) \<in> obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa_; kheap s a_ = Some (TCB tcb_); case the (ksPSpace s' a_) of KOTCB x \<Rightarrow> tcb_relation tcb_ x | _ \<Rightarrow> False; a_ \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa_\<rbrakk> \<Longrightarrow> \<exists>tcb'. ko = KOTCB tcb' \<and> etcb_relation y_ tcb' proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x = Some y; \<exists>tcb. kheap s x = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb'
 2. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) default_domain)) (retype_addrs ptr (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x) = dom (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa then Some ko else ksPSpace s' x); \<forall>x\<in>dom (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) then Some (default_object (APIType_map2 ty) dev us) else kheap s x). (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (default_object (APIType_map2 ty) dev us) x. case x of (y, P) \<Rightarrow> P (default_object (APIType_map2 ty) dev us) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))) \<and> (x \<in> set (retype_addrs ptr (APIType_map2 ty) n us) \<or> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (if \<exists>x\<in>set (retype_addrs ptr (APIType_map2 ty) n us). y \<in> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) x then Some ko else ksPSpace s' y)))); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev ty = Some ko; x_ \<notin> set (retype_addrs ptr (APIType_map2 ty) n us); ekheap s x_ = Some y_; \<exists>tcb. kheap s x_ = Some (TCB tcb); \<forall>xa\<in>set (retype_addrs ptr (APIType_map2 ty) n us). x_ \<notin> fst ` obj_relation_cuts (default_object (APIType_map2 ty) dev us) xa\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x_ = Some (KOTCB tcb') \<and> etcb_relation y_ tcb' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) default_domain)) (retype_addrs ptr (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) n us) then default_ext (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) default_domain else ekheap s x) (\<lambda>x. if x \<in> set (new_cap_addrs m ptr ko) then Some ko else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); makeObjectKO dev (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) = Some ko; ekheap_relation (ekheap s) (ksPSpace s')\<rbrakk> \<Longrightarrow> ekheap_relation (\<lambda>x. if x \<in> set (retype_addrs ptr (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) n us) then default_ext (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) default_domain else ekheap s x) (\<lambda>x. if \<exists>xa\<in>set (retype_addrs ptr (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) n us). x \<in> fst ` obj_relation_cuts (default_object (APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject))) dev us) xa then Some ko else ksPSpace s' x) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); \<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation (the (ekheap s x)) tcb'; ko = KOTCB makeObject; x \<notin> set (retype_addrs ptr Structures_A.apiobject_type.TCBObject n us); ekheap s x = Some y\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> etcb_relation y tcb' proof (prove)
goal:
No subgoals! proof (state)
this:
ekheap_relation (foldr (\<lambda>p ps. ps(p := default_ext (APIType_map2 ty) default_domain)) (retype_addrs ptr (APIType_map2 ty) n us) (ekheap s)) (foldr (\<lambda>addr. data_map_insert addr ko) (new_cap_addrs m ptr ko) (ksPSpace s'))

goal:
No subgoals!