theory GlobalsSwap

lemma globals_swap_hrs_htd_update:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
        globals_list_valid symtab g_hrs g_hrs_upd xs \<rbrakk>
    \<Longrightarrow> g_hrs_upd (hrs_htd_update ufn) (globals_swap g_hrs g_hrs_upd symtab xs gs)
         = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_htd_update ufn) gs)" apply (clarsimp simp: globals_swap_def hrs_htd_update
                        global_acc_valid_def) apply (rule foldr_update_commutes) apply (clarsimp simp: globals_list_valid_def, drule(1) bspec) apply (simp add: global_swap_def o_def global_data_valid_def
                   hrs_htd_update
            split: global_data.split_asm prod.split bool.split) apply (simp add: hrs_htd_update_def hrs_mem_update_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_valid symtab g_hrs g_hrs_upd xs\<rbrakk> \<Longrightarrow> g_hrs_upd (hrs_htd_update ufn) (globals_swap g_hrs g_hrs_upd symtab xs gs) = globals_swap g_hrs g_hrs_upd symtab xs (g_hrs_upd (hrs_htd_update ufn) gs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_valid symtab g_hrs g_hrs_upd xs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f \<circ> f') s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s\<rbrakk> \<Longrightarrow> g_hrs_upd (hrs_htd_update ufn) (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = foldr (global_swap g_hrs g_hrs_upd symtab) xs (g_hrs_upd (hrs_htd_update ufn) gs) proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>globals_list_valid symtab g_hrs g_hrs_upd xs; \<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f \<circ> f') s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; x \<in> set xs\<rbrakk> \<Longrightarrow> g_hrs_upd (hrs_htd_update ufn) (global_swap g_hrs g_hrs_upd symtab x s) = global_swap g_hrs g_hrs_upd symtab x (g_hrs_upd (hrs_htd_update ufn) s) proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>\<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (f \<circ> f') s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; x \<in> set xs; distinct_prop global_data_swappable xs; \<forall>x\<in>set xs. global_data_ok symtab x; global_data_valid g_hrs g_hrs_upd x\<rbrakk> \<Longrightarrow> g_hrs_upd (hrs_htd_update ufn) (global_swap g_hrs g_hrs_upd symtab x s) = global_swap g_hrs g_hrs_upd symtab x (g_hrs_upd (hrs_htd_update ufn) s) proof (prove)
goal (1 subgoal):
 1. \<And>x s x11 x12 x13 x14 x15. \<lbrakk>\<forall>f s. g_hrs (g_hrs_upd f s) = f (g_hrs s); \<forall>f f' s. g_hrs_upd f (g_hrs_upd f' s) = g_hrs_upd (\<lambda>x. f (f' x)) s; \<forall>s. g_hrs_upd (\<lambda>_. g_hrs s) s = s; GlobalData x11 x12 x13 x14 x15 \<in> set xs; distinct_prop global_data_swappable xs; \<forall>x\<in>set xs. global_data_ok symtab x; x = GlobalData x11 x12 x13 x14 x15; (\<forall>gs. length (x14 gs) = x12) \<and> (\<forall>v v' gs. x15 v (x15 v' gs) = x15 v gs) \<and> (\<forall>gs. x15 (x14 gs) gs = gs) \<and> (\<forall>v. length v = x12 \<longrightarrow> (\<forall>gs. x14 (x15 v gs) = v)) \<and> (\<forall>v f gs. x15 v (g_hrs_upd f gs) = g_hrs_upd f (x15 v gs)) \<and> (\<forall>v gs. g_hrs (x15 v gs) = g_hrs gs) \<and> (\<forall>f gs. x14 (g_hrs_upd f gs) = x14 gs) \<and> x12 < addr_card\<rbrakk> \<Longrightarrow> g_hrs_upd (\<lambda>x. hrs_htd_update ufn (hrs_mem_update (heap_update_list (symtab x11) (x14 s)) (g_hrs s))) (x15 (heap_list (hrs_mem (g_hrs s)) x12 (symtab x11)) s) = g_hrs_upd (\<lambda>x. hrs_mem_update (heap_update_list (symtab x11) (x14 s)) (hrs_htd_update ufn (g_hrs s))) (x15 (heap_list (hrs_mem (g_hrs s)) x12 (symtab x11)) s) proof (prove)
goal:
No subgoals!