kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchScheduler_IF

lemma set_object_reads_respects_scheduler[Scheduler_IF_assms, wp]:
  "reads_respects_scheduler aag l \<top> (set_object ptr obj)" unfolding equiv_valid_def2 equiv_valid_2_def by (auto simp: set_object_def bind_def get_def put_def return_def get_object_def assert_def
                 fail_def gets_def scheduler_equiv_def domain_fields_equiv_def equiv_for_def
                 globals_equiv_scheduler_def arch_globals_equiv_scheduler_def silc_dom_equiv_def
                 scheduler_affects_equiv_def arch_scheduler_affects_equiv_def
                 scheduler_globals_frame_equiv_def identical_kheap_updates_def
          intro: states_equiv_for_identical_kheap_updates idle_equiv_identical_kheap_updates)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (set_object ptr obj) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. True \<and> True \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>(rva, s')\<in>fst (set_object ptr obj s). \<forall>(rvb, t')\<in>fst (set_object ptr obj t). rva = rvb \<and> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')
theory ArchScheduler_IF

lemma arch_activate_idle_thread_reads_respects_scheduler[Scheduler_IF_assms, wp]:
  "reads_respects_scheduler aag l \<top> (arch_activate_idle_thread rv)" unfolding arch_activate_idle_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (arch_activate_idle_thread rv) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (return ())
theory UserOp_IF

