theory Noninterference

lemma schedule_reads_respects_g:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_g aag (l :: 'a subject_label)
           ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and
            pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag)
           schedule" supply ethread_get_wp[wp del] supply set_scheduler_action_wp[wp del] supply conj_cong[cong del]  (* knowing the scheduler action messes with valid_sched_2 *)
   apply (simp add: schedule_def) apply wp apply wpc 
           (* resume current thread *)
            apply wp[1] prefer 2 
          (* choose new thread *)
           apply ((wp set_scheduler_action_reads_respects_g tcb_sched_action_reads_respects_g
                     schedule_choose_new_thread_reads_respects_g when_ev
                  | wpc | simp)+)[1] 
         (* now switch_thread case *)
          apply (wpsimp wp: schedule_choose_new_thread_reads_respects_g enqueue_thread_queued
                           set_scheduler_action_reads_respects_g tcb_sched_action_reads_respects_g
                           set_scheduler_action_cnt_valid_sched)+ 
                        (* tcb_sched_action tcb_sched_append *)
                         apply (wp append_thread_queued set_scheduler_action_reads_respects_g
                                  guarded_switch_to_reads_respects_g
                                  reads_respects_g_from_inv[OF reads_respects_is_highest_prio]
                                  reads_equiv_valid_g_inv_schedule_switch_thread_fastfail)+ 
                 (* fastfail calculation *)
                  apply (wpsimp wp: reads_respects_g_from_inv[OF reads_respects_ethread_get]
                                   reads_respects_g_from_inv[OF reads_respects_ethread_get_when]
                                   when_ev gts_wp tcb_sched_action_reads_respects_g
                                   tcb_sched_action_enqueue_valid_blocked_except
                                   get_thread_state_reads_respects_g
                        | wp (once) hoare_drop_imp)+ apply (clarsimp simp: invs_valid_idle) apply (intro allI conjI impI; (elim conjE)?;
         ((fastforce simp: valid_sched_def valid_sched_action_switch_is_subject[OF domains_distinct]
                    dest!: reads_equiv_gD intro!: globals_equiv_idle_thread_ptr))?) apply (tactic \<open>distinct_subgoals_tac\<close>) apply (all \<open>(erule requiv_g_cur_thread_eq)?\<close>) apply (simp_all add: requiv_sched_act_eq[OF reads_equiv_gD[THEN conjunct1]]) apply (all \<open>(solves \<open>clarsimp elim!: st_tcb_weakenE\<close>)?\<close>) apply (all \<open>(solves \<open>clarsimp simp: not_cur_thread_def\<close>)?\<close>) apply (clarsimp simp: valid_sched_def valid_sched_action_def weak_valid_sched_action_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) schedule proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) schedule proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) schedule proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) schedule proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) schedule proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) (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 tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<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) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od) proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q2 rv rva rvb) (case rvb of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable rva \<or> rv = id)
od | switch_thread candidate \<Rightarrow> do y <- when (runnable rva) (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 tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<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 y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 2. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
 3. \<And>rv rva. \<lbrace>?P''2 rv rva\<rbrace> gets scheduler_action \<lbrace>?Q2 rv rva\<rbrace>
 4. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'1 rv) (get_thread_state rv)
 5. \<And>rv. \<lbrace>?P''1 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'2 rv rva s \<and> ?P''2 rv rva s\<rbrace>
 6. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets cur_thread)
 7. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 8. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb. rvb = resume_cur_thread \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R11 rv rva rvb) (do id <- gets idle_thread;
assert (runnable rva \<or> rv = id)
od)
 2. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R10 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<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)
 3. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R8 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 4. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
 5. \<And>rv rva. \<lbrace>?P''2 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> ?R11 rv rva rvb s) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R10 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R8 rv rva rvb s)\<rbrace>
 6. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'1 rv) (get_thread_state rv)
 7. \<And>rv. \<lbrace>?P''1 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'2 rv rva s \<and> ?P''2 rv rva s\<rbrace>
 8. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets cur_thread)
 9. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 10. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb. rvb = resume_cur_thread \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R11 rv rva rvb) (do id <- gets idle_thread;
assert (runnable rva \<or> rv = id)
od)
 2. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R10 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<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)
 3. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R8 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 4. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
 5. \<And>rv rva. \<lbrace>?P''2 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> ?R11 rv rva rvb s) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R10 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R8 rv rva rvb s)\<rbrace>
 6. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'1 rv) (get_thread_state rv)
 7. \<And>rv. \<lbrace>?P''1 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'2 rv rva s \<and> ?P''2 rv rva s\<rbrace>
 8. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets cur_thread)
 9. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 10. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R10 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<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)
 2. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R8 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 3. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
 4. \<And>rv rva. \<lbrace>?P''2 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R10 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R8 rv rva rvb s)\<rbrace>
 5. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'1 rv) (get_thread_state rv)
 6. \<And>rv. \<lbrace>?P''1 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'2 rv rva s \<and> ?P''2 rv rva s\<rbrace>
 7. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets cur_thread)
 8. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 9. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R8 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R10 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<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)
 3. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
 4. \<And>rv rva. \<lbrace>?P''2 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R10 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R8 rv rva rvb s)\<rbrace>
 5. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'1 rv) (get_thread_state rv)
 6. \<And>rv. \<lbrace>?P''1 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'2 rv rva s \<and> ?P''2 rv rva s\<rbrace>
 7. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets cur_thread)
 8. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 9. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb. rvb = choose_new_thread \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R8 rv rva rvb) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
