theory Refine

lemma entry_corres:
  "corres (=) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
                  (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and
                  (\<lambda>s. scheduler_action s = resume_cur_thread))
                 (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and
                  (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and
                  (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
                  (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
          (kernel_entry event tc) (kernelEntry event tc)" apply (simp add: kernel_entry_def kernelEntry_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply (rule corres_split) apply simp apply (rule threadset_corresT) apply (simp add: tcb_relation_def arch_tcb_relation_def
                             arch_tcb_context_set_def atcbContextSet_def) apply (clarsimp simp: tcb_cap_cases_def) apply (clarsimp simp: tcb_cte_cases_def) apply (simp add: exst_same_def) apply (rule corres_split[OF kernel_corres]) apply (rule corres_split_eqr[OF getCurThread_corres]) apply (rule threadGet_corres) apply (simp add: tcb_relation_def arch_tcb_relation_def
                             arch_tcb_context_get_def atcbContextGet_def) apply wp+ apply (rule hoare_strengthen_post, rule akernel_invs_det_ext, simp add: invs_def cur_tcb_def) apply (rule hoare_strengthen_post, rule ckernel_invs, simp add: invs'_def cur_tcb'_def) apply (wp thread_set_invs_trivial thread_set_ct_running
                 threadSet_invs_trivial threadSet_ct_running'
                 thread_set_not_state_valid_sched hoare_weak_lift_imp
                 hoare_vcg_disj_lift ct_in_state_thread_state_lift
              | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state
              | (wps, wp threadSet_st_tcb_at2) )+ apply (clarsimp simp: invs_def cur_tcb_def) apply (clarsimp simp: ct_in_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (kernel_entry event tc) (kernelEntry event tc) proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do t <- getCurThread;
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t;
y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do t <- getCurThread;
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t;
y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 2. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>t ta. t = ta \<Longrightarrow> corres (=) (?R4 t) (?R'4 ta) (do y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta;
y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 2. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t ta. t = ta \<Longrightarrow> corres (?r'8 t ta) (?P9 t) (?P'11 ta) (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t) (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta)
 2. \<And>t ta y ya. \<lbrakk>t = ta; ?r'8 t ta y ya\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta y) (?R'8 t ta ya) (do y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>?R'8 t ta\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. ?P9 t and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. ?P'11 ta and ?Q'12 ta\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t. corres (?r'8 t t) (?P9 t) (?P'11 t) (thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t) (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t)
 2. \<And>t ta y ya. \<lbrakk>t = ta; ?r'8 t ta y ya\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta y) (?R'8 t ta ya) (do y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>?R'8 t ta\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. ?P9 t and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. ?P'11 ta and ?Q'12 ta\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (11 subgoals):
 1. \<And>t tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_relation (tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb')) tcb')
 2. \<And>t tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) = getF tcb
 3. \<And>t. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) = getF tcb
 4. \<And>t tcb'. exst_same tcb' (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb')) tcb')
 5. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta y) (?R'8 t ta ya) (do y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 7. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>?R'8 t ta\<rbrace>
 8. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>t tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) = getF tcb
 2. \<And>t. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) = getF tcb
 3. \<And>t tcb'. exst_same tcb' (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb')) tcb')
 4. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta y) (?R'8 t ta ya) (do y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>?R'8 t ta\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 9. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>t. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) = getF tcb
 2. \<And>t tcb'. exst_same tcb' (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb')) tcb')
 3. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta y) (?R'8 t ta ya) (do y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>?R'8 t ta\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 8. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t tcb'. exst_same tcb' (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb')) tcb')
 2. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta y) (?R'8 t ta ya) (do y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>?R'8 t ta\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?R8 t ta y) (?R'8 t ta ya) (do y <- call_kernel event;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od) (do y <- callKernel event;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od)
 2. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?R8 t ta\<rbrace>
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>?R'8 t ta\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 6. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>t ta y ya yb yc. \<lbrakk>t = ta; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R46 t ta y ya yb) (?R'46 t ta y ya yc) (gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)) (getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch))
 2. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 t ta y\<rbrace> call_kernel event \<lbrace>?R46 t ta y ya\<rbrace>
 3. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'51 t ta ya\<rbrace> callKernel event \<lbrace>?R'46 t ta y ya\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) and ?Q49 t ta y\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'51 t ta ya\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 8. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (11 subgoals):
 1. \<And>t ta y ya yb yc rv. \<lbrakk>t = ta; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R55 t ta y ya yb yc rv) (?R'55 t ta y ya yb yc rv) (thread_get (arch_tcb_context_get \<circ> tcb_arch) rv) (threadGet (atcbContextGet \<circ> tcbArch) rv)
 2. \<And>t ta y ya yb yc. \<lbrakk>t = ta; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 t ta y ya yb\<rbrace> gets cur_thread \<lbrace>?R55 t ta y ya yb yc\<rbrace>
 3. \<And>t ta y ya yb yc. \<lbrakk>t = ta; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 t ta y ya yc\<rbrace> getCurThread \<lbrace>?R'55 t ta y ya yb yc\<rbrace>
 4. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 t ta y\<rbrace> call_kernel event \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q56 t ta y ya yb\<rbrace>
 5. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'51 t ta ya\<rbrace> callKernel event \<lbrace>\<lambda>yc. (\<lambda>_. True) and ?Q'57 t ta y ya yc\<rbrace>
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) and ?Q49 t ta y\<rbrace>
 7. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'51 t ta ya\<rbrace>
 8. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>t ta y ya yb yc rv tcb tcb'. \<lbrakk>t = ta; dc y ya; dc yb yc; tcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (arch_tcb_context_get \<circ> tcb_arch) tcb = (atcbContextGet \<circ> tcbArch) tcb'
 2. \<And>t ta y ya yb yc. \<lbrakk>t = ta; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 t ta y ya yb\<rbrace> gets cur_thread \<lbrace>tcb_at\<rbrace>
 3. \<And>t ta y ya yb yc. \<lbrakk>t = ta; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 t ta y ya yc\<rbrace> getCurThread \<lbrace>tcb_at'\<rbrace>
 4. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 t ta y\<rbrace> call_kernel event \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q56 t ta y ya yb\<rbrace>
 5. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'51 t ta ya\<rbrace> callKernel event \<lbrace>\<lambda>yc. (\<lambda>_. True) and ?Q'57 t ta y ya yc\<rbrace>
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) and ?Q49 t ta y\<rbrace>
 7. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'51 t ta ya\<rbrace>
 8. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 10. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>t ta y ya yb yc. \<lbrakk>t = ta; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q56 t ta y ya yb\<rbrace> gets cur_thread \<lbrace>tcb_at\<rbrace>
 2. \<And>t ta y ya yb yc. \<lbrakk>t = ta; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 t ta y ya yc\<rbrace> getCurThread \<lbrace>tcb_at'\<rbrace>
 3. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 t ta y\<rbrace> call_kernel event \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q56 t ta y ya yb\<rbrace>
 4. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'51 t ta ya\<rbrace> callKernel event \<lbrace>\<lambda>yc. (\<lambda>_. True) and ?Q'57 t ta y ya yc\<rbrace>
 5. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) and ?Q49 t ta y\<rbrace>
 6. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'51 t ta ya\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 9. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?P'73 t ta y\<rbrace> call_kernel event \<lbrace>\<lambda>rv s. tcb_at (cur_thread s) s\<rbrace>
 2. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'51 t ta ya\<rbrace> callKernel event \<lbrace>\<lambda>yc. (\<lambda>_. True) and (\<lambda>a. tcb_at' (ksCurThread a) a)\<rbrace>
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) and (\<lambda>s. True \<and> ?P'73 t ta y s)\<rbrace>
 4. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'51 t ta ya\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 7. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>t ta y ya. \<lbrakk>t = ta; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'51 t ta ya\<rbrace> callKernel event \<lbrace>\<lambda>yc. (\<lambda>_. True) and (\<lambda>a. tcb_at' (ksCurThread a) a)\<rbrace>
 2. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) and (\<lambda>s. True \<and> (invs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)) s)\<rbrace>
 3. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ?Q'51 t ta ya\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 6. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q10 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>y. einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s \<and> valid_domain_list s) and (\<lambda>s. True \<and> (invs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)) s)\<rbrace>
 2. \<And>t ta. t = ta \<Longrightarrow> \<lbrace>?Q'12 ta\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) ta \<lbrace>\<lambda>ya. invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>\<lambda>t. tcb_at t and ?Q10 t\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>\<lambda>ta. tcb_at' ta and ?Q'12 ta\<rbrace>
 5. \<And>s. (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> (event \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> 0 < domain_time s \<and> valid_domain_list s \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread \<Longrightarrow> tcb_at (cur_thread s) s \<and> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)
 2. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. (invs' sa \<and> tcb_at' (ksCurThread s) sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)) \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko d p. ko_at' ko (ksCurThread s) sa \<and> inQ d p (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) \<and> \<not> inQ d p ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)) \<longrightarrow> ex_nonz_cap_to' (ksCurThread s) sa \<and> ksCurThread s \<noteq> ksCurThread sa) \<and> (\<forall>tcb. tcbQueued (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) \<and> ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> ksCurThread s \<noteq> ksCurThread sa)) \<and> (event \<noteq> Interrupt \<longrightarrow> ct_running' sa) \<and> (st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread sa) sa \<or> st_tcb_at' idle' (ksCurThread sa) sa) \<and> ksSchedulerAction sa = ResumeCurrentThread \<and> vs_valid_duplicates' (ksPSpace sa) \<and> (invs' sa \<and> tcb_at' (ksCurThread s) sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)) \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko d p. ko_at' ko (ksCurThread s) sa \<and> inQ d p (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) \<and> \<not> inQ d p ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)) \<longrightarrow> ex_nonz_cap_to' (ksCurThread s) sa \<and> ksCurThread s \<noteq> ksCurThread sa) \<and> (\<forall>tcb. tcbQueued (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) \<and> ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> ksCurThread s \<noteq> ksCurThread sa)) \<and> vs_valid_duplicates' (ksPSpace sa) \<and> (event \<noteq> Interrupt \<longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread sa) sa) \<and> ksSchedulerAction sa = ResumeCurrentThread)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. (tcb_at' (ksCurThread s) and (\<lambda>sa. (invs' sa \<and> tcb_at' (ksCurThread s) sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)) \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko d p. ko_at' ko (ksCurThread s) sa \<and> inQ d p (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) \<and> \<not> inQ d p ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)) \<longrightarrow> ex_nonz_cap_to' (ksCurThread s) sa \<and> ksCurThread s \<noteq> ksCurThread sa) \<and> (\<forall>tcb. tcbQueued (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) \<and> ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> ksCurThread s \<noteq> ksCurThread sa)) \<and> (event \<noteq> Interrupt \<longrightarrow> ct_running' sa) \<and> (st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread sa) sa \<or> st_tcb_at' idle' (ksCurThread sa) sa) \<and> ksSchedulerAction sa = ResumeCurrentThread \<and> vs_valid_duplicates' (ksPSpace sa) \<and> (invs' sa \<and> tcb_at' (ksCurThread s) sa \<and> (\<forall>d p. (\<exists>tcb. inQ d p tcb \<and> \<not> inQ d p (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)) \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues sa (d, p))) \<and> (\<forall>ko d p. ko_at' ko (ksCurThread s) sa \<and> inQ d p (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch ko)) ko) \<and> \<not> inQ d p ko \<longrightarrow> ksCurThread s \<in> set (ksReadyQueues sa (d, p))) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb)) \<longrightarrow> ex_nonz_cap_to' (ksCurThread s) sa \<and> ksCurThread s \<noteq> ksCurThread sa) \<and> (\<forall>tcb. tcbQueued (tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) \<and> ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> tcbQueued tcb \<or> ksCurThread s \<noteq> ksCurThread sa)) \<and> vs_valid_duplicates' (ksPSpace sa) \<and> (event \<noteq> Interrupt \<longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread sa) sa) \<and> ksSchedulerAction sa = ResumeCurrentThread)) s)) s proof (prove)
goal:
No subgoals!