theory Retype_R

lemma retype_region2_ext_retype_region_ext_futz:
  "retype_region2_ext ptrs type >>= (\<lambda>_. retype_region2_extra_ext ptrs type)
 = retype_region_ext ptrs type" proof(cases type) case TCBObject have complete_futz:
    "\<And>F x. modify (ekheap_update (\<lambda>_. F (cur_domain x) (ekheap x))) x = modify (ekheap_update (\<lambda>ekh. F (cur_domain x) ekh)) x" by (simp add: modify_def get_def get_etcb_def put_def bind_def return_def) have second_futz:
  "\<And>f G.
   do modify (ekheap_update f);
      cdom \<leftarrow> gets (\<lambda>s. cur_domain s);
      G cdom
   od =
   do cdom \<leftarrow> gets (\<lambda>s. cur_domain s);
      modify (ekheap_update f);
      G cdom
   od" by (simp add: bind_def gets_def get_def return_def simpler_modify_def) from TCBObject show ?thesis apply (clarsimp simp: retype_region_ext_def retype_region2_ext_def retype_region2_extra_ext_def when_def bind_assoc) apply (clarsimp simp: exec_gets fun_eq_iff) apply (subst complete_futz) apply (simp add: second_futz[simplified] exec_gets) apply (simp add: default_ext_def exec_modify) apply (subst mapM_x_modify_futz[where ptrs="rev ptrs", simplified]) apply (simp add: foldr_upd_app_if_eta_futz) apply (simp add: modify_def exec_get put_def o_def) apply (simp add: foldr_upd_app_if_eta_futz foldr_conv_fold awkward_fold_futz) apply (simp cong: if_cong) done qed (auto simp: fun_eq_iff retype_region_ext_def retype_region2_ext_def retype_region2_extra_ext_def
                put_def gets_def get_def bind_def return_def mk_ef_def modify_def foldr_upd_app_if' when_def default_ext_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type proof (state)
goal (6 subgoals):
 1. type = Structures_A.apiobject_type.Untyped \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 2. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 3. type = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 4. type = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 5. type = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 6. \<And>x6. type = ArchObject x6 \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type proof (state)
this:
type = Structures_A.apiobject_type.TCBObject

goal (6 subgoals):
 1. type = Structures_A.apiobject_type.Untyped \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 2. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 3. type = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 4. type = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 5. type = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 6. \<And>x6. type = ArchObject x6 \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type proof (prove)
goal (1 subgoal):
 1. \<And>F x. modify (ekheap_update (\<lambda>_. F (cur_domain x) (ekheap x))) x = modify (ekheap_update (F (cur_domain x))) x proof (state)
this:
modify (ekheap_update (\<lambda>_. ?F (cur_domain ?x) (ekheap ?x))) ?x = modify (ekheap_update (?F (cur_domain ?x))) ?x

goal (6 subgoals):
 1. type = Structures_A.apiobject_type.Untyped \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 2. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 3. type = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 4. type = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 5. type = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 6. \<And>x6. type = ArchObject x6 \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type proof (prove)
goal (1 subgoal):
 1. \<And>f G. do modify (ekheap_update f);
gets cur_domain >>= G
od = do cdom <- gets cur_domain;
modify (ekheap_update f);
G cdom
od proof (state)
this:
do modify (ekheap_update ?f);
gets cur_domain >>= ?G
od = do cdom <- gets cur_domain;
modify (ekheap_update ?f);
?G cdom
od

goal (6 subgoals):
 1. type = Structures_A.apiobject_type.Untyped \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 2. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 3. type = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 4. type = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 5. type = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 6. \<And>x6. type = ArchObject x6 \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type proof (chain)
picking this:
type = Structures_A.apiobject_type.TCBObject proof (prove)
using this:
type = Structures_A.apiobject_type.TCBObject

goal (1 subgoal):
 1. do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type proof (prove)
goal (1 subgoal):
 1. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> do _ <- modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext Structures_A.apiobject_type.TCBObject default_domain)) ptrs));
cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od = do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext Structures_A.apiobject_type.TCBObject cdom)) ptrs ekh))
od proof (prove)
goal (1 subgoal):
 1. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> (do _ <- modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext Structures_A.apiobject_type.TCBObject default_domain)) ptrs));
cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od) x = modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext Structures_A.apiobject_type.TCBObject (cur_domain x))) ptrs (ekheap x))) x proof (prove)
goal (1 subgoal):
 1. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> (do _ <- modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext Structures_A.apiobject_type.TCBObject default_domain)) ptrs));
cdom <- gets cur_domain;
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cdom))) ptrs
od) x = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext Structures_A.apiobject_type.TCBObject (cur_domain x))) ptrs)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> (do _ <- modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext Structures_A.apiobject_type.TCBObject default_domain)) ptrs));
mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cur_domain x))) ptrs
od) x = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext Structures_A.apiobject_type.TCBObject (cur_domain x))) ptrs)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> mapM_x (ethread_set (tcb_domain_update (\<lambda>_. cur_domain x))) ptrs (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb)) ptrs) x) = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb\<lparr>tcb_domain := cur_domain x\<rparr>)) ptrs)) x proof (prove)
goal (2 subgoals):
 1. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> \<forall>ptr\<in>set ptrs. \<exists>y. ekheap (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb)) ptrs) x) ptr = Some y
 2. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> the (ekh p)\<lparr>tcb_domain := cur_domain x\<rparr>)) (rev ptrs))) (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb)) ptrs) x) = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb\<lparr>tcb_domain := cur_domain x\<rparr>)) ptrs)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> the (ekh p)\<lparr>tcb_domain := cur_domain x\<rparr>)) (rev ptrs))) (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb)) ptrs) x) = modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb\<lparr>tcb_domain := cur_domain x\<rparr>)) ptrs)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ekheap_update (\<lambda>xa. foldr (\<lambda>p ekh. ekh(p \<mapsto> the (ekh p)\<lparr>tcb_domain := cur_domain x\<rparr>)) (rev ptrs) (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb)) ptrs xa)) x = ekheap_update (foldr (\<lambda>p ekh. ekh(p \<mapsto> default_etcb\<lparr>tcb_domain := cur_domain x\<rparr>)) ptrs) x proof (prove)
goal (1 subgoal):
 1. \<And>x. type = Structures_A.apiobject_type.TCBObject \<Longrightarrow> ekheap_update (\<lambda>xa xb. if xb \<in> set ptrs then Some (the (if xb \<in> set ptrs then Some default_etcb else xa xb)\<lparr>tcb_domain := cur_domain x\<rparr>) else xa xb) x = ekheap_update (\<lambda>g xa. if xa \<in> set ptrs then Some (default_etcb\<lparr>tcb_domain := cur_domain x\<rparr>) else g xa) x proof (prove)
goal:
No subgoals! proof (state)
this:
do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type

goal (5 subgoals):
 1. type = Structures_A.apiobject_type.Untyped \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 2. type = Structures_A.apiobject_type.EndpointObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 3. type = Structures_A.apiobject_type.NotificationObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 4. type = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type
 5. \<And>x6. type = ArchObject x6 \<Longrightarrow> do _ <- retype_region2_ext ptrs type;
retype_region2_extra_ext ptrs type
od = retype_region_ext ptrs type