theory IsolatedThreadAction

lemma isolate_thread_actions_asUser:
  "\<lbrakk> idx t' = t; inj idx; f = (\<lambda>s. ({(v, g s)}, False)) \<rbrakk> \<Longrightarrow>
   monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s)
      (asUser t f)
      (isolate_thread_actions idx (return v)
           (\<lambda>tsrs. (tsrs (t' := TCBStateRegs (tsrState (tsrs t'))
                                    (g (tsrContext (tsrs t'))))))
            id)" apply (simp add: asUser_def liftM_def isolate_thread_actions_def split_def
                   select_f_returns bind_assoc select_f_singleton_return
                   threadGet_def threadSet_def) apply (clarsimp simp: monadic_rewrite_def) apply (frule_tac x=t' in spec) apply (drule obj_at_ko_at', clarsimp) apply (simp add: exec_gets getSchedulerAction_def exec_modify objBits_defs
                   getObject_return_tcb setObject_modify_tcb o_def
             cong: bind_apply_cong)+ apply (simp add: partial_overwrite_fun_upd return_def get_tcb_state_regs_ko_at') apply (rule kernel_state.fold_congs[OF refl refl]) apply (clarsimp simp: partial_overwrite_get_tcb_state_regs
                        put_tcb_state_regs_ko_at') apply (case_tac ko, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx t' = t; inj idx; f = (\<lambda>s. ({(v, g s)}, False))\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (asUser t f) (isolate_thread_actions idx (return v) (\<lambda>tsrs. tsrs(t' := TCBStateRegs (tsrState (tsrs t')) (g (tsrContext (tsrs t'))))) id) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx t' = t; inj idx; f = (\<lambda>s. ({(v, g s)}, False))\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (do x <- getObject t;
xa <- getObject t;
y <- setObject t (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch x))) (tcbArch xa)) xa);
return v
od) (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- getSchedulerAction;
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx (tcbs(t' := TCBStateRegs (tsrState (tcbs t')) (g (tsrContext (tcbs t')))))) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return v
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; f = (\<lambda>s. ({(v, g s)}, False)); t = idx t'; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (do x <- getObject (idx t');
xa <- getObject (idx t');
y <- setObject (idx t') (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch x))) (tcbArch xa)) xa);
return v
od) s = (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- getSchedulerAction;
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx (tcbs(t' := TCBStateRegs (tsrState (tcbs t')) (g (tsrContext (tcbs t')))))) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return v
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; f = (\<lambda>s. ({(v, g s)}, False)); t = idx t'; \<forall>x. tcb_at' (idx x) s; tcb_at' (idx t') s\<rbrakk> \<Longrightarrow> (do x <- getObject (idx t');
xa <- getObject (idx t');
y <- setObject (idx t') (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch x))) (tcbArch xa)) xa);
return v
od) s = (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- getSchedulerAction;
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx (tcbs(t' := TCBStateRegs (tsrState (tcbs t')) (g (tsrContext (tcbs t')))))) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return v
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>inj idx; f = (\<lambda>s. ({(v, g s)}, False)); t = idx t'; \<forall>x. tcb_at' (idx x) s; ko_at' ko (idx t') s\<rbrakk> \<Longrightarrow> (do x <- getObject (idx t');
xa <- getObject (idx t');
y <- setObject (idx t') (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch x))) (tcbArch xa)) xa);
return v
od) s = (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- getSchedulerAction;
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx (tcbs(t' := TCBStateRegs (tsrState (tcbs t')) (g (tsrContext (tcbs t')))))) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return v
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>inj idx; f = (\<lambda>s. ({(v, g s)}, False)); t = idx t'; \<forall>x. tcb_at' (idx x) s; ko_at' ko (idx t') s\<rbrakk> \<Longrightarrow> return v (ksPSpace_update (\<lambda>ps. ps(idx t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch ko))) (tcbArch ko)) ko))) s) = return v (ksPSpace_update (partial_overwrite idx ((\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x)))(t' := TCBStateRegs (tsrState (get_tcb_state_regs (ksPSpace s (idx t')))) (g (tsrContext (get_tcb_state_regs (ksPSpace s (idx t')))))))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>inj idx; f = (\<lambda>s. ({(v, g s)}, False)); t = idx t'; \<forall>x. tcb_at' (idx x) s; ko_at' ko (idx t') s\<rbrakk> \<Longrightarrow> ksPSpace_update (\<lambda>ps. ps(idx t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch ko))) (tcbArch ko)) ko))) s = ksPSpace_update (\<lambda>ps. (partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x))) ps)(idx t' := put_tcb_state_regs (TCBStateRegs (tcbState ko) (g (atcbContextGet (tcbArch ko)))) (ps (idx t')))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko va. \<lbrakk>inj idx; f = (\<lambda>s. ({(v, g s)}, False)); t = idx t'; \<forall>x. tcb_at' (idx x) s; ko_at' ko (idx t') s; ksPSpace s = va\<rbrakk> \<Longrightarrow> va(idx t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch ko))) (tcbArch ko)) ko)) = (partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x))) va)(idx t' := put_tcb_state_regs (TCBStateRegs (tcbState ko) (g (atcbContextGet (tcbArch ko)))) (va (idx t'))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>inj idx; f = (\<lambda>s. ({(v, g s)}, False)); t = idx t'; \<forall>x. tcb_at' (idx x) s; ko_at' ko (idx t') s\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch ko))) (tcbArch ko)) ko)) = (ksPSpace s)(idx t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (g (atcbContextGet (tcbArch ko))) (tcbArch ko)) (tcbState_update (\<lambda>_. tcbState ko) ko))) proof (prove)
goal:
No subgoals!