theory IsolatedThreadAction

lemma monadic_rewrite_isolate_final2:
  assumes  mr: "monadic_rewrite F E Q f g"
      and eqs: "\<And>s tsrs. \<lbrakk> P s; tsrs = get_tcb_state_regs o ksPSpace s o idx \<rbrakk>
                      \<Longrightarrow> f' tsrs = g' tsrs"
               "\<And>s. P s \<Longrightarrow> f'' (ksSchedulerAction s) = g'' (ksSchedulerAction s)"
               "\<And>s tsrs sa. R s \<Longrightarrow>
                           Q ((ksPSpace_update (partial_overwrite idx tsrs)
                                      s) (| ksSchedulerAction := sa |))"
  shows
  "monadic_rewrite F E (P and R)
         (isolate_thread_actions idx f f' f'')
         (isolate_thread_actions idx g g' g'')" apply (simp add: isolate_thread_actions_def split_def) apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_bind_tail)+ apply (rule_tac P="\<lambda> s'. Q s" in monadic_rewrite_bind) apply (insert mr)[1] apply (simp add: monadic_rewrite_def select_f_def) apply auto[1] apply (rule_tac P="P and (\<lambda>s. tcbs = get_tcb_state_regs o ksPSpace s o idx
                                             \<and> sa = ksSchedulerAction s)"
                    in monadic_rewrite_pre_imp_eq) apply (clarsimp simp: exec_modify eqs return_def) apply wp+ apply (clarsimp simp: o_def eqs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (P and R) (isolate_thread_actions idx f f' f'') (isolate_thread_actions idx g g' g'') proof (prove)
goal (1 subgoal):
 1. monadic_rewrite F E (P and R) (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 (f s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd p\<lparr>ksSchedulerAction := f'' 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 (g s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (g' tcbs)) (snd p\<lparr>ksSchedulerAction := g'' sa\<rparr>));
return (fst p)
od) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite F E ?Q (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 (f s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd p\<lparr>ksSchedulerAction := f'' 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 (g s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (g' tcbs)) (snd p\<lparr>ksSchedulerAction := g'' sa\<rparr>));
return (fst p)
od)
 2. \<And>s. (P and R) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>s tcbs sa. monadic_rewrite F E (?Q9 s tcbs sa) (do p <- select_f (f s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd p\<lparr>ksSchedulerAction := f'' sa\<rparr>));
return (fst p)
od) (do p <- select_f (g s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (g' tcbs)) (snd p\<lparr>ksSchedulerAction := g'' sa\<rparr>));
return (fst p)
od)
 2. \<And>s tcbs. \<lbrace>?Q6 s tcbs\<rbrace> getSchedulerAction \<lbrace>?Q9 s tcbs\<rbrace>
 3. \<And>s. \<lbrace>?Q3 s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q6 s\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q3\<rbrace>
 5. \<And>s. (P and R) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>s tcbs sa. monadic_rewrite F E (\<lambda>s'. Q s) (select_f (f s)) (select_f (g s))
 2. \<And>s tcbs sa x. monadic_rewrite F E (?Q12 s tcbs sa x) (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd x\<lparr>ksSchedulerAction := f'' sa\<rparr>));
return (fst x)
od) (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (g' tcbs)) (snd x\<lparr>ksSchedulerAction := g'' sa\<rparr>));
return (fst x)
od)
 3. \<And>s tcbs sa. \<lbrace>?R12 s tcbs sa\<rbrace> select_f (g s) \<lbrace>?Q12 s tcbs sa\<rbrace>
 4. \<And>s tcbs. \<lbrace>?Q6 s tcbs\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. (\<lambda>s'. Q s) and ?R12 s tcbs sa\<rbrace>
 5. \<And>s. \<lbrace>?Q3 s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q6 s\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q3\<rbrace>
 7. \<And>s. (P and R) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>s tcbs sa. monadic_rewrite F E Q f g \<Longrightarrow> monadic_rewrite F E (\<lambda>s'. Q s) (select_f (f s)) (select_f (g s))
 2. \<And>s tcbs sa x. monadic_rewrite F E (?Q12 s tcbs sa x) (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd x\<lparr>ksSchedulerAction := f'' sa\<rparr>));
return (fst x)
od) (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (g' tcbs)) (snd x\<lparr>ksSchedulerAction := g'' sa\<rparr>));
return (fst x)
od)
 3. \<And>s tcbs sa. \<lbrace>?R12 s tcbs sa\<rbrace> select_f (g s) \<lbrace>?Q12 s tcbs sa\<rbrace>
 4. \<And>s tcbs. \<lbrace>?Q6 s tcbs\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. (\<lambda>s'. Q s) and ?R12 s tcbs sa\<rbrace>
 5. \<And>s. \<lbrace>?Q3 s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q6 s\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q3\<rbrace>
 7. \<And>s. (P and R) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>s. \<forall>s. Q s \<and> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (E \<longrightarrow> f s = g s) \<and> (\<not> E \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s))) \<Longrightarrow> Q s \<and> (F \<longrightarrow> \<not> snd (f s)) \<longrightarrow> \<not> E \<longrightarrow> (\<forall>sa. fst (g s) \<times> {sa} \<subseteq> fst (f s) \<times> {sa}) \<and> (snd (g s) \<longrightarrow> snd (f s))
 2. \<And>s tcbs sa x. monadic_rewrite F E (?Q12 s tcbs sa x) (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd x\<lparr>ksSchedulerAction := f'' sa\<rparr>));
return (fst x)
od) (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (g' tcbs)) (snd x\<lparr>ksSchedulerAction := g'' sa\<rparr>));
return (fst x)
od)
 3. \<And>s tcbs sa. \<lbrace>?R12 s tcbs sa\<rbrace> select_f (g s) \<lbrace>?Q12 s tcbs sa\<rbrace>
 4. \<And>s tcbs. \<lbrace>?Q6 s tcbs\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. (\<lambda>s'. Q s) and ?R12 s tcbs sa\<rbrace>
 5. \<And>s. \<lbrace>?Q3 s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q6 s\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q3\<rbrace>
 7. \<And>s. (P and R) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>s tcbs sa x. monadic_rewrite F E (?Q12 s tcbs sa x) (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd x\<lparr>ksSchedulerAction := f'' sa\<rparr>));
return (fst x)
od) (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (g' tcbs)) (snd x\<lparr>ksSchedulerAction := g'' sa\<rparr>));
return (fst x)
od)
 2. \<And>s tcbs sa. \<lbrace>?R12 s tcbs sa\<rbrace> select_f (g s) \<lbrace>?Q12 s tcbs sa\<rbrace>
 3. \<And>s tcbs. \<lbrace>?Q6 s tcbs\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. (\<lambda>s'. Q s) and ?R12 s tcbs sa\<rbrace>
 4. \<And>s. \<lbrace>?Q3 s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q6 s\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q3\<rbrace>
 6. \<And>s. (P and R) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>s tcbs sa x sb. (P and (\<lambda>s. tcbs = get_tcb_state_regs \<circ> ksPSpace s \<circ> idx \<and> sa = ksSchedulerAction s)) sb \<Longrightarrow> (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd x\<lparr>ksSchedulerAction := f'' sa\<rparr>));
return (fst x)
od) sb = (do y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (g' tcbs)) (snd x\<lparr>ksSchedulerAction := g'' sa\<rparr>));
return (fst x)
od) sb
 2. \<And>s tcbs sa. \<lbrace>?R12 s tcbs sa\<rbrace> select_f (g s) \<lbrace>\<lambda>x. P and (\<lambda>s. tcbs = get_tcb_state_regs \<circ> ksPSpace s \<circ> idx \<and> sa = ksSchedulerAction s)\<rbrace>
 3. \<And>s tcbs. \<lbrace>?Q6 s tcbs\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. (\<lambda>s'. Q s) and ?R12 s tcbs sa\<rbrace>
 4. \<And>s. \<lbrace>?Q3 s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q6 s\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q3\<rbrace>
 6. \<And>s. (P and R) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>s tcbs sa. \<lbrace>?R12 s tcbs sa\<rbrace> select_f (g s) \<lbrace>\<lambda>x. P and (\<lambda>s. tcbs = get_tcb_state_regs \<circ> ksPSpace s \<circ> idx \<and> sa = ksSchedulerAction s)\<rbrace>
 2. \<And>s tcbs. \<lbrace>?Q6 s tcbs\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. (\<lambda>s'. Q s) and ?R12 s tcbs sa\<rbrace>
 3. \<And>s. \<lbrace>?Q3 s\<rbrace> gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<lbrace>?Q6 s\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) \<lbrace>?Q3\<rbrace>
 5. \<And>s. (P and R) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and R) s \<Longrightarrow> ((\<lambda>s'. Q ((ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) s)) and (\<lambda>sa. \<forall>x\<in>fst (g ((ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) s)). (P and (\<lambda>sa. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx = get_tcb_state_regs \<circ> ksPSpace sa \<circ> idx \<and> ksSchedulerAction s = ksSchedulerAction sa)) sa)) s proof (prove)
goal:
No subgoals!