theory BCorres2_AI

lemma schedule_bcorres1:
  notes bsplits =
          s_bcorres_underlying_split[where g'="\<lambda>_. return ()",
                                     OF _ choose_thread_bcorres, simplified]
          s_bcorres_underlying_split[where g'="\<lambda>_. return ()",
                                     OF _ BCorres2_AI.guarded_switch_bcorres, simplified]
          s_bcorres_underlying_split[where f'="return ()", simplified]
  notes bdefs = schedule_det_ext_ext_def s_bcorres_get_left
                gets_def get_thread_state_def thread_get_def gets_the_def
                bind_assoc get_before_assert_opt ethread_get_def
                schedule_switch_thread_fastfail_def when_def
                tcb_sched_action_bcorres drop_sbcorres_underlying return_s_bcorres_underlying
  notes unfolds = s_bcorres_underlying_def set_scheduler_action_def
                   simpler_modify_def return_def
  shows "BCorres2_AI TYPE(det_ext) \<Longrightarrow> bcorres (schedule :: (unit,det_ext) s_monad) schedule" supply if_split[split del] apply (clarsimp simp: bcorres_underlying_def fail_def) apply (simp add: bdefs) apply (simp add: assert_opt_def) apply (simp split: option.split, intro conjI impI) apply (simp add: s_bcorres_underlying_def fail_def) apply clarsimp apply (split scheduler_action.split, intro conjI impI) 
    (* resume current *)
     subgoal for s apply (clarsimp simp: s_bcorres_underlying_def schedule_def allActiveTCBs_def
                            in_monad in_select getActiveTCB_def
                       split: if_split) apply (fastforce simp add: switch_to_idle_thread_def in_monad in_select ex_bool_eq) done 
   (* switch to *)
    subgoal for s cttcb apply clarsimp apply (rule bsplits)+ apply (simp add: bdefs) apply (simp add: assert_opt_def) apply (split option.split, simp, intro conjI impI) apply (simp add: s_bcorres_underlying_def fail_def) apply (clarsimp simp: ethread_get_when_def split: if_split) apply (rule conjI; clarsimp) apply (simp add: bdefs) apply (simp add: assert_opt_def) apply (split option.split, simp, intro conjI impI) apply (simp add: s_bcorres_underlying_def fail_def) apply (clarsimp simp: bdefs split: if_split
              | rule conjI
              | rule bsplits
              | erule drop_sbcorres_underlying[OF schedule_choose_new_thread_bcorres1]
              | fastforce simp: unfolds)+ done apply (clarsimp simp: bdefs split: if_split
         | rule conjI
         | rule bsplits
         | erule drop_sbcorres_underlying[OF schedule_choose_new_thread_bcorres1])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. BCorres2_AI TYPE(det_ext) \<Longrightarrow> bcorres schedule schedule proof (prove)
goal (1 subgoal):
 1. BCorres2_AI TYPE(det_ext) \<Longrightarrow> bcorres schedule schedule proof (prove)
goal (1 subgoal):
 1. \<And>s. BCorres2_AI TYPE(det_ext) \<Longrightarrow> s_bcorres schedule schedule s proof (prove)
goal (1 subgoal):
 1. \<And>s. BCorres2_AI TYPE(det_ext) \<Longrightarrow> s_bcorres (do tcb <- assert_opt (get_tcb (cur_thread s) s);
case scheduler_action s of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable (tcb_state tcb) \<or> cur_thread s = id);
return ()
od | switch_thread candidate \<Rightarrow> do when (runnable (tcb_state tcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state tcb) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when (runnable (tcb_state tcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od
od) schedule s proof (prove)
goal (1 subgoal):
 1. \<And>s. BCorres2_AI TYPE(det_ext) \<Longrightarrow> s_bcorres (do tcb <- case get_tcb (cur_thread s) s of None \<Rightarrow> fail | Some v \<Rightarrow> return v;
case scheduler_action s of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable (tcb_state tcb) \<or> cur_thread s = id);
return ()
od | switch_thread candidate \<Rightarrow> do when (runnable (tcb_state tcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state tcb) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when (runnable (tcb_state tcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od
od) schedule s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = None\<rbrakk> \<Longrightarrow> s_bcorres fail schedule s
 2. \<And>s. BCorres2_AI TYPE(det_ext) \<Longrightarrow> \<forall>x2. get_tcb (cur_thread s) s = Some x2 \<longrightarrow> s_bcorres (case scheduler_action s of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable (tcb_state x2) \<or> cur_thread s = id);
return ()
od | switch_thread candidate \<Rightarrow> do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state x2) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od) schedule s proof (prove)
goal (1 subgoal):
 1. \<And>s. BCorres2_AI TYPE(det_ext) \<Longrightarrow> \<forall>x2. get_tcb (cur_thread s) s = Some x2 \<longrightarrow> s_bcorres (case scheduler_action s of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable (tcb_state x2) \<or> cur_thread s = id);
return ()
od | switch_thread candidate \<Rightarrow> do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state x2) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od) schedule s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2\<rbrakk> \<Longrightarrow> s_bcorres (case scheduler_action s of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable (tcb_state x2) \<or> cur_thread s = id);
return ()
od | switch_thread candidate \<Rightarrow> do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state x2) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od) schedule s proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2; scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow> s_bcorres (do id <- gets idle_thread;
assert (runnable (tcb_state x2) \<or> cur_thread s = id);
return ()
od) schedule s
 2. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2\<rbrakk> \<Longrightarrow> \<forall>x2a. scheduler_action s = switch_thread x2a \<longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2a;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue x2a;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state x2) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2a;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2a;
