theory GlobalsSwap

lemma const_globals_in_memory_after_swap:
  "global_acc_valid t_hrs_' t_hrs_'_update
    \<Longrightarrow> globals_list_distinct D symbol_table gxs
    \<Longrightarrow> const_globals_in_memory symbol_table gxs
            (hrs_mem (t_hrs_' (globals_swap t_hrs_' t_hrs_'_update symbol_table gxs gs)))
        = const_globals_in_memory symbol_table gxs (hrs_mem (t_hrs_' gs))" apply (simp add: const_globals_in_memory_def) apply (rule ball_cong, simp_all) apply (clarsimp split: global_data.split) apply (subst disjoint_heap_list_globals_swap_filter[OF _ _ order_refl],
    assumption+, simp_all) apply (clarsimp simp: globals_list_distinct_def distinct_prop_map
                        distinct_prop_filter distinct_prop_weaken) apply (drule(2) distinct_prop_memD) apply (clarsimp simp: is_global_data_def ball_Un distinct_prop_append
                        global_data_region_def Int_commute
                 split: global_data.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid t_hrs_' t_hrs_'_update; globals_list_distinct D symbol_table gxs\<rbrakk> \<Longrightarrow> const_globals_in_memory symbol_table gxs (hrs_mem (t_hrs_' (globals_swap t_hrs_' t_hrs_'_update symbol_table gxs gs))) = const_globals_in_memory symbol_table gxs (hrs_mem (t_hrs_' gs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid t_hrs_' t_hrs_'_update; globals_list_distinct D symbol_table gxs\<rbrakk> \<Longrightarrow> (\<forall>gd\<in>set gxs. case gd of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list (hrs_mem (t_hrs_' (globals_swap t_hrs_' t_hrs_'_update symbol_table gxs gs))) l (symbol_table nm)) | _ \<Rightarrow> True) = (\<forall>gd\<in>set gxs. case gd of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list (hrs_mem (t_hrs_' gs)) l (symbol_table nm)) | _ \<Rightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>gd. \<lbrakk>global_acc_valid t_hrs_' t_hrs_'_update; globals_list_distinct D symbol_table gxs; gd \<in> set gxs\<rbrakk> \<Longrightarrow> (case gd of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list (hrs_mem (t_hrs_' (globals_swap t_hrs_' t_hrs_'_update symbol_table gxs gs))) l (symbol_table nm)) | _ \<Rightarrow> True) = (case gd of ConstGlobalData nm l ok v chk \<Rightarrow> chk (heap_list (hrs_mem (t_hrs_' gs)) l (symbol_table nm)) | _ \<Rightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>global_acc_valid t_hrs_' t_hrs_'_update; globals_list_distinct D symbol_table gxs; ConstGlobalData x21 x22 x23 x24 x25 \<in> set gxs\<rbrakk> \<Longrightarrow> x25 (heap_list (hrs_mem (t_hrs_' (globals_swap t_hrs_' t_hrs_'_update symbol_table gxs gs))) x22 (symbol_table x21)) = x25 (heap_list (hrs_mem (t_hrs_' gs)) x22 (symbol_table x21)) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25. \<lbrakk>global_acc_valid t_hrs_' t_hrs_'_update; globals_list_distinct D symbol_table gxs; ConstGlobalData x21 x22 x23 x24 x25 \<in> set gxs\<rbrakk> \<Longrightarrow> globals_list_distinct {symbol_table x21..+x22} symbol_table (filter is_global_data gxs) proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25 y. \<lbrakk>global_acc_valid t_hrs_' t_hrs_'_update; ConstGlobalData x21 x22 x23 x24 x25 \<in> set gxs; \<forall>y\<in>set gxs. D \<inter> global_data_region symbol_table y = {}; distinct_prop (\<lambda>x y. global_data_region symbol_table x \<inter> global_data_region symbol_table y = {}) gxs; y \<in> set gxs; is_global_data y\<rbrakk> \<Longrightarrow> {symbol_table x21..+x22} \<inter> global_data_region symbol_table y = {} proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 x25 y. \<lbrakk>global_acc_valid t_hrs_' t_hrs_'_update; \<forall>y\<in>set gxs. D \<inter> global_data_region symbol_table y = {}; distinct_prop (\<lambda>x y. global_data_region symbol_table x \<inter> global_data_region symbol_table y = {}) gxs; y \<in> set gxs; is_global_data y; ConstGlobalData x21 x22 x23 x24 x25 = y \<or> global_data_region symbol_table (ConstGlobalData x21 x22 x23 x24 x25) \<inter> global_data_region symbol_table y = {} \<or> global_data_region symbol_table y \<inter> global_data_region symbol_table (ConstGlobalData x21 x22 x23 x24 x25) = {}\<rbrakk> \<Longrightarrow> {symbol_table x21..+x22} \<inter> global_data_region symbol_table y = {} proof (prove)
goal:
No subgoals!