theory GlobalsSwap

lemma const_globals_in_memory_heap_update_list:
  "\<lbrakk> const_globals_in_memory symtab xs hmem;
    globals_list_distinct D symtab (filter is_const_global_data xs);
    {p ..+ length ys} \<subseteq> D \<rbrakk>
    \<Longrightarrow> const_globals_in_memory symtab xs (heap_update_list p ys hmem)" apply (clarsimp simp: const_globals_in_memory_def globals_list_distinct_def
                 split: global_data.split) apply (drule(1) bspec) apply (drule spec, drule mp, erule conjI, simp add: is_const_global_data_def) apply (simp add: global_data_region_def) apply (subst heap_list_update_disjoint_same) apply blast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const_globals_in_memory symtab xs hmem; globals_list_distinct D symtab (filter is_const_global_data xs); {p..+length ys} \<subseteq> D\<rbrakk> \<Longrightarrow> const_globals_in_memory symtab xs (heap_update_list p ys hmem) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>\<forall>x\<in>set xs. case x of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list hmem l (symtab nm)) | _ \<Rightarrow> True; {p..+length ys} \<subseteq> D; ConstGlobalData x21 x22 x23 x24 x25 \<in> set xs; \<forall>y. y \<in> set xs \<and> is_const_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_const_global_data xs))\<rbrakk> \<Longrightarrow> x25 (heap_list (heap_update_list p ys hmem) x22 (symtab x21)) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>{p..+length ys} \<subseteq> D; ConstGlobalData x21 x22 x23 x24 x25 \<in> set xs; \<forall>y. y \<in> set xs \<and> is_const_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_const_global_data xs)); case ConstGlobalData x21 x22 x23 x24 x25 of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list hmem l (symtab nm)) | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> x25 (heap_list (heap_update_list p ys hmem) x22 (symtab x21)) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>{p..+length ys} \<subseteq> D; ConstGlobalData x21 x22 x23 x24 x25 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_const_global_data xs)); case ConstGlobalData x21 x22 x23 x24 x25 of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list hmem l (symtab nm)) | _ \<Rightarrow> True; D \<inter> global_data_region symtab (ConstGlobalData x21 x22 x23 x24 x25) = {}\<rbrakk> \<Longrightarrow> x25 (heap_list (heap_update_list p ys hmem) x22 (symtab x21)) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>{p..+length ys} \<subseteq> D; ConstGlobalData x21 x22 x23 x24 x25 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_const_global_data xs)); x25 (heap_list hmem x22 (symtab x21)); D \<inter> {symtab x21..+x22} = {}\<rbrakk> \<Longrightarrow> x25 (heap_list (heap_update_list p ys hmem) x22 (symtab x21)) proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>{p..+length ys} \<subseteq> D; ConstGlobalData x21 x22 x23 x24 x25 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_const_global_data xs)); x25 (heap_list hmem x22 (symtab x21)); D \<inter> {symtab x21..+x22} = {}\<rbrakk> \<Longrightarrow> {p..+length ys} \<inter> {symtab x21..+x22} = {}
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>{p..+length ys} \<subseteq> D; ConstGlobalData x21 x22 x23 x24 x25 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_const_global_data xs)); x25 (heap_list hmem x22 (symtab x21)); D \<inter> {symtab x21..+x22} = {}\<rbrakk> \<Longrightarrow> x25 (heap_list hmem x22 (symtab x21)) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>{p..+length ys} \<subseteq> D; ConstGlobalData x21 x22 x23 x24 x25 \<in> set xs; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_const_global_data xs)); x25 (heap_list hmem x22 (symtab x21)); D \<inter> {symtab x21..+x22} = {}\<rbrakk> \<Longrightarrow> x25 (heap_list hmem x22 (symtab x21)) proof (prove)
goal:
No subgoals!