set_scheduler_action resume_cur_thread
od
od) schedule s
 3. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od) schedule s proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2; scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow> s_bcorres (do id <- gets idle_thread;
assert (runnable (tcb_state x2) \<or> cur_thread s = id);
return ()
od) schedule s
 2. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2\<rbrakk> \<Longrightarrow> \<forall>x2a. scheduler_action s = switch_thread x2a \<longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2a;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue x2a;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state x2) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2a;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2a;
set_scheduler_action resume_cur_thread
od
od) schedule s
 3. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od) schedule s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2_; scheduler_action s = resume_cur_thread\<rbrakk> \<Longrightarrow> s_bcorres (do id <- gets idle_thread;
assert (runnable (tcb_state x2_) \<or> cur_thread s = id);
return ()
od) schedule s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2_; scheduler_action s = resume_cur_thread; runnable (tcb_state x2_) \<or> cur_thread s = idle_thread s\<rbrakk> \<Longrightarrow> (runnable (tcb_state x2_) \<longrightarrow> idle_thread s \<noteq> cur_thread s \<longrightarrow> (\<exists>thread. thread \<noteq> cur_thread s \<longrightarrow> (\<exists>y. (case get_tcb thread s of None \<Rightarrow> None | Some tcb \<Rightarrow> if runnable (tcb_state tcb) then Some tcb else None) = Some y) \<and> ((), truncate_state s) \<in> fst (switch_to_thread thread (truncate_state s))) \<or> ((), truncate_state s) \<in> fst (switch_to_idle_thread (truncate_state s))) \<and> (\<not> runnable (tcb_state x2_) \<longrightarrow> idle_thread s \<noteq> cur_thread s \<longrightarrow> (\<exists>thread. thread \<noteq> cur_thread s \<and> (thread \<noteq> cur_thread s \<longrightarrow> (\<exists>y. (case get_tcb thread s of None \<Rightarrow> None | Some tcb \<Rightarrow> if runnable (tcb_state tcb) then Some tcb else None) = Some y) \<and> ((), truncate_state s) \<in> fst (switch_to_thread thread (truncate_state s)))) \<or> ((), truncate_state s) \<in> fst (switch_to_idle_thread (truncate_state s))) proof (prove)
goal:
No subgoals! proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2\<rbrakk> \<Longrightarrow> \<forall>x2a. scheduler_action s = switch_thread x2a \<longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2a;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue x2a;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state x2) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2a;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2a;
set_scheduler_action resume_cur_thread
od
od) schedule s
 2. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od) schedule s proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2\<rbrakk> \<Longrightarrow> \<forall>x2a. scheduler_action s = switch_thread x2a \<longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2a;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue x2a;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state x2) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2a;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2a;
set_scheduler_action resume_cur_thread
od
od) schedule s
 2. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od) schedule s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb\<rbrakk> \<Longrightarrow> \<forall>x2. scheduler_action s = switch_thread x2 \<longrightarrow> s_bcorres (do when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable (tcb_state cttcb) \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od) schedule s proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (do y <- when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 (tcb_state cttcb) \<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) schedule s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s'. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s)) s)\<rbrakk> \<Longrightarrow> s_bcorres (do it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
ct_prio <- ethread_get_when (cur_thread s \<noteq> it) tcb_priority (cur_thread s);
fastfail <- schedule_switch_thread_fastfail (cur_thread s) 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 (tcb_state cttcb) \<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) schedule s'
 2. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s'. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s)\<rbrakk> \<Longrightarrow> s_bcorres (do tcb <- assert_opt (get_etcb x2 s');