schedule_choose_new_thread
od)
 2. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R10 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<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)
 3. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
 4. \<And>rv rva. \<lbrace>?P''2 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R10 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> ?R8 rv rva rvb s)\<rbrace>
 5. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'1 rv) (get_thread_state rv)
 6. \<And>rv. \<lbrace>?P''1 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'2 rv rva s \<and> ?P''2 rv rva s\<rbrace>
 7. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets cur_thread)
 8. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 9. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R10 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<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)
 2. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
 3. \<And>rv rva. \<lbrace>?P''2 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R10 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> (runnable rva \<longrightarrow> pas_refined aag s) \<and> (if runnable rva then \<lambda>s. domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable rv and not_cur_thread rv and valid_blocked_except rv) s \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) else (\<lambda>s. domain_time s \<noteq> 0 \<and> einvs s \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)))) s)\<rbrace>
 4. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'1 rv) (get_thread_state rv)
 5. \<And>rv. \<lbrace>?P''1 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'2 rv rva s \<and> ?P''2 rv rva s\<rbrace>
 6. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets cur_thread)
 7. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 8. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?R10 rv rva rvb x2) (do y <- when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 tcb_sched_action tcb_sched_enqueue x2;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable rva \<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)
 2. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
 3. \<And>rv rva. \<lbrace>?P''2 rv rva\<rbrace> gets scheduler_action \<lbrace>\<lambda>rvb s. (rvb = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> True) \<and> (\<forall>x. rvb = switch_thread x \<longrightarrow> ?R10 rv rva rvb x s) \<and> (rvb = choose_new_thread \<longrightarrow> (runnable rva \<longrightarrow> pas_refined aag s) \<and> (if runnable rva then \<lambda>s. domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable rv and not_cur_thread rv and valid_blocked_except rv) s \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) else (\<lambda>s. domain_time s \<noteq> 0 \<and> einvs s \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)))) s)\<rbrace>
 4. \<And>rv. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'1 rv) (get_thread_state rv)
 5. \<And>rv. \<lbrace>?P''1 rv\<rbrace> get_thread_state rv \<lbrace>\<lambda>rva s. ?P'2 rv rva s \<and> ?P''2 rv rva s\<rbrace>
 6. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets cur_thread)
 7. \<lbrace>?P''\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. ?P'1 rv s \<and> ?P''1 rv s\<rbrace>
 8. \<And>s. ((\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and einvs and pas_cur_domain aag and (\<lambda>s. domain_time s \<noteq> 0) and pas_refined aag) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (23 subgoals):
 1. \<And>rv rva x2 rvd rve rvg rvh rvi. \<lbrakk>rvg \<longrightarrow> rvi; runnable rva\<rbrakk> \<Longrightarrow> \<lbrace>?P'155 rv rva (switch_thread x2) x2 () rvd rve rve rvg rvh rvi\<rbrace> tcb_sched_action tcb_sched_append x2 \<lbrace>\<lambda>rvb s. (\<exists>d p. ?t159 rv rva (switch_thread x2) x2 () rvd rve rve rvg rvh rvi \<in> set (ready_queues s d p)) \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace>
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; \<not> (rvg \<and> \<not> rvi); \<not> (runnable rva \<and> rvf = rve)\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q113 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'56 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''56 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> pas_refined aag s \<and> True \<and> domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable x2 and not_cur_thread x2 and valid_blocked_except x2) s \<and> scheduler_action s = switch_thread x2 \<and> True \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> pas_refined aag s \<and> True \<and> domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable x2 and not_cur_thread x2 and valid_blocked_except x2) s \<and> scheduler_action s = switch_thread (?t159 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) \<and> ?P'155 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> ?Q113 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s))\<rbrace>
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'55 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 6. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''55 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'56 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''56 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'54 rv rva rvb x2 rvc rvd rve rvf) (schedule_switch_thread_fastfail rv rvd rvf rve)
 8. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''54 rv rva rvb x2 rvc rvd rve rvf\<rbrace> schedule_switch_thread_fastfail rv rvd rvf rve \<lbrace>\<lambda>rvg s. ?P'55 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''55 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'53 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 10. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''53 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'54 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''54 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
