theory TcbAcc_R

lemma sts_sch_act':
  "\<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
  setThreadState st t  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: setThreadState_def) apply (wp | simp)+ prefer 2 apply assumption apply (case_tac "runnable' st") apply ((wp threadSet_runnable_sch_act hoare_drop_imps | simp)+)[1] apply (rule_tac Q="\<lambda>rv s. st_tcb_at' (Not \<circ> runnable') t s \<and>
                     (ksCurThread s \<noteq> t \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow>
                            sch_act_wf (ksSchedulerAction s) s)"
               in hoare_post_imp) apply (clarsimp simp: pred_tcb_at'_def obj_at'_def projectKOs) apply (simp only: imp_conv_disj) apply (wp threadSet_pred_tcb_at_state threadSet_sch_act_wf
            hoare_vcg_disj_lift|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) 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. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. runnable' st \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<not> runnable' st \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> runnable' st \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>\<not> runnable' st; st_tcb_at' (Not \<circ> runnable') t s \<and> (ksCurThread s \<noteq> t \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow> sch_act_wf (ksSchedulerAction s) s)\<rbrakk> \<Longrightarrow> (ksCurThread s = t \<longrightarrow> st_tcb_at' runnable' t s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> sch_act_wf (ksSchedulerAction s) s
 2. \<not> runnable' st \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv s. st_tcb_at' (Not \<circ> runnable') t s \<and> (ksCurThread s \<noteq> t \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow> sch_act_wf (ksSchedulerAction s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> runnable' st \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv s. st_tcb_at' (Not \<circ> runnable') t s \<and> (ksCurThread s \<noteq> t \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow> sch_act_wf (ksSchedulerAction s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> runnable' st \<Longrightarrow> \<lbrace>\<lambda>s. (\<not> \<not> False \<or> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv s. st_tcb_at' (Not \<circ> runnable') t s \<and> (\<not> (ksCurThread s \<noteq> t \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<or> sch_act_wf (ksSchedulerAction s) s)\<rbrace> proof (prove)
goal:
No subgoals!