theory Example_Valid_State

lemma Sys1_valid_initial_state_noenabled:
  assumes extras_s0: "step_restrict s0"
  assumes utf_det: "\<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s
                   \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})"
  assumes utf_non_empty: "\<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}"
  assumes utf_non_interrupt: "\<forall>t pl pr pxn tc ms e f g. (e,f,g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt"
  assumes det_inv_invariant: "invariant_over_ADT_if det_inv utf"
  assumes det_inv_s0: "det_inv KernelExit (cur_context s0_internal) s0_internal"
  shows "valid_initial_state_noenabled det_inv utf s0_internal Sys1PAS timer_irq s0_context" apply (unfold_locales, simp_all only: pasMaySendIrqs_Sys1PAS) apply (insert det_inv_invariant)[9] apply (erule(2) invariant_over_ADT_if.det_inv_abs_state) apply ((erule invariant_over_ADT_if.det_inv_abs_state
                                  invariant_over_ADT_if.check_active_irq_if_Idle_det_inv
                                  invariant_over_ADT_if.check_active_irq_if_User_det_inv
                                  invariant_over_ADT_if.do_user_op_if_det_inv
                                  invariant_over_ADT_if.handle_preemption_if_det_inv
                                  invariant_over_ADT_if.kernel_entry_if_Interrupt_det_inv
                                  invariant_over_ADT_if.kernel_entry_if_det_inv
                                  invariant_over_ADT_if.kernel_exit_if_det_inv
                                  invariant_over_ADT_if.schedule_if_det_inv)+)[8] apply (rule Sys1_pas_cur_domain) apply (rule Sys1_pas_wellformed_noninterference) apply (simp only: einvs_s0) apply (simp add: Sys1_current_subject_idemp) apply (simp add: only_timer_irq_inv_s0 silc_inv_s0 Sys1_pas_cur_domain
                           domain_sep_inv_s0 Sys1_pas_refined Sys1_guarded_pas_domain
                           idle_equiv_refl) apply (clarsimp simp: obj_valid_pdpt_kh0 valid_domain_list_2_def s0_internal_def exst0_def) apply (simp add: det_inv_s0) apply (simp add: s0_internal_def exst0_def) apply (simp add: ct_in_state_def st_tcb_at_tcb_states_of_state_eq
                        identity_eq[symmetric] tcb_states_of_state_s0) apply (simp add: s0_ptr_defs s0_internal_def) apply (simp add: s0_internal_def exst0_def) apply (rule utf_det) apply (rule utf_non_empty) apply (rule utf_non_interrupt) apply (simp add: extras_s0[simplified s0_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_initial_state_noenabled det_inv utf s0_internal Sys1PAS timer_irq s0_context proof (prove)
goal (20 subgoals):
 1. \<And>e tc s. \<lbrakk>valid_machine_state s; det_inv e tc s\<rbrakk> \<Longrightarrow> det_inv e tc (abs_state s)
 2. \<And>e tc. \<lbrace>einvs and det_inv (KernelEntry e) tc and ct_running and K (e \<noteq> Interrupt)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. case fst rv of Inl irq \<Rightarrow> det_inv KernelPreempted (cur_context s) s | Inr () \<Rightarrow> det_inv (KernelSchedule False) (cur_context s) s\<rbrace>
 3. \<And>tc. \<lbrace>einvs and det_inv (KernelEntry Interrupt) tc and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> kernel_entry_if Interrupt tc \<lbrace>\<lambda>rv s. case fst rv of Inl irq \<Rightarrow> det_inv KernelPreempted (cur_context s) s | Inr () \<Rightarrow> det_inv (KernelSchedule True) (cur_context s) s\<rbrace>
 4. \<And>tc. \<lbrace>einvs and (\<lambda>s. det_inv KernelPreempted (cur_context s) s)\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>rv s. det_inv (KernelSchedule True) (cur_context s) s\<rbrace>
 5. \<And>b tc. \<lbrace>einvs and (\<lambda>s. det_inv (KernelSchedule b) (cur_context s) s)\<rbrace> schedule_if tc \<lbrace>\<lambda>rv s. det_inv KernelExit (cur_context s) s\<rbrace>
 6. \<And>tc. \<lbrace>einvs and (\<lambda>s. det_inv KernelExit (cur_context s) s) and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>rv s. if ct_running s then det_inv InUserMode rv s else det_inv InIdleMode rv s\<rbrace>
 7. \<And>tc. \<lbrace>einvs and det_inv InUserMode tc and ct_running\<rbrace> do_user_op_if utf tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InUserMode (snd rv) | Some e \<Rightarrow> det_inv (KernelEntry e) (snd rv)\<rbrace>
 8. \<And>tc. \<lbrace>einvs and det_inv InUserMode tc and ct_running\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InUserMode (snd rv) | Some irq \<Rightarrow> det_inv (KernelEntry Interrupt) (snd rv)\<rbrace>
 9. \<And>tc. \<lbrace>einvs and det_inv InIdleMode tc and ct_idle\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InIdleMode (snd rv) | Some irq \<Rightarrow> det_inv (KernelEntry Interrupt) (snd rv)\<rbrace>
 10. pas_cur_domain Sys1PAS s0_internal
A total of 20 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>e tc s. \<lbrakk>valid_machine_state s; det_inv e tc s; invariant_over_ADT_if det_inv utf\<rbrakk> \<Longrightarrow> det_inv e tc (abs_state s)
 2. \<And>e tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry e) tc and ct_running and K (e \<noteq> Interrupt)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. case fst rv of Inl irq \<Rightarrow> det_inv KernelPreempted (cur_context s) s | Inr () \<Rightarrow> det_inv (KernelSchedule False) (cur_context s) s\<rbrace>
 3. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry Interrupt) tc and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> kernel_entry_if Interrupt tc \<lbrace>\<lambda>rv s. case fst rv of Inl irq \<Rightarrow> det_inv KernelPreempted (cur_context s) s | Inr () \<Rightarrow> det_inv (KernelSchedule True) (cur_context s) s\<rbrace>
 4. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and (\<lambda>s. det_inv KernelPreempted (cur_context s) s)\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>rv s. det_inv (KernelSchedule True) (cur_context s) s\<rbrace>
 5. \<And>b tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and (\<lambda>s. det_inv (KernelSchedule b) (cur_context s) s)\<rbrace> schedule_if tc \<lbrace>\<lambda>rv s. det_inv KernelExit (cur_context s) s\<rbrace>
 6. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and (\<lambda>s. det_inv KernelExit (cur_context s) s) and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>rv s. if ct_running s then det_inv InUserMode rv s else det_inv InIdleMode rv s\<rbrace>
 7. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv InUserMode tc and ct_running\<rbrace> do_user_op_if utf tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InUserMode (snd rv) | Some e \<Rightarrow> det_inv (KernelEntry e) (snd rv)\<rbrace>
 8. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv InUserMode tc and ct_running\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InUserMode (snd rv) | Some irq \<Rightarrow> det_inv (KernelEntry Interrupt) (snd rv)\<rbrace>
 9. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv InIdleMode tc and ct_idle\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InIdleMode (snd rv) | Some irq \<Rightarrow> det_inv (KernelEntry Interrupt) (snd rv)\<rbrace>
 10. pas_cur_domain Sys1PAS s0_internal
