theory IsolatedThreadAction

lemma monadic_rewrite_in_isolate_thread_actions:
  "\<lbrakk> inj idx; monadic_rewrite F True P a d \<rbrakk> \<Longrightarrow>
   monadic_rewrite F True (\<lambda>s. P (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread)
                            (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)))
     (isolate_thread_actions idx a b c) (isolate_thread_actions idx d b c)" apply (clarsimp simp: isolate_thread_actions_def split_def) apply (rule monadic_rewrite_bind_tail)+ apply (rule_tac P="\<lambda>_. P s" in monadic_rewrite_bind_head) apply (simp add: monadic_rewrite_def select_f_def) apply wp+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> monadic_rewrite F True (\<lambda>s. P (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)) (isolate_thread_actions idx a b c) (isolate_thread_actions idx d b c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> monadic_rewrite F True (\<lambda>s. P (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)) (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;
p <- select_f (a s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (b tcbs)) (snd p\<lparr>ksSchedulerAction := c sa\<rparr>));
return (fst p)
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;
p <- select_f (d s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (b tcbs)) (snd p\<lparr>ksSchedulerAction := c sa\<rparr>));
return (fst p)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s tcbs sa. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> monadic_rewrite F True (?Q6 s tcbs sa) (do p <- select_f (a s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (b tcbs)) (snd p\<lparr>ksSchedulerAction := c sa\<rparr>));
return (fst p)
od) (do p <- select_f (d s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (b tcbs)) (snd p\<lparr>ksSchedulerAction := c sa\<rparr>));
return (fst p)
od)
 2. \<And>s tcbs. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>?Q3 s tcbs\<rbrace> getSchedulerAction \<lbrace>?Q6 s tcbs\<rbrace>
 3. \<And>s. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>?Q s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q3 s\<rbrace>
 4. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s tcbs sa. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> monadic_rewrite F True (\<lambda>_. P s) (select_f (a s)) (select_f (d s))
 2. \<And>s tcbs. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>?Q3 s tcbs\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa _. P s\<rbrace>
 3. \<And>s. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>?Q s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q3 s\<rbrace>
 4. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s tcbs. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>?Q3 s tcbs\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa _. P s\<rbrace>
 2. \<And>s. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>?Q s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q3 s\<rbrace>
 3. \<lbrakk>inj idx; monadic_rewrite F True P a d\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; monadic_rewrite F True P a d; P (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>)\<rbrakk> \<Longrightarrow> P ((ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) s) proof (prove)
goal:
No subgoals!