theory Schedule_R

lemma setThreadState_rct:
  "\<lbrace>\<lambda>s. (runnable' st \<or> ksCurThread s \<noteq> t)
        \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace>
   setThreadState st t
   \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>" apply (simp add: setThreadState_def) apply (rule hoare_pre_disj') apply (rule hoare_seq_ext [OF _
                 hoare_vcg_conj_lift
                   [OF threadSet_tcbState_st_tcb_at' [where P=runnable']
                       threadSet_nosch]]) apply (rule hoare_seq_ext [OF _
                 hoare_vcg_conj_lift [OF isRunnable_const isRunnable_inv]]) apply (clarsimp simp: when_def) apply (case_tac x) apply (clarsimp, wp)[1] apply (clarsimp) apply (rule hoare_seq_ext [OF _
                hoare_vcg_conj_lift
                  [OF threadSet_ct threadSet_nosch]]) apply (rule hoare_seq_ext [OF _ isRunnable_inv]) apply (rule hoare_seq_ext [OF _
                hoare_vcg_conj_lift
                  [OF gct_wp gct_wp]]) apply (rename_tac ct) apply (case_tac "ct\<noteq>t") apply (clarsimp simp: when_def) apply (wp)[1] apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (runnable' st \<or> ksCurThread s \<noteq> t) \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (runnable' st \<or> ksCurThread s \<noteq> t) \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. runnable' st \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace>
 2. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>\<lambda>s. st_tcb_at' runnable' t s \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 2. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y x. \<lbrace>\<lambda>s. x \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> x \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 2. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. x \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
if \<not> x \<and> curThread = t \<and> action = ResumeCurrentThread then rescheduleRequired else return ()
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 2. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<Longrightarrow> \<lbrace>\<lambda>s. x \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
if \<not> x \<and> curThread = t \<and> action = ResumeCurrentThread then rescheduleRequired else return ()
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 2. \<And>x. \<not> x \<Longrightarrow> \<lbrace>\<lambda>s. x \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
if \<not> x \<and> curThread = t \<and> action = ResumeCurrentThread then rescheduleRequired else return ()
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 3. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<not> x \<Longrightarrow> \<lbrace>\<lambda>s. x \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
if \<not> x \<and> curThread = t \<and> action = ResumeCurrentThread then rescheduleRequired else return ()
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 2. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = 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 = ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y x. \<lbrace>\<lambda>s. ksCurThread s \<noteq> t \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> x \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y x xa. \<lbrace>\<lambda>s. xa \<noteq> t \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do action <- getSchedulerAction;
when (\<not> x \<and> xa = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y x ct. \<lbrace>\<lambda>s. ct \<noteq> t \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do action <- getSchedulerAction;
when (\<not> x \<and> ct = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y x ct. ct \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. ct \<noteq> t \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do action <- getSchedulerAction;
when (\<not> x \<and> ct = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 2. \<And>y x ct. \<not> ct \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. ct \<noteq> t \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do action <- getSchedulerAction;
when (\<not> x \<and> ct = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ct. ct \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> do action <- getSchedulerAction;
return ()
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 2. \<And>y x ct. \<not> ct \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. ct \<noteq> t \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do action <- getSchedulerAction;
when (\<not> x \<and> ct = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y x ct. \<not> ct \<noteq> t \<Longrightarrow> \<lbrace>\<lambda>s. ct \<noteq> t \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> do action <- getSchedulerAction;
when (\<not> x \<and> ct = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace> proof (prove)
goal:
No subgoals!