theory TcbAcc_R

lemma rescheduleRequired_corres_simple:
  "corres dc \<top> sch_act_simple
     (set_scheduler_action choose_new_thread) rescheduleRequired" apply (simp add: rescheduleRequired_def) apply (rule corres_symb_exec_r[where Q'="\<lambda>rv s. rv = ResumeCurrentThread \<or> rv = ChooseNewThread"]) apply (rule corres_symb_exec_r) apply (rule setSchedulerAction_corres, simp) apply (wp | clarsimp split: scheduler_action.split)+ apply (wp | clarsimp simp: sch_act_simple_def split: scheduler_action.split)+ apply (simp add: getSchedulerAction_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) sch_act_simple (set_scheduler_action choose_new_thread) rescheduleRequired proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) sch_act_simple (set_scheduler_action choose_new_thread) (do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od) proof (prove)
goal (4 subgoals):
 1. \<And>action. corres dc (\<lambda>_. True) (\<lambda>s. action = ResumeCurrentThread \<or> action = ChooseNewThread) (set_scheduler_action choose_new_thread) (do y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od)
 2. \<lbrace>sch_act_simple\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. action = ResumeCurrentThread \<or> action = ChooseNewThread\<rbrace>
 3. \<And>s. sch_act_simple s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. True \<Longrightarrow> no_fail sch_act_simple getSchedulerAction proof (prove)
goal (7 subgoals):
 1. \<And>action y. corres dc (\<lambda>_. True) (?Q'5 action y) (set_scheduler_action choose_new_thread) (setSchedulerAction ChooseNewThread)
 2. \<And>action. \<lbrace>\<lambda>s. action = ResumeCurrentThread \<or> action = ChooseNewThread\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q'5 action\<rbrace>
 3. \<And>action s. action = ResumeCurrentThread \<or> action = ChooseNewThread \<Longrightarrow> \<lbrace>(=) s\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>action. True \<Longrightarrow> no_fail (\<lambda>s. action = ResumeCurrentThread \<or> action = ChooseNewThread) (case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 5. \<lbrace>sch_act_simple\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. action = ResumeCurrentThread \<or> action = ChooseNewThread\<rbrace>
 6. \<And>s. sch_act_simple s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. True \<Longrightarrow> no_fail sch_act_simple getSchedulerAction proof (prove)
goal (6 subgoals):
 1. \<And>action. \<lbrace>\<lambda>s. action = ResumeCurrentThread \<or> action = ChooseNewThread\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>action s. action = ResumeCurrentThread \<or> action = ChooseNewThread \<Longrightarrow> \<lbrace>(=) s\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>action. True \<Longrightarrow> no_fail (\<lambda>s. action = ResumeCurrentThread \<or> action = ChooseNewThread) (case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 4. \<lbrace>sch_act_simple\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. action = ResumeCurrentThread \<or> action = ChooseNewThread\<rbrace>
 5. \<And>s. sch_act_simple s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. True \<Longrightarrow> no_fail sch_act_simple getSchedulerAction proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sch_act_simple s; ksSchedulerAction s \<noteq> ChooseNewThread\<rbrakk> \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread
 2. \<And>s. sch_act_simple s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. True \<Longrightarrow> no_fail sch_act_simple getSchedulerAction proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread) getSchedulerAction proof (prove)
goal:
No subgoals!