theory GlobalsSwap

lemma const_globals_in_memory_to_h_val_with_swap:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
    globals_list_distinct D symtab xs;
    const_global_data nm v \<in> set xs;
    const_globals_in_memory symtab xs (hrs_mem (g_hrs gs)) \<rbrakk>
    \<Longrightarrow> v = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs)))
        (Ptr (symtab nm))" apply (subst disjoint_h_val_globals_swap_filter, assumption,
    erule(1) globals_list_distinct_filter_member) apply simp apply (simp add: global_data_region_def const_global_data_def) apply (rule order_trans, rule s_footprint_intvl_subset) apply simp apply (erule(1) const_globals_in_memory_h_val[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> v = h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) (PTR('b) (symtab nm)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> \<not> is_global_data (const_global_data nm v)
 2. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> s_footprint (PTR('b) (symtab nm)) \<subseteq> global_data_region symtab (const_global_data nm v) \<times> UNIV
 3. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> v = h_val (hrs_mem (g_hrs gs)) (PTR('b) (symtab nm)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> s_footprint (PTR('b) (symtab nm)) \<subseteq> global_data_region symtab (const_global_data nm v) \<times> UNIV
 2. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> v = h_val (hrs_mem (g_hrs gs)) (PTR('b) (symtab nm)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; ConstGlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p v) (\<lambda>xs. from_bytes xs = v) \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> s_footprint (PTR('b) (symtab nm)) \<subseteq> {symtab nm..+size_of TYPE('b)} \<times> UNIV
 2. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> v = h_val (hrs_mem (g_hrs gs)) (PTR('b) (symtab nm)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; ConstGlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p v) (\<lambda>xs. from_bytes xs = v) \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> {ptr_val (PTR('b) (symtab nm))..+size_of TYPE('b)} \<times> UNIV \<subseteq> {symtab nm..+size_of TYPE('b)} \<times> UNIV
 2. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> v = h_val (hrs_mem (g_hrs gs)) (PTR('b) (symtab nm)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data nm v \<in> set xs; const_globals_in_memory symtab xs (hrs_mem (g_hrs gs))\<rbrakk> \<Longrightarrow> v = h_val (hrs_mem (g_hrs gs)) (PTR('b) (symtab nm)) proof (prove)
goal:
No subgoals!