theory GlobalsSwap

lemma globals_swap_absorb_update:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
     \<forall>s. v (g_hrs s) = v'; length v' = m;
     globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # xs);
     globals_list_distinct D symtab (GlobalData nm m ok g s # xs) \<rbrakk>
    \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs)
        = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs)
               (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)" apply (induct xs) apply (simp add: globals_swap_def global_acc_valid_def) apply (simp add: global_swap_def global_data_def hrs_mem_update) apply (simp add: globals_list_valid_def global_data_valid_def K_def o_def) apply (simp add: hrs_mem_def hrs_mem_update_def split_def
                    heap_update_def h_val_def heap_update_list_overwrite
                    heap_list_update_eq order_less_imp_le
               del: SepCode.inv_p) apply (drule meta_mp, simp add: globals_list_valid_def globals_list_distinct_def)+ apply (rename_tac x xs) apply (subgoal_tac "\<forall>gs.
                globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs
                 = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs)") apply (subgoal_tac "\<forall>gs. s v' (global_swap g_hrs g_hrs_upd symtab x gs) = global_swap g_hrs g_hrs_upd symtab x (s v' gs)") apply (simp add: global_acc_valid_def) apply (clarsimp simp: globals_list_valid_def global_data_swappable_def
                         global_data_def global_swap_def K_def
                         global_data_valid_def order_less_imp_le
               simp del: SepCode.inv_p split: global_data.split_asm prod.split bool.split) apply (clarsimp simp: globals_swap_def globals_list_distinct_def
                        global_data_def globals_list_valid_def) apply (rule global_swap_swap, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd [GlobalData nm m ok g s]; globals_list_distinct D symtab [GlobalData nm m ok g s]\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab [GlobalData nm m ok g s] gs) = globals_swap g_hrs g_hrs_upd symtab [GlobalData nm m ok g s] (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)
 2. \<And>x1 xs. \<lbrakk>\<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x1 # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x1 # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s)) \<and> (\<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f \<circ> f') s) \<and> (\<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s); \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd [GlobalData nm m ok g s]; globals_list_distinct D symtab [GlobalData nm m ok g s]\<rbrakk> \<Longrightarrow> s v' (global_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s) gs) = global_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)
 2. \<And>x1 xs. \<lbrakk>\<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x1 # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x1 # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s)) \<and> (\<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f \<circ> f') s) \<and> (\<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s); \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd [GlobalData nm m ok g s]; globals_list_distinct D symtab [GlobalData nm m ok g s]\<rbrakk> \<Longrightarrow> s v' (g_hrs_upd (\<lambda>_. hrs_mem_update (heap_update_list (symtab nm) (take m (g (g_hrs_upd (\<lambda>y. undefined) gs)))) (g_hrs gs)) (s (heap_list (hrs_mem (g_hrs gs)) m (symtab nm)) (g_hrs_upd (\<lambda>y. undefined) gs))) = g_hrs_upd (\<lambda>_. hrs_mem_update (heap_update_list (symtab nm) (take m (g (g_hrs_upd (\<lambda>y. undefined) gs)))) (hrs_mem_update (heap_update_list (symtab nm) v') (g_hrs gs))) (s (heap_list (heap_update_list (symtab nm) v' (hrs_mem (g_hrs gs))) m (symtab nm)) (g_hrs_upd (\<lambda>y. undefined) gs))
 2. \<And>x1 xs. \<lbrakk>\<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x1 # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x1 # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s)) \<and> (\<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s) \<and> (\<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s); \<forall>s. v (g_hrs s) = v'; length v' = m; (\<forall>gs. length (g gs) = m) \<and> (\<forall>v v' gs. s v (s v' gs) = s v gs) \<and> (\<forall>gs. s (g gs) gs = gs) \<and> (\<forall>v. length v = m \<longrightarrow> (\<forall>gs. g (s v gs) = v)) \<and> (\<forall>v f gs. s v (g_hrs_upd f gs) = g_hrs_upd f (s v gs)) \<and> (\<forall>v gs. g_hrs (s v gs) = g_hrs gs) \<and> (\<forall>f gs. g (g_hrs_upd f gs) = g gs) \<and> m < addr_card \<and> global_data_ok symtab (GlobalData nm m ok g s); globals_list_distinct D symtab [GlobalData nm m ok g s]\<rbrakk> \<Longrightarrow> g_hrs_upd (\<lambda>x. hrs_mem_update (heap_update_list (symtab nm) (g gs)) (g_hrs gs)) (s v' gs) = g_hrs_upd (\<lambda>x. hrs_mem_update (heap_update_list (symtab nm) (g gs)) (hrs_mem_update (heap_update_list (symtab nm) v') (g_hrs gs))) (s (heap_list (heap_update_list (symtab nm) v' (hrs_mem (g_hrs gs))) m (symtab nm)) gs)
 2. \<And>x1 xs. \<lbrakk>\<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x1 # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x1 # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs) proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>\<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x1 # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x1 # xs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs) proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x1 # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x1 # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x1 # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs) proof (prove)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); \<forall>gs. globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)
 2. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)\<rbrakk> \<Longrightarrow> \<forall>gs. globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) proof (prove)
