theory TcbAcc_R

lemma rescheduleRequired_corres:
  "corres dc (weak_valid_sched_action and valid_etcbs) (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))
     (reschedule_required) rescheduleRequired" apply (simp add: rescheduleRequired_def reschedule_required_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getSchedulerAction_corres]) apply (rule_tac P="case action of switch_thread t \<Rightarrow> P t | _ \<Rightarrow> \<top>"
                  and P'="case actiona of SwitchToThread t \<Rightarrow> P' t | _ \<Rightarrow> \<top>" for P P'
              in corres_split[where r'=dc]) apply (case_tac action) apply simp apply simp apply (rule tcbSchedEnqueue_corres) apply simp apply (rule setSchedulerAction_corres) apply simp apply (wp | wpc | simp)+ apply (force dest: st_tcb_weakenE simp: in_monad weak_valid_sched_action_def valid_etcbs_def
               split: Deterministic_A.scheduler_action.split) apply simp apply (clarsimp simp: weak_sch_act_wf_def pred_tcb_at' split: scheduler_action.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (weak_valid_sched_action and valid_etcbs) (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) reschedule_required rescheduleRequired proof (prove)
goal (1 subgoal):
 1. corres dc (weak_valid_sched_action and valid_etcbs) (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) (do action <- gets scheduler_action;
y <- case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
set_scheduler_action choose_new_thread
od) (do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do action <- gets scheduler_action;
y <- case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
set_scheduler_action choose_new_thread
od) (do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od)
 2. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ?Q s
 3. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> corres dc (?R4 action) (?R'4 actiona) (do y <- case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
set_scheduler_action choose_new_thread
od) (do y <- case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od)
 2. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>?R'4\<rbrace>
 4. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> corres dc (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) (case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ()) (case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 2. \<And>action actiona rv rv'. \<lbrakk>sched_act_relation action actiona; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R8 action actiona rv) (?R'8 action actiona rv') (set_scheduler_action choose_new_thread) (setSchedulerAction ChooseNewThread)
 3. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q14 action\<rbrace> case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?R8 action actiona\<rbrace>
 4. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q'16 actiona\<rbrace> case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?R'8 action actiona\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) and ?Q14 action\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) and ?Q'16 actiona\<rbrace>
 7. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>action actiona. \<lbrakk>sched_act_relation action actiona; action = resume_cur_thread\<rbrakk> \<Longrightarrow> corres dc (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) (case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ()) (case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 2. \<And>action actiona x2. \<lbrakk>sched_act_relation action actiona; action = switch_thread x2\<rbrakk> \<Longrightarrow> corres dc (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) (case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ()) (case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 3. \<And>action actiona. \<lbrakk>sched_act_relation action actiona; action = choose_new_thread\<rbrakk> \<Longrightarrow> corres dc (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) (case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ()) (case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 4. \<And>action actiona rv rv'. \<lbrakk>sched_act_relation action actiona; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R8 action actiona rv) (?R'8 action actiona rv') (set_scheduler_action choose_new_thread) (setSchedulerAction ChooseNewThread)
 5. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q14 action\<rbrace> case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?R8 action actiona\<rbrace>
 6. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q'16 actiona\<rbrace> case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?R'8 action actiona\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) and ?Q14 action\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) and ?Q'16 actiona\<rbrace>
 9. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>action actiona x2. \<lbrakk>sched_act_relation action actiona; action = switch_thread x2\<rbrakk> \<Longrightarrow> corres dc (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) (case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ()) (case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 2. \<And>action actiona. \<lbrakk>sched_act_relation action actiona; action = choose_new_thread\<rbrakk> \<Longrightarrow> corres dc (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) (case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ()) (case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 3. \<And>action actiona rv rv'. \<lbrakk>sched_act_relation action actiona; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R8 action actiona rv) (?R'8 action actiona rv') (set_scheduler_action choose_new_thread) (setSchedulerAction ChooseNewThread)
 4. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q14 action\<rbrace> case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?R8 action actiona\<rbrace>
 5. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q'16 actiona\<rbrace> case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?R'8 action actiona\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) and ?Q14 action\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) and ?Q'16 actiona\<rbrace>
 8. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>action actiona x2. \<lbrakk>actiona = SwitchToThread x2; action = switch_thread x2\<rbrakk> \<Longrightarrow> corres dc (?P13 (switch_thread x2) x2) (?P'15 (SwitchToThread x2) x2) (tcb_sched_action tcb_sched_enqueue x2) (tcbSchedEnqueue x2)
 2. \<And>action actiona. \<lbrakk>sched_act_relation action actiona; action = choose_new_thread\<rbrakk> \<Longrightarrow> corres dc (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) (case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ()) (case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 3. \<And>action actiona rv rv'. \<lbrakk>sched_act_relation action actiona; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R8 action actiona rv) (?R'8 action actiona rv') (set_scheduler_action choose_new_thread) (setSchedulerAction ChooseNewThread)
 4. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q14 action\<rbrace> case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?R8 action actiona\<rbrace>
 5. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q'16 actiona\<rbrace> case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?R'8 action actiona\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. (case action of switch_thread t \<Rightarrow> ?P13 action t | _ \<Rightarrow> \<lambda>_. True) and ?Q14 action\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. (case actiona of SwitchToThread t \<Rightarrow> ?P'15 actiona t | _ \<Rightarrow> \<lambda>_. True) and ?Q'16 actiona\<rbrace>
 8. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>action actiona. \<lbrakk>sched_act_relation action actiona; action = choose_new_thread\<rbrakk> \<Longrightarrow> corres dc (case action of switch_thread t \<Rightarrow> is_etcb_at t | _ \<Rightarrow> \<lambda>_. True) (case actiona of SwitchToThread t \<Rightarrow> tcb_at' t and Invariants_H.valid_queues and valid_queues' | _ \<Rightarrow> \<lambda>_. True) (case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ()) (case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ())
 2. \<And>action actiona rv rv'. \<lbrakk>sched_act_relation action actiona; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R8 action actiona rv) (?R'8 action actiona rv') (set_scheduler_action choose_new_thread) (setSchedulerAction ChooseNewThread)
 3. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q14 action\<rbrace> case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?R8 action actiona\<rbrace>
 4. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q'16 actiona\<rbrace> case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?R'8 action actiona\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. (case action of switch_thread t \<Rightarrow> is_etcb_at t | _ \<Rightarrow> \<lambda>_. True) and ?Q14 action\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. (case actiona of SwitchToThread t \<Rightarrow> tcb_at' t and Invariants_H.valid_queues and valid_queues' | _ \<Rightarrow> \<lambda>_. True) and ?Q'16 actiona\<rbrace>
 7. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>action actiona rv rv'. \<lbrakk>sched_act_relation action actiona; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R8 action actiona rv) (?R'8 action actiona rv') (set_scheduler_action choose_new_thread) (setSchedulerAction ChooseNewThread)
 2. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q14 action\<rbrace> case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>?R8 action actiona\<rbrace>
 3. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q'16 actiona\<rbrace> case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?R'8 action actiona\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. (case action of switch_thread t \<Rightarrow> is_etcb_at t | _ \<Rightarrow> \<lambda>_. True) and ?Q14 action\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. (case actiona of SwitchToThread t \<Rightarrow> tcb_at' t and Invariants_H.valid_queues and valid_queues' | _ \<Rightarrow> \<lambda>_. True) and ?Q'16 actiona\<rbrace>
 6. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>action actiona rv rv'. \<lbrakk>sched_act_relation action actiona; dc rv rv'\<rbrakk> \<Longrightarrow> sched_act_relation choose_new_thread ChooseNewThread
 2. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q14 action\<rbrace> case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q'16 actiona\<rbrace> case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. (case action of switch_thread t \<Rightarrow> is_etcb_at t | _ \<Rightarrow> \<lambda>_. True) and ?Q14 action\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. (case actiona of SwitchToThread t \<Rightarrow> tcb_at' t and Invariants_H.valid_queues and valid_queues' | _ \<Rightarrow> \<lambda>_. True) and ?Q'16 actiona\<rbrace>
 6. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q14 action\<rbrace> case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return () \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>action actiona. sched_act_relation action actiona \<Longrightarrow> \<lbrace>?Q'16 actiona\<rbrace> case actiona of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. (case action of switch_thread t \<Rightarrow> is_etcb_at t | _ \<Rightarrow> \<lambda>_. True) and ?Q14 action\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. (case actiona of SwitchToThread t \<Rightarrow> tcb_at' t and Invariants_H.valid_queues and valid_queues' | _ \<Rightarrow> \<lambda>_. True) and ?Q'16 actiona\<rbrace>
 5. \<And>s. (weak_valid_sched_action and valid_etcbs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. weak_valid_sched_action s \<and> valid_etcbs s \<Longrightarrow> (case scheduler_action s of switch_thread t \<Rightarrow> is_etcb_at t | _ \<Rightarrow> \<lambda>_. True) s
 2. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((case ksSchedulerAction s of SwitchToThread t \<Rightarrow> tcb_at' t and Invariants_H.valid_queues and valid_queues' | _ \<Rightarrow> \<lambda>_. True) and (\<lambda>_. True)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((case ksSchedulerAction s of SwitchToThread t \<Rightarrow> tcb_at' t and Invariants_H.valid_queues and valid_queues' | _ \<Rightarrow> \<lambda>_. True) and (\<lambda>_. True)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> tcb_at' t and Invariants_H.valid_queues and valid_queues' | _ \<Rightarrow> \<lambda>_. True) s proof (prove)
goal:
No subgoals!