theory IsolatedThreadAction

lemma isolate_thread_actions_threadSet_tcbState:
  "\<lbrakk> inj idx; idx t' = t \<rbrakk> \<Longrightarrow>
   monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s)
     (threadSet (tcbState_update (\<lambda>_. st)) t)
     (isolate_thread_actions idx (return ())
         (\<lambda>tsrs. (tsrs (t' := TCBStateRegs st (tsrContext (tsrs t')))))
             id)" apply (simp add: isolate_thread_actions_def bind_assoc split_def
                   select_f_returns getSchedulerAction_def) apply (clarsimp simp: monadic_rewrite_def exec_gets threadSet_def
                        getObject_get_assert bind_assoc liftM_def
                        setObject_modify_assert) apply (frule_tac x=t' in spec, drule obj_at_ko_at') apply (clarsimp simp: exec_gets simpler_modify_def o_def
                intro!: kernel_state.fold_congs[OF refl refl]) apply (simp add: partial_overwrite_fun_upd
                   partial_overwrite_get_tcb_state_regs) apply (clarsimp simp: put_tcb_state_regs_def put_tcb_state_regs_tcb_def
                        projectKOs get_tcb_state_regs_def
                 elim!: obj_atE') apply (case_tac ko) apply (simp add: projectKO_opt_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; idx t' = t\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (threadSet (tcbState_update (\<lambda>_. st)) t) (isolate_thread_actions idx (return ()) (\<lambda>tsrs. tsrs(t' := TCBStateRegs st (tsrContext (tsrs t')))) id) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; idx t' = t\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (threadSet (tcbState_update (\<lambda>_. st)) t) (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 <- gets ksSchedulerAction;
modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx (tcbs(t' := TCBStateRegs st (tsrContext (tcbs t'))))) (s\<lparr>ksSchedulerAction := sa\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; t = idx t'; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(idx t' \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) (the (projectKO_opt (the (ksPSpace s (idx t'))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx ((get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)(t' := TCBStateRegs st (tsrContext (get_tcb_state_regs (ksPSpace s (idx t')))))) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; t = idx t'; \<forall>x. tcb_at' (idx x) s; \<exists>ko. ko_at' ko (idx t') s \<and> True\<rbrakk> \<Longrightarrow> modify (ksPSpace_update (\<lambda>ps. ps(idx t' \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) (the (projectKO_opt (the (ksPSpace s (idx t'))))))))) s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx ((get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)(t' := TCBStateRegs st (tsrContext (get_tcb_state_regs (ksPSpace s (idx t')))))) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>inj idx; t = idx t'; \<forall>x. tcb_at' (idx x) s; ko_at' ko (idx t') s\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx t' \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) (the (projectKO_opt (the (ksPSpace s (idx t'))))))) = partial_overwrite idx ((\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x)))(t' := TCBStateRegs st (tsrContext (get_tcb_state_regs (ksPSpace s (idx t')))))) (ksPSpace s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>inj idx; t = idx t'; \<forall>x. tcb_at' (idx x) s; ko_at' ko (idx t') s\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx t' \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) (the (projectKO_opt (the (ksPSpace s (idx t'))))))) = (ksPSpace s)(idx t' := put_tcb_state_regs (TCBStateRegs st (tsrContext (get_tcb_state_regs (ksPSpace s (idx t'))))) (ksPSpace s (idx t'))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>inj idx; t = idx t'; \<forall>x. tcb_at' (idx x) s; ksPSpace s (idx t') = Some (KOTCB ko); is_aligned (idx t') (objBitsKO (KOTCB ko)); ps_clear (idx t') (objBitsKO (KOTCB ko)) s\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx t' \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) (the (projectKO_opt (KOTCB ko))))) = (ksPSpace s)(idx t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16. \<lbrakk>inj idx; t = idx t'; \<forall>x. tcb_at' (idx x) s; ksPSpace s (idx t') = Some (KOTCB ko); is_aligned (idx t') (objBitsKO (KOTCB ko)); ps_clear (idx t') (objBitsKO (KOTCB ko)) s; ko = Thread x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> (ksPSpace s)(idx t' \<mapsto> KOTCB (tcbState_update (\<lambda>_. st) (the (projectKO_opt (KOTCB ko))))) = (ksPSpace s)(idx t' \<mapsto> KOTCB (tcbArch_update (\<lambda>_. tcbArch ko) (tcbState_update (\<lambda>_. st) ko))) proof (prove)
goal:
No subgoals!