theory IsolatedThreadAction

lemma setThreadState_rewrite_simple:
  "monadic_rewrite True True
     (\<lambda>s. (runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s)
     (setThreadState st t)
     (threadSet (tcbState_update (\<lambda>_. st)) t)" supply if_split[split del] apply (simp add: setThreadState_def when_def) apply (monadic_rewrite_l monadic_rewrite_if_l_False
           \<open>wpsimp wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at'\<close>) 
   (* take the threadSet, drop everything until return () *)
    apply (rule monadic_rewrite_trans[OF monadic_rewrite_bind_tail]) apply (rule monadic_rewrite_symb_exec_l_drop)+ apply (rule monadic_rewrite_refl) apply (wpsimp simp: getCurThread_def
                        wp: hoare_vcg_disj_lift hoare_vcg_imp_lift' threadSet_tcbState_st_tcb_at')+ apply (rule monadic_rewrite_refl) apply (clarsimp simp: obj_at'_def sch_act_simple_def st_tcb_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. (runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s) (setThreadState st t) (threadSet (tcbState_update (\<lambda>_. st)) t) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. (runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s) (setThreadState st t) (threadSet (tcbState_update (\<lambda>_. st)) t) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> runnable' st \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s) (do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
if \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread then rescheduleRequired else return ()
od) (threadSet (tcbState_update (\<lambda>_. st)) t) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
return ()
od) (threadSet (tcbState_update (\<lambda>_. st)) t)
 2. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> runnable' st \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s \<Longrightarrow> ((\<lambda>s. \<not> ksCurThread s \<noteq> t \<longrightarrow> runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
return ()
od) (threadSet (tcbState_update (\<lambda>_. st)) t)
 2. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> runnable' st \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s \<Longrightarrow> ((\<lambda>s. \<not> ksCurThread s \<noteq> t \<longrightarrow> runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) and ?Q1) s proof (prove)
goal (4 subgoals):
 1. \<And>y. monadic_rewrite True True (?Q58 y) (do runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
return ()
od) (?j58 y)
 2. \<lbrace>?P57\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>?Q58\<rbrace>
 3. monadic_rewrite True True ?Q57 (threadSet (tcbState_update (\<lambda>_. st)) t >>= ?j58) (threadSet (tcbState_update (\<lambda>_. st)) t)
 4. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> runnable' st \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s \<Longrightarrow> ((\<lambda>s. \<not> ksCurThread s \<noteq> t \<longrightarrow> runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) and (?P57 and ?Q57)) s proof (prove)
goal (10 subgoals):
 1. \<And>y. monadic_rewrite True True (?Q58 y) (return ()) (?j58 y)
 2. \<And>y P. \<lbrace>P\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. P\<rbrace>
 3. \<And>y. empty_fail getSchedulerAction
 4. \<And>y P. \<lbrace>P\<rbrace> getCurThread \<lbrace>\<lambda>curThread. P\<rbrace>
 5. \<And>y. empty_fail getCurThread
 6. \<And>y P. \<lbrace>P\<rbrace> isRunnable t \<lbrace>\<lambda>runnable. P\<rbrace>
 7. \<And>y. empty_fail (isRunnable t)
 8. \<lbrace>?P57\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>?Q58\<rbrace>
 9. monadic_rewrite True True ?Q57 (threadSet (tcbState_update (\<lambda>_. st)) t >>= ?j58) (threadSet (tcbState_update (\<lambda>_. st)) t)
 10. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> runnable' st \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s \<Longrightarrow> ((\<lambda>s. \<not> ksCurThread s \<noteq> t \<longrightarrow> runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) and (?P57 and ?Q57)) s proof (prove)
goal (9 subgoals):
 1. \<And>y P. \<lbrace>P\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. P\<rbrace>
 2. \<And>y. empty_fail getSchedulerAction
 3. \<And>y P. \<lbrace>P\<rbrace> getCurThread \<lbrace>\<lambda>curThread. P\<rbrace>
 4. \<And>y. empty_fail getCurThread
 5. \<And>y P. \<lbrace>P\<rbrace> isRunnable t \<lbrace>\<lambda>runnable. P\<rbrace>
 6. \<And>y. empty_fail (isRunnable t)
 7. \<lbrace>?P57\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y _. True\<rbrace>
 8. monadic_rewrite True True ?Q57 (do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
return ()
od) (threadSet (tcbState_update (\<lambda>_. st)) t)
 9. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> runnable' st \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s \<Longrightarrow> ((\<lambda>s. \<not> ksCurThread s \<noteq> t \<longrightarrow> runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) and (?P57 and ?Q57)) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q57 (threadSet (tcbState_update (\<lambda>_. st)) t) (threadSet (tcbState_update (\<lambda>_. st)) t)
 2. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> runnable' st \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s \<Longrightarrow> ((\<lambda>s. \<not> ksCurThread s \<noteq> t \<longrightarrow> runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) and ((\<lambda>s. True) and ?Q57)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> runnable' st \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s \<Longrightarrow> ((\<lambda>s. \<not> ksCurThread s \<noteq> t \<longrightarrow> runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) and ((\<lambda>s. True) and (\<lambda>_. True))) s proof (prove)
goal:
No subgoals!