theory Retype_AC

lemma retype_region_ext_pas_refined:
  "\<lbrace>pas_refined aag and pas_cur_domain aag and K (\<forall>x\<in> set xs. is_subject aag x)\<rbrace>
   retype_region_ext xs ty
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" including no_pre apply (subst and_assoc[symmetric]) apply (wp retype_region_ext_extended.pas_refined_tcb_domain_map_wellformed') apply (simp add: retype_region_ext_def, wp) apply (clarsimp simp: tcb_domain_map_wellformed_aux_def) apply (erule domains_of_state_aux.cases) apply (clarsimp simp: foldr_upd_app_if' fun_upd_def[symmetric] split: if_split_asm) apply (clarsimp simp: default_ext_def default_etcb_def split: apiobject_type.splits) defer apply (force intro: domtcbs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and K (\<forall>x\<in>set xs. is_subject aag x)\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and K (\<forall>x\<in>set xs. is_subject aag x)\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (pas_cur_domain aag and K (\<forall>x\<in>set xs. is_subject aag x))\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_domain_map_wellformed aag and (pas_cur_domain aag and K (\<forall>x\<in>set xs. is_subject aag x))\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. tcb_domain_map_wellformed aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_domain_map_wellformed aag and (pas_cur_domain aag and (\<lambda>y. \<forall>x\<in>set xs. is_subject aag x))) s \<Longrightarrow> tcb_domain_map_wellformed aag (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext ty (cur_domain s))) xs (ekheap s)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> domains_of_state_aux (foldr (\<lambda>p ekh a. if a = p then default_ext ty (cur_domain s) else ekh a) xs (ekheap s)); \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; pas_cur_domain aag s; \<forall>x\<in>set xs. is_subject aag x\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal (1 subgoal):
 1. \<And>s a b ptr etcb d. \<lbrakk>\<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; pas_cur_domain aag s; \<forall>x\<in>set xs. is_subject aag x; a = ptr; b = d; foldr (\<lambda>p ekh a. if a = p then default_ext ty (cur_domain s) else ekh a) xs (ekheap s) ptr = Some etcb; d = tcb_domain etcb\<rbrakk> \<Longrightarrow> pasObjectAbs aag a \<in> pasDomainAbs aag b proof (prove)
goal (2 subgoals):
 1. \<And>s ptr etcb. \<lbrakk>\<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; pas_cur_domain aag s; \<forall>x\<in>set xs. is_subject aag x; ptr \<in> set xs; default_ext ty (cur_domain s) = Some etcb\<rbrakk> \<Longrightarrow> pasSubject aag \<in> pasDomainAbs aag (tcb_domain etcb)
 2. \<And>s ptr etcb. \<lbrakk>\<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; pas_cur_domain aag s; \<forall>x\<in>set xs. is_subject aag x; ptr \<notin> set xs; ekheap s ptr = Some etcb\<rbrakk> \<Longrightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag (tcb_domain etcb) proof (prove)
goal (1 subgoal):
 1. \<And>s ptr etcb. \<lbrakk>\<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; pas_cur_domain aag s; \<forall>x\<in>set xs. is_subject aag x; ptr \<notin> set xs; ekheap s ptr = Some etcb\<rbrakk> \<Longrightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag (tcb_domain etcb) proof (prove)
goal (1 subgoal):
 1. \<And>s ptr etcb. \<lbrakk>\<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; pas_cur_domain aag s; \<forall>x\<in>set xs. is_subject aag x; ptr \<notin> set xs; ekheap s ptr = Some etcb\<rbrakk> \<Longrightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag (tcb_domain etcb) proof (prove)
goal:
No subgoals!