theory ADT_IF_Refine_C

lemma schedule_if_corres_C:
  "corres_underlying rf_sr False False (=)
     (invs' and ex_abs einvs and valid_domain_list'
            and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) \<top>
     (schedule'_if tc) (schedule_C_if' tc)" apply (simp add: schedule'_if_def schedule_C_if'_def) apply (subst bind_assoc[symmetric], rule corres_stateAssert_no_fail) using corres_nofail[OF schedule_if_corres[of tc], simplified] apply (simp add: schedule'_if_def bind_assoc) apply (erule no_fail_pre) apply (clarsimp simp: ex_abs_def) apply (rule exI, rule conjI, assumption) apply (clarsimp simp: domain_time_rel_eq domain_list_rel_eq) apply (clarsimp simp: state_relation_def) apply (simp only: bind_assoc) apply (rule corres_guard_imp) apply (rule_tac r'="dc" in corres_split) apply (rule ccorres_corres_u') apply (rule schedule_ccorres) apply (rule corres_nofail) apply (rule schedule_corres) apply (erule FalseE) apply simp apply simp apply simp apply (rule_tac r'="dc" in corres_split) apply (rule ccorres_corres_u') apply (rule activateThread_ccorres) apply (rule corres_nofail) apply (rule activateThread_corres) apply (erule FalseE) apply simp apply simp apply simp apply (rule hoare_post_taut[where P=\<top>])+ apply (rule_tac Q="\<lambda>r. ct_in_state' activatable' and invs' and
                            ex_abs (invs and ct_in_state activatable)" in hoare_strengthen_post) apply (wp schedule_invs' corres_ex_abs_lift) apply (rule schedule_corres) apply wp apply (clarsimp simp: ex_abs_def invs'_def valid_state'_def valid_pspace'_def) apply fastforce apply simp apply (rule hoare_post_taut[where P=\<top>]) apply (auto simp: ex_abs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (schedule'_if tc) (schedule_C_if' tc) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- ThreadDecls_H.schedule;
y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (2 subgoals):
 1. no_fail (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od)
 2. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