ct_prio <- ethread_get_when (cur_thread s \<noteq> idle_thread s') tcb_priority (cur_thread s);
fastfail <- if cur_thread s \<noteq> idle_thread s' then return (tcb_priority tcb < ct_prio) else return True;
s <- get;
sa <- get;
if fastfail \<and> \<not> is_highest_prio (cur_domain s) (tcb_priority tcb) sa 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 (tcb_state cttcb) \<and> ct_prio = tcb_priority tcb 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) schedule s'
 2. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s'. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s)\<rbrakk> \<Longrightarrow> s_bcorres (do tcb <- case get_etcb x2 s' of None \<Rightarrow> fail | Some v \<Rightarrow> return v;
ct_prio <- ethread_get_when (cur_thread s \<noteq> idle_thread s') tcb_priority (cur_thread s);
fastfail <- if cur_thread s \<noteq> idle_thread s' then return (tcb_priority tcb < ct_prio) else return True;
s <- get;
sa <- get;
if fastfail \<and> \<not> is_highest_prio (cur_domain s) (tcb_priority tcb) sa 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 (tcb_state cttcb) \<and> ct_prio = tcb_priority tcb 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) schedule s'
 2. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (3 subgoals):
 1. \<And>x2 s'. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s); get_etcb x2 s' = None\<rbrakk> \<Longrightarrow> s_bcorres fail schedule s'
 2. \<And>x2 s'. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s)\<rbrakk> \<Longrightarrow> \<forall>x2a. get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do ct_prio <- ethread_get_when (cur_thread s \<noteq> idle_thread s') tcb_priority (cur_thread s);
fastfail <- if cur_thread s \<noteq> idle_thread s' then return (tcb_priority x2a < ct_prio) else return True;
s <- get;
sa <- get;
if fastfail \<and> \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa 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 (tcb_state cttcb) \<and> ct_prio = tcb_priority x2a 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) schedule s'
 3. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s'. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s)\<rbrakk> \<Longrightarrow> \<forall>x2a. get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do ct_prio <- ethread_get_when (cur_thread s \<noteq> idle_thread s') tcb_priority (cur_thread s);
fastfail <- if cur_thread s \<noteq> idle_thread s' then return (tcb_priority x2a < ct_prio) else return True;
s <- get;
sa <- get;
if fastfail \<and> \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa 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 (tcb_state cttcb) \<and> ct_prio = tcb_priority x2a 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) schedule s'
 2. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s'. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s)\<rbrakk> \<Longrightarrow> (cur_thread s \<noteq> idle_thread s' \<longrightarrow> (\<forall>x2a. get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do ct_prio <- ethread_get tcb_priority (cur_thread s);
s <- get;
sa <- get;
if tcb_priority x2a < ct_prio \<and> \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa 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 (tcb_state cttcb) \<and> ct_prio = tcb_priority x2a 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) schedule s')) \<and> (cur_thread s = idle_thread s' \<longrightarrow> (\<forall>x2a. (runnable (tcb_state cttcb) \<and> undefined = tcb_priority x2a \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) undefined sa then do y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od
od) schedule s') \<and> ((runnable (tcb_state cttcb) \<longrightarrow> undefined \<noteq> tcb_priority x2a) \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa then do y <- tcb_sched_action tcb_sched_enqueue 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) schedule s')))
 2. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (3 subgoals):
 1. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s); cur_thread s \<noteq> idle_thread s'; get_etcb x2 s' = Some x2a\<rbrakk> \<Longrightarrow> s_bcorres (do ct_prio <- ethread_get tcb_priority (cur_thread s);
s <- get;
sa <- get;
if tcb_priority x2a < ct_prio \<and> \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa 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 (tcb_state cttcb) \<and> ct_prio = tcb_priority x2a 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) schedule s'
 2. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (idle_thread s') s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (idle_thread s') else return ()) s); cur_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> (runnable (tcb_state cttcb) \<and> undefined = tcb_priority x2a \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) undefined sa then do y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od
od) schedule s') \<and> ((runnable (tcb_state cttcb) \<longrightarrow> undefined \<noteq> tcb_priority x2a) \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa then do y <- tcb_sched_action tcb_sched_enqueue 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) schedule s')
 3. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (3 subgoals):
 1. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s); cur_thread s \<noteq> idle_thread s'; get_etcb x2 s' = Some x2a\<rbrakk> \<Longrightarrow> s_bcorres (do tcb <- assert_opt (get_etcb (cur_thread s) s');
if tcb_priority x2a < tcb_priority tcb \<and> \<not> is_highest_prio (cur_domain s') (tcb_priority x2a) s' 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 (tcb_state cttcb) \<and> tcb_priority tcb = tcb_priority x2a 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) schedule s'
 2. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (idle_thread s') s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (idle_thread s') else return ()) s); cur_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> (runnable (tcb_state cttcb) \<and> undefined = tcb_priority x2a \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) undefined sa then do y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od
