kings-crown/FVELER_Isabelle huggingface dataset:
theory Invocations_H

lemma retypeFreeRegionBase_retypeIsDevice_update [simp]:
  "retypeFreeRegionBase (retypeIsDevice_update f v) = retypeFreeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeFreeRegionBase (retypeIsDevice_update f v) = retypeFreeRegionBase v
theory Invocations_H

lemma retypeNewType_retypeSource_update [simp]:
  "retypeNewType (retypeSource_update f v) = retypeNewType v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewType (retypeSource_update f v) = retypeNewType v
theory Invocations_H

lemma retypeNewType_retypeRegionBase_update [simp]:
  "retypeNewType (retypeRegionBase_update f v) = retypeNewType v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewType (retypeRegionBase_update f v) = retypeNewType v
theory Invocations_H

lemma retypeNewType_retypeFreeRegionBase_update [simp]:
  "retypeNewType (retypeFreeRegionBase_update f v) = retypeNewType v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewType (retypeFreeRegionBase_update f v) = retypeNewType v
theory Invocations_H

lemma retypeNewType_retypeNewType_update [simp]:
  "retypeNewType (retypeNewType_update f v) = f (retypeNewType v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewType (retypeNewType_update f v) = f (retypeNewType v)
theory Invocations_H

lemma retypeNewType_retypeNewSizeBits_update [simp]:
  "retypeNewType (retypeNewSizeBits_update f v) = retypeNewType v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewType (retypeNewSizeBits_update f v) = retypeNewType v
theory Invocations_H

lemma retypeNewType_retypeSlots_update [simp]:
  "retypeNewType (retypeSlots_update f v) = retypeNewType v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewType (retypeSlots_update f v) = retypeNewType v
theory Invocations_H

lemma retypeNewType_retypeIsDevice_update [simp]:
  "retypeNewType (retypeIsDevice_update f v) = retypeNewType v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewType (retypeIsDevice_update f v) = retypeNewType v
theory Invocations_H

lemma retypeNewSizeBits_retypeSource_update [simp]:
  "retypeNewSizeBits (retypeSource_update f v) = retypeNewSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewSizeBits (retypeSource_update f v) = retypeNewSizeBits v
theory Invocations_H

lemma retypeNewSizeBits_retypeResetUntyped_update [simp]:
  "retypeNewSizeBits (retypeResetUntyped_update f v) = retypeNewSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewSizeBits (retypeResetUntyped_update f v) = retypeNewSizeBits v
theory Invocations_H

lemma retypeNewSizeBits_retypeRegionBase_update [simp]:
  "retypeNewSizeBits (retypeRegionBase_update f v) = retypeNewSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewSizeBits (retypeRegionBase_update f v) = retypeNewSizeBits v
theory Invocations_H

lemma retypeNewSizeBits_retypeFreeRegionBase_update [simp]:
  "retypeNewSizeBits (retypeFreeRegionBase_update f v) = retypeNewSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewSizeBits (retypeFreeRegionBase_update f v) = retypeNewSizeBits v
theory Invocations_H

lemma retypeNewSizeBits_retypeNewType_update [simp]:
  "retypeNewSizeBits (retypeNewType_update f v) = retypeNewSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewSizeBits (retypeNewType_update f v) = retypeNewSizeBits v
theory Invocations_H

lemma retypeNewSizeBits_retypeNewSizeBits_update [simp]:
  "retypeNewSizeBits (retypeNewSizeBits_update f v) = f (retypeNewSizeBits v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewSizeBits (retypeNewSizeBits_update f v) = f (retypeNewSizeBits v)
theory Invocations_H

lemma retypeNewSizeBits_retypeSlots_update [simp]:
  "retypeNewSizeBits (retypeSlots_update f v) = retypeNewSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewSizeBits (retypeSlots_update f v) = retypeNewSizeBits v
theory Invocations_H

lemma retypeNewSizeBits_retypeIsDevice_update [simp]:
  "retypeNewSizeBits (retypeIsDevice_update f v) = retypeNewSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeNewSizeBits (retypeIsDevice_update f v) = retypeNewSizeBits v
theory Invocations_H

lemma retypeSlots_retypeSource_update [simp]:
  "retypeSlots (retypeSource_update f v) = retypeSlots v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSlots (retypeSource_update f v) = retypeSlots v
theory Invocations_H