A total of 23 subgoals... proof (prove)
goal (23 subgoals):
 1. \<And>rv rva x2 rvd rve rvg rvh rvi. \<lbrakk>rvg \<longrightarrow> rvi; runnable rva\<rbrakk> \<Longrightarrow> \<lbrace>?P'155 rv rva (switch_thread x2) x2 () rvd rve rve rvg rvh rvi\<rbrace> tcb_sched_action tcb_sched_append x2 \<lbrace>\<lambda>rvb s. (\<exists>d p. ?t159 rv rva (switch_thread x2) x2 () rvd rve rve rvg rvh rvi \<in> set (ready_queues s d p)) \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace>
 2. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi. \<lbrakk>rvb = switch_thread x2; \<not> (rvg \<and> \<not> rvi); \<not> (runnable rva \<and> rvf = rve)\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q113 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) (do guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od)
 3. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'56 rv rva rvb x2 rvc rvd rve rvf rvg rvh) (gets (is_highest_prio rvh rve))
 4. \<And>rv rva rvb x2 rvc rvd rve rvf rvg rvh. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''56 rv rva rvb x2 rvc rvd rve rvf rvg rvh\<rbrace> gets (is_highest_prio rvh rve) \<lbrace>\<lambda>rvi s. (rvg \<and> \<not> rvi \<longrightarrow> pas_refined aag s \<and> True \<and> domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable x2 and not_cur_thread x2 and valid_blocked_except x2) s \<and> scheduler_action s = switch_thread x2 \<and> True \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))) \<and> (\<not> (rvg \<and> \<not> rvi) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> pas_refined aag s \<and> True \<and> domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable x2 and not_cur_thread x2 and valid_blocked_except x2) s \<and> scheduler_action s = switch_thread (?t159 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi) \<and> ?P'155 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> ?Q113 rv rva rvb x2 rvc rvd rve rvf rvg rvh rvi s))\<rbrace>
 5. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'55 rv rva rvb x2 rvc rvd rve rvf rvg) (gets cur_domain)
 6. \<And>rv rva rvb x2 rvc rvd rve rvf rvg. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''55 rv rva rvb x2 rvc rvd rve rvf rvg\<rbrace> gets cur_domain \<lbrace>\<lambda>rvh s. ?P'56 rv rva rvb x2 rvc rvd rve rvf rvg rvh s \<and> ?P''56 rv rva rvb x2 rvc rvd rve rvf rvg rvh s\<rbrace>
 7. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'54 rv rva rvb x2 rvc rvd rve rvf) (schedule_switch_thread_fastfail rv rvd rvf rve)
 8. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''54 rv rva rvb x2 rvc rvd rve rvf\<rbrace> schedule_switch_thread_fastfail rv rvd rvf rve \<lbrace>\<lambda>rvg s. ?P'55 rv rva rvb x2 rvc rvd rve rvf rvg s \<and> ?P''55 rv rva rvb x2 rvc rvd rve rvf rvg s\<rbrace>
 9. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'53 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 10. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''53 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. ?P'54 rv rva rvb x2 rvc rvd rve rvf s \<and> ?P''54 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