od) schedule s') \<and> ((runnable (tcb_state cttcb) \<longrightarrow> undefined \<noteq> tcb_priority x2a) \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa then do y <- tcb_sched_action tcb_sched_enqueue 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) schedule s')
 3. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (3 subgoals):
 1. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s); cur_thread s \<noteq> idle_thread s'; get_etcb x2 s' = Some x2a\<rbrakk> \<Longrightarrow> s_bcorres (do tcb <- case get_etcb (cur_thread s) s' of None \<Rightarrow> fail | Some v \<Rightarrow> return v;
if tcb_priority x2a < tcb_priority tcb \<and> \<not> is_highest_prio (cur_domain s') (tcb_priority x2a) s' 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 (tcb_state cttcb) \<and> tcb_priority tcb = tcb_priority x2a 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) schedule s'
 2. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (idle_thread s') s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (idle_thread s') else return ()) s); cur_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> (runnable (tcb_state cttcb) \<and> undefined = tcb_priority x2a \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) undefined sa then do y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od
od) schedule s') \<and> ((runnable (tcb_state cttcb) \<longrightarrow> undefined \<noteq> tcb_priority x2a) \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa then do y <- tcb_sched_action tcb_sched_enqueue 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) schedule s')
 3. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (4 subgoals):
 1. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s); cur_thread s \<noteq> idle_thread s'; get_etcb x2 s' = Some x2a; get_etcb (cur_thread s) s' = None\<rbrakk> \<Longrightarrow> s_bcorres fail schedule s'
 2. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s); cur_thread s \<noteq> idle_thread s'; get_etcb x2 s' = Some x2a\<rbrakk> \<Longrightarrow> \<forall>x2b. get_etcb (cur_thread s) s' = Some x2b \<longrightarrow> s_bcorres (if tcb_priority x2a < tcb_priority x2b \<and> \<not> is_highest_prio (cur_domain s') (tcb_priority x2a) s' 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 (tcb_state cttcb) \<and> tcb_priority x2b = tcb_priority x2a 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) schedule s'
 3. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (idle_thread s') s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (idle_thread s') else return ()) s); cur_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> (runnable (tcb_state cttcb) \<and> undefined = tcb_priority x2a \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) undefined sa then do y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od
od) schedule s') \<and> ((runnable (tcb_state cttcb) \<longrightarrow> undefined \<noteq> tcb_priority x2a) \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa then do y <- tcb_sched_action tcb_sched_enqueue 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) schedule s')
 4. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal (3 subgoals):
 1. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (cur_thread s) else return ()) s); cur_thread s \<noteq> idle_thread s'; get_etcb x2 s' = Some x2a\<rbrakk> \<Longrightarrow> \<forall>x2b. get_etcb (cur_thread s) s' = Some x2b \<longrightarrow> s_bcorres (if tcb_priority x2a < tcb_priority x2b \<and> \<not> is_highest_prio (cur_domain s') (tcb_priority x2a) s' 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 (tcb_state cttcb) \<and> tcb_priority x2b = tcb_priority x2a 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) schedule s'
 2. \<And>x2 s' x2a. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (idle_thread s') s = Some cttcb; scheduler_action s = switch_thread x2; ((), s') \<in> fst ((if runnable (tcb_state cttcb) then tcb_sched_action tcb_sched_enqueue (idle_thread s') else return ()) s); cur_thread s = idle_thread s'\<rbrakk> \<Longrightarrow> (runnable (tcb_state cttcb) \<and> undefined = tcb_priority x2a \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) undefined sa then do y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od
od) schedule s') \<and> ((runnable (tcb_state cttcb) \<longrightarrow> undefined \<noteq> tcb_priority x2a) \<longrightarrow> get_etcb x2 s' = Some x2a \<longrightarrow> s_bcorres (do s <- get;
sa <- get;
if \<not> is_highest_prio (cur_domain s) (tcb_priority x2a) sa then do y <- tcb_sched_action tcb_sched_enqueue 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) schedule s')
 3. \<And>x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some cttcb; scheduler_action s = switch_thread x2\<rbrakk> \<Longrightarrow> s_bcorres (when (runnable (tcb_state cttcb)) (tcb_sched_action tcb_sched_enqueue (cur_thread s))) (return ()) s proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>BCorres2_AI TYPE(det_ext); get_tcb (cur_thread s) s = Some x2; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> s_bcorres (do when (runnable (tcb_state x2)) (tcb_sched_action tcb_sched_enqueue (cur_thread s));
schedule_choose_new_thread
od) schedule s proof (prove)
goal:
No subgoals!