theory TcbAcc_R

lemma sts_sch_act[wp]:
  "\<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_simple 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 apply simp prefer 2 apply assumption apply (case_tac "runnable' st") apply (rule_tac Q="\<lambda>s. sch_act_wf (ksSchedulerAction s) s"
                in hoare_pre_imp, simp) apply ((wp hoare_drop_imps threadSet_runnable_sch_act | 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 (rule hoare_pre) apply (wp threadSet_pred_tcb_at_state threadSet_sch_act_wf
             hoare_vcg_disj_lift|simp)+ apply (auto simp: sch_act_simple_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<not> runnable' st \<longrightarrow> sch_act_simple 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_simple 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. (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then \<lambda>_. True else (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) s\<rbrace>
 2. \<And>s. (\<not> runnable' st \<longrightarrow> sch_act_simple s) \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s 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_simple 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_simple 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_simple 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_simple 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_simple 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. 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_simple 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_simple 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_simple 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_simple 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_simple 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 (2 subgoals):
 1. \<not> runnable' st \<Longrightarrow> \<lbrace>?Q46\<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>
 2. \<And>s. \<lbrakk>\<not> runnable' st; (\<not> \<not> False \<or> sch_act_simple s) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> ?Q46 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> runnable' st; sch_act_simple s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread \<or> sch_act_not t s \<and> (ksCurThread s = t \<longrightarrow> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) proof (prove)
goal:
No subgoals!