theory IsolatedThreadAction

lemma setThreadState_no_sch_change:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
      setThreadState st t
   \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
  (is "Nondet_VCG.valid ?P ?f ?Q") apply (simp add: setThreadState_def setSchedulerAction_def) apply (wp hoare_pre_cont[where f=rescheduleRequired]) apply (rule_tac Q="\<lambda>_. ?P and st_tcb_at' ((=) st) t" in hoare_post_imp) apply (clarsimp split: if_split) apply (clarsimp simp: obj_at'_def st_tcb_at'_def projectKOs) apply (wp threadSet_pred_tcb_at_state) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then \<lambda>_. False else (\<lambda>s. P (ksSchedulerAction s))) s\<rbrace>
 2. \<And>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. ((\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)) and st_tcb_at' ((=) st) t) s \<Longrightarrow> (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then \<lambda>_. False else (\<lambda>s. P (ksSchedulerAction s))) s
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. (\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)) and st_tcb_at' ((=) st) t\<rbrace>
 3. \<And>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>P ResumeCurrentThread; runnable' st; st_tcb_at' ((=) st) (ksCurThread s) s; t = ksCurThread s; \<not> st_tcb_at' runnable' (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> False
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. (\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)) and st_tcb_at' ((=) st) t\<rbrace>
 3. \<And>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_. (\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)) and st_tcb_at' ((=) st) t\<rbrace>
 2. \<And>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s) \<Longrightarrow> P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s) \<and> (tcb_at' t s \<longrightarrow> (if t = t then obj_at' (\<lambda>tcb. st = itcbState (tcb_to_itcb' (tcbState_update (\<lambda>_. st) tcb))) t s else st_tcb_at' ((=) st) t s)) proof (prove)
goal:
No subgoals!