using this:
no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_sched s \<and> valid_list s \<and> valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> invs' s') (schedule'_if tc)

goal (2 subgoals):
 1. no_fail (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od)
 2. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (2 subgoals):
 1. no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s \<and> valid_sched s \<and> valid_list s \<and> valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> invs' s') (do y <- ThreadDecls_H.schedule;
y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od) \<Longrightarrow> no_fail (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (do x <- ThreadDecls_H.schedule;
y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od)
 2. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> valid_domain_list sa \<and> (domain_time sa = 0 \<longrightarrow> scheduler_action sa = choose_new_thread) \<and> invs' s
 2. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>invs' s; valid_domain_list' s; ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa\<rbrakk> \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> valid_domain_list sa \<and> (domain_time sa = 0 \<longrightarrow> scheduler_action sa = choose_new_thread)
 2. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>invs' s; valid_domain_list' s; ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa\<rbrakk> \<Longrightarrow> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> valid_domain_list sa \<and> (domain_time sa = 0 \<longrightarrow> scheduler_action sa = choose_new_thread)
 2. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>invs' s; valid_domain_list sa; (sa, s) \<in> state_relation; invs sa; valid_list sa; valid_sched sa; domain_time sa = 0; ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> scheduler_action sa = choose_new_thread
 2. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do y <- do x <- ThreadDecls_H.schedule;
activateThread
od;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False False (=) (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) (\<lambda>_. True) (do x <- ThreadDecls_H.schedule;
y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying rf_sr False False (=) ?Q26 ?Q'26 (do x <- ThreadDecls_H.schedule;
y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call schedule_'proc);
y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 2. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ?Q26 s
 3. \<And>s. True \<Longrightarrow> ?Q'26 s proof (prove)
goal (6 subgoals):
 1. corres_underlying rf_sr False False dc ?P30 ?P'30 ThreadDecls_H.schedule (exec_C \<Gamma> (com.Call schedule_'proc))
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R30 rv) (?R'30 rv') (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 3. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 4. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 5. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (?P30 and ?Q30) s
 6. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (9 subgoals):
 1. ccorres dc xfdc ?P'34 ?Q'34 [] ThreadDecls_H.schedule (com.Call schedule_'proc)
 2. no_fail ?P''34 ThreadDecls_H.schedule
 3. \<And>s. ?P30 s \<Longrightarrow> ?P'34 s \<and> ?P''34 s
 4. Collect ?P'30 \<subseteq> ?Q'34
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R30 rv) (?R'30 rv') (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 6. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 7. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 8. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (?P30 and ?Q30) s
 9. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (8 subgoals):
 1. no_fail ?P''34 ThreadDecls_H.schedule
 2. \<And>s. ?P30 s \<Longrightarrow> invs' s \<and> ?P''34 s
 3. Collect ?P'30 \<subseteq> UNIV
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R30 rv) (?R'30 rv') (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 5. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 6. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 7. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (?P30 and ?Q30) s
 8. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (9 subgoals):
 1. corres_underlying ?state_relation39 ?nf39 True ?r39 ?P39 ?P'39 ?f39 ThreadDecls_H.schedule
 2. ?nf39 \<Longrightarrow> no_fail ?P39 ?f39
 3. \<And>s. ?P30 s \<Longrightarrow> invs' s \<and> (\<exists>sa. (sa, s) \<in> ?state_relation39 \<and> ?P39 sa \<and> ?P'39 s)
 4. Collect ?P'30 \<subseteq> UNIV
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R30 rv) (?R'30 rv') (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 6. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 7. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 8. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (?P30 and ?Q30) s
 9. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (8 subgoals):
 1. False \<Longrightarrow> no_fail (invs and valid_sched and valid_list) state_ext_sched_class.schedule
 2. \<And>s. ?P30 s \<Longrightarrow> invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> (invs and valid_sched and valid_list) sa \<and> invs' s)
 3. Collect ?P'30 \<subseteq> UNIV
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R30 rv) (?R'30 rv') (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 5. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 6. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 7. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (?P30 and ?Q30) s
 8. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (7 subgoals):
 1. \<And>s. ?P30 s \<Longrightarrow> invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> (invs and valid_sched and valid_list) sa \<and> invs' s)
 2. Collect ?P'30 \<subseteq> UNIV
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R30 rv) (?R'30 rv') (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 4. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 5. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 6. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> (?P30 and ?Q30) s
 7. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (6 subgoals):
 1. Collect ?P'30 \<subseteq> UNIV
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R30 rv) (?R'30 rv') (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 3. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 4. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 5. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 6. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R30 rv) (?R'30 rv') (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 2. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 3. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 4. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 5. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (5 subgoals):
 1. corres_underlying rf_sr False False (=) (?R30 ()) (?R'30 ()) (do y <- activateThread;
return tc
od) (do y <- exec_C \<Gamma> (com.Call activateThread_'proc);
return tc
od)
 2. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>?R30\<rbrace>
 3. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?R'30\<rbrace>
 4. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 5. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (8 subgoals):
 1. corres_underlying rf_sr False False dc (?P54 ()) (?P'52 ()) activateThread (exec_C \<Gamma> (com.Call activateThread_'proc))
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R43 rv) (?R'43 rv') (return tc) (return tc)
 3. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 4. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 5. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ?P54 a and ?Q53 a\<rbrace>
 6. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 7. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 8. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (11 subgoals):
 1. ccorres dc xfdc ?P'55 ?Q'55 [] activateThread (com.Call activateThread_'proc)
 2. no_fail ?P''55 activateThread
 3. \<And>s. ?P54 () s \<Longrightarrow> ?P'55 s \<and> ?P''55 s
 4. {a. ?P'52 () a} \<subseteq> ?Q'55
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R43 rv) (?R'43 rv') (return tc) (return tc)
 6. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 7. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 8. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ?P54 a and ?Q53 a\<rbrace>
 9. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 10. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. no_fail ?P''55 activateThread
 2. \<And>s. ?P54 () s \<Longrightarrow> (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s \<and> ?P''55 s
 3. {a. ?P'52 () a} \<subseteq> UNIV
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R43 rv) (?R'43 rv') (return tc) (return tc)
 5. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 6. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 7. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ?P54 a and ?Q53 a\<rbrace>
 8. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 9. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 10. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (11 subgoals):
 1. corres_underlying ?state_relation60 ?nf60 True ?r60 ?P60 ?P'60 ?f60 activateThread
 2. ?nf60 \<Longrightarrow> no_fail ?P60 ?f60
 3. \<And>s. ?P54 () s \<Longrightarrow> (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s \<and> (\<exists>sa. (sa, s) \<in> ?state_relation60 \<and> ?P60 sa \<and> ?P'60 s)
 4. {a. ?P'52 () a} \<subseteq> UNIV
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R43 rv) (?R'43 rv') (return tc) (return tc)
 6. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 7. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 8. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ?P54 a and ?Q53 a\<rbrace>
 9. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 10. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. False \<Longrightarrow> no_fail (invs and ct_in_state activatable) activate_thread
 2. \<And>s. ?P54 () s \<Longrightarrow> (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> (invs and ct_in_state activatable) sa \<and> (invs' and ct_in_state' activatable') s)
 3. {a. ?P'52 () a} \<subseteq> UNIV
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R43 rv) (?R'43 rv') (return tc) (return tc)
 5. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 6. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 7. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ?P54 a and ?Q53 a\<rbrace>
 8. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 9. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 10. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (9 subgoals):
 1. \<And>s. ?P54 () s \<Longrightarrow> (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> (invs and ct_in_state activatable) sa \<and> (invs' and ct_in_state' activatable') s)
 2. {a. ?P'52 () a} \<subseteq> UNIV
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R43 rv) (?R'43 rv') (return tc) (return tc)
 4. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 5. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 6. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. ?P54 a and ?Q53 a\<rbrace>
 7. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 8. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 9. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (8 subgoals):
 1. {a. ?P'52 () a} \<subseteq> UNIV
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R43 rv) (?R'43 rv') (return tc) (return tc)
 3. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 4. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 5. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. (\<lambda>a. ct_in_state' activatable' a \<and> sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> (\<exists>s. (s, a) \<in> state_relation \<and> invs s \<and> ct_in_state activatable s \<and> invs' a \<and> ct_in_state' activatable' a)) and ?Q53 a\<rbrace>
 6. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 7. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 8. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres_underlying rf_sr False False (=) (?R43 rv) (?R'43 rv') (return tc) (return tc)
 2. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 3. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 4. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. (\<lambda>a. ct_in_state' activatable' a \<and> sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> (\<exists>s. (s, a) \<in> state_relation \<and> invs s \<and> ct_in_state activatable s \<and> invs' a \<and> ct_in_state' activatable' a)) and ?Q53 a\<rbrace>
 5. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 6. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 7. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?Q53 ()\<rbrace> activateThread \<lbrace>?R43\<rbrace>
 2. \<lbrace>?Q'51 ()\<rbrace> exec_C \<Gamma> (com.Call activateThread_'proc) \<lbrace>?R'43\<rbrace>
 3. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. (\<lambda>a. ct_in_state' activatable' a \<and> sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> (\<exists>s. (s, a) \<in> state_relation \<and> invs s \<and> ct_in_state activatable s \<and> invs' a \<and> ct_in_state' activatable' a)) and ?Q53 a\<rbrace>
 4. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and ?Q'51 a\<rbrace>
 5. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 6. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>a. (\<lambda>a. ct_in_state' activatable' a \<and> sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> (\<exists>s. (s, a) \<in> state_relation \<and> invs s \<and> ct_in_state activatable s \<and> invs' a \<and> ct_in_state' activatable' a)) and (\<lambda>a. True)\<rbrace>
 2. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and (\<lambda>a. True)\<rbrace>
 3. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 4. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q30\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>r. ct_in_state' activatable' and invs' and ex_abs (invs and ct_in_state activatable)\<rbrace>
 2. \<And>rv s. (ct_in_state' activatable' and invs' and ex_abs (invs and ct_in_state activatable)) s \<Longrightarrow> ((\<lambda>a. ct_in_state' activatable' a \<and> sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> (\<exists>s. (s, a) \<in> state_relation \<and> invs s \<and> ct_in_state activatable s \<and> invs' a \<and> ct_in_state' activatable' a)) and (\<lambda>a. True)) s
 3. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and (\<lambda>a. True)\<rbrace>
 4. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and ?Q30) s
 5. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (6 subgoals):
 1. corres ?r75 ?S75 ?P'75 ?f75 ThreadDecls_H.schedule
 2. \<lbrace>?P75\<rbrace> ?f75 \<lbrace>\<lambda>rv. invs and ct_in_state activatable\<rbrace>
 3. \<And>rv s. (ct_in_state' activatable' and invs' and ex_abs (invs and ct_in_state activatable)) s \<Longrightarrow> ((\<lambda>a. ct_in_state' activatable' a \<and> sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> (\<exists>s. (s, a) \<in> state_relation \<and> invs s \<and> ct_in_state activatable s \<and> invs' a \<and> ct_in_state' activatable' a)) and (\<lambda>a. True)) s
 4. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and (\<lambda>a. True)\<rbrace>
 5. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and (\<lambda>s. invs' s \<and> invs' s \<and> (ex_abs (?P75 and ?S75) and ?P'75) s)) s
 6. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P75\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>rv. invs and ct_in_state activatable\<rbrace>
 2. \<And>rv s. (ct_in_state' activatable' and invs' and ex_abs (invs and ct_in_state activatable)) s \<Longrightarrow> ((\<lambda>a. ct_in_state' activatable' a \<and> sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> (\<exists>s. (s, a) \<in> state_relation \<and> invs s \<and> ct_in_state activatable s \<and> invs' a \<and> ct_in_state' activatable' a)) and (\<lambda>a. True)) s
 3. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and (\<lambda>a. True)\<rbrace>
 4. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and (\<lambda>s. invs' s \<and> invs' s \<and> (ex_abs (?P75 and (invs and valid_sched and valid_list)) and invs') s)) s
 5. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. (ct_in_state' activatable' and invs' and ex_abs (invs and ct_in_state activatable)) s \<Longrightarrow> ((\<lambda>a. ct_in_state' activatable' a \<and> sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> (\<exists>s. (s, a) \<in> state_relation \<and> invs s \<and> ct_in_state activatable s \<and> invs' a \<and> ct_in_state' activatable' a)) and (\<lambda>a. True)) s
 2. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and (\<lambda>a. True)\<rbrace>
 3. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and (\<lambda>s. invs' s \<and> invs' s \<and> (ex_abs ((\<lambda>s. invs s \<and> invs s) and (invs and valid_sched and valid_list)) and invs') s)) s
 4. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<lbrakk>ct_in_state' activatable' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule s = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; (sa, s) \<in> state_relation; invs sa; ct_in_state activatable sa\<rbrakk> \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> ct_in_state activatable sa
 2. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and (\<lambda>a. True)\<rbrace>
 3. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and (\<lambda>s. invs' s \<and> invs' s \<and> (ex_abs ((\<lambda>s. invs s \<and> invs s) and (invs and valid_sched and valid_list)) and invs') s)) s
 4. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>\<lambda>a. ?P'52 a and (\<lambda>a. True)\<rbrace>
 2. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and (\<lambda>s. invs' s \<and> invs' s \<and> (ex_abs ((\<lambda>s. invs s \<and> invs s) and (invs and valid_sched and valid_list)) and invs') s)) s
 3. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'30\<rbrace> exec_C \<Gamma> (com.Call schedule_'proc) \<lbrace>?P'52\<rbrace>
 2. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and (\<lambda>s. invs' s \<and> invs' s \<and> (ex_abs ((\<lambda>s. invs s \<and> invs s) and (invs and valid_sched and valid_list)) and invs') s)) s
 3. \<And>s. True \<Longrightarrow> (?P'30 and ?Q'30) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<Longrightarrow> ((\<lambda>s. invs' s \<and> (\<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_sched sa \<and> valid_list sa \<and> invs' s)) and (\<lambda>s. invs' s \<and> invs' s \<and> (ex_abs ((\<lambda>s. invs s \<and> invs s) and (invs and valid_sched and valid_list)) and invs') s)) s
 2. \<And>s. True \<Longrightarrow> (?P'30 and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!