theory ADT_IF_Refine

lemma haskell_invs:
  "global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop)
                         kernelCall_H_if handlePreemption_H_if
                         schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV" supply nonzero_gt_zero[simp] gt_zero_nonzero[simp] supply conj_cong[cong] apply (unfold_locales) apply (simp add: ADT_H_if_def) apply (simp_all add: checkActiveIRQ_H_if_def doUserOp_H_if_def
                                    kernelCall_H_if_def handlePreemption_H_if_def
                                    schedule'_H_if_def kernelExit_H_if_def split del: if_split)[12] apply (rule preserves_lifts | wp | simp add: full_invs_if'_def
                  | wp (once) hoare_vcg_disj_lift)+ apply (wp | wp (once) hoare_vcg_disj_lift hoare_drop_imps)+ apply simp apply (rule preserves_lifts) apply (simp add: full_invs_if'_def) apply (wp kernelEntry_if_valid_domain_time; simp) subgoal for e apply (rule preserves_lifts, simp add: full_invs_if'_def) apply wp apply (case_tac "e = Interrupt"; wpsimp wp: kernelEntry_if_valid_domain_time) apply fastforce+ done subgoal apply (rule preserves_lifts, simp add: full_invs_if'_def) apply (wp handlePreemption_if_valid_domain_time) apply fastforce done subgoal apply (rule preserves_lifts, simp add: full_invs_if'_def) apply (wp schedule'_if_valid_domain_time) apply fastforce done subgoal by (rule preserves_lifts, simp add: full_invs_if'_def)
                (wp, fastforce) apply (clarsimp simp: ADT_H_if_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV proof (prove)
goal (1 subgoal):
 1. global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV proof (prove)
goal (1 subgoal):
 1. global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV proof (prove)
goal (14 subgoals):
 1. Step (ADT_H_if uop) = (\<lambda>u. global_automaton_if checkActiveIRQ_H_if (doUserOp_H_if uop) kernelCall_H_if handlePreemption_H_if schedule'_H_if kernelExit_H_if \<inter> {(s, s'). s' \<in> UNIV})
 2. preserves InUserMode InUserMode full_invs_if' checkActiveIRQ_H_if
 3. preserves InIdleMode InIdleMode full_invs_if' checkActiveIRQ_H_if
 4. preserves InUserMode (KernelEntry Interrupt) full_invs_if' checkActiveIRQ_H_if
 5. preserves InIdleMode (KernelEntry Interrupt) full_invs_if' checkActiveIRQ_H_if
 6. preserves InUserMode InUserMode full_invs_if' (doUserOp_H_if uop)
 7. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if' (doUserOp_H_if uop)
 8. \<And>e. e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted full_invs_if' (kernelCall_H_if e)
 9. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' (kernelCall_H_if e)
 10. preserves KernelPreempted (KernelSchedule True) full_invs_if' handlePreemption_H_if
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. preserves InUserMode InUserMode full_invs_if' checkActiveIRQ_H_if
 2. preserves InIdleMode InIdleMode full_invs_if' checkActiveIRQ_H_if
 3. preserves InUserMode (KernelEntry Interrupt) full_invs_if' checkActiveIRQ_H_if
 4. preserves InIdleMode (KernelEntry Interrupt) full_invs_if' checkActiveIRQ_H_if
 5. preserves InUserMode InUserMode full_invs_if' (doUserOp_H_if uop)
 6. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if' (doUserOp_H_if uop)
 7. \<And>e. e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted full_invs_if' (kernelCall_H_if e)
 8. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' (kernelCall_H_if e)
 9. preserves KernelPreempted (KernelSchedule True) full_invs_if' handlePreemption_H_if
 10. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' schedule'_H_if
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. preserves InUserMode InUserMode full_invs_if' {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)}
 2. preserves InIdleMode InIdleMode full_invs_if' {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)}
 3. preserves InUserMode (KernelEntry Interrupt) full_invs_if' {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)}
 4. preserves InIdleMode (KernelEntry Interrupt) full_invs_if' {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)}
 5. preserves InUserMode InUserMode full_invs_if' {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_if uop a b)}
 6. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if' {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (doUserOp_if uop a b)}
 7. \<And>e. e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 8. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 9. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 10. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
A total of 13 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>e tc. \<lbrace>?P'172 e tc\<rbrace> doUserOp_if uop tc \<lbrace>\<lambda>rv s. (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and> (ct_running' s \<or> ct_idle' s) \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace>
 2. \<And>e tc s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<and> ct_running' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<and> ?P'172 e tc s
 3. \<And>e. e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 4. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 5. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 6. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 7. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 8. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 9. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>e tc s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<and> ct_running' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs einvs) s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<and> ct_running' s \<and> (ct_running' s \<or> ct_idle' s) \<and> ksSchedulerAction s = ResumeCurrentThread
 2. \<And>e. e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 3. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 4. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 5. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 6. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 7. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 8. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>e. e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 2. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 3. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 4. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 5. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 6. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 7. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>e tc. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. ((tc, s), KernelEntry e) \<in> full_invs_if'\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>tc' s'. ((snd tc', s'), KernelPreempted) \<in> full_invs_if'\<rbrace>
 2. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 3. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 4. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 5. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 6. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 7. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>e tc. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<and> ct_running' s \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>tc' s'. invs' s' \<and> ex_abs einvs s' \<and> arch_extras s' \<and> 0 < ksDomainTime s' \<and> valid_domain_list' s'\<rbrace>
 2. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 3. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 4. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 5. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 6. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 7. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 2. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 3. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 4. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 5. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 6. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (1 subgoal):
 1. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (kernelEntry_if e a b) \<and> ba = (r \<noteq> Inr ())} proof (prove)
