theory ADT_IF_Refine

lemma abstract_invs:
  "global_automaton_invs check_active_irq_A_if (do_user_op_A_if uop)
                         kernel_call_A_if kernel_handle_preemption_if
                         kernel_schedule_if kernel_exit_A_if
                         (full_invs_if) (ADT_A_if uop) {s. step_restrict s}" supply nonzero_gt_zero[simp] gt_zero_nonzero[simp] supply conj_cong[cong] apply (unfold_locales) apply (simp add: ADT_A_if_def) apply (simp_all add: check_active_irq_A_if_def do_user_op_A_if_def
                                   kernel_call_A_if_def kernel_handle_preemption_if_def
                                   kernel_schedule_if_def kernel_exit_A_if_def
                              del: unit_Inl_or_Inr(2) split del: if_split)[12] apply (rule preserves_lifts |
                     wp check_active_irq_if_wp do_user_op_if_invs
                    | clarsimp simp add: full_invs_if_def)+ apply (rule_tac Q="\<lambda>r s'. (invs and ct_running) s' \<and>
                   valid_list s' \<and>
                   valid_sched s' \<and> scheduler_action s' = resume_cur_thread \<and>
                   valid_domain_list s' \<and>
                   (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread)" in hoare_post_imp) apply (clarsimp) apply (wp do_user_op_if_invs hoare_vcg_imp_lift) apply clarsimp+ apply (rule preserves_lifts) apply (simp add: full_invs_if_def) apply (rule_tac Q="\<lambda>r s'. (invs and ct_running) s' \<and>
                  valid_list s' \<and>
                   valid_domain_list s' \<and>
                  domain_time s' \<noteq> 0 \<and>
                  valid_sched s' \<and> scheduler_action s' = resume_cur_thread" in hoare_post_imp) apply (clarsimp simp: active_from_running) apply (wp do_user_op_if_invs kernel_entry_if_invs kernel_entry_if_valid_sched ; clarsimp) 
        (* KernelEntry \<rightarrow> KernelPreempted *)
         apply (rule preserves_lifts, simp add: full_invs_if_def) subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched
                        kernel_entry_if_domain_time_inv
                     ; clarsimp simp: active_from_running) 

       (* KernelEntry \<rightarrow> KernelSchedule (e = Interrupt) *)
        apply (rule preserves_lifts, simp add: full_invs_if_def) apply (case_tac "e = Interrupt") subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched kernel_entry_if_valid_domain_time
                     | clarsimp simp: active_from_running)+ apply (clarsimp simp: conj_left_commute) subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched kernel_entry_if_domain_time_inv
                    ; clarsimp simp: active_from_running) 
      (* KernelPreempted \<rightarrow> KernelSchedule True *)
       apply (rule preserves_lifts, simp add: full_invs_if_def) subgoal for tc apply (rule hoare_pre) apply (wp handle_preemption_if_invs) apply (wp handle_preemption_if_valid_domain_time) apply clarsimp done 
     (* KernelSchedule \<rightarrow> KernelExit *)
      apply (rule preserves_lifts, simp add: full_invs_if_def) subgoal by (rule hoare_pre, wp schedule_if_domain_time_left, fastforce) 
    (* KernelExit \<rightarrow> InUserMode \<or> InIdleMode *)
     apply (rule preserves_lifts, simp add: full_invs_if_def) subgoal by (clarsimp cong: conj_cong | wp)+ apply (fastforce simp: full_invs_if_def ADT_A_if_def step_restrict_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_automaton_invs check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. global_automaton_invs check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. global_automaton_invs check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if full_invs_if (ADT_A_if uop) {s. step_restrict s} proof (prove)
goal (14 subgoals):
 1. Step (ADT_A_if uop) = (\<lambda>u. global_automaton_if check_active_irq_A_if (do_user_op_A_if uop) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, s'). s' \<in> {s. step_restrict s}})
 2. preserves InUserMode InUserMode full_invs_if check_active_irq_A_if
 3. preserves InIdleMode InIdleMode full_invs_if check_active_irq_A_if
 4. preserves InUserMode (KernelEntry Interrupt) full_invs_if check_active_irq_A_if
 5. preserves InIdleMode (KernelEntry Interrupt) full_invs_if check_active_irq_A_if
 6. preserves InUserMode InUserMode full_invs_if (do_user_op_A_if uop)
 7. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if (do_user_op_A_if uop)
 8. \<And>e. e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted full_invs_if (kernel_call_A_if e)
 9. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if (kernel_call_A_if e)
 10. preserves KernelPreempted (KernelSchedule True) full_invs_if kernel_handle_preemption_if
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. preserves InUserMode InUserMode full_invs_if check_active_irq_A_if
 2. preserves InIdleMode InIdleMode full_invs_if check_active_irq_A_if
 3. preserves InUserMode (KernelEntry Interrupt) full_invs_if check_active_irq_A_if
 4. preserves InIdleMode (KernelEntry Interrupt) full_invs_if check_active_irq_A_if
 5. preserves InUserMode InUserMode full_invs_if (do_user_op_A_if uop)
 6. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if (do_user_op_A_if uop)
 7. \<And>e. e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted full_invs_if (kernel_call_A_if e)
 8. \<And>e. preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) full_invs_if (kernel_call_A_if e)
 9. preserves KernelPreempted (KernelSchedule True) full_invs_if kernel_handle_preemption_if
 10. \<And>b. preserves (KernelSchedule b) KernelExit full_invs_if kernel_schedule_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 (check_active_irq_if tc s)}
 2. preserves InIdleMode InIdleMode full_invs_if {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (check_active_irq_if tc s)}
 3. preserves InUserMode (KernelEntry Interrupt) full_invs_if {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (check_active_irq_if tc s)}
 4. preserves InIdleMode (KernelEntry Interrupt) full_invs_if {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (check_active_irq_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 (do_user_op_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 (do_user_op_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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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>tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> ct_running s' \<and> scheduler_action s' = resume_cur_thread\<rbrace>
 2. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (do_user_op_if uop a b)}
 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 8. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 9. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (10 subgoals):
 1. \<And>tc rv s. (invs and ct_running) s \<and> valid_list s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread \<and> valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<Longrightarrow> invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread
 2. \<And>tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>r s'. (invs and ct_running) s' \<and> valid_list s' \<and> valid_sched s' \<and> scheduler_action s' = resume_cur_thread \<and> valid_domain_list s' \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread)\<rbrace>
 3. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (do_user_op_if uop a b)}
 4. \<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 (kernel_entry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 5. \<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 (kernel_entry_if e a b) \<and> ba = (r \<noteq> Inr ())}
 6. preserves KernelPreempted (KernelSchedule True) full_invs_if {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handle_preemption_if x xa)}
 7. \<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)}
 8. preserves' KernelExit full_invs_if {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 9. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 10. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (9 subgoals):
 1. \<And>tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>r s'. (invs and ct_running) s' \<and> valid_list s' \<and> valid_sched s' \<and> scheduler_action s' = resume_cur_thread \<and> valid_domain_list s' \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread)\<rbrace>
 2. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (do_user_op_if uop a b)}
 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 8. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 9. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (9 subgoals):
 1. \<And>tc s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread \<Longrightarrow> (invs and ct_running) s \<and> valid_list s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread \<and> valid_domain_list s \<and> (domain_time s \<noteq> 0 \<or> scheduler_action s = choose_new_thread)
 2. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (do_user_op_if uop a b)}
 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 8. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 9. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (8 subgoals):
 1. \<And>e. preserves InUserMode (KernelEntry e) full_invs_if {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (do_user_op_if uop a b)}
 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 7. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 8. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (8 subgoals):
 1. \<And>e tc. \<lbrace>\<lambda>s. ((tc, s), InUserMode) \<in> full_invs_if\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>tc' s'. ((snd tc', s'), KernelEntry e) \<in> full_invs_if\<rbrace>
 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 7. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 8. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (8 subgoals):
 1. \<And>e tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s') \<and> (ct_running s' \<or> ct_idle s') \<and> scheduler_action s' = resume_cur_thread\<rbrace>
 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 7. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 8. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (9 subgoals):
 1. \<And>e tc rv s. (invs and ct_running) s \<and> valid_list s \<and> valid_domain_list s \<and> domain_time s \<noteq> 0 \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread \<Longrightarrow> invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread
 2. \<And>e tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>r s'. (invs and ct_running) s' \<and> valid_list s' \<and> valid_domain_list s' \<and> domain_time s' \<noteq> 0 \<and> valid_sched s' \<and> scheduler_action s' = resume_cur_thread\<rbrace>
 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 8. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 9. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (8 subgoals):
 1. \<And>e tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread\<rbrace> do_user_op_if uop tc \<lbrace>\<lambda>r s'. (invs and ct_running) s' \<and> valid_list s' \<and> valid_domain_list s' \<and> domain_time s' \<noteq> 0 \<and> valid_sched s' \<and> scheduler_action s' = resume_cur_thread\<rbrace>
 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 7. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 8. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 7. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} 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 (kernel_entry_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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 7. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (7 subgoals):
 1. \<And>e tc. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> 0 < domain_time 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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 7. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. e_ \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> ct_running s \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e_ tc_ \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> 0 < domain_time s' \<and> valid_domain_list s'\<rbrace> 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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 5. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} 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 (kernel_entry_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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 5. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (6 subgoals):
 1. \<And>e tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (e \<noteq> Interrupt \<longrightarrow> 0 < domain_time s') \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread) \<and> valid_domain_list s'\<rbrace>
 2. preserves KernelPreempted (KernelSchedule True) full_invs_if {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 5. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (7 subgoals):
 1. \<And>e tc. e = Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (e \<noteq> Interrupt \<longrightarrow> 0 < domain_time s') \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread) \<and> valid_domain_list s'\<rbrace>
 2. \<And>e tc. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (e \<noteq> Interrupt \<longrightarrow> 0 < domain_time s') \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread) \<and> valid_domain_list s'\<rbrace>
 3. preserves KernelPreempted (KernelSchedule True) full_invs_if {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 7. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. e_ = Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> (e_ \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e_ tc_ \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (e_ \<noteq> Interrupt \<longrightarrow> 0 < domain_time s') \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread) \<and> valid_domain_list s'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>e tc. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> (ct_running s \<or> ct_idle s) \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (e \<noteq> Interrupt \<longrightarrow> 0 < domain_time s') \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread) \<and> valid_domain_list s'\<rbrace>
 2. preserves KernelPreempted (KernelSchedule True) full_invs_if {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 5. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (6 subgoals):
 1. \<And>e tc. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> valid_domain_list s \<and> 0 < domain_time s \<and> valid_list s \<and> ct_running s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>tc' s'. invs s' \<and> 0 < domain_time s' \<and> valid_list s' \<and> valid_sched s' \<and> valid_domain_list s'\<rbrace>
 2. preserves KernelPreempted (KernelSchedule True) full_invs_if {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 5. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 6. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. e_ \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. invs s \<and> valid_domain_list s \<and> 0 < domain_time s \<and> valid_list s \<and> ct_running s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread\<rbrace> kernel_entry_if e_ tc_ \<lbrace>\<lambda>tc' s'. invs s' \<and> 0 < domain_time s' \<and> valid_list s' \<and> valid_sched s' \<and> valid_domain_list s'\<rbrace> 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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 4. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 5. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} 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> handle_preemption_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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 4. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 5. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (5 subgoals):
 1. \<And>tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread) \<and> valid_domain_list s'\<rbrace>
 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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 4. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 5. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread) \<and> valid_domain_list s'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched s' \<and> (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread) \<and> valid_domain_list s'\<rbrace>
 2. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'8\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>rv s. (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> valid_domain_list s\<rbrace>
 2. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<Longrightarrow> invs s \<and> valid_list s \<and> (valid_sched and invs) s \<and> ?P'8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> 0 < domain_time s \<and> valid_domain_list s \<Longrightarrow> invs s \<and> valid_list s \<and> (valid_sched and invs) s \<and> 0 < domain_time s \<and> valid_domain_list s 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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 3. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 4. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} 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> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 3. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 4. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (4 subgoals):
 1. \<And>b tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> (\<not> b \<longrightarrow> 0 < domain_time s) \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> valid_domain_list s\<rbrace> schedule_if tc \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched 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\<rbrace>
 2. preserves' KernelExit full_invs_if {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 3. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 4. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> (\<not> b_ \<longrightarrow> 0 < domain_time s) \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> valid_domain_list s\<rbrace> schedule_if tc_ \<lbrace>\<lambda>tc' s'. invs s' \<and> valid_list s' \<and> valid_sched 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\<rbrace> proof (prove)
goal (3 subgoals):
 1. preserves' KernelExit full_invs_if {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 2. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 3. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (3 subgoals):
 1. preserves' KernelExit full_invs_if {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> kernel_exit_if x xa) \<and> m = (if ct_running (snd s') then InUserMode else InIdleMode)}
 2. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 3. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (3 subgoals):
 1. \<And>tc. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched 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\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>tc' s'. (ct_running s' \<longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread) \<and> (\<not> ct_running s' \<longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> ct_idle s' \<and> scheduler_action s' = resume_cur_thread)\<rbrace>
 2. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 3. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> valid_list s \<and> valid_sched 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\<rbrace> kernel_exit_if tc_ \<lbrace>\<lambda>tc' s'. (ct_running s' \<longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> scheduler_action s' = resume_cur_thread) \<and> (\<not> ct_running s' \<longrightarrow> invs s' \<and> valid_list s' \<and> valid_sched s' \<and> 0 < domain_time s' \<and> valid_domain_list s' \<and> ct_idle s' \<and> scheduler_action s' = resume_cur_thread)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. Init (ADT_A_if uop) s \<subseteq> full_invs_if
 2. \<And>s. Init (ADT_A_if uop) s \<subseteq> {s. step_restrict s} proof (prove)
goal:
No subgoals!