theory IpcCancel_C

lemma rescheduleRequired_ccorres:
  "ccorres dc xfdc (valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs')
           UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)" apply cinit apply (rule ccorres_symb_exec_l) apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) apply (simp add: scheduler_action_case_switch_to_if
                      cong: if_weak_cong split del: if_split) apply (rule_tac R="\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s"
                     in ccorres_cond) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                                  cscheduler_action_relation_def) subgoal by (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL
                           split: scheduler_action.split_asm dest!: pred_tcb_at') apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule ccorres_return_Skip) apply ceqv apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: setSchedulerAction_def simpler_modify_def) subgoal by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                              cscheduler_action_relation_def
                              carch_state_relation_def cmachine_state_relation_def) apply wp apply (simp add: guard_is_UNIV_def) apply wp+ apply (simp add: getSchedulerAction_def) apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def
                        Let_def cscheduler_action_relation_def) by (auto simp: tcb_at_not_NULL tcb_at_1
                    tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym]
                 split: scheduler_action.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') UNIV [] rescheduleRequired (Call rescheduleRequired_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 [SKIP] (do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od) (IF \<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1 THEN
  CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction)
FI;;
\<acute>ksSchedulerAction :== tcb_Ptr 1)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (5 subgoals):
 1. \<And>action. ccorres dc xfdc (?Q15 action) (?Q'15 action) [SKIP] (do y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od) (IF \<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1 THEN
  CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction)
FI;;
\<acute>ksSchedulerAction :== tcb_Ptr 1)
 2. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>?Q15\<rbrace>
 4. empty_fail getSchedulerAction
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q15 rv s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (9 subgoals):
 1. \<And>action. ccorres dc xfdc (?P20 action) (?Q'15 action) [] (case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ()) (IF \<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1 THEN
  CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction)
FI)
 2. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 3. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 4. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 5. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 6. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. ?P20 action and ?R20 action\<rbrace>
 8. empty_fail getSchedulerAction
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P20 rv and ?R20 rv) s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (9 subgoals):
 1. \<And>action. ccorres dc xfdc (?P20 action) (?Q'15 action) [] (if \<exists>t. action = SwitchToThread t then tcbSchedEnqueue (case action of SwitchToThread t \<Rightarrow> t) else return ()) (IF \<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1 THEN
  CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction)