A total of 20 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>e tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry e) tc and ct_running and K (e \<noteq> Interrupt)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. case fst rv of Inl irq \<Rightarrow> det_inv KernelPreempted (cur_context s) s | Inr () \<Rightarrow> det_inv (KernelSchedule False) (cur_context s) s\<rbrace>
 2. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry Interrupt) tc and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> kernel_entry_if Interrupt tc \<lbrace>\<lambda>rv s. case fst rv of Inl irq \<Rightarrow> det_inv KernelPreempted (cur_context s) s | Inr () \<Rightarrow> det_inv (KernelSchedule True) (cur_context s) s\<rbrace>
 3. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and (\<lambda>s. det_inv KernelPreempted (cur_context s) s)\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>rv s. det_inv (KernelSchedule True) (cur_context s) s\<rbrace>
 4. \<And>b tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and (\<lambda>s. det_inv (KernelSchedule b) (cur_context s) s)\<rbrace> schedule_if tc \<lbrace>\<lambda>rv s. det_inv KernelExit (cur_context s) s\<rbrace>
 5. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and (\<lambda>s. det_inv KernelExit (cur_context s) s) and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> kernel_exit_if tc \<lbrace>\<lambda>rv s. if ct_running s then det_inv InUserMode rv s else det_inv InIdleMode rv s\<rbrace>
 6. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv InUserMode tc and ct_running\<rbrace> do_user_op_if utf tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InUserMode (snd rv) | Some e \<Rightarrow> det_inv (KernelEntry e) (snd rv)\<rbrace>
 7. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv InUserMode tc and ct_running\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InUserMode (snd rv) | Some irq \<Rightarrow> det_inv (KernelEntry Interrupt) (snd rv)\<rbrace>
 8. \<And>tc. invariant_over_ADT_if det_inv utf \<Longrightarrow> \<lbrace>einvs and det_inv InIdleMode tc and ct_idle\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>rv. case fst rv of None \<Rightarrow> det_inv InIdleMode (snd rv) | Some irq \<Rightarrow> det_inv (KernelEntry Interrupt) (snd rv)\<rbrace>
 9. pas_cur_domain Sys1PAS s0_internal
 10. pas_wellformed_noninterference Sys1PAS
