theory GlobalsSwap

lemma disjoint_heap_update_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 :: ('a :: wf_type) ptr) \<subseteq> D \<times> UNIV \<rbrakk>
     \<Longrightarrow> g_hrs_upd (hrs_mem_update (heap_update p 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 p v)) gs)" apply (clarsimp simp: globals_swap_def global_acc_valid_def) apply (rule foldr_update_commutes) apply (clarsimp simp: global_swap_def hrs_mem_update h_val_def
                        heap_update_def o_def K_def
                        globals_list_distinct_def
                 split: global_data.split) apply (drule spec, drule mp, erule conjI, simp add: is_global_data_def) apply (rule_tac f="g_hrs_upd" in arg_cong2[rotated]) apply (subst heap_list_update_disjoint_same, simp_all) apply (rule ptr_set_disjoint_footprint) apply (simp add: global_data_region_def) apply blast apply (clarsimp simp: hrs_mem_update_def split_def) apply (subst heap_update_list_commute) apply (simp add: to_bytes_def length_fa_ti size_of_def
                    global_data_region_def) apply (intro disjoint_int_intvl_min
                ptr_set_disjoint_footprint[unfolded size_of_def]) apply blast apply (subst heap_list_update_disjoint_same,
         simp_all add: global_data_region_def) apply (simp add: Int_commute) apply (intro disjoint_int_intvl_min
               ptr_set_disjoint_footprint) apply blast 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> g_hrs_upd (hrs_mem_update (heap_update p 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 p v)) gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_distinct D symtab (filter is_global_data xs); s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f \<circ> f') s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s\<rbrakk> \<Longrightarrow> g_hrs_upd (hrs_mem_update (heap_update p v)) (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = foldr (global_swap g_hrs g_hrs_upd symtab) xs (g_hrs_upd (hrs_mem_update (heap_update p v)) gs) proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>globals_list_distinct D symtab (filter is_global_data xs); s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f \<circ> f') s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; x \<in> set xs\<rbrakk> \<Longrightarrow> g_hrs_upd (hrs_mem_update (heap_update p v)) (global_swap g_hrs g_hrs_upd symtab x s) = global_swap g_hrs g_hrs_upd symtab x (g_hrs_upd (hrs_mem_update (heap_update p v)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; \<forall>y. y \<in> set xs \<and> is_global_data y \<longrightarrow> D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs))\<rbrakk> \<Longrightarrow> g_hrs_upd (\<lambda>x. hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s)))) (g_hrs s))) (x15 (heap_list (hrs_mem (g_hrs s)) x12 (symtab x11)) (g_hrs_upd (\<lambda>y. undefined) s)) = g_hrs_upd (\<lambda>_. hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s)))) (hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (g_hrs s))) (x15 (heap_list (heap_update_list (ptr_val p) (to_bytes v (heap_list (hrs_mem (g_hrs s)) (size_of TYPE('a)) (ptr_val p))) (hrs_mem (g_hrs s))) x12 (symtab x11)) (g_hrs_upd (\<lambda>x. undefined) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> g_hrs_upd (\<lambda>x. hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s)))) (g_hrs s))) (x15 (heap_list (hrs_mem (g_hrs s)) x12 (symtab x11)) (g_hrs_upd (\<lambda>y. undefined) s)) = g_hrs_upd (\<lambda>_. hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s)))) (hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (g_hrs s))) (x15 (heap_list (heap_update_list (ptr_val p) (to_bytes v (heap_list (hrs_mem (g_hrs s)) (size_of TYPE('a)) (ptr_val p))) (hrs_mem (g_hrs s))) x12 (symtab x11)) (g_hrs_upd (\<lambda>x. undefined) s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> x15 (heap_list (hrs_mem (g_hrs s)) x12 (symtab x11)) (g_hrs_upd (\<lambda>y. undefined) s) = x15 (heap_list (heap_update_list (ptr_val p) (to_bytes v (heap_list (hrs_mem (g_hrs s)) (size_of TYPE('a)) (ptr_val p))) (hrs_mem (g_hrs s))) x12 (symtab x11)) (g_hrs_upd (\<lambda>x. undefined) s)
 2. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s)))) (g_hrs s))) = (\<lambda>_. hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s)))) (hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (g_hrs s))) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> {ptr_val p..+size_of TYPE('a)} \<inter> {symtab x11..+x12} = {}
 2. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s)))) (g_hrs s))) = (\<lambda>_. hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s)))) (hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (g_hrs s))) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> {symtab x11..+x12} \<times> UNIV = {}
 2. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s)))) (g_hrs s))) = (\<lambda>_. hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s)))) (hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (g_hrs s))) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> {symtab x11..+x12} = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> {symtab x11..+x12} \<times> UNIV = {}
 2. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s)))) (g_hrs s))) = (\<lambda>_. hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s)))) (hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (g_hrs s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s)))) (g_hrs s))) = (\<lambda>_. hrs_mem_update (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s)))) (hrs_mem_update (\<lambda>a. heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('a)) (ptr_val p))) a) (g_hrs s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. (heap_update_list (ptr_val p) (to_bytes v (heap_list (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (fst (g_hrs s))) (size_of TYPE('a)) (ptr_val p))) (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (fst (g_hrs s))), snd (g_hrs s))) = (\<lambda>_. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (fst (g_hrs s)) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x12 x13 x14 x15 x. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> {ptr_val p..+length (to_bytes v (heap_list (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (fst (g_hrs s))) (size_of TYPE('a)) (ptr_val p)))} \<inter> {symtab x11..+length (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s)))} = {}
 2. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (fst (g_hrs s))) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) = (\<lambda>_. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (fst (g_hrs s)) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> {symtab x11..+x12} = {}\<rbrakk> \<Longrightarrow> {ptr_val p..+size_td (typ_info_t TYPE('a))} \<inter> {symtab x11..+min (length (x14 (g_hrs_upd (\<lambda>y. undefined) s))) x12} = {}
 2. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (fst (g_hrs s))) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) = (\<lambda>_. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (fst (g_hrs s)) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> {symtab x11..+x12} = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> {symtab x11..+x12} \<times> UNIV = {}
 2. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (fst (g_hrs s))) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) = (\<lambda>_. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (fst (g_hrs s)) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> (\<lambda>x. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (fst (g_hrs s))) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) = (\<lambda>_. (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>x. undefined) s))) (heap_update_list (ptr_val p) (to_bytes v (heap_list (fst (g_hrs s)) (size_of TYPE('a)) (ptr_val p))) (fst (g_hrs s))), snd (g_hrs s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> {symtab x11..+x12} = {}\<rbrakk> \<Longrightarrow> {symtab x11..+min (length (x14 (g_hrs_upd (\<lambda>y. undefined) s))) x12} \<inter> {ptr_val p..+size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> {symtab x11..+x12} = {}\<rbrakk> \<Longrightarrow> {ptr_val p..+size_of TYPE('a)} \<inter> {symtab x11..+min (length (x14 (g_hrs_upd (\<lambda>y. undefined) s))) x12} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>s_footprint p \<subseteq> D \<times> UNIV; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); D \<inter> {symtab x11..+x12} = {}\<rbrakk> \<Longrightarrow> s_footprint p \<inter> {symtab x11..+x12} \<times> UNIV = {} proof (prove)
goal:
No subgoals!