theory IsolatedThreadAction

lemma isolate_thread_actions_wrap_bind:
  "inj idx \<Longrightarrow>
   do x \<leftarrow> isolate_thread_actions idx a b c;
      isolate_thread_actions idx (d x) e f
   od =
   isolate_thread_actions idx
             (do x \<leftarrow> isolate_thread_actions idx a id id;
                 isolate_thread_actions idx (d x) id id
                od) (e o b) (f o c)
   " apply (rule ext) apply (clarsimp simp: isolate_thread_actions_def bind_assoc split_def
                        bind_select_f_bind[symmetric] liftM_def
                        select_f_returns select_f_selects
                        getSchedulerAction_def) apply (clarsimp simp: exec_gets getSchedulerAction_def o_def) apply (rule select_bind_eq) apply (simp add: exec_gets exec_modify o_def) apply (rule select_bind_eq) apply (simp add: exec_modify) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> do x <- isolate_thread_actions idx a b c;
isolate_thread_actions idx (d x) e f
od = isolate_thread_actions idx (do x <- isolate_thread_actions idx a id id;
isolate_thread_actions idx (d x) id id
od) (e \<circ> b) (f \<circ> c) proof (prove)
goal (1 subgoal):
 1. \<And>x. inj idx \<Longrightarrow> (do x <- isolate_thread_actions idx a b c;
isolate_thread_actions idx (d x) e f
od) x = isolate_thread_actions idx (do x <- isolate_thread_actions idx a id id;
isolate_thread_actions idx (d x) id id
od) (e \<circ> b) (f \<circ> c) x proof (prove)
goal (1 subgoal):
 1. \<And>x. inj idx \<Longrightarrow> (do x <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
xa <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
xb <- gets ksSchedulerAction;
x <- select_f (a x);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (b xa)) (snd x\<lparr>ksSchedulerAction := c xb\<rparr>));
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;
p <- select_f (d (fst x) s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e tcbs)) (snd p\<lparr>ksSchedulerAction := f sa\<rparr>));
return (fst p)
od) x = (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;
x <- select_f (a (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
xa <- select_f (d (fst x) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined) \<circ> partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (snd x)\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx (e (b tcbs)) \<circ> partial_overwrite idx (get_tcb_state_regs \<circ> partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) (ksPSpace (snd x)) \<circ> idx)) (snd xa\<lparr>ksSchedulerAction := f (c sa)\<rparr>));
return (fst xa)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. inj idx \<Longrightarrow> (do xa <- select_f (a (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) x\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa))))) (snd xa\<lparr>ksSchedulerAction := c (ksSchedulerAction x)\<rparr>));
s <- gets (\<lambda>x. ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) x\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>);
tcbs <- gets (\<lambda>s x. get_tcb_state_regs (ksPSpace s (idx x)));
sa <- gets ksSchedulerAction;
p <- select_f (d (fst xa) s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e tcbs)) (snd p\<lparr>ksSchedulerAction := f sa\<rparr>));
return (fst p)
od) x = (do xa <- select_f (a (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) x\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
xa <- select_f (d (fst xa) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) (snd xa)\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa)))))) (snd xa\<lparr>ksSchedulerAction := f (c (ksSchedulerAction x))\<rparr>));
return (fst xa)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>inj idx; xa \<in> fst (a (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) x\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))\<rbrakk> \<Longrightarrow> (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa))))) (snd xa\<lparr>ksSchedulerAction := c (ksSchedulerAction x)\<rparr>));
s <- gets (\<lambda>x. ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) x\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>);
tcbs <- gets (\<lambda>s x. get_tcb_state_regs (ksPSpace s (idx x)));
sa <- gets ksSchedulerAction;
p <- select_f (d (fst xa) s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e tcbs)) (snd p\<lparr>ksSchedulerAction := f sa\<rparr>));
return (fst p)
od) x = (do xa <- select_f (d (fst xa) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) (snd xa)\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa)))))) (snd xa\<lparr>ksSchedulerAction := f (c (ksSchedulerAction x))\<rparr>));
return (fst xa)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>inj idx; xa \<in> fst (a (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) x\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))\<rbrakk> \<Longrightarrow> (do p <- select_f (d (fst xa) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) (snd xa)\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa)))))) (snd p\<lparr>ksSchedulerAction := f (c (ksSchedulerAction x))\<rparr>));
return (fst p)
od) (ksPSpace_update (partial_overwrite idx (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa))))) (snd xa\<lparr>ksSchedulerAction := c (ksSchedulerAction x)\<rparr>)) = (do xa <- select_f (d (fst xa) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) (snd xa)\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa)))))) (snd xa\<lparr>ksSchedulerAction := f (c (ksSchedulerAction x))\<rparr>));
return (fst xa)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>inj idx; xa \<in> fst (a (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) x\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)); xb \<in> fst (d (fst xa) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) (snd xa)\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))\<rbrakk> \<Longrightarrow> (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa)))))) (snd xb\<lparr>ksSchedulerAction := f (c (ksSchedulerAction x))\<rparr>));
return (fst xb)
od) (ksPSpace_update (partial_overwrite idx (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa))))) (snd xa\<lparr>ksSchedulerAction := c (ksSchedulerAction x)\<rparr>)) = (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (e (b (\<lambda>xa. get_tcb_state_regs (ksPSpace x (idx xa)))))) (snd xb\<lparr>ksSchedulerAction := f (c (ksSchedulerAction x))\<rparr>));
return (fst xb)
od) x proof (prove)
goal:
No subgoals!