A total of 19 subgoals... proof (prove)
goal (11 subgoals):
 1. pas_cur_domain Sys1PAS s0_internal
 2. pas_wellformed_noninterference Sys1PAS
 3. einvs s0_internal \<and> only_timer_irq_inv timer_irq s0_internal s0_internal \<and> silc_inv (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal s0_internal \<and> domain_sep_inv False s0_internal s0_internal \<and> pas_refined (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal \<and> guarded_pas_domain (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal \<and> idle_equiv s0_internal s0_internal \<and> valid_domain_list s0_internal \<and> valid_vspace_objs_if s0_internal
 4. det_inv KernelExit (cur_context s0_internal) s0_internal
 5. scheduler_action s0_internal = resume_cur_thread
 6. ct_running s0_internal \<or> ct_idle s0_internal
 7. 0 < domain_time s0_internal
 8. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 9. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 10. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. pas_wellformed_noninterference Sys1PAS
 2. einvs s0_internal \<and> only_timer_irq_inv timer_irq s0_internal s0_internal \<and> silc_inv (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal s0_internal \<and> domain_sep_inv False s0_internal s0_internal \<and> pas_refined (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal \<and> guarded_pas_domain (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal \<and> idle_equiv s0_internal s0_internal \<and> valid_domain_list s0_internal \<and> valid_vspace_objs_if s0_internal
 3. det_inv KernelExit (cur_context s0_internal) s0_internal
 4. scheduler_action s0_internal = resume_cur_thread
 5. ct_running s0_internal \<or> ct_idle s0_internal
 6. 0 < domain_time s0_internal
 7. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 8. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 9. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 10. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (9 subgoals):
 1. einvs s0_internal \<and> only_timer_irq_inv timer_irq s0_internal s0_internal \<and> silc_inv (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal s0_internal \<and> domain_sep_inv False s0_internal s0_internal \<and> pas_refined (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal \<and> guarded_pas_domain (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal \<and> idle_equiv s0_internal s0_internal \<and> valid_domain_list s0_internal \<and> valid_vspace_objs_if s0_internal
 2. det_inv KernelExit (cur_context s0_internal) s0_internal
 3. scheduler_action s0_internal = resume_cur_thread
 4. ct_running s0_internal \<or> ct_idle s0_internal
 5. 0 < domain_time s0_internal
 6. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 7. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 8. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 9. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (9 subgoals):
 1. True \<and> only_timer_irq_inv timer_irq s0_internal s0_internal \<and> silc_inv (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal s0_internal \<and> domain_sep_inv False s0_internal s0_internal \<and> pas_refined (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal \<and> guarded_pas_domain (Sys1PAS\<lparr>pasSubject := the_elem (pasDomainAbs Sys1PAS (cur_domain s0_internal))\<rparr>) s0_internal \<and> idle_equiv s0_internal s0_internal \<and> valid_domain_list s0_internal \<and> valid_vspace_objs_if s0_internal
 2. det_inv KernelExit (cur_context s0_internal) s0_internal
 3. scheduler_action s0_internal = resume_cur_thread
 4. ct_running s0_internal \<or> ct_idle s0_internal
 5. 0 < domain_time s0_internal
 6. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 7. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 8. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 9. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (9 subgoals):
 1. only_timer_irq_inv timer_irq s0_internal s0_internal \<and> silc_inv Sys1PAS s0_internal s0_internal \<and> domain_sep_inv False s0_internal s0_internal \<and> pas_refined Sys1PAS s0_internal \<and> guarded_pas_domain Sys1PAS s0_internal \<and> idle_equiv s0_internal s0_internal \<and> valid_domain_list s0_internal \<and> Ball (ran (kheap s0_internal)) obj_valid_pdpt
 2. det_inv KernelExit (cur_context s0_internal) s0_internal
 3. scheduler_action s0_internal = resume_cur_thread
 4. ct_running s0_internal \<or> ct_idle s0_internal
 5. 0 < domain_time s0_internal
 6. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 7. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 8. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 9. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (9 subgoals):
 1. valid_domain_list s0_internal \<and> Ball (ran (kheap s0_internal)) obj_valid_pdpt
 2. det_inv KernelExit (cur_context s0_internal) s0_internal
 3. scheduler_action s0_internal = resume_cur_thread
 4. ct_running s0_internal \<or> ct_idle s0_internal
 5. 0 < domain_time s0_internal
 6. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 7. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 8. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 9. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (8 subgoals):
 1. det_inv KernelExit (cur_context s0_internal) s0_internal
 2. scheduler_action s0_internal = resume_cur_thread
 3. ct_running s0_internal \<or> ct_idle s0_internal
 4. 0 < domain_time s0_internal
 5. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 6. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 7. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 8. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (7 subgoals):
 1. scheduler_action s0_internal = resume_cur_thread
 2. ct_running s0_internal \<or> ct_idle s0_internal
 3. 0 < domain_time s0_internal
 4. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 5. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 6. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 7. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (6 subgoals):
 1. ct_running s0_internal \<or> ct_idle s0_internal
 2. 0 < domain_time s0_internal
 3. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 4. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 5. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 6. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (6 subgoals):
 1. cur_thread s0_internal \<noteq> High_tcb_ptr \<and> (cur_thread s0_internal \<noteq> High_tcb_ptr \<longrightarrow> cur_thread s0_internal \<noteq> Low_tcb_ptr \<longrightarrow> cur_thread s0_internal = idle_tcb_ptr)
 2. 0 < domain_time s0_internal
 3. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 4. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 5. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 6. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (5 subgoals):
 1. 0 < domain_time s0_internal
 2. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 3. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 4. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 5. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (4 subgoals):
 1. \<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 2. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 3. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 4. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (3 subgoals):
 1. \<forall>t pl pr pxn tc ms. utf t pl pr pxn (tc, ms) \<noteq> {}
 2. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 3. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (2 subgoals):
 1. \<forall>t pl pr pxn tc ms e f g. (e, f, g) \<in> utf t pl pr pxn (tc, ms) \<longrightarrow> e \<noteq> Some Interrupt
 2. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal (1 subgoal):
 1. step_restrict ((if ct_idle s0_internal then idle_context s0_internal else s0_context, s0_internal), KernelExit) proof (prove)
goal:
No subgoals!