lemma equiv_symmetric:
  "equiv_for a b c d = equiv_for a b d c" by (auto simp: equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_for a b c d = equiv_for a b d c
theory UserOp_IF

lemma gets_ev''':
  "equiv_valid_inv I A (\<lambda>s. P s \<and> (\<forall>t. I s t \<and> A s t \<and> P t \<longrightarrow> f s = f t)) (gets f)" apply (simp add: equiv_valid_def2) apply (auto simp: equiv_valid_2_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. P s \<and> (\<forall>t. I s t \<and> A s t \<and> P t \<longrightarrow> f s = f t)) (gets f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (=) (\<lambda>s. P s \<and> (\<forall>t. I s t \<and> A s t \<and> P t \<longrightarrow> f s = f t)) (gets f) proof (prove)
goal:
No subgoals!
theory UserOp_IF

lemma spec_equiv_valid_add_asm:
  "(P st \<Longrightarrow> spec_equiv_valid_inv st I A P f) \<Longrightarrow> spec_equiv_valid_inv st I A P f" by (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P st \<Longrightarrow> spec_equiv_valid_inv st I A P f) \<Longrightarrow> spec_equiv_valid_inv st I A P f
theory UserOp_IF

lemma spec_equiv_valid_add_rel:
  "\<lbrakk> spec_equiv_valid_inv st I A (P and I st) f; \<And>s. I s s \<rbrakk>
     \<Longrightarrow> spec_equiv_valid_inv st I A P f" by (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_equiv_valid_inv st I A (P and I st) f; \<And>s. I s s\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st I A P f
theory UserOp_IF

lemma spec_equiv_valid_add_rel':
  "\<lbrakk> spec_equiv_valid_inv st I A (P and A st) f; \<And>s. A s s \<rbrakk>
     \<Longrightarrow> spec_equiv_valid_inv st I A P f" by (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_equiv_valid_inv st I A (P and A st) f; \<And>s. A s s\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv st I A P f
theory UserOp_IF

lemma reads_equiv_g_refl:
  "reads_equiv_g aag s s" apply (rule reads_equiv_gI) apply (rule reads_equiv_refl) apply (rule globals_equiv_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_g aag s s proof (prove)
goal (2 subgoals):
 1. reads_equiv aag s s
 2. globals_equiv s s proof (prove)
goal (1 subgoal):
 1. globals_equiv s s proof (prove)
goal:
No subgoals!
theory UserOp_IF

lemma restrict_eq_imp_dom_eq:
  "a |` r = b|` r \<Longrightarrow> dom a \<inter> r = dom b \<inter> r" apply (clarsimp simp: set_eq_iff restrict_map_def) apply (drule_tac x = x in fun_cong) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a |` r = b |` r \<Longrightarrow> dom a \<inter> r = dom b \<inter> r proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<lambda>x. if x \<in> r then a x else None) = (\<lambda>x. if x \<in> r then b x else None) \<Longrightarrow> (x \<in> dom a \<and> x \<in> r) = (x \<in> dom b \<and> x \<in> r) proof (prove)
goal (1 subgoal):
 1. \<And>x. (if x \<in> r then a x else None) = (if x \<in> r then b x else None) \<Longrightarrow> (x \<in> dom a \<and> x \<in> r) = (x \<in> dom b \<and> x \<in> r) proof (prove)
goal:
No subgoals!
theory UserOp_IF

lemma restrict_map_eq_same_domain:
  "(\<And>x. x\<in> dom a \<Longrightarrow> b x = c x) \<Longrightarrow> a |` dom b = a |` dom c" apply (rule ext) apply (clarsimp simp: restrict_map_def) apply (intro conjI impI) apply fastforce apply (rule ccontr) apply (drule not_sym) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> dom a \<Longrightarrow> b x = c x) \<Longrightarrow> a |` dom b = a |` dom c proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>x. x \<in> dom a \<Longrightarrow> b x = c x) \<Longrightarrow> (a |` dom b) x = (a |` dom c) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>x. x \<in> dom a \<Longrightarrow> b x = c x) \<Longrightarrow> (x \<in> dom b \<longrightarrow> x \<notin> dom c \<longrightarrow> a x = None) \<and> (x \<notin> dom b \<longrightarrow> x \<in> dom c \<longrightarrow> None = a x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<in> dom b; x \<notin> dom c\<rbrakk> \<Longrightarrow> a x = None
 2. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<notin> dom b; x \<in> dom c\<rbrakk> \<Longrightarrow> None = a x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<notin> dom b; x \<in> dom c\<rbrakk> \<Longrightarrow> None = a x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<notin> dom b; x \<in> dom c; None \<noteq> a x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<notin> dom b; x \<in> dom c; a x \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory UserOp_IF

lemma restrict_map_eq_same_domain_compl:
  "(\<And>x. x\<in> dom a \<Longrightarrow> b x = c x) \<Longrightarrow> a |` (- dom b) = a |` (- dom c)" apply (rule ext) apply (clarsimp simp: restrict_map_def) apply (intro conjI impI) apply fastforce apply (rule ccontr) apply (drule not_sym) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> dom a \<Longrightarrow> b x = c x) \<Longrightarrow> a |` (- dom b) = a |` (- dom c) proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>x. x \<in> dom a \<Longrightarrow> b x = c x) \<Longrightarrow> (a |` (- dom b)) x = (a |` (- dom c)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>x. x \<in> dom a \<Longrightarrow> b x = c x) \<Longrightarrow> (x \<notin> dom b \<longrightarrow> x \<in> dom c \<longrightarrow> a x = None) \<and> (x \<in> dom b \<longrightarrow> x \<notin> dom c \<longrightarrow> None = a x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<notin> dom b; x \<in> dom c\<rbrakk> \<Longrightarrow> a x = None
 2. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<in> dom b; x \<notin> dom c\<rbrakk> \<Longrightarrow> None = a x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<in> dom b; x \<notin> dom c\<rbrakk> \<Longrightarrow> None = a x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<in> dom b; x \<notin> dom c; None \<noteq> a x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. x \<in> dom a \<Longrightarrow> b x = c x; x \<in> dom b; x \<notin> dom c; a x \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory UserOp_IF

lemma map_add_eq:
  "ms x = ms' x \<Longrightarrow> (ms ++ um) x = (ms' ++ um) x" by (clarsimp simp: map_add_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ms x = ms' x \<Longrightarrow> (ms ++ um) x = (ms' ++ um) x
theory ArchUserOp_IF

lemma arch_globals_equiv_underlying_memory_update[UserOp_IF_assms, simp]:
  "arch_globals_equiv ct it kh kh' as as' (underlying_memory_update f ms) ms' =
   arch_globals_equiv ct it kh kh' as as' ms ms'"
  "arch_globals_equiv ct it kh kh' as as' ms (underlying_memory_update f ms') =
   arch_globals_equiv ct it kh kh' as as' ms ms'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_globals_equiv ct it kh kh' as as' (underlying_memory_update f ms) ms' = arch_globals_equiv ct it kh kh' as as' ms ms' &&& arch_globals_equiv ct it kh kh' as as' ms (underlying_memory_update f ms') = arch_globals_equiv ct it kh kh' as as' ms ms'
theory ArchUserOp_IF

lemma arch_globals_equiv_device_state_update[UserOp_IF_assms, simp]:
  "arch_globals_equiv ct it kh kh' as as' (device_state_update f ms) ms' =
   arch_globals_equiv ct it kh kh' as as' ms ms'"
  "arch_globals_equiv ct it kh kh' as as' ms (device_state_update f ms') =
   arch_globals_equiv ct it kh kh' as as' ms ms'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_globals_equiv ct it kh kh' as as' (device_state_update f ms) ms' = arch_globals_equiv ct it kh kh' as as' ms ms' &&& arch_globals_equiv ct it kh kh' as as' ms (device_state_update f ms') = arch_globals_equiv ct it kh kh' as as' ms ms'
theory ArchUserOp_IF

lemma requiv_get_pt_info_eq:
  "\<lbrakk> reads_equiv aag s s'; pas_refined aag s; is_subject aag pt \<rbrakk>
     \<Longrightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) pt x =
         get_pt_info (\<lambda>obj. get_arch_obj (kheap s' obj)) pt x" apply (simp add: get_pt_info_def) apply (subst requiv_get_pt_entry_eq, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; is_subject aag pt\<rbrakk> \<Longrightarrow> get_pt_info (\<lambda>obj. get_arch_obj (kheap s obj)) pt x = get_pt_info (\<lambda>obj. get_arch_obj (kheap s' obj)) pt x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; is_subject aag pt\<rbrakk> \<Longrightarrow> (case get_pt_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pt x of None \<Rightarrow> None | Some InvalidPTE \<Rightarrow> None | Some (LargePagePTE base attrs rights) \<Rightarrow> Some (base, 16::'b, attrs, rights) | Some (SmallPagePTE base attrs rights) \<Rightarrow> Some (base, 12::'b, attrs, rights)) = (case get_pt_entry (\<lambda>obj. get_arch_obj (kheap s' obj)) pt x of None \<Rightarrow> None | Some InvalidPTE \<Rightarrow> None | Some (LargePagePTE base attrs rights) \<Rightarrow> Some (base, 16::'b, attrs, rights) | Some (SmallPagePTE base attrs rights) \<Rightarrow> Some (base, 12::'b, attrs, rights)) proof (prove)
goal:
No subgoals!
theory ArchUserOp_IF

lemma requiv_ptable_xn_eq:
  "\<lbrakk> reads_equiv aag s s'; pas_refined aag s; pas_refined aag s';
     is_subject aag (cur_thread s); invs s; invs s'; ptable_rights_s s x \<noteq> {} \<rbrakk>
     \<Longrightarrow> ptable_xn_s s x = ptable_xn_s s' x" by (simp add: ptable_xn_s_def requiv_ptable_attrs_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; is_subject aag (cur_thread s); invs s; invs s'; ptable_rights_s s x \<noteq> {}\<rbrakk> \<Longrightarrow> ptable_xn_s s x = ptable_xn_s s' x
theory ArchUserOp_IF

lemma obj_range_data_for_cong:
  "obj_range ptr (ArchObj (DataPage dev sz')) = obj_range ptr (ArchObj (DataPage False sz'))" by (simp add: obj_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_range ptr (ArchObj (DataPage dev sz')) = obj_range ptr (ArchObj (DataPage False sz'))
theory ArchUserOp_IF

lemma pspace_distinct_def':
  "pspace_distinct \<equiv>
     \<lambda>s. \<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y
                      \<longrightarrow> obj_range x ko \<inter> obj_range y ko' = {}" by (auto simp: pspace_distinct_def obj_range_def field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct \<equiv> \<lambda>s. \<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> obj_range x ko \<inter> obj_range y ko' = {}
theory ArchUserOp_IF

lemma ptrFromPAddr_mask_simp:
  "ptrFromPAddr z && ~~ mask (pageBitsForSize l) =
   ptrFromPAddr (z && ~~ mask (pageBitsForSize l))" apply (simp add: ptrFromPAddr_def field_simps) apply (subst mask_out_add_aligned[OF is_aligned_pptrBaseOffset]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptrFromPAddr z && ~~ mask (pageBitsForSize l) = ptrFromPAddr (z && ~~ mask (pageBitsForSize l)) proof (prove)
goal (1 subgoal):
 1. pptrBaseOffset + z && ~~ mask (pageBitsForSize l) = pptrBaseOffset + (z && ~~ mask (pageBitsForSize l)) proof (prove)
goal (1 subgoal):
 1. pptrBaseOffset + z && ~~ mask (pageBitsForSize l) = pptrBaseOffset + z && ~~ mask (pageBitsForSize l) proof (prove)
goal:
No subgoals!
theory ArchUserOp_IF

lemma valid_pdpt_align_ptD:
  "\<lbrakk> kheap s ptr = Some (ArchObj (PageTable pt)); valid_pdpt_objs s; pt a = entry \<rbrakk>
     \<Longrightarrow> is_aligned a (pte_range_sz entry)" apply (drule (1) valid_pdpt_objs_ptD) apply (clarsimp simp: entries_align_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (PageTable pt)); \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pt a = entry\<rbrakk> \<Longrightarrow> is_aligned a (pte_range_sz entry) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (PageTable pt)); pt a = entry; valid_entries pte_range pt \<and> entries_align pte_range_sz pt\<rbrakk> \<Longrightarrow> is_aligned a (pte_range_sz entry) proof (prove)
goal:
No subgoals!
theory ArchUserOp_IF

lemma valid_pdpt_align_pdD:
  "\<lbrakk> kheap s ptr = Some (ArchObj (PageDirectory pd));valid_pdpt_objs s; pd a = entry \<rbrakk>
     \<Longrightarrow> is_aligned a (pde_range_sz entry)" apply (drule (1) valid_pdpt_objs_pdD) apply (clarsimp simp: entries_align_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (PageDirectory pd)); \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pd a = entry\<rbrakk> \<Longrightarrow> is_aligned a (pde_range_sz entry) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some (ArchObj (PageDirectory pd)); pd a = entry; valid_entries pde_range pd \<and> entries_align pde_range_sz pd\<rbrakk> \<Longrightarrow> is_aligned a (pde_range_sz entry) proof (prove)
goal:
No subgoals!
theory ArchUserOp_IF

lemma valid_vspace_objsD2:
  "\<lbrakk> (\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s; valid_vspace_objs s \<rbrakk>
     \<Longrightarrow> valid_vspace_obj ao s" by (clarsimp simp: valid_vspace_objsD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>ref. (ref \<rhd> p) s; ako_at ao p s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
theory ArchUserOp_IF

lemma user_frame_at_equiv:
  "\<lbrakk> typ_at (AArch (AUserData sz)) p s; equiv_for P kheap s s'; P p \<rbrakk>
     \<Longrightarrow> typ_at (AArch (AUserData sz)) p s'" by (clarsimp simp: equiv_for_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch (AUserData sz)) p s; equiv_for P kheap s s'; P p\<rbrakk> \<Longrightarrow> typ_at (AArch (AUserData sz)) p s'
theory ArchUserOp_IF

lemma device_frame_at_equiv:
  "\<lbrakk> typ_at (AArch (ADeviceData sz)) p s; equiv_for P kheap s s'; P p \<rbrakk>
     \<Longrightarrow> typ_at (AArch (ADeviceData sz)) p s'" by (clarsimp simp: equiv_for_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch (ADeviceData sz)) p s; equiv_for P kheap s s'; P p\<rbrakk> \<Longrightarrow> typ_at (AArch (ADeviceData sz)) p s'
theory ArchUserOp_IF

lemma typ_at_user_data_at:
  "typ_at (AArch (AUserData sz)) p s \<Longrightarrow> data_at sz p s" by (simp add: data_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at (AArch (AUserData sz)) p s \<Longrightarrow> data_at sz p s
theory ArchUserOp_IF

lemma typ_at_device_data_at:
  "typ_at (AArch (ADeviceData sz)) p s \<Longrightarrow> data_at sz p s" by (simp add: data_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at (AArch (ADeviceData sz)) p s \<Longrightarrow> data_at sz p s
theory ArchUserOp_IF

lemma dmo_setExMonitor_reads_respects_g:
  "reads_respects_g aag l \<top> (do_machine_op (setExMonitor es))" apply (simp add: setExMonitor_def) apply (wp dmo_ev ev_modify) apply (auto simp: reads_equiv_g_def reads_equiv_def affects_equiv_def states_equiv_for_def
                    equiv_for_def equiv_asids_def equiv_asid_def globals_equiv_def idle_equiv_def
             split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (do_machine_op (setExMonitor es)) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>_. True) (do_machine_op (modify (exclusive_state_update (\<lambda>_. es)))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa t. \<lbrakk>K (True \<and> True) sa; K (True \<and> True) t; affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); reads_equiv_g aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> reads_equiv_g aag (s\<lparr>machine_state := sa\<lparr>exclusive_state := es\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := es\<rparr>\<rparr>) \<and> affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := es\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := es\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchUserOp_IF

lemma dmo_getExMonitor_reads_respects_g:
  "reads_respects_g aag l (\<lambda>s. cur_thread s \<noteq> idle_thread s) (do_machine_op getExMonitor)" apply (simp add: getExMonitor_def) apply (wp dmo_ev gets_ev'') apply (clarsimp simp: reads_equiv_g_def globals_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. cur_thread s \<noteq> idle_thread s) (do_machine_op getExMonitor) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. cur_thread s \<noteq> idle_thread s) (do_machine_op (gets exclusive_state)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>sa t. reads_equiv_g aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>) \<and> affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>) \<and> K (cur_thread s \<noteq> idle_thread s \<and> cur_thread s' \<noteq> idle_thread s') sa \<and> K (cur_thread s \<noteq> idle_thread s \<and> cur_thread s' \<noteq> idle_thread s') t \<longrightarrow> exclusive_state sa = exclusive_state t proof (prove)
goal:
No subgoals!
theory ArchUserOp_IF

lemma getExMonitor_wp[wp]:
  "\<lbrace>\<lambda>ms. P (exclusive_state ms) ms\<rbrace> getExMonitor \<lbrace>P\<rbrace>" by (simp add: getExMonitor_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (exclusive_state ms) ms\<rbrace> getExMonitor \<lbrace>P\<rbrace>
theory ADT_IF

lemma system_Step_def_raw:
  "system.Step = (\<lambda>A a. {(s,s'). s' \<in> execution A s [a]})" apply (rule ext) apply (rule ext) apply (subst system.Step_def) by (rule refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. system.Step = (\<lambda>A a. {(s, s'). s' \<in> execution A s [a]}) proof (prove)
goal (1 subgoal):
 1. \<And>A. system.Step A = (\<lambda>a. {(s, s'). s' \<in> execution A s [a]}) proof (prove)
goal (1 subgoal):
 1. \<And>A a. system.Step A a = {(s, s'). s' \<in> execution A s [a]} proof (prove)
goal (1 subgoal):
 1. \<And>A a. {(s, s'). s' \<in> execution A s [a]} = {(s, s'). s' \<in> execution A s [a]}
theory ADT_IF

lemma big_stepsD:
  "(s,t) \<in> big_steps A R exmap ev
   \<Longrightarrow> \<exists>s' as a. (s',as) \<in> sub_big_steps A R s \<and> (s',t) \<in> Step A a \<and> R s t \<and> ev = exmap (as @ [a])" apply (erule big_steps.induct) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, t) \<in> big_steps A R exmap ev \<Longrightarrow> \<exists>s' as a. (s', as) \<in> sub_big_steps A R s \<and> (s', t) \<in> Step A a \<and> R s t \<and> ev = exmap (as @ [a]) proof (prove)
goal (1 subgoal):
 1. \<And>s' as s t a. \<lbrakk>(s', as) \<in> sub_big_steps A R s; (s', t) \<in> Step A a; R s t; ev = exmap (as @ [a])\<rbrakk> \<Longrightarrow> \<exists>s' as a. (s', as) \<in> sub_big_steps A R s \<and> (s', t) \<in> Step A a \<and> R s t \<and> ev = exmap (as @ [a]) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma big_stepsE:
  assumes bs: "(s,t) \<in> big_steps A R exmap ev"
  obtains s' as a where "(s',as) \<in> sub_big_steps A R s"
                        "(s',t) \<in> Step A a"
                        "R s t"
                        "ev =  exmap (as @ [a])" using bs[THEN big_stepsD] by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s' as a. \<lbrakk>(s', as) \<in> sub_big_steps A R s; (s', t) \<in> Step A a; R s t; ev = exmap (as @ [a])\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
\<exists>s' as a. (s', as) \<in> sub_big_steps A R s \<and> (s', t) \<in> Step A a \<and> R s t \<and> ev = exmap (as @ [a])

goal (1 subgoal):
 1. (\<And>s' as a. \<lbrakk>(s', as) \<in> sub_big_steps A R s; (s', t) \<in> Step A a; R s t; ev = exmap (as @ [a])\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory ADT_IF

lemma Run_subset:
  "(\<And>ev. Stepf ev \<subseteq> Stepf' ev) \<Longrightarrow> Run Stepf as \<subseteq> Run Stepf' as" apply (induct as) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>ev. Stepf ev \<subseteq> Stepf' ev) \<Longrightarrow> Run Stepf as \<subseteq> Run Stepf' as proof (prove)
goal (2 subgoals):
 1. (\<And>ev. Stepf ev \<subseteq> Stepf' ev) \<Longrightarrow> Run Stepf [] \<subseteq> Run Stepf' []
 2. \<And>a as. \<lbrakk>(\<And>ev. Stepf ev \<subseteq> Stepf' ev) \<Longrightarrow> Run Stepf as \<subseteq> Run Stepf' as; \<And>ev. Stepf ev \<subseteq> Stepf' ev\<rbrakk> \<Longrightarrow> Run Stepf (a # as) \<subseteq> Run Stepf' (a # as) proof (prove)
goal (1 subgoal):
 1. \<And>a as. \<lbrakk>(\<And>ev. Stepf ev \<subseteq> Stepf' ev) \<Longrightarrow> Run Stepf as \<subseteq> Run Stepf' as; \<And>ev. Stepf ev \<subseteq> Stepf' ev\<rbrakk> \<Longrightarrow> Run Stepf (a # as) \<subseteq> Run Stepf' (a # as) proof (prove)
goal:
No subgoals!