lemma retypeSlots_retypeResetUntyped_update [simp]:
  "retypeSlots (retypeResetUntyped_update f v) = retypeSlots v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSlots (retypeResetUntyped_update f v) = retypeSlots v
theory Invocations_H

lemma retypeSlots_retypeRegionBase_update [simp]:
  "retypeSlots (retypeRegionBase_update f v) = retypeSlots v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSlots (retypeRegionBase_update f v) = retypeSlots v
theory Invocations_H

lemma retypeSlots_retypeFreeRegionBase_update [simp]:
  "retypeSlots (retypeFreeRegionBase_update f v) = retypeSlots v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSlots (retypeFreeRegionBase_update f v) = retypeSlots v
theory Invocations_H

lemma retypeSlots_retypeNewType_update [simp]:
  "retypeSlots (retypeNewType_update f v) = retypeSlots v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSlots (retypeNewType_update f v) = retypeSlots v
theory Invocations_H

lemma retypeSlots_retypeNewSizeBits_update [simp]:
  "retypeSlots (retypeNewSizeBits_update f v) = retypeSlots v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSlots (retypeNewSizeBits_update f v) = retypeSlots v
theory Invocations_H

lemma retypeSlots_retypeSlots_update [simp]:
  "retypeSlots (retypeSlots_update f v) = f (retypeSlots v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSlots (retypeSlots_update f v) = f (retypeSlots v)
theory Invocations_H

lemma retypeSlots_retypeIsDevice_update [simp]:
  "retypeSlots (retypeIsDevice_update f v) = retypeSlots v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSlots (retypeIsDevice_update f v) = retypeSlots v
theory Invocations_H

lemma retypeIsDevice_retypeSource_update [simp]:
  "retypeIsDevice (retypeSource_update f v) = retypeIsDevice v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeIsDevice (retypeSource_update f v) = retypeIsDevice v
theory Invocations_H

lemma retypeIsDevice_retypeResetUntyped_update [simp]:
  "retypeIsDevice (retypeResetUntyped_update f v) = retypeIsDevice v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeIsDevice (retypeResetUntyped_update f v) = retypeIsDevice v
theory Invocations_H

lemma retypeIsDevice_retypeRegionBase_update [simp]:
  "retypeIsDevice (retypeRegionBase_update f v) = retypeIsDevice v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeIsDevice (retypeRegionBase_update f v) = retypeIsDevice v
theory Invocations_H

lemma retypeIsDevice_retypeFreeRegionBase_update [simp]:
  "retypeIsDevice (retypeFreeRegionBase_update f v) = retypeIsDevice v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeIsDevice (retypeFreeRegionBase_update f v) = retypeIsDevice v
theory Invocations_H

lemma retypeIsDevice_retypeNewType_update [simp]:
  "retypeIsDevice (retypeNewType_update f v) = retypeIsDevice v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeIsDevice (retypeNewType_update f v) = retypeIsDevice v
theory Invocations_H

lemma retypeIsDevice_retypeNewSizeBits_update [simp]:
  "retypeIsDevice (retypeNewSizeBits_update f v) = retypeIsDevice v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeIsDevice (retypeNewSizeBits_update f v) = retypeIsDevice v
theory Invocations_H

lemma retypeIsDevice_retypeSlots_update [simp]:
  "retypeIsDevice (retypeSlots_update f v) = retypeIsDevice v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeIsDevice (retypeSlots_update f v) = retypeIsDevice v
theory Invocations_H

lemma retypeIsDevice_retypeIsDevice_update [simp]:
  "retypeIsDevice (retypeIsDevice_update f v) = f (retypeIsDevice v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeIsDevice (retypeIsDevice_update f v) = f (retypeIsDevice v)
theory Delete_H

