theory Schedule_R

lemma possibleSwitchTo_corres:
  "corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t)
    (Invariants_H.valid_queues and valid_queues' and
    (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs')
      (possible_switch_to t)
      (possibleSwitchTo t)" supply ethread_get_wp[wp del] apply (simp add: possible_switch_to_def possibleSwitchTo_def cong: if_cong) apply (rule corres_guard_imp) apply (rule corres_split[OF curDomain_corres], simp) apply (rule corres_split) apply (rule ethreadget_corres[where r="(=)"]) apply (clarsimp simp: etcb_relation_def) apply (rule corres_split[OF getSchedulerAction_corres]) apply (rule corres_if, simp) apply (rule tcbSchedEnqueue_corres) apply (rule corres_if, simp) apply (case_tac action; simp) apply (rule corres_split[OF rescheduleRequired_corres]) apply (rule tcbSchedEnqueue_corres) apply (wp rescheduleRequired_valid_queues'_weak)+ apply (rule setSchedulerAction_corres, simp) apply (wpsimp simp: if_apply_def2
                       wp: hoare_drop_imp[where f="ethread_get a b" for a b])+ apply (wp hoare_drop_imps)[1] apply wp+ apply (fastforce simp: valid_sched_def invs_def valid_state_def cur_tcb_def
                          valid_sched_action_def weak_valid_sched_action_def
                          tcb_at_is_etcb_at[OF st_tcb_at_tcb_at[rotated]]) apply (simp add: tcb_at_is_etcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') (possible_switch_to t) (possibleSwitchTo t) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') (possible_switch_to t) (possibleSwitchTo t) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') (do cur_dom <- gets cur_domain;
target_dom <- ethread_get tcb_domain t;
action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue t else if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)
od) (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q6 ?Q'6 (do cur_dom <- gets cur_domain;
target_dom <- ethread_get tcb_domain t;
action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue t else if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)
od) (do curDom <- curDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od)
 2. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ?Q6 s
 3. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ?Q'6 s proof (prove)
goal (5 subgoals):
 1. \<And>cur_dom. corres dc (?R10 cur_dom) (?R'10 cur_dom) (do target_dom <- ethread_get tcb_domain t;
action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue t else if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)
od) (do targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> cur_dom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od)
 2. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>?R10\<rbrace>
 3. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>?R'10\<rbrace>
 4. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 5. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (8 subgoals):
 1. \<And>cur_dom. corres (?r'14 cur_dom) (?P14 cur_dom) (?P'14 cur_dom) (ethread_get tcb_domain t) (threadGet tcbDomain t)
 2. \<And>cur_dom target_dom targetDom. ?r'14 cur_dom target_dom targetDom \<Longrightarrow> corres dc (?R14 cur_dom target_dom) (?R'14 cur_dom targetDom) (do action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue t else if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)
