theory Retype_AI

lemma valid_objs: "valid_objs s'" apply (clarsimp simp:valid_objs_def) apply (rule valid_pspaceE[OF vp]) apply (clarsimp simp:valid_objs_def s'_def ps_def split:if_splits) apply (simp add:valid_obj_default_object[OF tyunt tyct]) apply (simp (no_asm) add:valid_obj_def) apply (drule bspec) apply (erule domI) apply (clarsimp simp:valid_obj_def split:Structures_A.kernel_object.splits) apply (clarsimp simp: valid_cs_def) apply (drule (1) bspec) apply (clarsimp simp: ran_def) apply (erule valid_cap_pres[unfolded s'_def ps_def]) apply (clarsimp simp add: cte_wp_at_cases valid_cs_size_def s'_def ps_def) apply fastforce apply (clarsimp simp: valid_tcb_def) apply (rule conjI) apply (rule ballI, drule(1) bspec, clarsimp elim!: ranE) apply (erule valid_cap_pres[unfolded s'_def ps_def]) apply (rule cte_wp_at_tcbI, fastforce+)[1] apply (fastforce simp: valid_tcb_state_def valid_bound_ntfn_def
                   elim!: obj_at_pres[unfolded s'_def ps_def] valid_arch_tcb_typ_at
                   split: Structures_A.thread_state.splits option.splits) apply (fastforce simp: valid_ep_def
                  elim!: obj_at_pres[unfolded s'_def ps_def]
                  split: Structures_A.endpoint.splits) apply (fastforce simp: valid_ntfn_def valid_bound_tcb_def
                  elim!: obj_at_pres[unfolded s'_def ps_def]
                 split: Structures_A.ntfn.splits option.splits) apply (clarsimp simp: wellformed_default_obj[unfolded s'_def ps_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_objs s' proof (prove)
goal (1 subgoal):
 1. \<And>ptr y. kheap s' ptr = Some y \<Longrightarrow> valid_obj ptr y s' proof (prove)
goal (1 subgoal):
 1. \<And>ptr y. \<lbrakk>kheap s' ptr = Some y; valid_objs s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s\<rbrakk> \<Longrightarrow> valid_obj ptr y s' proof (prove)
goal (2 subgoals):
 1. \<And>ptra. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> valid_obj ptra (default_object ty dev us) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 2. \<And>ptra y. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some y\<rbrakk> \<Longrightarrow> valid_obj ptra y (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ptra y. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some y\<rbrakk> \<Longrightarrow> valid_obj ptra y (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ptra y. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some y\<rbrakk> \<Longrightarrow> case y of CNode sz cs \<Rightarrow> valid_cs sz cs (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | TCB t \<Rightarrow> valid_tcb ptra t (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | Endpoint p \<Rightarrow> valid_ep p (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | Notification p \<Rightarrow> valid_ntfn p (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | ArchObj ao \<Rightarrow> arch_valid_obj ao (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ptra y. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some y\<rbrakk> \<Longrightarrow> ?ptr27 ptra y \<in> dom (kheap s)
 2. \<And>ptra y. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some y; \<exists>obj. kheap s (?ptr27 ptra y) = Some obj \<and> valid_obj (?ptr27 ptra y) obj s\<rbrakk> \<Longrightarrow> case y of CNode sz cs \<Rightarrow> valid_cs sz cs (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | TCB t \<Rightarrow> valid_tcb ptra t (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | Endpoint p \<Rightarrow> valid_ep p (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | Notification p \<Rightarrow> valid_ntfn p (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | ArchObj ao \<Rightarrow> arch_valid_obj ao (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ptra y. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some y; \<exists>obj. kheap s ptra = Some obj \<and> valid_obj ptra obj s\<rbrakk> \<Longrightarrow> case y of CNode sz cs \<Rightarrow> valid_cs sz cs (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | TCB t \<Rightarrow> valid_tcb ptra t (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | Endpoint p \<Rightarrow> valid_ep p (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | Notification p \<Rightarrow> valid_ntfn p (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) | ArchObj ao \<Rightarrow> arch_valid_obj ao (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x11 x12. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (CNode x11 x12); valid_cs x11 x12 s\<rbrakk> \<Longrightarrow> valid_cs x11 x12 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_tcb ptra x2 s\<rbrakk> \<Longrightarrow> valid_tcb ptra x2 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x11 x12 cap. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (CNode x11 x12); cap \<in> ran x12; \<forall>cap\<in>ran x12. s \<turnstile> cap; valid_cs_size x11 x12\<rbrakk> \<Longrightarrow> s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> cap
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_tcb ptra x2 s\<rbrakk> \<Longrightarrow> valid_tcb ptra x2 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x11 x12 cap. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (CNode x11 x12); cap \<in> ran x12; valid_cs_size x11 x12; s \<turnstile> cap\<rbrakk> \<Longrightarrow> s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> cap
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_tcb ptra x2 s\<rbrakk> \<Longrightarrow> valid_tcb ptra x2 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x11 x12 cap a. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (CNode x11 x12); valid_cs_size x11 x12; s \<turnstile> cap; x12 a = Some cap\<rbrakk> \<Longrightarrow> s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> cap
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_tcb ptra x2 s\<rbrakk> \<Longrightarrow> valid_tcb ptra x2 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x11 x12 cap a. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (CNode x11 x12); valid_cs_size x11 x12; x12 a = Some cap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (?oref86 ptra x11 x12 cap a, ?cref86 ptra x11 x12 cap a) s
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_tcb ptra x2 s\<rbrakk> \<Longrightarrow> valid_tcb ptra x2 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x11 x12 cap a. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (CNode x11 x12); x12 a = Some cap; x11 < word_bits - cte_level_bits; well_formed_cnode_n x11 x12; \<forall>tcb. kheap s (?oref86 ptra x11 x12 cap a) = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases (?cref86 ptra x11 x12 cap a) \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get tcb)\<rbrakk> \<Longrightarrow> \<exists>sz fun. kheap s (?oref86 ptra x11 x12 cap a) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (?cref86 ptra x11 x12 cap a) = Some cap
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_tcb ptra x2 s\<rbrakk> \<Longrightarrow> valid_tcb ptra x2 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_tcb ptra x2 s\<rbrakk> \<Longrightarrow> valid_tcb ptra x2 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 2. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr ptra (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr ptra (tcb_state x2) (getF x2))) \<and> valid_tcb_state (tcb_state x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_bound_ntfn (tcb_bound_notification x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_arch_tcb (tcb_arch x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 2. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr ptra (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr ptra (tcb_state x2) (getF x2))
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr ptra (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_bound_ntfn (tcb_bound_notification x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_arch_tcb (tcb_arch x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x2 a aa b x. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s; tcb_cap_cases x = Some (a, aa, b); s \<turnstile> a x2; b ptra (tcb_state x2) (a x2)\<rbrakk> \<Longrightarrow> s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr> \<turnstile> a x2
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr ptra (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_bound_ntfn (tcb_bound_notification x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_arch_tcb (tcb_arch x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>ptra x2 a aa b x. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s; tcb_cap_cases x = Some (a, aa, b); b ptra (tcb_state x2) (a x2)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (a x2)) (?oref121 ptra x2 a aa b x, ?cref121 ptra x2 a aa b x) s
 2. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr ptra (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_bound_ntfn (tcb_bound_notification x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_arch_tcb (tcb_arch x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 5. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>ptra x2. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (TCB x2); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr ptra (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_bound_ntfn (tcb_bound_notification x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) \<and> valid_arch_tcb (tcb_arch x2) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 2. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>ptra x3. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Endpoint x3); valid_ep x3 s\<rbrakk> \<Longrightarrow> valid_ep x3 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 2. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 3. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ptra x4. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (Notification x4); valid_ntfn x4 s\<rbrakk> \<Longrightarrow> valid_ntfn x4 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 2. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ptra x5. \<lbrakk>pspace_aligned s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; ptra \<notin> set (retype_addrs ptr ty n us); kheap s ptra = Some (ArchObj x5); arch_valid_obj x5 s\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal:
No subgoals!