FI)
 2. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 3. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 4. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 5. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 6. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. ?P20 action and ?R20 action\<rbrace>
 8. empty_fail getSchedulerAction
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P20 rv and ?R20 rv) s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (11 subgoals):
 1. \<And>action. \<forall>s s'. (s, s') \<in> rf_sr \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf action s \<longrightarrow> (\<exists>t. action = SwitchToThread t) = (s' \<in> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>)
 2. \<And>action. ccorres dc xfdc (?Pt27 action) (?Rt27 action) [] (tcbSchedEnqueue (case action of SwitchToThread t \<Rightarrow> t)) (CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction))
 3. \<And>action. ccorres dc xfdc (?Pf27 action) (?Rf27 action) [] (return ()) SKIP
 4. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 5. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 6. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 7. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 8. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> ?Pt27 action s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> ?Pf27 action s) and ?R20 action\<rbrace>
 10. empty_fail getSchedulerAction
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s s'. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); case ksSchedulerAction s of ResumeCurrentThread \<Rightarrow> ksSchedulerAction_' (globals s') = NULL | ChooseNewThread \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_Ptr 1 | SwitchToThread p' \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr p'; carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; weak_sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> (\<exists>t. ksSchedulerAction s = SwitchToThread t) = (ksSchedulerAction_' (globals s') \<noteq> NULL \<and> ksSchedulerAction_' (globals s') \<noteq> tcb_Ptr 1)
 2. \<And>action. ccorres dc xfdc (?Pt27 action) (?Rt27 action) [] (tcbSchedEnqueue (case action of SwitchToThread t \<Rightarrow> t)) (CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction))
 3. \<And>action. ccorres dc xfdc (?Pf27 action) (?Rf27 action) [] (return ()) SKIP
 4. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 5. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 6. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 7. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 8. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> ?Pt27 action s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> ?Pf27 action s) and ?R20 action\<rbrace>
 10. empty_fail getSchedulerAction
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s_) (underlying_memory (ksMachineState s_)) (t_hrs_' (globals s'_)); cready_queues_relation (cslift s'_) (ksReadyQueues_' (globals s'_)) (ksReadyQueues s_); zero_ranges_are_zero (gsUntypedZeroRanges s_) (t_hrs_' (globals s'_)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s'_)) (ksReadyQueuesL1Bitmap s_); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s'_)) (ksReadyQueuesL2Bitmap s_); ksCurThread_' (globals s'_) = tcb_ptr_to_ctcb_ptr (ksCurThread s_); ksIdleThread_' (globals s'_) = tcb_ptr_to_ctcb_ptr (ksIdleThread s_); cinterrupt_relation (ksInterruptState s_) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s'_)); case ksSchedulerAction s_ of ResumeCurrentThread \<Rightarrow> ksSchedulerAction_' (globals s'_) = NULL | ChooseNewThread \<Rightarrow> ksSchedulerAction_' (globals s'_) = tcb_Ptr 1 | SwitchToThread p' \<Rightarrow> ksSchedulerAction_' (globals s'_) = tcb_ptr_to_ctcb_ptr p'; carch_state_relation (ksArchState s_) (globals s'_); cmachine_state_relation (ksMachineState s_) (globals s'_); cte_array_relation s_ (globals s'_); tcb_cte_array_relation s_ (globals s'_); apsnd fst (ghost'state_' (globals s'_)) = (gsUserPages s_, gsCNodes s_); ghost_size_rel (ghost'state_' (globals s'_)) (gsMaxObjectSize s_); ksWorkUnitsCompleted_' (globals s'_) = ksWorkUnitsCompleted s_; s'_ \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s'_ \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'_))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s_) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s'_) = word_of_nat (ksDomScheduleIdx s_); ksCurDomain_' (globals s'_) = UCAST(8 \<rightarrow> 32) (ksCurDomain s_); ksDomainTime_' (globals s'_) = ksDomainTime s_; weak_sch_act_wf (ksSchedulerAction s_) s_\<rbrakk> \<Longrightarrow> (\<exists>t. ksSchedulerAction s_ = SwitchToThread t) = (ksSchedulerAction_' (globals s'_) \<noteq> NULL \<and> ksSchedulerAction_' (globals s'_) \<noteq> tcb_Ptr 1) proof (prove)
goal (10 subgoals):
 1. \<And>action. ccorres dc xfdc (?Pt27 action) (?Rt27 action) [] (tcbSchedEnqueue (case action of SwitchToThread t \<Rightarrow> t)) (CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction))
 2. \<And>action. ccorres dc xfdc (?Pf27 action) (?Rf27 action) [] (return ()) SKIP
 3. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 4. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 5. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 6. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 7. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> ?Pt27 action s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> ?Pf27 action s) and ?R20 action\<rbrace>
 9. empty_fail getSchedulerAction
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> ?Pt27 rv s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> ?Pf27 rv s) and ?R20 rv) s \<longrightarrow> s' \<in> ?Rt27 rv \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> ?Rf27 rv \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (9 subgoals):
 1. \<And>action. ccorres dc xfdc (?Pf27 action) (?Rf27 action) [] (return ()) SKIP
 2. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 3. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 4. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 5. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 6. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> ?Pf27 action s) and ?R20 action\<rbrace>
 8. empty_fail getSchedulerAction
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> ?Pf27 rv s) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> ?Rf27 rv \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (8 subgoals):
 1. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 2. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 3. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 4. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 5. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 7. empty_fail getSchedulerAction
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (\<acute>ksSchedulerAction :== tcb_Ptr 1)
 2. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 3. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 4. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 6. empty_fail getSchedulerAction
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>action y rv'. dc y rv' \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ksSchedulerAction :== tcb_Ptr 1 {s. \<exists>(rv, \<sigma>')\<in>fst (setSchedulerAction ChooseNewThread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 4. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 6. empty_fail getSchedulerAction
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>action y rv' \<sigma>. dc y rv' \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setSchedulerAction ChooseNewThread \<sigma>). (\<sigma>', globals_update (ksSchedulerAction_'_update (\<lambda>_. tcb_Ptr 1)) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (ksSchedulerAction_'_update (\<lambda>_. tcb_Ptr 1)) s))}
 2. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 4. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 6. empty_fail getSchedulerAction
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> (\<sigma>\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>, globals_update (ksSchedulerAction_'_update (\<lambda>_. tcb_Ptr 1)) x) \<in> rf_sr
 2. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 4. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 6. empty_fail getSchedulerAction
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (1 subgoal):
 1. (\<sigma>_, x_) \<in> rf_sr \<Longrightarrow> (\<sigma>_\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>, globals_update (ksSchedulerAction_'_update (\<lambda>_. tcb_Ptr 1)) x_) \<in> rf_sr proof (prove)
goal (6 subgoals):
 1. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 3. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 5. empty_fail getSchedulerAction
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 2. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)\<rbrace>
 4. empty_fail getSchedulerAction
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> weak_sch_act_wf action s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)\<rbrace>
 3. empty_fail getSchedulerAction
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>sa. ksSchedulerAction s = ksSchedulerAction sa \<and> weak_sch_act_wf (ksSchedulerAction s) sa) and (\<lambda>sa. (\<exists>t. ksSchedulerAction s = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> t) and valid_objs') sa) and (\<lambda>sa. (\<nexists>t. ksSchedulerAction s = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> weak_sch_act_wf rv s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; Invariants_H.valid_queues s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> ((\<exists>t. ksSchedulerAction s = SwitchToThread t) \<longrightarrow> tcb_at' (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> t) s) \<and> (\<forall>s. (s, s') \<in> rf_sr \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> ((\<exists>t. ksSchedulerAction s = SwitchToThread t) \<longrightarrow> Invariants_H.valid_queues s \<and> tcb_at' (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> t) s \<and> valid_objs' s) \<longrightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> t) \<and> ksSchedulerAction_' (globals s') \<noteq> NULL \<and> ksSchedulerAction_' (globals s') \<noteq> tcb_Ptr 1 \<or> ksSchedulerAction_' (globals s') = NULL \<or> ksSchedulerAction_' (globals s') = tcb_Ptr 1) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); Invariants_H.valid_queues s; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s; valid_objs' s; zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); case ksSchedulerAction s of ResumeCurrentThread \<Rightarrow> ksSchedulerAction_' (globals s') = NULL | ChooseNewThread \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_Ptr 1 | SwitchToThread p' \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr p'; carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> ((\<exists>t. ksSchedulerAction s = SwitchToThread t) \<longrightarrow> tcb_at' (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> t) s) \<and> (\<forall>sa. cpspace_relation (ksPSpace sa) (underlying_memory (ksMachineState sa)) (t_hrs_' (globals s')) \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues sa) \<and> zero_ranges_are_zero (gsUntypedZeroRanges sa) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap sa) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap sa) \<and> ksCurThread s = ksCurThread sa \<and> ksIdleThread s = ksIdleThread sa \<and> cinterrupt_relation (ksInterruptState sa) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> (case ksSchedulerAction sa of ResumeCurrentThread \<Rightarrow> ksSchedulerAction_' (globals s') = NULL | ChooseNewThread \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_Ptr 1 | SwitchToThread p' \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr p') \<and> carch_state_relation (ksArchState sa) (globals s') \<and> cmachine_state_relation (ksMachineState sa) (globals s') \<and> cte_array_relation sa (globals s') \<and> tcb_cte_array_relation sa (globals s') \<and> gsUserPages s = gsUserPages sa \<and> gsCNodes s = gsCNodes sa \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize sa) \<and> ksWorkUnitsCompleted s = ksWorkUnitsCompleted sa \<and> cdom_schedule_relation (kernel_state.ksDomSchedule sa) kernel_all_global_addresses.ksDomSchedule \<and> word_of_nat (ksDomScheduleIdx s) = word_of_nat (ksDomScheduleIdx sa) \<and> ksCurDomain s = ksCurDomain sa \<and> ksDomainTime s = ksDomainTime sa \<and> (\<forall>t. ksSchedulerAction sa = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t sa \<and> tcb_in_cur_domain' t sa) \<and> ((\<exists>t. ksSchedulerAction sa = SwitchToThread t) \<longrightarrow> Invariants_H.valid_queues sa \<and> tcb_at' (case ksSchedulerAction sa of SwitchToThread t \<Rightarrow> t) sa \<and> valid_objs' sa) \<longrightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr (case ksSchedulerAction sa of SwitchToThread t \<Rightarrow> t) \<and> ksSchedulerAction_' (globals s') \<noteq> NULL \<and> ksSchedulerAction_' (globals s') \<noteq> tcb_Ptr 1 \<or> ksSchedulerAction_' (globals s') = NULL \<or> ksSchedulerAction_' (globals s') = tcb_Ptr 1)