od) (do action <- getSchedulerAction;
if targetDom \<noteq> cur_dom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od)
 3. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>?R14 cur_dom\<rbrace>
 4. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>?R'14 cur_dom\<rbrace>
 5. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. ?P14 cur_dom and ?Q14 cur_dom\<rbrace>
 6. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. ?P'14 cur_dom and ?Q'14 cur_dom\<rbrace>
 7. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 8. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (8 subgoals):
 1. \<And>cur_dom etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> tcb_domain etcb = tcbDomain tcb'
 2. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> corres dc (?R14 cur_dom target_dom) (?R'14 cur_dom targetDom) (do action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue t else if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)
od) (do action <- getSchedulerAction;
if targetDom \<noteq> cur_dom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od)
 3. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>?R14 cur_dom\<rbrace>
 4. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>?R'14 cur_dom\<rbrace>
 5. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 6. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 7. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 8. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (7 subgoals):
 1. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> corres dc (?R14 cur_dom target_dom) (?R'14 cur_dom targetDom) (do action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue t else if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)
od) (do action <- getSchedulerAction;
if targetDom \<noteq> cur_dom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od)
 2. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>?R14 cur_dom\<rbrace>
 3. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>?R'14 cur_dom\<rbrace>
 4. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 5. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 6. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 7. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (9 subgoals):
 1. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?R21 cur_dom target_dom targetDom action) (?R'21 cur_dom target_dom targetDom actiona) (if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue t else if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)) (if targetDom \<noteq> cur_dom then tcbSchedEnqueue t else if actiona \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t))
 2. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>?R21 cur_dom target_dom targetDom\<rbrace>
 3. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>?R'21 cur_dom target_dom targetDom\<rbrace>
 4. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 5. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 6. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 7. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 8. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 9. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (10 subgoals):
 1. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?P29 cur_dom target_dom targetDom action) (?P'32 cur_dom target_dom targetDom actiona) (tcb_sched_action tcb_sched_enqueue t) (tcbSchedEnqueue t)
 2. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?Q30 cur_dom target_dom targetDom action) (?Q'33 cur_dom target_dom targetDom actiona) (if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)) (if actiona \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t))
 3. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if target_dom \<noteq> cur_dom then ?P29 cur_dom target_dom targetDom action else ?Q30 cur_dom target_dom targetDom action\<rbrace>
 4. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. if targetDom \<noteq> cur_dom then ?P'32 cur_dom target_dom targetDom actiona else ?Q'33 cur_dom target_dom targetDom actiona\<rbrace>
 5. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 6. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 7. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 8. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 9. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 10. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (9 subgoals):
 1. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?Q30 cur_dom target_dom targetDom action) (?Q'33 cur_dom target_dom targetDom actiona) (if action \<noteq> resume_cur_thread then do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od else set_scheduler_action (switch_thread t)) (if actiona \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t))
 2. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if target_dom \<noteq> cur_dom then is_etcb_at t else ?Q30 cur_dom target_dom targetDom action\<rbrace>
 3. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. if targetDom \<noteq> cur_dom then tcb_at' t and Invariants_H.valid_queues and valid_queues' else ?Q'33 cur_dom target_dom targetDom actiona\<rbrace>
 4. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 5. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 6. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 7. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 8. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 9. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (11 subgoals):
 1. \<And>target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> (action = resume_cur_thread) = (actiona = ResumeCurrentThread)
 2. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?P42 cur_dom target_dom targetDom action) (?P'45 cur_dom target_dom targetDom actiona) (do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od) (do y <- rescheduleRequired;
tcbSchedEnqueue t
od)
 3. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?Q43 cur_dom target_dom targetDom action) (?Q'46 cur_dom target_dom targetDom actiona) (set_scheduler_action (switch_thread t)) (setSchedulerAction (SwitchToThread t))
 4. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if target_dom \<noteq> cur_dom then is_etcb_at t else if action \<noteq> resume_cur_thread then ?P42 cur_dom target_dom targetDom action else ?Q43 cur_dom target_dom targetDom action\<rbrace>
 5. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. if targetDom \<noteq> cur_dom then tcb_at' t and Invariants_H.valid_queues and valid_queues' else if actiona \<noteq> ResumeCurrentThread then ?P'45 cur_dom target_dom targetDom actiona else ?Q'46 cur_dom target_dom targetDom actiona\<rbrace>
 6. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 7. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 8. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 9. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 10. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?P42 cur_dom target_dom targetDom action) (?P'45 cur_dom target_dom targetDom actiona) (do y <- reschedule_required;
tcb_sched_action tcb_sched_enqueue t
od) (do y <- rescheduleRequired;
tcbSchedEnqueue t
od)
 2. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?Q43 cur_dom target_dom targetDom action) (?Q'46 cur_dom target_dom targetDom actiona) (set_scheduler_action (switch_thread t)) (setSchedulerAction (SwitchToThread t))
 3. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if target_dom \<noteq> cur_dom then is_etcb_at t else if action \<noteq> resume_cur_thread then ?P42 cur_dom target_dom targetDom action else ?Q43 cur_dom target_dom targetDom action\<rbrace>
 4. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. if targetDom \<noteq> cur_dom then tcb_at' t and Invariants_H.valid_queues and valid_queues' else if actiona \<noteq> ResumeCurrentThread then ?P'45 cur_dom target_dom targetDom actiona else ?Q'46 cur_dom target_dom targetDom actiona\<rbrace>
 5. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 6. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 7. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 8. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 9. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 10. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (12 subgoals):
 1. \<And>cur_dom target_dom targetDom action actiona y ya. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R59 cur_dom target_dom targetDom action actiona y) (?R'59 cur_dom target_dom targetDom action actiona ya) (tcb_sched_action tcb_sched_enqueue t) (tcbSchedEnqueue t)
 2. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur_dom target_dom targetDom action\<rbrace> reschedule_required \<lbrace>?R59 cur_dom target_dom targetDom action actiona\<rbrace>
 3. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> \<lbrace>?Q'61 cur_dom target_dom targetDom actiona\<rbrace> rescheduleRequired \<lbrace>?R'59 cur_dom target_dom targetDom action actiona\<rbrace>
 4. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?Q43 cur_dom target_dom targetDom action) (?Q'46 cur_dom target_dom targetDom actiona) (set_scheduler_action (switch_thread t)) (setSchedulerAction (SwitchToThread t))
 5. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if target_dom \<noteq> cur_dom then is_etcb_at t else if action \<noteq> resume_cur_thread then weak_valid_sched_action and valid_etcbs and ?Q60 cur_dom target_dom targetDom action else ?Q43 cur_dom target_dom targetDom action\<rbrace>
 6. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. if targetDom \<noteq> cur_dom then tcb_at' t and Invariants_H.valid_queues and valid_queues' else if actiona \<noteq> ResumeCurrentThread then Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and ?Q'61 cur_dom target_dom targetDom actiona else ?Q'46 cur_dom target_dom targetDom actiona\<rbrace>
 7. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 8. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 9. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 10. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> \<lbrace>?Q60 cur_dom target_dom targetDom action\<rbrace> reschedule_required \<lbrace>\<lambda>y. is_etcb_at t\<rbrace>
 2. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> \<lbrace>?Q'61 cur_dom target_dom targetDom actiona\<rbrace> rescheduleRequired \<lbrace>\<lambda>ya. tcb_at' t and Invariants_H.valid_queues and valid_queues'\<rbrace>
 3. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?Q43 cur_dom target_dom targetDom action) (?Q'46 cur_dom target_dom targetDom actiona) (set_scheduler_action (switch_thread t)) (setSchedulerAction (SwitchToThread t))
 4. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if target_dom \<noteq> cur_dom then is_etcb_at t else if action \<noteq> resume_cur_thread then weak_valid_sched_action and valid_etcbs and ?Q60 cur_dom target_dom targetDom action else ?Q43 cur_dom target_dom targetDom action\<rbrace>
 5. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. if targetDom \<noteq> cur_dom then tcb_at' t and Invariants_H.valid_queues and valid_queues' else if actiona \<noteq> ResumeCurrentThread then Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and ?Q'61 cur_dom target_dom targetDom actiona else ?Q'46 cur_dom target_dom targetDom actiona\<rbrace>
 6. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 7. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 8. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 9. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 10. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>cur_dom target_dom targetDom action actiona. \<lbrakk>target_dom = targetDom; sched_act_relation action actiona\<rbrakk> \<Longrightarrow> corres dc (?Q43 cur_dom target_dom targetDom action) (?Q'46 cur_dom target_dom targetDom actiona) (set_scheduler_action (switch_thread t)) (setSchedulerAction (SwitchToThread t))
 2. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if target_dom \<noteq> cur_dom then is_etcb_at t else if action \<noteq> resume_cur_thread then weak_valid_sched_action and valid_etcbs and is_etcb_at t else ?Q43 cur_dom target_dom targetDom action\<rbrace>
 3. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. if targetDom \<noteq> cur_dom then tcb_at' t and Invariants_H.valid_queues and valid_queues' else if actiona \<noteq> ResumeCurrentThread then Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. tcb_at' t s \<and> (Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) else ?Q'46 cur_dom target_dom targetDom actiona\<rbrace>
 4. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 5. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 6. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 7. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 8. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 9. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (8 subgoals):
 1. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q22 cur_dom target_dom\<rbrace> gets scheduler_action \<lbrace>\<lambda>action. if target_dom \<noteq> cur_dom then is_etcb_at t else if action \<noteq> resume_cur_thread then weak_valid_sched_action and valid_etcbs and is_etcb_at t else (\<lambda>_. True)\<rbrace>
 2. \<And>cur_dom target_dom targetDom. target_dom = targetDom \<Longrightarrow> \<lbrace>?Q'23 cur_dom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>actiona. if targetDom \<noteq> cur_dom then tcb_at' t and Invariants_H.valid_queues and valid_queues' else if actiona \<noteq> ResumeCurrentThread then Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. tcb_at' t s \<and> (Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s) else (\<lambda>_. True)\<rbrace>
 3. \<And>cur_dom. \<lbrace>?Q14 cur_dom\<rbrace> ethread_get tcb_domain t \<lbrace>\<lambda>target_dom. (\<lambda>_. True) and ?Q22 cur_dom target_dom\<rbrace>
 4. \<And>cur_dom. \<lbrace>?Q'14 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>targetDom. (\<lambda>_. True) and ?Q'23 cur_dom targetDom\<rbrace>
 5. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and ?Q14 cur_dom\<rbrace>
 6. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and ?Q'14 cur_dom\<rbrace>
 7. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 8. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (5 subgoals):
 1. \<And>cur_dom. \<lbrace>?P'121 cur_dom\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>rv s. (rv \<noteq> cur_dom \<longrightarrow> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> valid_queues' s) \<and> (rv = cur_dom \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and (\<lambda>s. True \<and> is_etcb_at t s \<and> weak_valid_sched_action s \<and> valid_etcbs s \<and> is_etcb_at t s)\<rbrace>
 3. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and (\<lambda>s. True \<and> ?P'121 cur_dom s)\<rbrace>
 4. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 5. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q10\<rbrace> gets cur_domain \<lbrace>\<lambda>cur_dom. is_etcb_at t and (\<lambda>s. True \<and> is_etcb_at t s \<and> weak_valid_sched_action s \<and> valid_etcbs s \<and> is_etcb_at t s)\<rbrace>
 2. \<lbrace>?Q'10\<rbrace> curDomain \<lbrace>\<lambda>cur_dom. tcb_at' t and (\<lambda>s. True \<and> (tcb_at' t s \<and> Invariants_H.valid_queues s \<and> valid_queues' s) \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q10) s
 4. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'10) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) s \<Longrightarrow> ((\<lambda>_. True) and (is_etcb_at t and (\<lambda>s. True \<and> is_etcb_at t s \<and> weak_valid_sched_action s \<and> valid_etcbs s \<and> is_etcb_at t s))) s
 2. \<And>s. (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and (tcb_at' t and (\<lambda>s. True \<and> (tcb_at' t s \<and> Invariants_H.valid_queues s \<and> valid_queues' s) \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) 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) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ((\<lambda>_. True) and (tcb_at' t and (\<lambda>s. True \<and> (tcb_at' t s \<and> Invariants_H.valid_queues s \<and> valid_queues' s) \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s))) s proof (prove)
goal:
No subgoals!