theory GlobalsSwap

lemma disjoint_heap_list_globals_swap_filter:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
     globals_list_distinct D symtab (filter is_global_data xs);
     {p ..+ n} \<subseteq> D \<rbrakk>
     \<Longrightarrow> heap_list (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) n p
            = heap_list (hrs_mem (g_hrs gs)) n p" apply (clarsimp simp: globals_swap_def) apply (rule foldr_does_nothing_to_xf) apply (clarsimp simp: global_swap_def hrs_mem_update
                        global_acc_valid_def globals_list_distinct_def
                 split: global_data.split) apply (subst heap_list_update_disjoint_same, simp_all) apply (drule spec, drule mp, erule conjI, simp add: is_global_data_def) apply (simp add: Int_commute global_data_region_def) apply (rule disjoint_int_intvl_min) 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); {p..+n} \<subseteq> D\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) n p = heap_list (hrs_mem (g_hrs gs)) n 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); {p..+n} \<subseteq> D\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (g_hrs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs))) n p = heap_list (hrs_mem (g_hrs gs)) n p proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab (filter is_global_data xs); {p..+n} \<subseteq> D; x \<in> set xs\<rbrakk> \<Longrightarrow> heap_list (hrs_mem (g_hrs (global_swap g_hrs g_hrs_upd symtab x s))) n p = heap_list (hrs_mem (g_hrs s)) n p proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>{p..+n} \<subseteq> D; GlobalData x11 x12 x13 x14 x15 \<in> set xs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<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)); \<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> heap_list (heap_update_list (symtab x11) (take x12 (x14 (g_hrs_upd (\<lambda>y. undefined) s))) (hrs_mem (g_hrs s))) n p = heap_list (hrs_mem (g_hrs s)) n p proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>{p..+n} \<subseteq> D; GlobalData x11 x12 x13 x14 x15 \<in> set xs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<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)); \<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> {symtab x11..+min (length (x14 (g_hrs_upd (\<lambda>y. undefined) s))) x12} \<inter> {p..+n} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>{p..+n} \<subseteq> D; GlobalData x11 x12 x13 x14 x15 \<in> set xs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); \<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; D \<inter> global_data_region symtab (GlobalData x11 x12 x13 x14 x15) = {}\<rbrakk> \<Longrightarrow> {symtab x11..+min (length (x14 (g_hrs_upd (\<lambda>y. undefined) s))) x12} \<inter> {p..+n} = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x11 x12 x13 x14 x15. \<lbrakk>{p..+n} \<subseteq> D; GlobalData x11 x12 x13 x14 x15 \<in> set xs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); \<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; D \<inter> {symtab x11..+x12} = {}\<rbrakk> \<Longrightarrow> {p..+n} \<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>{p..+n} \<subseteq> D; GlobalData x11 x12 x13 x14 x15 \<in> set xs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter is_global_data xs)); \<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; D \<inter> {symtab x11..+x12} = {}\<rbrakk> \<Longrightarrow> {p..+n} \<inter> {symtab x11..+x12} = {} proof (prove)
goal:
No subgoals!