lemma card_reduce:
  "(s :: ('a :: finite) set) \<inter> s' = {} \<Longrightarrow> card (UNIV - (s \<union> s')) < card (UNIV - s) = (s' \<noteq> {})" apply (case_tac "s' \<subseteq> s") apply (simp add: Un_absorb2) apply (simp add: Int_absorb1) apply (clarsimp simp: subset_iff) apply (subst psubset_card_mono) apply simp apply blast apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<inter> s' = {} \<Longrightarrow> (card (UNIV - (s \<union> s')) < card (UNIV - s)) = (s' \<noteq> {}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<inter> s' = {}; s' \<subseteq> s\<rbrakk> \<Longrightarrow> (card (UNIV - (s \<union> s')) < card (UNIV - s)) = (s' \<noteq> {})
 2. \<lbrakk>s \<inter> s' = {}; \<not> s' \<subseteq> s\<rbrakk> \<Longrightarrow> (card (UNIV - (s \<union> s')) < card (UNIV - s)) = (s' \<noteq> {}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<inter> s' = {}; s' \<subseteq> s\<rbrakk> \<Longrightarrow> s' = {}
 2. \<lbrakk>s \<inter> s' = {}; \<not> s' \<subseteq> s\<rbrakk> \<Longrightarrow> (card (UNIV - (s \<union> s')) < card (UNIV - s)) = (s' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<inter> s' = {}; \<not> s' \<subseteq> s\<rbrakk> \<Longrightarrow> (card (UNIV - (s \<union> s')) < card (UNIV - s)) = (s' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s \<inter> s' = {}; t \<in> s'; t \<notin> s\<rbrakk> \<Longrightarrow> (card (UNIV - (s \<union> s')) < card (UNIV - s)) = (s' \<noteq> {}) proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrakk>s \<inter> s' = {}; t \<in> s'; t \<notin> s\<rbrakk> \<Longrightarrow> finite (UNIV - s)
 2. \<And>t. \<lbrakk>s \<inter> s' = {}; t \<in> s'; t \<notin> s\<rbrakk> \<Longrightarrow> UNIV - (s \<union> s') \<subset> UNIV - s
 3. \<And>t. \<lbrakk>s \<inter> s' = {}; t \<in> s'; t \<notin> s\<rbrakk> \<Longrightarrow> True = (s' \<noteq> {}) proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>s \<inter> s' = {}; t \<in> s'; t \<notin> s\<rbrakk> \<Longrightarrow> UNIV - (s \<union> s') \<subset> UNIV - s
 2. \<And>t. \<lbrakk>s \<inter> s' = {}; t \<in> s'; t \<notin> s\<rbrakk> \<Longrightarrow> True = (s' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>s \<inter> s' = {}; t \<in> s'; t \<notin> s\<rbrakk> \<Longrightarrow> True = (s' \<noteq> {}) proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma foldr_does_nothing_to_xf:
  "\<lbrakk> \<And>x s. x \<in> set xs \<Longrightarrow> xf (f x s) = xf s \<rbrakk>
       \<Longrightarrow> xf (foldr f xs s) = xf s" by (induct xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x s. x \<in> set xs \<Longrightarrow> xf (f x s) = xf s) \<Longrightarrow> xf (foldr f xs s) = xf s
theory GlobalsSwap

lemma intvl_empty2:
  "({p ..+ n} = {}) = (n = 0)" by (auto simp add: intvl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({p..+n} = {}) = (n = 0)
theory GlobalsSwap

lemma heap_update_list_commute:
  "{p ..+ length xs} \<inter> {q ..+ length ys} = {}
      \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp)
        = heap_update_list q ys (heap_update_list p xs hp)" apply (cases "length xs < addr_card") apply (cases "length ys < addr_card") apply (rule ext, simp add: heap_update_list_value) apply blast apply (simp_all add: addr_card intvl_overflow intvl_empty2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {p..+length xs} \<inter> {q..+length ys} = {} \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; length xs < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp)
 2. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; \<not> length xs < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; length xs < addr_card; length ys < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp)
 2. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; length xs < addr_card; \<not> length ys < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp)
 3. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; \<not> length xs < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; length xs < addr_card; length ys < addr_card\<rbrakk> \<Longrightarrow> x \<in> {p..+length xs} \<longrightarrow> x \<in> {q..+length ys} \<longrightarrow> xs ! unat (x - p) = ys ! unat (x - q)
 2. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; length xs < addr_card; \<not> length ys < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp)
 3. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; \<not> length xs < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; length xs < addr_card; \<not> length ys < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp)
 2. \<lbrakk>{p..+length xs} \<inter> {q..+length ys} = {}; \<not> length xs < addr_card\<rbrakk> \<Longrightarrow> heap_update_list p xs (heap_update_list q ys hp) = heap_update_list q ys (heap_update_list p xs hp) proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma heap_update_commute:
  "\<lbrakk>d,g \<Turnstile>\<^sub>t p; d,g' \<Turnstile>\<^sub>t q; \<not> TYPE('a) <\<^sub>\<tau> TYPE('b); \<not> field_of_t q p;
       wf_fd (typ_info_t TYPE('a)); wf_fd (typ_info_t TYPE('b)) \<rbrakk>
        \<Longrightarrow> heap_update p v (heap_update q (u :: 'b :: c_type) h)
              = heap_update q u (heap_update p (v :: 'a :: c_type) h)" apply (drule(3) h_t_valid_neq_disjoint) apply (simp add: heap_update_def) apply (simp add: heap_update_list_commute heap_list_update_disjoint_same
                   to_bytes_def length_fa_ti size_of_def Int_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d,g \<Turnstile>\<^sub>t p; d,g' \<Turnstile>\<^sub>t q; \<not> TYPE('a) <\<^sub>\<tau> TYPE('b); \<not> field_of_t q p; wf_fd (typ_info_t TYPE('a)); wf_fd (typ_info_t TYPE('b))\<rbrakk> \<Longrightarrow> heap_update p v (heap_update q u h) = heap_update q u (heap_update p v h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d,g \<Turnstile>\<^sub>t p; \<not> TYPE('a) <\<^sub>\<tau> TYPE('b); \<not> field_of_t q p; wf_fd (typ_info_t TYPE('a)); wf_fd (typ_info_t TYPE('b)); {ptr_val q..+size_of TYPE('b)} \<inter> {ptr_val p..+size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> heap_update p v (heap_update q u h) = heap_update q u (heap_update p v h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d,g \<Turnstile>\<^sub>t p; \<not> TYPE('a) <\<^sub>\<tau> TYPE('b); \<not> field_of_t q p; wf_fd (typ_info_t TYPE('a)); wf_fd (typ_info_t TYPE('b)); {ptr_val q..+size_of TYPE('b)} \<inter> {ptr_val p..+size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> heap_update_list (ptr_val p) (to_bytes v (heap_list (heap_update_list (ptr_val q) (to_bytes u (heap_list h (size_of TYPE('b)) (ptr_val q))) h) (size_of TYPE('a)) (ptr_val p))) (heap_update_list (ptr_val q) (to_bytes u (heap_list h (size_of TYPE('b)) (ptr_val q))) h) = heap_update_list (ptr_val q) (to_bytes u (heap_list (heap_update_list (ptr_val p) (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p))) h) (size_of TYPE('b)) (ptr_val q))) (heap_update_list (ptr_val p) (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p))) h) proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma heap_update_list_double_id:
  "\<lbrakk> heap_list hp n ptr = xs; length xs' = length xs;
         length xs < addr_card \<rbrakk> \<Longrightarrow>
    heap_update_list ptr xs (heap_update_list ptr xs' hp) = hp" apply (rule ext, simp add: heap_update_list_value') apply (clarsimp simp: heap_list_nth intvl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_list hp n ptr = xs; length xs' = length xs; length xs < addr_card\<rbrakk> \<Longrightarrow> heap_update_list ptr xs (heap_update_list ptr xs' hp) = hp proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>heap_list hp n ptr = xs; length xs' = length xs; length xs < addr_card\<rbrakk> \<Longrightarrow> unat (x - ptr) < length xs \<longrightarrow> xs ! unat (x - ptr) = hp x proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma foldr_update_commutes:
  "\<lbrakk> \<And>x s. x \<in> set xs \<Longrightarrow> f (g x s) = g x (f s) \<rbrakk>
       \<Longrightarrow> f (foldr g xs s) = foldr g xs (f s)" by (induct xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x s. x \<in> set xs \<Longrightarrow> f (g x s) = g x (f s)) \<Longrightarrow> f (foldr g xs s) = foldr g xs (f s)
theory GlobalsSwap

lemma global_data_swappable_sym:
  "global_data_swappable x y = global_data_swappable y x" by (auto simp add: global_data_swappable_def
              split: global_data.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_data_swappable x y = global_data_swappable y x
theory GlobalsSwap

lemma hrs_htd_globals_swap:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
        \<forall>x \<in> set xs. global_data_valid g_hrs g_hrs_upd x \<rbrakk>
    \<Longrightarrow> hrs_htd (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))
        = hrs_htd (g_hrs gs)" unfolding globals_swap_def apply (rule foldr_does_nothing_to_xf) apply (simp add: global_swap_def global_acc_valid_def
            split: global_data.split prod.split bool.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x\<rbrakk> \<Longrightarrow> hrs_htd (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs)) = hrs_htd (g_hrs gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x\<rbrakk> \<Longrightarrow> hrs_htd (g_hrs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs)) = hrs_htd (g_hrs gs) proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x; x \<in> set xs\<rbrakk> \<Longrightarrow> hrs_htd (g_hrs (global_swap g_hrs g_hrs_upd symtab x s)) = hrs_htd (g_hrs s) proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma disjoint_int_intvl_min:
  "\<lbrakk> S \<inter> {p ..+ n} = {} \<rbrakk>
      \<Longrightarrow> S \<inter> {p ..+ min m n} = {}" using intvl_start_le[where x="min m n" and y=n] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<inter> {p..+n} = {} \<Longrightarrow> S \<inter> {p..+min m n} = {} proof (prove)
using this:
min m n \<le> n \<Longrightarrow> {?p..+min m n} \<subseteq> {?p..+n}

goal (1 subgoal):
 1. S \<inter> {p..+n} = {} \<Longrightarrow> S \<inter> {p..+min m n} = {}
theory GlobalsSwap

lemma ptr_set_disjoint_footprint:
  "(s_footprint (p :: ('a :: c_type) ptr) \<inter> (S \<times> UNIV) = {})
    \<Longrightarrow> ({ptr_val p ..+ size_of TYPE('a)} \<inter> S = {})" by (auto simp add: s_footprint_intvl[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_footprint p \<inter> S \<times> UNIV = {} \<Longrightarrow> {ptr_val p..+size_of TYPE('a)} \<inter> S = {}
theory GlobalsSwap

lemma disjoint_h_val_globals_swap_filter:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
     globals_list_distinct D symtab (filter is_global_data xs);
     s_footprint p \<subseteq> D \<times> UNIV \<rbrakk>
     \<Longrightarrow> h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) p
            = h_val (hrs_mem (g_hrs gs)) p" apply (clarsimp simp: h_val_def) apply (subst disjoint_heap_list_globals_swap_filter[where g_hrs=g_hrs], assumption+) apply (auto simp: s_footprint_intvl[symmetric])[1] apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab (filter is_global_data xs); s_footprint p \<subseteq> D \<times> UNIV\<rbrakk> \<Longrightarrow> h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) p = h_val (hrs_mem (g_hrs gs)) p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab (filter is_global_data xs); s_footprint p \<subseteq> D \<times> UNIV\<rbrakk> \<Longrightarrow> from_bytes (heap_list (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) (size_of TYPE('b)) (ptr_val p)) = from_bytes (heap_list (hrs_mem (g_hrs gs)) (size_of TYPE('b)) (ptr_val p)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab (filter is_global_data xs); s_footprint p \<subseteq> D \<times> UNIV\<rbrakk> \<Longrightarrow> {ptr_val p..+size_of TYPE('b)} \<subseteq> D
 2. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab (filter is_global_data xs); s_footprint p \<subseteq> D \<times> UNIV\<rbrakk> \<Longrightarrow> from_bytes (heap_list (hrs_mem (g_hrs gs)) (size_of TYPE('b)) (ptr_val p)) = from_bytes (heap_list (hrs_mem (g_hrs gs)) (size_of TYPE('b)) (ptr_val p)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab (filter is_global_data xs); s_footprint p \<subseteq> D \<times> UNIV\<rbrakk> \<Longrightarrow> from_bytes (heap_list (hrs_mem (g_hrs gs)) (size_of TYPE('b)) (ptr_val p)) = from_bytes (heap_list (hrs_mem (g_hrs gs)) (size_of TYPE('b)) (ptr_val p)) proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma distinct_prop_filter:
  "distinct_prop P (filter Q xs)
    = distinct_prop (\<lambda>x y. Q x \<and> Q y \<longrightarrow> P x y) xs" by (induct xs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_prop P (filter Q xs) = distinct_prop (\<lambda>x y. Q x \<and> Q y \<longrightarrow> P x y) xs
theory GlobalsSwap

lemma distinct_prop_weaken:
  "\<lbrakk> distinct_prop P xs; \<And>x y. P x y \<Longrightarrow> Q x y \<rbrakk>
    \<Longrightarrow> distinct_prop Q xs" by (induct xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_prop P xs; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> distinct_prop Q xs