goal (3 subgoals):
 1. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); \<forall>gs. globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs); \<forall>gs. s v' (global_swap g_hrs g_hrs_upd symtab x gs) = global_swap g_hrs g_hrs_upd symtab x (s v' gs)\<rbrakk> \<Longrightarrow> s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)
 2. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); \<forall>gs. globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs)\<rbrakk> \<Longrightarrow> \<forall>gs. s v' (global_swap g_hrs g_hrs_upd symtab x gs) = global_swap g_hrs g_hrs_upd symtab x (s v' gs)
 3. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)\<rbrakk> \<Longrightarrow> \<forall>gs. globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) proof (prove)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs); \<forall>gs. globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs)\<rbrakk> \<Longrightarrow> \<forall>gs. s v' (global_swap g_hrs g_hrs_upd symtab x gs) = global_swap g_hrs g_hrs_upd symtab x (s v' gs)
 2. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)\<rbrakk> \<Longrightarrow> \<forall>gs. globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; length v' = m; globals_list_valid symtab g_hrs g_hrs_upd (GlobalData nm m ok g s # x # xs); globals_list_distinct D symtab (GlobalData nm m ok g s # x # xs); s v' (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) = globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)\<rbrakk> \<Longrightarrow> \<forall>gs. globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # x # xs) gs = global_swap g_hrs g_hrs_upd symtab x (globals_swap g_hrs g_hrs_upd symtab (GlobalData nm m ok g s # xs) gs) proof (prove)
goal (1 subgoal):
 1. \<And>x xs gsa. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; \<forall>s. v (g_hrs s) = v'; s v' (global_swap g_hrs g_hrs_upd symtab (GlobalData nm (length v') ok g s) (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs)) = global_swap g_hrs g_hrs_upd symtab (GlobalData nm (length v') ok g s) (foldr (global_swap g_hrs g_hrs_upd symtab) xs (g_hrs_upd (\<lambda>hrs. hrs_mem_update (heap_update_list (symtab nm) (v hrs)) hrs) gs)); m = length v'; global_data_swappable (GlobalData nm (length v') ok g s) x; D \<inter> global_data_region symtab (GlobalData nm (length v') ok g s) = {}; \<forall>x\<in>set xs. global_data_swappable (GlobalData nm (length v') ok g s) x; D \<inter> global_data_region symtab x = {}; \<forall>xa\<in>set xs. global_data_swappable x xa; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; distinct_prop global_data_swappable xs; global_data_region symtab (GlobalData nm (length v') ok g s) \<inter> global_data_region symtab x = {}; global_data_valid g_hrs g_hrs_upd (GlobalData nm (length v') ok g s); \<forall>y\<in>set xs. global_data_region symtab (GlobalData nm (length v') ok g s) \<inter> global_data_region symtab y = {}; global_data_valid g_hrs g_hrs_upd x; \<forall>y\<in>set xs. global_data_region symtab x \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs); \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x; global_data_ok symtab (GlobalData nm (length v') ok g s); global_data_ok symtab x; \<forall>x\<in>set xs. global_data_ok symtab x\<rbrakk> \<Longrightarrow> global_swap g_hrs g_hrs_upd symtab (GlobalData nm (length v') ok g s) (global_swap g_hrs g_hrs_upd symtab x (foldr (global_swap g_hrs g_hrs_upd symtab) xs gsa)) = global_swap g_hrs g_hrs_upd symtab x (global_swap g_hrs g_hrs_upd symtab (GlobalData nm (length v') ok g s) (foldr (global_swap g_hrs g_hrs_upd symtab) xs gsa)) proof (prove)
goal:
No subgoals!