kings-crown/FVELER_Isabelle huggingface dataset:
theory GlobalsSwap

lemma globals_list_distinct_filter:
  "globals_list_distinct D symtab xs
    \<Longrightarrow> globals_list_distinct D symtab (filter P xs)" by (clarsimp simp: globals_list_distinct_def
                     distinct_prop_map distinct_prop_filter
              elim!: distinct_prop_weaken)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_list_distinct D symtab xs \<Longrightarrow> globals_list_distinct D symtab (filter P xs)
theory GlobalsSwap

lemma to_bytes_p_from_bytes:
  "length xs = size_of TYPE ('a :: packed_type)
    \<Longrightarrow> to_bytes_p (from_bytes xs :: 'a) = xs" by (simp add: to_bytes_p_def to_bytes_def from_bytes_def
                update_ti_t_def size_of_def
                field_access_update_same td_fafu_idem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = size_of TYPE('a) \<Longrightarrow> to_bytes_p (from_bytes xs) = xs
theory GlobalsSwap

lemma to_bytes_p_inj:
  "inj (to_bytes_p :: ('a :: packed_type) \<Rightarrow> _)" apply (rule inj_onI) apply (drule_tac f=from_bytes in arg_cong) apply (simp add: to_bytes_p_def) apply (subst(asm) CTypes.inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj to_bytes_p proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; to_bytes_p x = to_bytes_p y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; from_bytes (to_bytes_p x) = from_bytes (to_bytes_p y)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. from_bytes (to_bytes x (replicate (size_of TYPE('a)) 0)) = from_bytes (to_bytes y (replicate (size_of TYPE('a)) 0)) \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma globals_swap_reorder_append_n:
  "\<lbrakk> globals_list_valid symtab g_hrs g_hrs_upd xs; global_acc_valid g_hrs g_hrs_upd;
        globals_list_distinct D symtab xs \<rbrakk> \<Longrightarrow>
    globals_swap g_hrs g_hrs_upd symtab xs = globals_swap g_hrs g_hrs_upd symtab (drop n xs @ take n xs)" using globals_swap_reorder_append
    [where xs="take n xs" and ys="drop n xs"] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_valid symtab g_hrs g_hrs_upd xs; global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab xs = globals_swap g_hrs g_hrs_upd symtab (drop n xs @ take n xs) proof (prove)
using this:
\<lbrakk>globals_list_valid ?symtab ?g_hrs ?g_hrs_upd (take n xs @ drop n xs); global_acc_valid ?g_hrs ?g_hrs_upd; globals_list_distinct ?D ?symtab (take n xs @ drop n xs)\<rbrakk> \<Longrightarrow> globals_swap ?g_hrs ?g_hrs_upd ?symtab (take n xs @ drop n xs) = globals_swap ?g_hrs ?g_hrs_upd ?symtab (drop n xs @ take n xs)

goal (1 subgoal):
 1. \<lbrakk>globals_list_valid symtab g_hrs g_hrs_upd xs; global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab xs = globals_swap g_hrs g_hrs_upd symtab (drop n xs @ take n xs)
theory GlobalsSwap

lemma heap_update_list_overwrite:
  "\<lbrakk> length xs = length ys; length ys < addr_card \<rbrakk>
    \<Longrightarrow> heap_update_list w xs (heap_update_list w ys hp)
        = heap_update_list w xs hp" by (rule ext, simp add: heap_update_list_value)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; length ys < addr_card\<rbrakk> \<Longrightarrow> heap_update_list w xs (heap_update_list w ys hp) = heap_update_list w xs hp
theory GlobalsSwap

lemma heap_list_update_eq:
  "\<lbrakk> n = length v; n \<le> addr_card \<rbrakk>
    \<Longrightarrow> heap_list (heap_update_list p v h) n p = v" by (simp add: heap_list_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = length v; n \<le> addr_card\<rbrakk> \<Longrightarrow> heap_list (heap_update_list p v h) n p = v
theory GlobalsSwap

lemma append_2nd_simp_backward:
  "xs @ y # ys = (xs @ [y]) @ ys" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs @ y # ys = (xs @ [y]) @ ys
theory GlobalsSwap

lemma globals_swap_access_mem:
  "\<lbrakk> global_data nm g u \<in> set xs;
     global_acc_valid g_hrs g_hrs_upd;
     globals_list_valid symtab g_hrs g_hrs_upd xs;
     globals_list_distinct D symtab xs \<rbrakk>
    \<Longrightarrow> g (globals_swap g_hrs g_hrs_upd symtab xs gs) = h_val (hrs_mem (g_hrs gs)) (Ptr (symtab nm))" by (simp add: global_data_def globals_swap_access_mem_raw)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm g u \<in> set xs; global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> g (globals_swap g_hrs g_hrs_upd symtab xs gs) = h_val (hrs_mem (g_hrs gs)) (PTR('b) (symtab nm))
theory GlobalsSwap

lemma globals_swap_access_mem2:
  "\<lbrakk> global_data nm g u \<in> set xs;
     global_acc_valid g_hrs g_hrs_upd;
     globals_list_valid symtab g_hrs g_hrs_upd xs;
     globals_list_distinct D symtab xs \<rbrakk>
    \<Longrightarrow> g gs = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) (Ptr (symtab nm))" using globals_swap_twice_helper globals_swap_access_mem by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm g u \<in> set xs; global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> g gs = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) (PTR('b) (symtab nm)) proof (prove)
using this:
\<lbrakk>globals_list_valid ?symtab ?g_hrs ?g_hrs_upd ?xs; global_acc_valid ?g_hrs ?g_hrs_upd; globals_list_distinct ?D ?symtab ?xs\<rbrakk> \<Longrightarrow> globals_swap ?g_hrs ?g_hrs_upd ?symtab ?xs (globals_swap ?g_hrs ?g_hrs_upd ?symtab ?xs ?gs) = ?gs
\<lbrakk>global_data ?nm ?g ?u \<in> set ?xs; global_acc_valid ?g_hrs ?g_hrs_upd; globals_list_valid ?symtab ?g_hrs ?g_hrs_upd ?xs; globals_list_distinct ?D ?symtab ?xs\<rbrakk> \<Longrightarrow> ?g (globals_swap ?g_hrs ?g_hrs_upd ?symtab ?xs ?gs) = h_val (hrs_mem (?g_hrs ?gs)) (PTR(?'b) (?symtab ?nm))

goal (1 subgoal):
 1. \<lbrakk>global_data nm g u \<in> set xs; global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> g gs = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) (PTR('b) (symtab nm))
theory GlobalsSwap

lemma to_bytes_p_from_bytes_eq:
  "\<lbrakk> from_bytes ys = (v :: 'a :: packed_type); length ys = size_of TYPE('a) \<rbrakk>
        \<Longrightarrow> to_bytes_p v = ys" by (clarsimp simp: to_bytes_p_from_bytes)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>from_bytes ys = v; length ys = size_of TYPE('a)\<rbrakk> \<Longrightarrow> to_bytes_p v = ys
theory GlobalsSwap

lemma globals_swap_update_mem:
  "\<lbrakk> global_data nm g u \<in> set xs;
     global_acc_valid g_hrs g_hrs_upd;
     globals_list_valid symtab g_hrs g_hrs_upd xs;
     globals_list_distinct D symtab xs \<rbrakk>
    \<Longrightarrow> u (\<lambda>_. v) (globals_swap g_hrs g_hrs_upd symtab xs gs)
        = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update
            (\<lambda>hrs. heap_update (Ptr (symtab nm)) v hrs)) gs)" unfolding global_data_def apply (simp add: heap_update_def) apply (subst globals_swap_update_mem_raw[where v'="to_bytes_p v", rotated -1],
         assumption, simp_all add: K_def o_def) apply clarsimp apply (rule to_bytes_p_from_bytes_eq[symmetric], simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm g u \<in> set xs; global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> u (\<lambda>_. v) (globals_swap g_hrs g_hrs_upd symtab xs gs) = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update (heap_update (PTR('b) (symtab nm)) v)) gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p \<circ> g) (u \<circ> K \<circ> from_bytes) \<in> set xs; global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> u (\<lambda>_. v) (globals_swap g_hrs g_hrs_upd symtab xs gs) = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update (heap_update (PTR('b) (symtab nm)) v)) gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p \<circ> g) (u \<circ> (\<lambda>x y. x) \<circ> from_bytes) \<in> set xs; global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> u (\<lambda>_. v) (globals_swap g_hrs g_hrs_upd symtab xs gs) = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update (\<lambda>hrs. heap_update_list (symtab nm) (to_bytes v (heap_list hrs (size_of TYPE('b)) (symtab nm))) hrs)) gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (\<lambda>x. to_bytes_p (g x)) (\<lambda>x. u (\<lambda>y. from_bytes x)) \<in> set xs; global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> \<forall>hmem. to_bytes v (heap_list hmem (size_of TYPE('b)) (symtab nm)) = to_bytes_p v proof (prove)
goal (1 subgoal):
 1. \<And>hmem. \<lbrakk>GlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (\<lambda>x. to_bytes_p (g x)) (\<lambda>x. u (\<lambda>y. from_bytes x)) \<in> set xs; global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> to_bytes v (heap_list hmem (size_of TYPE('b)) (symtab nm)) = to_bytes_p v proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma globals_swap_update_mem2:
  assumes prems: "global_data nm g u \<in> set xs"
     "global_acc_valid g_hrs g_hrs_upd"
     "globals_list_valid symtab g_hrs g_hrs_upd xs"
     "globals_list_distinct D symtab xs"
  shows "globals_swap g_hrs g_hrs_upd symtab xs (u (\<lambda>_. v) gs)
        = g_hrs_upd (hrs_mem_update (\<lambda>hrs. heap_update (Ptr (symtab nm)) v hrs))
            (globals_swap g_hrs g_hrs_upd symtab xs gs)" using prems globals_swap_twice_helper globals_swap_update_mem by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_swap g_hrs g_hrs_upd symtab xs (u (\<lambda>_. v) gs) = g_hrs_upd (hrs_mem_update (heap_update (PTR('b) (symtab nm)) v)) (globals_swap g_hrs g_hrs_upd symtab xs gs) proof (prove)
using this:
global_data nm g u \<in> set xs
global_acc_valid g_hrs g_hrs_upd
globals_list_valid symtab g_hrs g_hrs_upd xs
globals_list_distinct D symtab xs
\<lbrakk>globals_list_valid ?symtab ?g_hrs ?g_hrs_upd ?xs; global_acc_valid ?g_hrs ?g_hrs_upd; globals_list_distinct ?D ?symtab ?xs\<rbrakk> \<Longrightarrow> globals_swap ?g_hrs ?g_hrs_upd ?symtab ?xs (globals_swap ?g_hrs ?g_hrs_upd ?symtab ?xs ?gs) = ?gs
\<lbrakk>global_data ?nm ?g ?u \<in> set ?xs; global_acc_valid ?g_hrs ?g_hrs_upd; globals_list_valid ?symtab ?g_hrs ?g_hrs_upd ?xs; globals_list_distinct ?D ?symtab ?xs\<rbrakk> \<Longrightarrow> ?u (\<lambda>_. ?v) (globals_swap ?g_hrs ?g_hrs_upd ?symtab ?xs ?gs) = globals_swap ?g_hrs ?g_hrs_upd ?symtab ?xs (?g_hrs_upd (hrs_mem_update (heap_update (PTR(?'b) (?symtab ?nm)) ?v)) ?gs)

goal (1 subgoal):
 1. globals_swap g_hrs g_hrs_upd symtab xs (u (\<lambda>_. v) gs) = g_hrs_upd (hrs_mem_update (heap_update (PTR('b) (symtab nm)) v)) (globals_swap g_hrs g_hrs_upd symtab xs gs)
theory GlobalsSwap

lemma is_global_data_simps[simp]:
  "is_global_data (global_data nm g s)"
  "\<not> is_global_data (const_global_data nm v)"
  "\<not> is_global_data (addressed_global_data nm tp)" by (simp_all add: global_data_def const_global_data_def
                    is_global_data_def addressed_global_data_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_global_data (global_data nm g s) &&& \<not> is_global_data (const_global_data nm v) &&& \<not> is_global_data (addressed_global_data nm tp)
theory GlobalsSwap

lemma is_const_global_data_simps[simp]:
  "is_const_global_data (const_global_data nm v)"
  "\<not> is_const_global_data (global_data nm g s)"
  "\<not> is_const_global_data (addressed_global_data nm tp)" by (simp_all add: global_data_def const_global_data_def
                    is_const_global_data_def addressed_global_data_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_const_global_data (const_global_data nm v) &&& \<not> is_const_global_data (global_data nm g s) &&& \<not> is_const_global_data (addressed_global_data nm tp)
theory GlobalsSwap

lemma distinct_prop_swappable_optimisation:
  "distinct_prop global_data_swappable (filter is_global_data gs)
    \<Longrightarrow> distinct_prop (\<lambda>x y. global_data_swappable x y) gs" apply (simp add: distinct_prop_filter is_global_data_def
                   global_data_swappable_def) apply (erule distinct_prop_weaken) apply (simp split: global_data.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_prop global_data_swappable (filter is_global_data gs) \<Longrightarrow> distinct_prop global_data_swappable gs proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. (case x of GlobalData x xa xb xc xd \<Rightarrow> True | _ \<Rightarrow> False) \<and> (case y of GlobalData x xa xb xc xd \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (case x of GlobalData x xa xb g s \<Rightarrow> case y of GlobalData xc xd xe g' s' \<Rightarrow> (\<forall>v v' gs. s v (s' v' gs) = s' v' (s v gs)) \<and> (\<forall>v gs. g (s' v gs) = g gs) \<and> (\<forall>v gs. g' (s v gs) = g' gs) | _ \<Rightarrow> True | _ \<Rightarrow> True)) gs \<Longrightarrow> distinct_prop (\<lambda>x y. case x of GlobalData x xa xb g s \<Rightarrow> case y of GlobalData xc xd xe g' s' \<Rightarrow> (\<forall>v v' gs. s v (s' v' gs) = s' v' (s v gs)) \<and> (\<forall>v gs. g (s' v gs) = g gs) \<and> (\<forall>v gs. g' (s v gs) = g' gs) | _ \<Rightarrow> True | _ \<Rightarrow> True) gs proof (prove)
goal (1 subgoal):
 1. \<And>x y. (case x of GlobalData x xa xb xc xd \<Rightarrow> True | _ \<Rightarrow> False) \<and> (case y of GlobalData x xa xb xc xd \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (case x of GlobalData x xa xb g s \<Rightarrow> case y of GlobalData xc xd xe g' s' \<Rightarrow> (\<forall>v v' gs. s v (s' v' gs) = s' v' (s v gs)) \<and> (\<forall>v gs. g (s' v gs) = g gs) \<and> (\<forall>v gs. g' (s v gs) = g' gs) | _ \<Rightarrow> True | _ \<Rightarrow> True) \<Longrightarrow> case x of GlobalData x xa xb g s \<Rightarrow> case y of GlobalData xc xd xe g' s' \<Rightarrow> (\<forall>v v' gs. s v (s' v' gs) = s' v' (s v gs)) \<and> (\<forall>v gs. g (s' v gs) = g gs) \<and> (\<forall>v gs. g' (s v gs) = g' gs) | _ \<Rightarrow> True | _ \<Rightarrow> True proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma globals_list_valid_optimisation:
  "distinct_prop global_data_swappable (filter is_global_data gs)
    \<Longrightarrow> \<forall>g \<in> set gs. global_data_valid g_hrs g_hrs_upd g
    \<Longrightarrow> \<forall>g \<in> set gs. global_data_ok symtab g
    \<Longrightarrow> globals_list_valid symtab g_hrs g_hrs_upd gs" using globals_list_valid_def distinct_prop_swappable_optimisation by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_prop global_data_swappable (filter is_global_data gs); \<forall>g\<in>set gs. global_data_valid g_hrs g_hrs_upd g; \<forall>g\<in>set gs. global_data_ok symtab g\<rbrakk> \<Longrightarrow> globals_list_valid symtab g_hrs g_hrs_upd gs proof (prove)
using this:
globals_list_valid ?symtab ?g_hrs ?g_hrs_upd ?xs = (distinct_prop global_data_swappable ?xs \<and> (\<forall>x\<in>set ?xs. global_data_valid ?g_hrs ?g_hrs_upd x) \<and> (\<forall>x\<in>set ?xs. global_data_ok ?symtab x))
distinct_prop global_data_swappable (filter is_global_data ?gs) \<Longrightarrow> distinct_prop global_data_swappable ?gs

goal (1 subgoal):
 1. \<lbrakk>distinct_prop global_data_swappable (filter is_global_data gs); \<forall>g\<in>set gs. global_data_valid g_hrs g_hrs_upd g; \<forall>g\<in>set gs. global_data_ok symtab g\<rbrakk> \<Longrightarrow> globals_list_valid symtab g_hrs g_hrs_upd gs
theory GlobalsSwap

lemma const_globals_in_memory_h_val_eq:
  "const_globals_in_memory symtab (const_global_data nm v # xs) hmem
    = (h_val hmem (Ptr (symtab nm)) = v \<and> const_globals_in_memory symtab xs hmem)" by (simp add: const_globals_in_memory_def const_global_data_def h_val_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. const_globals_in_memory symtab (const_global_data nm v # xs) hmem = (h_val hmem (PTR('b) (symtab nm)) = v \<and> const_globals_in_memory symtab xs hmem)
theory GlobalsSwap

lemma const_globals_in_memory_other_eqs:
  "const_globals_in_memory symtab (global_data nm g s # xs) hmem
    = const_globals_in_memory symtab xs hmem"
  "const_globals_in_memory symtab (addressed_global_data nm tp # xs) hmem
    = const_globals_in_memory symtab xs hmem"
  "const_globals_in_memory symtab [] hmem" by (auto simp add: const_globals_in_memory_def
                     global_data_def addressed_global_data_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. const_globals_in_memory symtab (global_data nm g s # xs) hmem = const_globals_in_memory symtab xs hmem &&& const_globals_in_memory symtab (addressed_global_data nm tp # xs) hmem = const_globals_in_memory symtab xs hmem &&& const_globals_in_memory symtab [] hmem
theory GlobalsSwap

lemma const_globals_in_memory_h_val:
  "\<lbrakk> const_global_data nm v \<in> set xs;
    const_globals_in_memory symtab xs hmem \<rbrakk>
    \<Longrightarrow> h_val hmem (Ptr (symtab nm)) = v" apply (simp add: const_globals_in_memory_def const_global_data_def) apply (drule (1) bspec) apply (clarsimp simp: h_val_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs hmem\<rbrakk> \<Longrightarrow> h_val hmem (PTR('b) (symtab nm)) = v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ConstGlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p v) (\<lambda>xs. from_bytes xs = v) \<in> set xs; \<forall>gd\<in>set xs. case gd of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list hmem l (symtab nm)) | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> h_val hmem (PTR('b) (symtab nm)) = v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ConstGlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p v) (\<lambda>xs. from_bytes xs = v) \<in> set xs; case ConstGlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p v) (\<lambda>xs. from_bytes xs = v) of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list hmem l (symtab nm)) | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> h_val hmem (PTR('b) (symtab nm)) = v proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma const_globals_in_memory_heap_update:
  "\<lbrakk> const_globals_in_memory symtab gs hmem;
    globals_list_distinct D symtab gs;
    ptr_safe (p :: ('a :: wf_type) ptr) htd; htd_safe D htd \<rbrakk>
     \<Longrightarrow> const_globals_in_memory symtab gs (heap_update p val hmem)" apply (simp add: split_def heap_update_def) apply (erule const_globals_in_memory_heap_update_list,
         erule globals_list_distinct_filter) apply (clarsimp simp: ptr_safe_def htd_safe_def s_footprint_intvl[symmetric]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const_globals_in_memory symtab gs hmem; globals_list_distinct D symtab gs; ptr_safe p htd; htd_safe D htd\<rbrakk> \<Longrightarrow> const_globals_in_memory symtab gs (heap_update p val hmem) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const_globals_in_memory symtab gs hmem; globals_list_distinct D symtab gs; ptr_safe p htd; htd_safe D htd\<rbrakk> \<Longrightarrow> const_globals_in_memory symtab gs (heap_update_list (ptr_val p) (to_bytes val (heap_list hmem (size_of TYPE('a)) (ptr_val p))) hmem) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_distinct D symtab gs; ptr_safe p htd; htd_safe D htd\<rbrakk> \<Longrightarrow> {ptr_val p..+length (to_bytes val (heap_list hmem (size_of TYPE('a)) (ptr_val p)))} \<subseteq> D proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>globals_list_distinct D symtab gs; s_footprint p \<subseteq> dom_s htd; dom_s htd \<subseteq> D \<times> UNIV; (x, SIndexVal) \<in> s_footprint p\<rbrakk> \<Longrightarrow> x \<in> D proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma distinct_prop_memD:
  "\<lbrakk> x \<in> set zs; y \<in> set zs; distinct_prop P zs \<rbrakk>
    \<Longrightarrow> x = y \<or> P x y \<or> P y x" by (induct zs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set zs; y \<in> set zs; distinct_prop P zs\<rbrakk> \<Longrightarrow> x = y \<or> P x y \<or> P y x
theory GlobalsSwap

lemma s_footprint_intvl_subset:
  "s_footprint (p :: 'a ptr) \<subseteq> {ptr_val p ..+ size_of TYPE ('a :: c_type)} \<times> UNIV" by (auto simp: s_footprint_def s_footprint_untyped_def
                 intvl_def size_of_def)

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