theory GlobalsSwap

lemma const_globals_in_memory_heap_update_global:
  "\<lbrakk> const_globals_in_memory symtab gs hmem;
     global_data nm (getter :: 'g \<Rightarrow> 'a) setter \<in> set gs;
     globals_list_distinct D symtab gs \<rbrakk>
    \<Longrightarrow> const_globals_in_memory symtab gs
        (heap_update (Ptr (symtab nm)) (v :: 'a :: packed_type) hmem)" apply (simp add: heap_update_def split_def) apply (erule const_globals_in_memory_heap_update_list[OF _ _ order_refl]) apply (clarsimp simp: globals_list_distinct_def distinct_prop_map
                        distinct_prop_filter) apply (simp add: distinct_prop_weaken) apply clarsimp apply (drule(2) distinct_prop_memD) apply (auto simp: global_data_region_def global_data_def
                    is_const_global_data_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const_globals_in_memory symtab gs hmem; global_data nm getter setter \<in> set gs; globals_list_distinct D symtab gs\<rbrakk> \<Longrightarrow> const_globals_in_memory symtab gs (heap_update (PTR('a) (symtab nm)) v hmem) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>const_globals_in_memory symtab gs hmem; global_data nm getter setter \<in> set gs; globals_list_distinct D symtab gs\<rbrakk> \<Longrightarrow> const_globals_in_memory symtab gs (heap_update_list (symtab nm) (to_bytes v (heap_list hmem (size_of TYPE('a)) (symtab nm))) hmem) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm getter setter \<in> set gs; globals_list_distinct D symtab gs\<rbrakk> \<Longrightarrow> globals_list_distinct {symtab nm..+length (to_bytes v (heap_list hmem (size_of TYPE('a)) (symtab nm)))} symtab (filter is_const_global_data gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm getter setter \<in> set gs; \<forall>y\<in>set gs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>x y. global_data_region symtab x \<inter> global_data_region symtab y = {}) gs\<rbrakk> \<Longrightarrow> (\<forall>y. y \<in> set gs \<and> is_const_global_data y \<longrightarrow> {symtab nm..+size_of TYPE('a)} \<inter> global_data_region symtab y = {}) \<and> distinct_prop (\<lambda>x y. is_const_global_data x \<and> is_const_global_data y \<longrightarrow> global_data_region symtab x \<inter> global_data_region symtab y = {}) gs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm getter setter \<in> set gs; \<forall>y\<in>set gs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>x y. global_data_region symtab x \<inter> global_data_region symtab y = {}) gs\<rbrakk> \<Longrightarrow> \<forall>y. y \<in> set gs \<and> is_const_global_data y \<longrightarrow> {symtab nm..+size_of TYPE('a)} \<inter> global_data_region symtab y = {} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>global_data nm getter setter \<in> set gs; \<forall>y\<in>set gs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>x y. global_data_region symtab x \<inter> global_data_region symtab y = {}) gs; y \<in> set gs; is_const_global_data y\<rbrakk> \<Longrightarrow> {symtab nm..+size_of TYPE('a)} \<inter> global_data_region symtab y = {} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<forall>y\<in>set gs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>x y. global_data_region symtab x \<inter> global_data_region symtab y = {}) gs; y \<in> set gs; is_const_global_data y; global_data nm getter setter = y \<or> global_data_region symtab (global_data nm getter setter) \<inter> global_data_region symtab y = {} \<or> global_data_region symtab y \<inter> global_data_region symtab (global_data nm getter setter) = {}\<rbrakk> \<Longrightarrow> {symtab nm..+size_of TYPE('a)} \<inter> global_data_region symtab y = {} proof (prove)
goal:
No subgoals!