theory IsolatedThreadAction

lemma modify_isolatable:
  assumes swap:"\<And>tsrs act s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow>
            (ksPSpace_update (partial_overwrite idx tsrs) ((f s)\<lparr> ksSchedulerAction := act \<rparr>))
                = f (ksPSpace_update (partial_overwrite idx tsrs)
                      (s \<lparr> ksSchedulerAction := act\<rparr>))"
  shows
     "thread_actions_isolatable idx (modify f)" apply (clarsimp simp: thread_actions_isolatable_def) apply (simp add: isolate_thread_actions_def select_f_returns
                   liftM_def bind_assoc) apply (clarsimp simp: monadic_rewrite_def exec_gets
                   getSchedulerAction_def) apply (simp add: simpler_modify_def) apply (subst swap) apply (simp add: obj_at_partial_overwrite_If) apply (simp add: ksPSpace_update_partial_id o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (modify f) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (modify f) (isolate_thread_actions idx (modify f) id id) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (modify f) (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;
modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx tcbs) (f s\<lparr>ksSchedulerAction := sa\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> modify f s = modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (f (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> f s = ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (f (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> \<forall>x. tcb_at' (idx x) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> f s = f (ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread, ksSchedulerAction := ksSchedulerAction s\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> f s = f (ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread, ksSchedulerAction := ksSchedulerAction s\<rparr>)) proof (prove)
goal:
No subgoals!