goal (1 subgoal):
 1. \<And>tc. \<lbrace>\<lambda>s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and> (ct_running' s \<or> ct_idle' s) \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>tc' s'. invs' s' \<and> ex_abs einvs s' \<and> arch_extras s' \<and> (e \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s') \<and> (ksDomainTime s' = 0 \<longrightarrow> ksSchedulerAction s' = ChooseNewThread) \<and> valid_domain_list' s'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tc. \<lbrace>?P'25 tc\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>rv s. (e \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace>
 2. \<And>tc s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and> (ct_running' s \<or> ct_idle' s) \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras) s \<and> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and ex_abs einvs) s \<and> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras) s \<and> ?P'25 tc s proof (prove)
goal (1 subgoal):
 1. \<And>tc s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<and> (ct_running' s \<or> ct_idle' s) \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras) s \<and> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and arch_extras and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and ex_abs einvs) s \<and> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and arch_extras) s \<and> True proof (prove)
goal:
No subgoals! proof (prove)
goal (5 subgoals):
 1. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)}
 2. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 3. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 4. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 5. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (1 subgoal):
 1. preserves KernelPreempted (KernelSchedule True) full_invs_if' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handlePreemption_if x xa)} proof (prove)
goal (1 subgoal):
 1. \<And>tc. \<lbrace>\<lambda>s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>tc' s'. invs' s' \<and> ex_abs einvs s' \<and> arch_extras s' \<and> (ksDomainTime s' = 0 \<longrightarrow> ksSchedulerAction s' = ChooseNewThread) \<and> valid_domain_list' s'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tc s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> 0 < ksDomainTime s \<and> valid_domain_list' s \<Longrightarrow> invs' s \<and> (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s)) s \<and> arch_extras s \<and> True proof (prove)
goal:
No subgoals! proof (prove)
goal (4 subgoals):
 1. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)}
 2. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 3. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 4. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (1 subgoal):
 1. preserves (KernelSchedule b_) KernelExit full_invs_if' {(s, e, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> schedule'_if x xa)} proof (prove)
goal (1 subgoal):
 1. \<And>tc. \<lbrace>\<lambda>s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> (\<not> b_ \<longrightarrow> 0 < ksDomainTime s) \<and> (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace> schedule'_if tc \<lbrace>\<lambda>tc' s'. invs' s' \<and> ex_abs einvs s' \<and> arch_extras s' \<and> 0 < ksDomainTime s' \<and> valid_domain_list' s' \<and> (ct_running' s' \<or> ct_idle' s') \<and> ksSchedulerAction s' = ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tc s. invs' s \<and> ex_abs einvs s \<and> arch_extras s \<and> (\<not> b_ \<longrightarrow> 0 < ksDomainTime s) \<and> (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s \<Longrightarrow> invs' s \<and> (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) s \<and> (invs' and arch_extras) s \<and> True \<and> True \<and> invs' s \<and> invs' s proof (prove)
goal:
No subgoals! proof (prove)
goal (3 subgoals):
 1. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)}
 2. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 3. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal (1 subgoal):
 1. preserves' KernelExit full_invs_if' {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernelExit_if x xa) \<and> m = (if ct_running' (snd s') then InUserMode else InIdleMode)} proof (prove)
goal (2 subgoals):
 1. \<And>s. Init (ADT_H_if uop) s \<subseteq> full_invs_if'
 2. \<And>s. Init (ADT_H_if uop) s \<subseteq> UNIV proof (prove)
goal:
No subgoals!