theory Ipc_R

lemma setThreadState_not_rct[wp]:
  "\<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<rbrace>
   setThreadState st t
   \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<rbrace>" apply (simp add: setThreadState_def) apply (wp) apply (rule hoare_post_imp [OF _ rescheduleRequired_notresume], simp) apply (simp) apply (wp)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>y runnable curThread action. \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread \<Longrightarrow> \<lbrace>?Q5 y runnable curThread action\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>y runnable curThread. \<lbrace>?B3 y runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. if \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread then ?Q5 y runnable curThread action else (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace>
 3. \<And>y runnable. \<lbrace>?B2 y runnable\<rbrace> getCurThread \<lbrace>?B3 y runnable\<rbrace>
 4. \<And>y. \<lbrace>?B1 y\<rbrace> isRunnable t \<lbrace>?B2 y\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>?B1\<rbrace>
 6. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>y runnable curThread. \<lbrace>?B3 y runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. if \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread then \<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread else (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace>
 2. \<And>y runnable. \<lbrace>?B2 y runnable\<rbrace> getCurThread \<lbrace>?B3 y runnable\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> isRunnable t \<lbrace>?B2 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>?B1\<rbrace>
 5. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>runnable curThread. \<lbrace>?B3 () runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>y runnable. \<lbrace>?B2 y runnable\<rbrace> getCurThread \<lbrace>?B3 y runnable\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> isRunnable t \<lbrace>?B2 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>?B1\<rbrace>
 5. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread proof (prove)
goal:
No subgoals!