A total of 23 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P'208 rv rva rvb x2 rvc rvd rve rvf\<rbrace> schedule_switch_thread_fastfail rv rvd rvf rve \<lbrace>\<lambda>rv s. (rv \<and> \<not> is_highest_prio (cur_domain s) rve s \<longrightarrow> pas_refined aag s \<and> True \<and> domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable x2 and not_cur_thread x2 and valid_blocked_except x2) s \<and> scheduler_action s = switch_thread x2 \<and> True \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))) \<and> (\<not> (rv \<and> \<not> is_highest_prio (cur_domain s) rve s) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> pas_refined aag s \<and> True \<and> domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable x2 and not_cur_thread x2 and valid_blocked_except x2) s \<and> scheduler_action s = switch_thread x2 \<and> True \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> (pas_refined aag and valid_idle and (\<lambda>s. is_subject aag x2)) s \<and> True))\<rbrace>
 2. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'53 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 3. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''53 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. (rv \<noteq> rvd \<longrightarrow> is_subject aag rv) \<and> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> pas_cur_domain aag s \<and> ?P'208 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 4. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'52 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
 5. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''52 rv rva rvb x2 rvc rvd\<rbrace> ethread_get tcb_priority x2 \<lbrace>\<lambda>rve s. ?P'53 rv rva rvb x2 rvc rvd rve s \<and> ?P''53 rv rva rvb x2 rvc rvd rve s\<rbrace>
 6. \<And>rv rva rvb x2 rvc. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'51 rv rva rvb x2 rvc) (gets idle_thread)
 7. \<And>rv rva rvb x2 rvc. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''51 rv rva rvb x2 rvc\<rbrace> gets idle_thread \<lbrace>\<lambda>rvd s. ?P'52 rv rva rvb x2 rvc rvd s \<and> ?P''52 rv rva rvb x2 rvc rvd s\<rbrace>
 8. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'50 rv rva rvb x2) (when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv))
 9. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''50 rv rva rvb x2\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvc s. ?P'51 rv rva rvb x2 rvc s \<and> ?P''51 rv rva rvb x2 rvc s\<rbrace>
 10. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rvb x2 rvc rvd rve rvf. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P'208 rv rva rvb x2 rvc rvd rve rvf\<rbrace> schedule_switch_thread_fastfail rv rvd rvf rve \<lbrace>\<lambda>rv s. (rv \<and> \<not> is_highest_prio (cur_domain s) rve s \<longrightarrow> pas_refined aag s \<and> True \<and> domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable x2 and not_cur_thread x2 and valid_blocked_except x2) s \<and> scheduler_action s = switch_thread x2 \<and> True \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))) \<and> (\<not> (rv \<and> \<not> is_highest_prio (cur_domain s) rve s) \<longrightarrow> (runnable rva \<and> rvf = rve \<longrightarrow> pas_refined aag s \<and> True \<and> domain_time s \<noteq> 0 \<and> invs s \<and> valid_list s \<and> (valid_sched_except_blocked and st_tcb_at runnable x2 and not_cur_thread x2 and valid_blocked_except x2) s \<and> scheduler_action s = switch_thread x2 \<and> True \<and> pas_cur_domain aag s \<and> pas_refined aag s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s))) \<and> (\<not> (runnable rva \<and> rvf = rve) \<longrightarrow> (pas_refined aag and valid_idle and (\<lambda>s. is_subject aag x2)) s \<and> True))\<rbrace>
 2. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'53 rv rva rvb x2 rvc rvd rve) (ethread_get_when (rv \<noteq> rvd) tcb_priority rv)
 3. \<And>rv rva rvb x2 rvc rvd rve. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''53 rv rva rvb x2 rvc rvd rve\<rbrace> ethread_get_when (rv \<noteq> rvd) tcb_priority rv \<lbrace>\<lambda>rvf s. (rv \<noteq> rvd \<longrightarrow> is_subject aag rv) \<and> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> pas_cur_domain aag s \<and> ?P'208 rv rva rvb x2 rvc rvd rve rvf s\<rbrace>
 4. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'52 rv rva rvb x2 rvc rvd) (ethread_get tcb_priority x2)
 5. \<And>rv rva rvb x2 rvc rvd. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''52 rv rva rvb x2 rvc rvd\<rbrace> ethread_get tcb_priority x2 \<lbrace>\<lambda>rve s. ?P'53 rv rva rvb x2 rvc rvd rve s \<and> ?P''53 rv rva rvb x2 rvc rvd rve s\<rbrace>
 6. \<And>rv rva rvb x2 rvc. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'51 rv rva rvb x2 rvc) (gets idle_thread)
 7. \<And>rv rva rvb x2 rvc. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''51 rv rva rvb x2 rvc\<rbrace> gets idle_thread \<lbrace>\<lambda>rvd s. ?P'52 rv rva rvb x2 rvc rvd s \<and> ?P''52 rv rva rvb x2 rvc rvd s\<rbrace>
 8. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'50 rv rva rvb x2) (when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv))
 9. \<And>rv rva rvb x2. rvb = switch_thread x2 \<Longrightarrow> \<lbrace>?P''50 rv rva rvb x2\<rbrace> when (runnable rva) (tcb_sched_action tcb_sched_enqueue rv) \<lbrace>\<lambda>rvc s. ?P'51 rv rva rvb x2 rvc s \<and> ?P''51 rv rva rvb x2 rvc s\<rbrace>
 10. \<And>rv rva. reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P'2 rv rva) (gets scheduler_action)
