kings-crown/FVELER_Isabelle huggingface dataset:
theory Example_Valid_State

lemma cap_refs_in_kernel_window_s0[simp]:
  "cap_refs_in_kernel_window s0_internal" apply (clarsimp simp: cap_refs_in_kernel_window_def valid_refs_def cap_range_def
                        Invariants_AI.cte_wp_at_caps_of_state) apply (drule s0_caps_of_state) apply (erule disjE | simp add: arch_state0_def s0_internal_def s0_ptr_defs mask_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_refs_in_kernel_window s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. caps_of_state s0_internal (a, b) = Some cap \<Longrightarrow> {x. arm_kernel_vspace (arch_state s0_internal) x \<noteq> ArmVSpaceKernelWindow} \<inter> (untyped_range cap \<union> obj_refs cap) = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. cap = NullCap \<or> ((a, b), cap) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)} \<Longrightarrow> {x. arm_kernel_vspace (arch_state s0_internal) x \<noteq> ArmVSpaceKernelWindow} \<inter> (untyped_range cap \<union> obj_refs cap) = {} proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma cur_tcb_s0[simp]:
  "cur_tcb s0_internal" by (simp add: cur_tcb_def s0_ptr_defs s0_internal_def kh0_def kh0_obj_def obj_at_def is_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_tcb s0_internal
theory Example_Valid_State

lemma valid_list_s0[simp]:
  "valid_list s0_internal" apply (simp add: valid_list_2_def s0_internal_def exst0_def const_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list s0_internal proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma einvs_s0:
  "einvs s0_internal" apply (simp add: valid_state_def invs_def respects_device_trivial) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. einvs s0_internal proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma obj_valid_pdpt_kh0:
  "x \<in> ran kh0 \<Longrightarrow> obj_valid_pdpt x" by (auto simp: kh0_def valid_entries_def obj_valid_pdpt_def idle_tcb_def High_tcb_def Low_tcb_def
                 High_pt_def High_pt'_def entries_align_def Low_pt_def High_pd_def Low_pt'_def High_pd'_def
                 Low_pd_def irq_cnode_def ntfn_def Silc_cnode_def High_cnode_def Low_cnode_def Low_pd'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> ran kh0 \<Longrightarrow> obj_valid_pdpt x
theory ADT_IF_Refine

lemma kernel_entry_if_domain_time_inv:
  "\<lbrace>K (e \<noteq> Interrupt) and (\<lambda>s. P (domain_time s))\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_ s. P (domain_time s) \<rbrace>" unfolding kernel_entry_if_def by (wp handle_event_domain_time_inv) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (e \<noteq> Interrupt) and (\<lambda>s. P (domain_time s))\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (e \<noteq> Interrupt) and (\<lambda>s. P (domain_time s))\<rbrace> do t <- gets cur_thread;
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, tc)
od \<lbrace>\<lambda>_ s. P (domain_time s)\<rbrace>
theory ADT_IF_Refine

lemma kernel_entry_if_valid_domain_time:
  "\<lbrace>\<lambda>s. 0 < domain_time s\<rbrace>
   kernel_entry_if Interrupt tc
   \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>" unfolding kernel_entry_if_def apply (rule hoare_pre) apply (wp handle_interrupt_valid_domain_time
          | clarsimp | wpc)+
     \<comment> \<open>strengthen post of do_machine_op; we know interrupt occurred\<close> apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce) apply (wp+, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> kernel_entry_if Interrupt tc \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> do t <- gets cur_thread;
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event Interrupt;
return (r, tc)
od \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do t <- gets cur_thread;
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event Interrupt;
return (r, tc)
od \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 2. \<And>s. 0 < domain_time s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrace>?B5 t ()\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>x s. (x = None \<longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<and> ((\<exists>xa. x = Some xa) \<longrightarrow> 0 < domain_time s)\<rbrace>
 2. \<And>t. \<lbrace>?B4 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?B5 t\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B4\<rbrace>
 4. \<And>s. 0 < domain_time s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrace>?B5 t ()\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. \<And>t. \<lbrace>?B4 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?B5 t\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B4\<rbrace>
 4. \<And>s. 0 < domain_time s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma kernel_entry_if_no_preempt:
  "\<lbrace>\<top>\<rbrace> kernel_entry_if Interrupt ctx \<lbrace>\<lambda>(interrupt,_) _. interrupt = Inr ()\<rbrace>" unfolding kernel_entry_if_def by (wp | clarsimp intro!: validE_cases_valid)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> kernel_entry_if Interrupt ctx \<lbrace>\<lambda>(interrupt, uu_) _. interrupt = Inr ()\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do t <- gets cur_thread;
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set ctx (tcb_arch tcb)\<rparr>) t;
r <- handle_event Interrupt;
return (r, ctx)
od \<lbrace>\<lambda>(interrupt, uu_) _. interrupt = Inr ()\<rbrace>
theory ADT_IF_Refine

lemma kernelExit_inv[wp]:
  "kernelExit_if tc \<lbrace>P\<rbrace>" by (wpsimp simp: kernelExit_if_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. P\<rbrace>
theory ADT_IF_Refine

lemma corres_ex_abs_lift:
  "\<lbrakk> corres r S P' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<rbrakk>
     \<Longrightarrow> \<lbrace>ex_abs (P and S) and P'\<rbrace> f' \<lbrace>\<lambda>_. ex_abs Q\<rbrace>" by (fastforce simp: corres_underlying_def valid_def ex_abs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres r S P' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>ex_abs (P and S) and P'\<rbrace> f' \<lbrace>\<lambda>_. ex_abs Q\<rbrace>
theory ADT_IF_Refine

lemma empty_fail_select_bind: "empty_fail (assert (S \<noteq> {}) >>= (\<lambda>_. select S))" by (clarsimp simp: empty_fail_def select_def assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (do _ <- assert (S \<noteq> {});
select S
od)
theory ADT_IF_Refine

lemma corres_assert_imp_r:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> Q'; corres_underlying state_relation a b rr P Q f (g ()) \<rbrakk>
     \<Longrightarrow> corres_underlying state_relation a b rr P Q f (assert Q' >>= g)" by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s \<Longrightarrow> Q'; corres_underlying state_relation a b rr P Q f (g ())\<rbrakk> \<Longrightarrow> corres_underlying state_relation a b rr P Q f (assert Q' >>= g)
theory ADT_IF_Refine

lemma corres_return_same_trivial:
  "corres_underlying sr b c (=) \<top> \<top> (return a) (return a)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr b c (=) (\<lambda>_. True) (\<lambda>_. True) (return a) (return a)
theory ADT_IF_Refine

lemma corres_ex_abs_lift':
  "\<lbrakk> corres_underlying state_relation False False r S P' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<rbrakk>
     \<Longrightarrow> \<lbrace>ex_abs (P and S) and P'\<rbrace> f' \<lbrace>\<lambda>_. ex_abs Q\<rbrace>" by (fastforce simp: corres_underlying_def valid_def ex_abs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying state_relation False False r S P' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>ex_abs (P and S) and P'\<rbrace> f' \<lbrace>\<lambda>_. ex_abs Q\<rbrace>
theory ADT_IF_Refine

lemma getCurThread_corres':
  "corres_underlying state_relation nf nf' (=) \<top> \<top> (gets cur_thread) getCurThread" by (simp add: getCurThread_def curthread_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying state_relation nf nf' (=) (\<lambda>_. True) (\<lambda>_. True) (gets cur_thread) getCurThread
theory ADT_IF_Refine

lemma user_mem_corres':
  "corres_underlying state_relation nf nf' (=) invs invs'
                     (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))" by (clarsimp simp: gets_def get_def return_def bind_def invs_def invs'_def
                     corres_underlying_def user_mem_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying state_relation nf nf' (=) invs invs' (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))
theory ADT_IF_Refine

lemma corres_machine_op':
  assumes P: "corres_underlying Id nf nf' r P Q x x'"
  shows "corres_underlying state_relation nf nf' r (P \<circ> machine_state) (Q \<circ> ksMachineState)
                           (do_machine_op x) (doMachineOp x')" apply (rule corres_submonad3[OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) by (auto simp: state_relation_def swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying state_relation nf nf' r (P \<circ> machine_state) (Q \<circ> ksMachineState) (do_machine_op x) (doMachineOp x') proof (prove)
goal (4 subgoals):
 1. \<forall>s s'. (s, s') \<in> state_relation \<and> True \<and> True \<longrightarrow> (machine_state s, ksMachineState s') \<in> Id
 2. \<forall>s s' ss ss'. (s, s') \<in> state_relation \<and> (ss, ss') \<in> Id \<longrightarrow> ((machine_state_update \<circ> K) ss s, (ksMachineState_update \<circ> K) ss' s') \<in> state_relation
 3. \<forall>s. (P \<circ> machine_state) s \<longrightarrow> True \<and> P (machine_state s)
 4. \<forall>s'. (Q \<circ> ksMachineState) s' \<longrightarrow> True \<and> Q (ksMachineState s')
theory ADT_IF_Refine

lemma corres_assert':
  "corres_underlying sr nf False dc \<top> \<top> (assert P) (assert P)" by (clarsimp simp: corres_underlying_def assert_def return_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf False dc (\<lambda>_. True) (\<lambda>_. True) (assert P) (assert P)
theory ADT_IF_Refine

lemma doUserOp_if_ct_in_state[wp]:
  "doUserOp_if f tc \<lbrace>ct_in_state' st\<rbrace>" by (wpsimp wp: ct_in_state_thread_state_lift')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' st\<rbrace> doUserOp_if f tc \<lbrace>\<lambda>_. ct_in_state' st\<rbrace>
theory ADT_IF_Refine

lemma checkActiveIRQ_if_wp:
  "\<lbrace>\<lambda>s. P ((irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s))), tc)
          (s\<lparr>ksMachineState := (ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>)\<rparr>)\<rbrace>
   checkActiveIRQ_if tc
   \<lbrace>P\<rbrace>" by (simp add: checkActiveIRQ_if_def | wp dmo'_getActiveIRQ_wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s)), tc) (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>\<rparr>)\<rbrace> checkActiveIRQ_if tc \<lbrace>P\<rbrace>
theory ADT_IF_Refine

lemma checkActiveIRQ_ct_in_state[wp]:
  "checkActiveIRQ_if tc \<lbrace>ct_in_state' st\<rbrace>" by (wpsimp wp: checkActiveIRQ_if_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' st\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. ct_in_state' st\<rbrace>
theory ADT_IF_Refine

lemma checkActiveIRQ_schedact[wp]:
  "checkActiveIRQ_if tc \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>" by (wpsimp wp: checkActiveIRQ_if_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
theory ADT_IF_Refine

lemma checkActiveIRQ_ex_abs[wp]:
  "checkActiveIRQ_if tc \<lbrace>ex_abs (einvs)\<rbrace>" apply (rule hoare_pre) apply (rule corres_ex_abs_lift[OF check_active_irq_if_corres]) apply (rule check_active_irq_if_wp) apply (clarsimp simp: ex_abs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_abs einvs\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace>
 2. \<And>s. ex_abs einvs s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P3\<rbrace> check_active_irq_if tc \<lbrace>\<lambda>_. einvs\<rbrace>
 2. \<And>s. ex_abs einvs s \<Longrightarrow> (ex_abs (?P3 and (\<lambda>_. True)) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_abs einvs s \<Longrightarrow> (ex_abs ((\<lambda>s. einvs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := irq_state_of_state s + 1\<rparr>\<rparr>)) and (\<lambda>_. True)) and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma handlePreemption_invs'[wp]:
  "handlePreemption_if tc \<lbrace>invs'\<rbrace>" apply (simp add: handlePreemption_if_def) apply (wp dmo'_getActiveIRQ_wp hoare_drop_imps) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do irq <- doMachineOp (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handleInterrupt (the irq));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> (if \<exists>y. irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s)) = Some y then invs' else invs') (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma handlePreemption_ex_abs[wp]:
  "\<lbrace>invs' and ex_abs (einvs) and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s)\<rbrace>
   handlePreemption_if tc
   \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" apply (rule hoare_pre) apply (rule corres_ex_abs_lift[OF handle_preemption_if_corres]) apply (wp handle_preemption_if_invs) apply (auto simp: ex_abs_def domain_list_rel_eq domain_time_rel_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s)\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_. ex_abs einvs\<rbrace>
 2. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P3\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>_. einvs\<rbrace>
 2. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s)) s \<Longrightarrow> (ex_abs (?P3 and (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s))) and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ex_abs einvs and valid_domain_list' and (\<lambda>s. 0 < ksDomainTime s)) s \<Longrightarrow> (ex_abs ((\<lambda>s. invs s \<and> valid_list s \<and> (valid_sched and invs) s) and (einvs and valid_domain_list and (\<lambda>s. 0 < domain_time s))) and invs') s proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma handle_preemption_if_valid_domain_time:
  "\<lbrace>\<lambda>s. 0 < domain_time s \<rbrace>
   handle_preemption_if tc
   \<lbrace>\<lambda>r s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>" unfolding handle_preemption_if_def apply (rule hoare_pre) apply (wp handle_interrupt_valid_domain_time) apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce) apply (wp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>r s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < domain_time s\<rbrace> do irq <- do_machine_op (getActiveIRQ True);
when (irq \<noteq> None) $ handle_interrupt (the irq);
return tc
od \<lbrace>\<lambda>r s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do irq <- do_machine_op (getActiveIRQ True);
when (irq \<noteq> None) $ handle_interrupt (the irq);
return tc
od \<lbrace>\<lambda>r s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
 2. \<And>s. 0 < domain_time s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. if irq \<noteq> None then \<lambda>s. 0 < domain_time s else (\<lambda>a. domain_time a = 0 \<longrightarrow> scheduler_action a = choose_new_thread)\<rbrace>
 2. \<And>s. 0 < domain_time s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. \<And>s. 0 < domain_time s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma schedule_if'_invs'_post:
  "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. invs' and (ct_running' or ct_idle')\<rbrace>" apply (simp add: schedule'_if_def) apply (wp activate_invs' schedule_invs' schedule_sch_act_simple hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. invs' and (ct_running' or ct_idle')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do y <- ThreadDecls_H.schedule;
y <- activateThread;
y <- stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od \<lbrace>\<lambda>_. invs' and (ct_running' or ct_idle')\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma schedule_if'_invs'[wp]:
  "schedule'_if tc \<lbrace>invs'\<rbrace>" apply (rule hoare_post_imp[OF _ schedule_if'_invs'_post]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (invs' and (ct_running' or ct_idle')) s \<Longrightarrow> invs' s proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma schedule_if'_ct_running_or_idle[wp]:
  "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>r s. ct_running' s \<or> ct_idle' s\<rbrace>" apply (rule hoare_post_imp[OF _ schedule_if'_invs'_post]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>r s. ct_running' s \<or> ct_idle' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (invs' and (ct_running' or ct_idle')) s \<Longrightarrow> ct_running' s \<or> ct_idle' s proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma nonzero_gt_zero:
  "x \<noteq> (0 :: obj_ref) \<Longrightarrow> x > 0" by (simp add: word_gt_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 < x
theory ADT_IF_Refine

lemma gt_zero_nonzero:
  "(0 :: obj_ref) < x \<Longrightarrow> x \<noteq> 0" by (simp add: word_gt_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> x \<noteq> 0
theory ADT_IF_Refine

lemma preservesE:
  assumes preserves: "preserves mode mode' P f"
  assumes inf: "(s,e,s') \<in> f"
  assumes P: "(s,mode) \<in> P"
  assumes a: "(s',mode') \<in> P \<Longrightarrow> Q"
  shows "Q" apply (rule a) apply (insert preserves inf P) apply (clarsimp simp: preserves_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q proof (prove)
goal (1 subgoal):
 1. (s', mode') \<in> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preserves mode mode' P f; (s, e, s') \<in> f; (s, mode) \<in> P\<rbrakk> \<Longrightarrow> (s', mode') \<in> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>f. case x of (s, e, s') \<Rightarrow> (s, mode) \<in> P \<longrightarrow> (s', mode') \<in> P; (s, e, s') \<in> f; (s, mode) \<in> P\<rbrakk> \<Longrightarrow> (s', mode') \<in> P proof (prove)
goal:
No subgoals!