kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF

lemma kernel_exit_irq_masks[wp]:
  "\<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> kernel_exit_if uc \<lbrace>\<lambda>r s. P (irq_masks_of_state s)\<rbrace>" apply (simp add: kernel_exit_if_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> kernel_exit_if uc \<lbrace>\<lambda>r s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace> gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch) \<lbrace>\<lambda>r s. P (irq_masks_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma invs_if_irq_is_recurring[simp]:
  "invs_if s \<Longrightarrow> irq_is_recurring timer_irq (internal_state_if s)" by (clarsimp simp: invs_if_def Invs_def only_timer_irq_inv_def only_timer_irq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs_if s \<Longrightarrow> irq_is_recurring timer_irq (internal_state_if s)
theory ADT_IF

lemma tranclp_s0:
  "big_step_R\<^sup>*\<^sup>* s0 s \<Longrightarrow> interrupted_modes (snd s) \<or> (snd s) = KernelExit" apply (simp only: rtranclp_def2) apply (erule disjE) apply (induct rule: tranclp.induct) apply (auto simp: big_step_R_def s0_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. big_step_R\<^sup>*\<^sup>* s0 s \<Longrightarrow> interrupted_modes (snd s) \<or> snd s = KernelExit proof (prove)
goal (1 subgoal):
 1. big_step_R\<^sup>+\<^sup>+ s0 s \<or> s = s0 \<Longrightarrow> interrupted_modes (snd s) \<or> snd s = KernelExit proof (prove)
goal (2 subgoals):
 1. big_step_R\<^sup>+\<^sup>+ s0 s \<Longrightarrow> interrupted_modes (snd s) \<or> snd s = KernelExit
 2. s = s0 \<Longrightarrow> interrupted_modes (snd s) \<or> snd s = KernelExit proof (prove)
goal (3 subgoals):
 1. \<And>a b. big_step_R a b \<Longrightarrow> interrupted_modes (snd b) \<or> snd b = KernelExit
 2. \<And>a b c. \<lbrakk>big_step_R\<^sup>+\<^sup>+ a b; interrupted_modes (snd b) \<or> snd b = KernelExit; big_step_R b c\<rbrakk> \<Longrightarrow> interrupted_modes (snd c) \<or> snd c = KernelExit
 3. s = s0 \<Longrightarrow> interrupted_modes (snd s) \<or> snd s = KernelExit proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma rah_simp:
  "(\<forall>b. b) = False" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>b. b) = False
theory ADT_IF

lemma invs_if_domain_sep_invs[intro]:
  "invs_if ((a,s),b) \<Longrightarrow> domain_sep_inv False s0_internal s" by (simp add: invs_if_def Invs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs_if ((a, s), b) \<Longrightarrow> domain_sep_inv False s0_internal s
theory ADT_IF

lemma invs_if_invs[intro]:
  "invs_if ((a,s),b) \<Longrightarrow> invs s" by (simp add: invs_if_def Invs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs_if ((a, s), b) \<Longrightarrow> invs s
theory ADT_IF

lemma steps_preserves_equivalence:
  "\<lbrakk> (s', as) \<in> sub_big_steps A R s1; \<forall>t t' as a. (t, as) \<in> sub_big_steps A R s1
                                                  \<longrightarrow> (t, t') \<in> Step A a
                                                  \<longrightarrow> \<not> R s1 t'
                                                  \<longrightarrow> f t = f t' \<rbrakk>
     \<Longrightarrow> f s1 = f s'" by (fastforce elim: sub_big_steps.induct)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps A R s1; \<forall>t t' as a. (t, as) \<in> sub_big_steps A R s1 \<longrightarrow> (t, t') \<in> Step A a \<longrightarrow> \<not> R s1 t' \<longrightarrow> f t = f t'\<rbrakk> \<Longrightarrow> f s1 = f s'
theory ADT_IF

lemma step_out_equivalent:
  "\<lbrakk> (s', as) \<in> sub_big_steps A R s1; (s', s2) \<in> data_type.Step A a; g s2 = f (g s');
     \<forall>t t' as a. (t, as) \<in> sub_big_steps A R s1
                 \<longrightarrow> (t, t') \<in> data_type.Step A a
                 \<longrightarrow> \<not> R s1 t'
                 \<longrightarrow> f (g t) = f (g t') \<rbrakk>
     \<Longrightarrow> f (g s1) = g s2" by (fastforce elim: steps_preserves_equivalence)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps A R s1; (s', s2) \<in> Step A a; g s2 = f (g s'); \<forall>t t' as a. (t, as) \<in> sub_big_steps A R s1 \<longrightarrow> (t, t') \<in> Step A a \<longrightarrow> \<not> R s1 t' \<longrightarrow> f (g t) = f (g t')\<rbrakk> \<Longrightarrow> f (g s1) = g s2
theory ADT_IF

lemma irq_state_back:
  "P (irq_state_of_state (internal_state_if ((a,b),c)))
     (irq_masks_of_state (internal_state_if ((a,b),c))) \<Longrightarrow>
   P (irq_state_of_state b) (irq_masks_of_state b)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (irq_state_of_state (internal_state_if ((a, b), c))) (irq_masks_of_state (internal_state_if ((a, b), c))) \<Longrightarrow> P (irq_state_of_state b) (irq_masks_of_state b)
theory ADT_IF

lemma sub_big_steps_not_related:
  "(s,a) \<in> sub_big_steps A R s1 \<Longrightarrow> \<not> R s1 s" by (erule sub_big_steps.cases,simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, a) \<in> sub_big_steps A R s1 \<Longrightarrow> \<not> R s1 s
theory ADT_IF

lemma small_step_to_big_step:
  assumes a:
    "\<And>s' evs. \<lbrakk> (s',evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1;
                (s', s2) \<in> data_type.Step (ADT_A_if utf) a; big_step_R s1 s2 \<rbrakk>
                \<Longrightarrow> S"
  assumes b: "(s1, s2) \<in> data_type.Step (big_step_ADT_A_if utf) a"
  shows S apply (insert b) apply (simp add: big_step_ADT_A_if_def big_step_adt_def) apply (erule big_steps.cases) apply (rule_tac s'=s' and evs=as in a) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S proof (prove)
goal (1 subgoal):
 1. (s1, s2) \<in> Step (big_step_ADT_A_if utf) a \<Longrightarrow> S proof (prove)
goal (1 subgoal):
 1. (s1, s2) \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap () \<Longrightarrow> S proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t a. \<lbrakk>s1 = s; s2 = t; (s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a])\<rbrakk> \<Longrightarrow> S proof (prove)
goal (3 subgoals):
 1. \<And>s' as s t a. \<lbrakk>s1 = s; s2 = t; (s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a])\<rbrakk> \<Longrightarrow> (s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s1
 2. \<And>s' as s t aa. \<lbrakk>s1 = s; s2 = t; (s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> Step (ADT_A_if utf) aa; big_step_R s t; () = big_step_evmap (as @ [aa])\<rbrakk> \<Longrightarrow> (s', s2) \<in> Step (ADT_A_if utf) a
 3. \<And>s' as s t a. \<lbrakk>s1 = s; s2 = t; (s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> Step (ADT_A_if utf) a; big_step_R s t; () = big_step_evmap (as @ [a])\<rbrakk> \<Longrightarrow> big_step_R s1 s2 proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma Step_ADT_A_if_def_global_automaton_if:
  "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, y). step_restrict y})" by (clarsimp simp: ADT_A_if_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 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, y). step_restrict y})
theory ADT_IF

lemma ADT_A_if_reachable_step_restrict:
  "system.reachable (ADT_A_if utf) s0 s \<Longrightarrow> step_restrict s" apply (clarsimp simp: system.reachable_def) apply (erule execution_restrict) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. system.reachable (ADT_A_if utf) s0 s \<Longrightarrow> step_restrict s proof (prove)
goal (1 subgoal):
 1. \<And>js. s \<in> execution (ADT_A_if utf) s0 js \<Longrightarrow> step_restrict s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma step_restrict_inv_holds_ADT_A_if:
  "ADT_A_if utf [> {s. step_restrict s}" apply (rule inv_holdsI) apply (clarsimp simp: Image_def ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_A_if utf [> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step (ADT_A_if utf) j `` {s. step_restrict s} \<subseteq> {s. step_restrict s} proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma invs_if_sub_big_steps_ADT_A_if:
  "\<lbrakk> (s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; invs_if s \<rbrakk>
     \<Longrightarrow> invs_if s'" apply (erule sub_big_steps.induct) apply simp apply (simp add: invs_if_Step_ADT_A_if) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', evs) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; invs_if s\<rbrakk> \<Longrightarrow> invs_if s' proof (prove)
goal (2 subgoals):
 1. \<And>evlist t. \<lbrakk>invs_if s; evlist = []; t = s; \<not> big_step_R s s\<rbrakk> \<Longrightarrow> invs_if t
 2. \<And>evlist evlist' e s' t. \<lbrakk>invs_if s; evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; invs_if s'; (s', t) \<in> Step (ADT_A_if utf) e; \<not> big_step_R s t\<rbrakk> \<Longrightarrow> invs_if t proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' e s' t. \<lbrakk>invs_if s; evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps (ADT_A_if utf) big_step_R s; invs_if s'; (s', t) \<in> Step (ADT_A_if utf) e; \<not> big_step_R s t\<rbrakk> \<Longrightarrow> invs_if t proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma big_step_irq_state_next_irq:
  "\<lbrakk> invs_if s1; big_step_R\<^sup>*\<^sup>* s0 s1; (s1, s2) \<in> Step (big_step_ADT_A_if utf) a;
     snd s1 = KernelExit; i_s1 = internal_state_if s1; i_s2 = internal_state_if s2 \<rbrakk>
     \<Longrightarrow> next_irq_state_of_state i_s1 = irq_state_of_state i_s2" apply simp apply (rule small_step_to_big_step) apply (rule small_step_irq_state_next_irq,(simp add: big_step_R_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs_if s1; big_step_R\<^sup>*\<^sup>* s0 s1; (s1, s2) \<in> Step (big_step_ADT_A_if utf) a; snd s1 = KernelExit; i_s1 = internal_state_if s1; i_s2 = internal_state_if s2\<rbrakk> \<Longrightarrow> next_irq_state_of_state i_s1 = irq_state_of_state i_s2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs_if s1; big_step_R\<^sup>*\<^sup>* s0 s1; (s1, s2) \<in> Step (big_step_ADT_A_if utf) (); snd s1 = KernelExit; i_s1 = internal_state_if s1; i_s2 = internal_state_if s2\<rbrakk> \<Longrightarrow> next_irq_state_of_state (internal_state_if s1) = irq_state_of_state (internal_state_if s2) proof (prove)
goal (2 subgoals):
 1. \<And>s' evs. \<lbrakk>invs_if s1; big_step_R\<^sup>*\<^sup>* s0 s1; (s1, s2) \<in> Step (big_step_ADT_A_if utf) (); snd s1 = KernelExit; i_s1 = internal_state_if s1; i_s2 = internal_state_if s2; (s', evs) \<in> sub_big_steps (ADT_A_if ?utf1) big_step_R ?s1.1; (s', ?s2.1) \<in> Step (ADT_A_if ?utf1) ?a1; big_step_R ?s1.1 ?s2.1\<rbrakk> \<Longrightarrow> next_irq_state_of_state (internal_state_if s1) = irq_state_of_state (internal_state_if s2)
 2. \<lbrakk>invs_if s1; big_step_R\<^sup>*\<^sup>* s0 s1; (s1, s2) \<in> Step (big_step_ADT_A_if utf) (); snd s1 = KernelExit; i_s1 = internal_state_if s1; i_s2 = internal_state_if s2\<rbrakk> \<Longrightarrow> (?s1.1, ?s2.1) \<in> Step (big_step_ADT_A_if ?utf1) ?a1 proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma ADT_A_if_Init_inv_Fin:
  "Init_inv_Fin_system (ADT_A_if utf) s0" apply unfold_locales apply (simp add: ADT_A_if_def invs_if_full_invs_if extras_s0) apply (frule ADT_A_if_reachable_invs_if) apply (drule ADT_A_if_reachable_step_restrict) apply (simp add: ADT_A_if_def invs_if_full_invs_if) apply (simp add: ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system (ADT_A_if utf) s0 proof (prove)
goal (3 subgoals):
 1. s0 \<in> Fin (ADT_A_if utf) ` Init (ADT_A_if utf) s0
 2. \<And>s. system.reachable (ADT_A_if utf) s0 s \<Longrightarrow> Init (ADT_A_if utf) s = {s'. Fin (ADT_A_if utf) s' = s}
 3. inj (Fin (ADT_A_if utf)) proof (prove)
goal (2 subgoals):
 1. \<And>s. system.reachable (ADT_A_if utf) s0 s \<Longrightarrow> Init (ADT_A_if utf) s = {s'. Fin (ADT_A_if utf) s' = s}
 2. inj (Fin (ADT_A_if utf)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>system.reachable (ADT_A_if utf) s0 s; invs_if s\<rbrakk> \<Longrightarrow> Init (ADT_A_if utf) s = {s'. Fin (ADT_A_if utf) s' = s}
 2. inj (Fin (ADT_A_if utf)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs_if s; step_restrict s\<rbrakk> \<Longrightarrow> Init (ADT_A_if utf) s = {s'. Fin (ADT_A_if utf) s' = s}
 2. inj (Fin (ADT_A_if utf)) proof (prove)
goal (1 subgoal):
 1. inj (Fin (ADT_A_if utf)) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma invs_if_inv_holds_ADT_A_if:
  "ADT_A_if utf [> Collect invs_if" by (force intro: inv_holdsI invs_if_Step_ADT_A_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_A_if utf [> Collect invs_if
theory ADT_IF

lemma ADT_A_if_Init_Fin_serial_weak:
  "Init_Fin_serial_weak (ADT_A_if utf) s0 ({s. invs_if s} \<inter> {s. step_restrict s})" apply (rule Init_Fin_serial_weak_strengthen) apply (rule Init_Fin_serial.serial_to_weak[OF ADT_A_if_Init_Fin_serial]) apply (intro inv_holds_conjI invs_if_inv_holds_ADT_A_if step_restrict_inv_holds_ADT_A_if) apply (clarsimp simp: invs_if_full_invs_if) apply (simp add: ADT_A_if_def) apply (insert invs_if_s0 extras_s0) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_Fin_serial_weak (ADT_A_if utf) s0 (Collect invs_if \<inter> {s. step_restrict s}) proof (prove)
goal (4 subgoals):
 1. Init_Fin_serial_weak (ADT_A_if utf) s0 ?I
 2. ADT_A_if utf [> Collect invs_if \<inter> {s. step_restrict s}
 3. Collect invs_if \<inter> {s. step_restrict s} \<subseteq> ?I
 4. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if \<inter> {s. step_restrict s} proof (prove)
goal (3 subgoals):
 1. ADT_A_if utf [> Collect invs_if \<inter> {s. step_restrict s}
 2. Collect invs_if \<inter> {s. step_restrict s} \<subseteq> full_invs_if \<inter> {s. step_restrict s}
 3. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if \<inter> {s. step_restrict s} proof (prove)
goal (2 subgoals):
 1. Collect invs_if \<inter> {s. step_restrict s} \<subseteq> full_invs_if \<inter> {s. step_restrict s}
 2. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if \<inter> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if \<inter> {s. step_restrict s} proof (prove)
goal (1 subgoal):
 1. {s0} \<inter> full_invs_if \<inter> Collect step_restrict \<subseteq> Collect invs_if proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs_if s0; step_restrict s0\<rbrakk> \<Longrightarrow> {s0} \<inter> full_invs_if \<inter> Collect step_restrict \<subseteq> Collect invs_if proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma invariant_holds_inv_holds:
  "A \<Turnstile> I \<Longrightarrow> A [> I" by (simp add: invariant_holds_def inv_holds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<Turnstile> I \<Longrightarrow> A [> I
theory ADT_IF

lemma inv_holdsE:
  assumes I: "A [> I"
  and step: "(s, t) \<in> Step A e"
  and s_I: "s \<in> I"
  and t_I: "t \<in> I \<Longrightarrow> P"
  shows "P" apply (rule t_I) apply (insert step I s_I) apply (force simp: inv_holds_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. t \<in> I proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> Step A e; A [> I; s \<in> I\<rbrakk> \<Longrightarrow> t \<in> I proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma refines_refines':
  "refines C A \<Longrightarrow> refines' C A s" by (auto simp: refines_def refines'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. C \<sqsubseteq> A \<Longrightarrow> refines' C A s
theory ArchADT_IF

lemma dmo_getExMonitor_wp[wp]:
  "\<lbrace>\<lambda>s. P (exclusive_state (machine_state s)) s\<rbrace>
   do_machine_op getExMonitor
   \<lbrace>P\<rbrace>" apply (simp add: do_machine_op_def) apply (wp modify_wp | wpc)+ apply clarsimp apply (erule use_valid) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (exclusive_state (machine_state s)) s\<rbrace> do_machine_op getExMonitor \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (exclusive_state (machine_state s)) s\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (getExMonitor ms);
y <- modify (machine_state_update (\<lambda>_. ms'));
return r
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (exclusive_state (machine_state s)) s \<Longrightarrow> \<forall>x\<in>fst (getExMonitor (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> P xa (s\<lparr>machine_state := xb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s aa bb x. \<lbrakk>P (exclusive_state (machine_state s)) s; ((aa, bb), x) \<in> fst (getExMonitor (machine_state s))\<rbrakk> \<Longrightarrow> P (aa, bb) (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s aa bb x. P (exclusive_state (machine_state s)) s \<Longrightarrow> \<lbrace>?P34 s aa bb x\<rbrace> getExMonitor \<lbrace>\<lambda>a b. P a (s\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>s aa bb x. P (exclusive_state (machine_state s)) s \<Longrightarrow> ?P34 s aa bb x (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s aa bb x. P (exclusive_state (machine_state s)) s \<Longrightarrow> P (exclusive_state (machine_state s)) (s\<lparr>machine_state := machine_state s\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchADT_IF

lemma setExMonitor_wp[wp]:
  "\<lbrace>\<lambda>ms. P (ms\<lparr>exclusive_state := es\<rparr>)\<rbrace>
   setExMonitor es
   \<lbrace>\<lambda>_. P\<rbrace>" by (simp add: setExMonitor_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (ms\<lparr>exclusive_state := es\<rparr>)\<rbrace> setExMonitor es \<lbrace>\<lambda>_. P\<rbrace>
theory ArchADT_IF

lemma dmo_setExMonitor_wp[wp]:
  "\<lbrace>\<lambda>s. P (s\<lparr>machine_state := machine_state s \<lparr>exclusive_state := es\<rparr>\<rparr>)\<rbrace>
   do_machine_op (setExMonitor es)
   \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: do_machine_op_def) apply (wp modify_wp | wpc)+ apply clarsimp apply (erule use_valid) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>)\<rbrace> do_machine_op (setExMonitor es) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>)\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (setExMonitor es ms);
modify (machine_state_update (\<lambda>_. ms'))
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) \<Longrightarrow> \<forall>x\<in>fst (setExMonitor es (machine_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> P (s\<lparr>machine_state := xb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>P (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>); ((), x) \<in> fst (setExMonitor es (machine_state s))\<rbrakk> \<Longrightarrow> P (s\<lparr>machine_state := x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x. P (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) \<Longrightarrow> \<lbrace>?P27 s x\<rbrace> setExMonitor es \<lbrace>\<lambda>a b. P (s\<lparr>machine_state := b\<rparr>)\<rbrace>
 2. \<And>s x. P (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) \<Longrightarrow> ?P27 s x (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. P (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) \<Longrightarrow> P (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchADT_IF

lemma valid_state_exclusive_state_update[iff]:
  "valid_state (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) = valid_state s" by (simp add: valid_state_def valid_irq_states_def valid_machine_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_state (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) = valid_state s
theory ArchADT_IF

lemma cur_tcb_exclusive_state_update[iff]:
  "cur_tcb (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) = cur_tcb s" by (simp add: cur_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_tcb (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) = cur_tcb s
theory ArchADT_IF

lemma invs_exclusive_state_update[iff]:
  "invs (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) = invs s" by (simp add: invs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := es\<rparr>\<rparr>) = invs s
theory ArchADT_IF

lemma do_user_op_if_scheduler_action[ADT_IF_assms, wp]:
  "do_user_op_if f tc \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace>" by (simp add: do_user_op_if_def | wp | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_user_op_if f tc \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>
theory ArchADT_IF

lemma do_user_op_silc_inv[ADT_IF_assms, wp]:
  "do_user_op_if f tc \<lbrace>silc_inv aag st\<rbrace>" apply (simp add: do_user_op_if_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> do_user_op_if f tc \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> do pr <- gets ptable_rights_s;
pxn <- gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s s x);
pl <- gets (\<lambda>s. ptable_lift_s s |` {x. pr x \<noteq> {}});
t <- gets cur_thread;
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
es <- do_machine_op getExMonitor;
y <- assert (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es) \<noteq> {});
(e, tc', um', ds', es') <- select (f t pl pr pxn (tc, um |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, (ds \<circ> ptrFromPAddr) |` {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}, es));
y <- do_machine_op (user_memory_update ((um' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` (- dom ds)));
y <- do_machine_op (device_memory_update ((ds' |` {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x} \<circ> addrFromPPtr) |` dom ds));
y <- do_machine_op (setExMonitor es');
return (e, tc')
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!