theory IsolatedThreadAction

lemma select_f_isolatable:
  "thread_actions_isolatable idx (select_f v)" apply (clarsimp simp: thread_actions_isolatable_def
                        isolate_thread_actions_def
                        split_def select_f_selects liftM_def bind_assoc) apply (rule monadic_rewrite_guard_imp, rule monadic_rewrite_transverse) apply (rule monadic_rewrite_drop_modify monadic_rewrite_bind_tail)+ apply wp+ apply (simp add: gets_bind_ign getSchedulerAction_def) apply (rule monadic_rewrite_refl) apply (simp add: ksPSpace_update_partial_id o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (select_f v) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (select_f v) (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;
x <- select_f v;
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx tcbs) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return x
od) proof (prove)
goal (3 subgoals):
 1. inj idx \<Longrightarrow> monadic_rewrite False True ?Q7 (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;
x <- select_f v;
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx tcbs) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return x
od) ?b7
 2. inj idx \<Longrightarrow> monadic_rewrite False True ?P7 (select_f v) ?b7
 3. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (?P7 and ?Q7) s proof (prove)
goal (6 subgoals):
 1. \<And>s tcbs sa. inj idx \<Longrightarrow> \<lbrace>?Q16 s tcbs sa\<rbrace> select_f v \<lbrace>\<lambda>x. (=) (ksPSpace_update (partial_overwrite idx tcbs) (s\<lparr>ksSchedulerAction := sa\<rparr>))\<rbrace>
 2. \<And>s tcbs. inj idx \<Longrightarrow> \<lbrace>?Q13 s tcbs\<rbrace> getSchedulerAction \<lbrace>?Q16 s tcbs\<rbrace>
 3. \<And>s. inj idx \<Longrightarrow> \<lbrace>?Q10 s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q13 s\<rbrace>
 4. inj idx \<Longrightarrow> \<lbrace>?Q7\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q10\<rbrace>
 5. inj idx \<Longrightarrow> monadic_rewrite False True ?P7 (select_f v) (do x <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
x <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
x <- getSchedulerAction;
select_f v >>= return
od)
 6. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (?P7 and ?Q7) s proof (prove)
goal (2 subgoals):
 1. inj idx \<Longrightarrow> monadic_rewrite False True ?P7 (select_f v) (do x <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
x <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
x <- getSchedulerAction;
select_f v >>= return
od)
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (?P7 and (\<lambda>s. \<forall>x\<in>fst v. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) ((ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) s\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>) = s)) s proof (prove)
goal (2 subgoals):
 1. inj idx \<Longrightarrow> monadic_rewrite False True ?P7 (select_f v) (select_f v)
 2. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (?P7 and (\<lambda>s. \<forall>x\<in>fst v. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) ((ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) s\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>) = s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<forall>x\<in>fst v. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) ((ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) s\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>) = s)) s proof (prove)
goal:
No subgoals!