theory GlobalsSwap

lemma globals_swap_update_mem_raw:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
     \<forall>hmem. (v hmem) = v'; length v' = m;
     globals_list_valid symtab g_hrs g_hrs_upd xs;
     globals_list_distinct D symtab xs;
     GlobalData nm m ok g st \<in> set xs \<rbrakk>
    \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update
            (\<lambda>hmem. heap_update_list (symtab nm) (v hmem) hmem)) gs)
        = st v' (globals_swap g_hrs g_hrs_upd symtab xs gs)" apply (clarsimp simp: in_set_conv_decomp) apply (subst globals_swap_reorder_append, simp+)+ apply (rule globals_swap_absorb_update[symmetric, where D=D], simp_all) apply (simp add: globals_list_valid_def distinct_prop_append) apply (insert global_data_swappable_sym) apply blast apply (simp add: globals_list_distinct_def ball_Un distinct_prop_append) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd xs; globals_list_distinct D symtab xs; GlobalData nm m ok g st \<in> set xs\<rbrakk> \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_mem_update (\<lambda>hmem. heap_update_list (symtab nm) (v hmem) hmem)) gs) = st v' (globals_swap g_hrs g_hrs_upd symtab xs gs) proof (prove)
goal (1 subgoal):
 1. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; globals_list_valid symtab g_hrs g_hrs_upd (ys @ GlobalData nm (length v') ok g st # zs); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs\<rbrakk> \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab (ys @ GlobalData nm (length v') ok g st # zs) (g_hrs_upd (hrs_mem_update (heap_update_list (symtab nm) v')) gs) = st v' (globals_swap g_hrs g_hrs_upd symtab (ys @ GlobalData nm (length v') ok g st # zs) gs) proof (prove)
goal (1 subgoal):
 1. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; globals_list_valid symtab g_hrs g_hrs_upd (ys @ GlobalData nm (length v') ok g st # zs); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs\<rbrakk> \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab (GlobalData nm (length v') ok g st # zs @ ys) (g_hrs_upd (hrs_mem_update (heap_update_list (symtab nm) v')) gs) = st v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm (length v') ok g st # zs @ ys) gs) proof (prove)
goal (2 subgoals):
 1. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; globals_list_valid symtab g_hrs g_hrs_upd (ys @ GlobalData nm (length v') ok g st # zs); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs\<rbrakk> \<Longrightarrow> globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm (length v') ok g st # zs @ ys)
 2. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; globals_list_valid symtab g_hrs g_hrs_upd (ys @ GlobalData nm (length v') ok g st # zs); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs\<rbrakk> \<Longrightarrow> globals_list_distinct D symtab (GlobalData nm (length v') ok g st # zs @ ys) proof (prove)
goal (2 subgoals):
 1. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; distinct_prop global_data_swappable ys \<and> Ball (set zs) (global_data_swappable (GlobalData nm (length v') ok g st)) \<and> distinct_prop global_data_swappable zs \<and> (\<forall>x\<in>set ys. global_data_swappable x (GlobalData nm (length v') ok g st) \<and> Ball (set zs) (global_data_swappable x)) \<and> global_data_valid g_hrs g_hrs_upd (GlobalData nm (length v') ok g st) \<and> Ball (set ys \<union> set zs) (global_data_valid g_hrs g_hrs_upd) \<and> global_data_ok symtab (GlobalData nm (length v') ok g st) \<and> Ball (set ys \<union> set zs) (global_data_ok symtab); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs\<rbrakk> \<Longrightarrow> Ball (set zs \<union> set ys) (global_data_swappable (GlobalData nm (length v') ok g st)) \<and> (\<forall>x\<in>set zs. Ball (set ys) (global_data_swappable x)) \<and> Ball (set zs \<union> set ys) (global_data_valid g_hrs g_hrs_upd) \<and> Ball (set zs \<union> set ys) (global_data_ok symtab)
 2. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; globals_list_valid symtab g_hrs g_hrs_upd (ys @ GlobalData nm (length v') ok g st # zs); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs\<rbrakk> \<Longrightarrow> globals_list_distinct D symtab (GlobalData nm (length v') ok g st # zs @ ys) proof (prove)
goal (2 subgoals):
 1. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; distinct_prop global_data_swappable ys \<and> Ball (set zs) (global_data_swappable (GlobalData nm (length v') ok g st)) \<and> distinct_prop global_data_swappable zs \<and> (\<forall>x\<in>set ys. global_data_swappable x (GlobalData nm (length v') ok g st) \<and> Ball (set zs) (global_data_swappable x)) \<and> global_data_valid g_hrs g_hrs_upd (GlobalData nm (length v') ok g st) \<and> Ball (set ys \<union> set zs) (global_data_valid g_hrs g_hrs_upd) \<and> global_data_ok symtab (GlobalData nm (length v') ok g st) \<and> Ball (set ys \<union> set zs) (global_data_ok symtab); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs; \<And>x y. global_data_swappable x y = global_data_swappable y x\<rbrakk> \<Longrightarrow> Ball (set zs \<union> set ys) (global_data_swappable (GlobalData nm (length v') ok g st)) \<and> (\<forall>x\<in>set zs. Ball (set ys) (global_data_swappable x)) \<and> Ball (set zs \<union> set ys) (global_data_valid g_hrs g_hrs_upd) \<and> Ball (set zs \<union> set ys) (global_data_ok symtab)
 2. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; globals_list_valid symtab g_hrs g_hrs_upd (ys @ GlobalData nm (length v') ok g st # zs); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs; \<And>x y. global_data_swappable x y = global_data_swappable y x\<rbrakk> \<Longrightarrow> globals_list_distinct D symtab (GlobalData nm (length v') ok g st # zs @ ys) proof (prove)
goal (1 subgoal):
 1. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; globals_list_valid symtab g_hrs g_hrs_upd (ys @ GlobalData nm (length v') ok g st # zs); globals_list_distinct D symtab (ys @ GlobalData nm (length v') ok g st # zs); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs; \<And>x y. global_data_swappable x y = global_data_swappable y x\<rbrakk> \<Longrightarrow> globals_list_distinct D symtab (GlobalData nm (length v') ok g st # zs @ ys) proof (prove)
goal (1 subgoal):
 1. \<And>ys zs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>hmem. v hmem = v'; globals_list_valid symtab g_hrs g_hrs_upd (ys @ GlobalData nm (length v') ok g st # zs); D \<inter> global_data_region symtab (GlobalData nm (length v') ok g st) = {} \<and> (\<forall>y\<in>set ys. D \<inter> global_data_region symtab y = {}) \<and> (\<forall>y\<in>set zs. D \<inter> global_data_region symtab y = {}) \<and> distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) ys) \<and> (\<forall>y\<in>set zs. global_data_region symtab (GlobalData nm (length v') ok g st) \<inter> global_data_region symtab y = {}) \<and> distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) zs) \<and> (\<forall>x\<in>set ys. global_data_region symtab x \<inter> global_data_region symtab (GlobalData nm (length v') ok g st) = {} \<and> (\<forall>y\<in>set zs. global_data_region symtab x \<inter> global_data_region symtab y = {})); m = length v'; xs = ys @ GlobalData nm (length v') ok g st # zs; \<And>x y. global_data_swappable x y = global_data_swappable y x\<rbrakk> \<Longrightarrow> (\<forall>y\<in>set ys. global_data_region symtab (GlobalData nm (length v') ok g st) \<inter> global_data_region symtab y = {}) \<and> (\<forall>x\<in>set zs. \<forall>y\<in>set ys. global_data_region symtab x \<inter> global_data_region symtab y = {}) proof (prove)
goal:
No subgoals!