A total of 16 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> valid_idle s \<and> (is_subject aag (cur_thread s) \<or> cur_thread s = idle_thread s) \<and> (\<forall>st. (runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t) \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> is_subject aag x \<and> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> valid_etcbs s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_etcbs s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_idle s \<and> is_subject aag x) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable (cur_thread s) s \<and> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s) \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) choose_new_thread (cur_thread s))) \<and> (\<not> runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t) \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> is_subject aag x \<and> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_idle s \<and> is_subject aag x) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t) \<and> (is_subject aag (cur_thread s) \<or> cur_thread s = idle_thread s) \<and> (\<forall>st. (runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t) \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> is_subject aag x \<and> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> valid_etcbs s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_etcbs s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> is_subject aag x) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable (cur_thread s) s \<and> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s) \<and> valid_blocked_except_2 (cur_thread s) (ready_queues s) (kheap s) choose_new_thread (cur_thread s))) \<and> (\<not> runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> scheduler_action s = scheduler_action t) \<and> (scheduler_action s = resume_cur_thread \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t)) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> idle_thread s = idle_thread t) \<and> is_subject aag x \<and> (\<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_domain s = cur_domain t) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s) \<and> valid_sched_action_2 (switch_thread x) (ekheap s) (kheap s) (cur_thread s) (cur_domain s) \<and> valid_idle_etcb s \<and> st_tcb_at runnable x s \<and> not_cur_thread_2 x (switch_thread x) (cur_thread s) \<and> valid_blocked_except_2 x (ready_queues s) (kheap s) (switch_thread x) (cur_thread s) \<and> is_subject aag x) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)))) proof (prove)
goal (14 subgoals):
 1. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 2. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s)
 3. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 4. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s)
 5. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 6. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s)
 7. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 8. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s)
 9. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 10. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s)
A total of 14 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 2. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s)
 3. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 4. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s)
 5. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 6. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s)
 7. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 8. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s) proof (prove)
goal (8 subgoals):
 1. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 2. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s)
 3. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 4. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s)
 5. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 6. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s)
 7. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 8. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched s; pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s) proof (prove)
goal (8 subgoals):
 1. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 2. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s)
 3. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 4. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s)
 5. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 6. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s)
 7. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 8. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s) proof (prove)
goal (6 subgoals):
 1. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) (switch_thread x) (cur_thread s)
 2. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 3. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s)
 4. \<And>s st. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) choose_new_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> not_cur_thread_2 (cur_thread s) choose_new_thread (cur_thread s)
 5. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 6. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> not_cur_thread_2 x (switch_thread x) (cur_thread s) proof (prove)
goal (2 subgoals):
 1. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s
 2. \<And>s st x. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s); invs s; valid_list s; valid_sched_2 (ready_queues s) (ekheap s) (switch_thread x) (cur_domain s) (kheap s) (cur_thread s) (idle_thread s); pas_cur_domain aag s; domain_time s \<noteq> 0; pas_refined aag s; \<not> runnable st; st_tcb_at ((=) st) (cur_thread s) s; scheduler_action s = switch_thread x\<rbrakk> \<Longrightarrow> st_tcb_at runnable x s proof (prove)
goal:
No subgoals!