theory Schedule_DR

lemma schedule_dcorres:
  "dcorres dc \<top> (invs and valid_sched and valid_etcbs) Schedule_D.schedule Schedule_A.schedule" supply if_cong[cong] apply (clarsimp simp: Schedule_A.schedule_def) apply (rule dcorres_symb_exec_r) apply (rename_tac cur) apply (rule dcorres_symb_exec_r) apply (rename_tac cur_ts) apply (rule dcorres_symb_exec_r) apply (rename_tac "sa", case_tac "sa") 
          (* sa = resume_cur_thread *)
           apply clarsimp apply (rule schedule_resume_cur_thread_dcorres) 
         (* sa = switch_thread *)
          apply clarsimp apply (rule schedule_switch_thread_dcorres) 
        (* sa = choose_new_thread *)
         apply clarsimp apply (rule schedule_choose_new_thread_dcorres_fragment) apply (wp gts_st_tcb | simp )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_sched and valid_etcbs) Schedule_D.schedule state_ext_sched_class.schedule proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_sched and valid_etcbs) Schedule_D.schedule state_ext_sched_class.schedule proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_sched and valid_etcbs) Schedule_D.schedule (do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres dc (\<lambda>_. True) (?Q'6 rv) Schedule_D.schedule (do ct_st <- get_thread_state rv;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> rv = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (rv \<noteq> it) tcb_priority rv;
fastfail <- schedule_switch_thread_fastfail rv it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
od)
 2. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cur. dcorres dc (\<lambda>_. True) (?Q'6 cur) Schedule_D.schedule (do ct_st <- get_thread_state cur;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> cur = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
od)
 2. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cur rv. dcorres dc (\<lambda>_. True) (?Q'10 cur rv) Schedule_D.schedule (gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable rv \<or> cur = id)
od) (\<lambda>candidate. do y <- when (runnable rv) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rv \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable rv) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od))
 2. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 3. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cur cur_ts. dcorres dc (\<lambda>_. True) (?Q'10 cur cur_ts) Schedule_D.schedule (gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od) (\<lambda>candidate. do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od))
 2. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 3. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cur cur_ts rv. dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts rv) Schedule_D.schedule (case rv of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 2. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>?Q'14 cur cur_ts\<rbrace>
 3. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 5. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>cur cur_ts sa. sa = resume_cur_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 2. \<And>cur cur_ts sa x2. sa = switch_thread x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 3. \<And>cur cur_ts sa. sa = choose_new_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 4. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>?Q'14 cur cur_ts\<rbrace>
 5. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 7. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>cur cur_ts sa. sa = resume_cur_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 2. \<And>cur cur_ts sa x2. sa = switch_thread x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 3. \<And>cur cur_ts sa. sa = choose_new_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 4. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>?Q'14 cur cur_ts\<rbrace>
 5. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 7. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>cur cur_ts. dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts resume_cur_thread) Schedule_D.schedule (do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od)
 2. \<And>cur cur_ts sa x2. sa = switch_thread x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 3. \<And>cur cur_ts sa. sa = choose_new_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'14 cur cur_ts sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 4. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>?Q'14 cur cur_ts\<rbrace>
 5. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 7. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 8. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 9. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>cur cur_ts sa x2. sa = switch_thread x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 2. \<And>cur cur_ts sa. sa = choose_new_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 3. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>\<lambda>r a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = r\<rbrace>
 4. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 6. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>cur cur_ts sa x2. sa = switch_thread x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 2. \<And>cur cur_ts sa. sa = choose_new_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 3. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>\<lambda>r a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = r\<rbrace>
 4. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 6. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>cur cur_ts x2. dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = switch_thread x2) Schedule_D.schedule (do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od)
 2. \<And>cur cur_ts sa. sa = choose_new_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 3. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>\<lambda>r a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = r\<rbrace>
 4. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 6. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 7. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 8. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cur cur_ts sa. sa = choose_new_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 2. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>\<lambda>r a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = r\<rbrace>
 3. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 5. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cur cur_ts sa. sa = choose_new_thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = sa) Schedule_D.schedule (case sa of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable cur_ts \<or> cur = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur \<noteq> it) tcb_priority cur;
fastfail <- schedule_switch_thread_fastfail cur it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable cur_ts \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 2. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>\<lambda>r a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = r\<rbrace>
 3. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 5. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cur cur_ts. dcorres dc (\<lambda>_. True) (\<lambda>a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = choose_new_thread) Schedule_D.schedule (do y <- when (runnable cur_ts) (tcb_sched_action tcb_sched_enqueue cur);
schedule_choose_new_thread
od)
 2. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>\<lambda>r a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = r\<rbrace>
 3. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 4. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 5. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 6. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 7. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cur cur_ts. \<lbrace>?Q'10 cur cur_ts\<rbrace> gets scheduler_action \<lbrace>\<lambda>r a. cur = cur_thread a \<and> st_tcb_at ((=) cur_ts) cur a \<and> valid_etcbs a \<and> valid_sched a \<and> invs a \<and> scheduler_action a = r\<rbrace>
 2. \<And>cur cur_ts cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets scheduler_action \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 3. \<And>cur. \<lbrace>?Q'6 cur\<rbrace> get_thread_state cur \<lbrace>?Q'10 cur\<rbrace>
 4. \<And>cur cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> get_thread_state cur \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 5. \<lbrace>invs and valid_sched and valid_etcbs\<rbrace> gets cur_thread \<lbrace>?Q'6\<rbrace>
 6. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> gets cur_thread \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!