theory GlobalsSwap

lemma globals_swap_twice_helper:
  "\<lbrakk> globals_list_valid symtab g_hrs g_hrs_upd xs;
        global_acc_valid g_hrs g_hrs_upd;
        globals_list_distinct D symtab xs \<rbrakk>
   \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab xs (globals_swap g_hrs g_hrs_upd symtab xs gs) = gs" apply (simp add: globals_swap_def) apply (clarsimp simp: foldr_hrs_htd_global_swap globals_list_valid_def) apply (induct xs) apply simp apply (clarsimp simp: globals_list_distinct_def) apply (subst foldr_update_commutes[where f="global_swap g_hrs g_hrs_upd symtab v" for v]) apply (rule global_swap_swap, auto)[1] apply (simp add: global_swap_cancel foldr_hrs_htd_global_swap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_valid symtab g_hrs g_hrs_upd xs; global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab xs (globals_swap g_hrs g_hrs_upd symtab xs gs) = gs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_valid symtab g_hrs g_hrs_upd xs; global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) xs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = gs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; distinct_prop global_data_swappable xs; \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x; \<forall>x\<in>set xs. global_data_ok symtab x\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) xs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = gs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab []; distinct_prop global_data_swappable []; Ball (set []) (global_data_valid g_hrs g_hrs_upd); Ball (set []) (global_data_ok symtab)\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) [] (foldr (global_swap g_hrs g_hrs_upd symtab) [] gs) = gs
 2. \<And>x1 xs. \<lbrakk>\<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; distinct_prop global_data_swappable xs; Ball (set xs) (global_data_valid g_hrs g_hrs_upd); Ball (set xs) (global_data_ok symtab)\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) xs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = gs; global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab (x1 # xs); distinct_prop global_data_swappable (x1 # xs); Ball (set (x1 # xs)) (global_data_valid g_hrs g_hrs_upd); Ball (set (x1 # xs)) (global_data_ok symtab)\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) (x1 # xs) (foldr (global_swap g_hrs g_hrs_upd symtab) (x1 # xs) gs) = gs proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>\<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; distinct_prop global_data_swappable xs; Ball (set xs) (global_data_valid g_hrs g_hrs_upd); Ball (set xs) (global_data_ok symtab)\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) xs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = gs; global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab (x1 # xs); distinct_prop global_data_swappable (x1 # xs); Ball (set (x1 # xs)) (global_data_valid g_hrs g_hrs_upd); Ball (set (x1 # xs)) (global_data_ok symtab)\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) (x1 # xs) (foldr (global_swap g_hrs g_hrs_upd symtab) (x1 # xs) gs) = gs proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>foldr (global_swap g_hrs g_hrs_upd symtab) xs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = gs; global_acc_valid g_hrs g_hrs_upd; D \<inter> global_data_region symtab x1 = {}; \<forall>y\<in>set xs. global_data_swappable x1 y; distinct_prop global_data_swappable xs; global_data_valid g_hrs g_hrs_upd x1; \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x; global_data_ok symtab x1; \<forall>x\<in>set xs. global_data_ok symtab x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; \<forall>y\<in>set xs. global_data_region symtab x1 \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs)\<rbrakk> \<Longrightarrow> global_swap g_hrs g_hrs_upd symtab x1 (foldr (global_swap g_hrs g_hrs_upd symtab) xs (global_swap g_hrs g_hrs_upd symtab x1 (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs))) = gs proof (prove)
goal (2 subgoals):
 1. \<And>x1 xs x s. \<lbrakk>foldr (global_swap g_hrs g_hrs_upd symtab) xs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = gs; global_acc_valid g_hrs g_hrs_upd; D \<inter> global_data_region symtab x1 = {}; \<forall>y\<in>set xs. global_data_swappable x1 y; distinct_prop global_data_swappable xs; global_data_valid g_hrs g_hrs_upd x1; \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x; global_data_ok symtab x1; \<forall>x\<in>set xs. global_data_ok symtab x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; \<forall>y\<in>set xs. global_data_region symtab x1 \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs); x \<in> set xs\<rbrakk> \<Longrightarrow> global_swap g_hrs g_hrs_upd symtab x1 (global_swap g_hrs g_hrs_upd symtab x s) = global_swap g_hrs g_hrs_upd symtab x (global_swap g_hrs g_hrs_upd symtab x1 s)
 2. \<And>x1 xs. \<lbrakk>foldr (global_swap g_hrs g_hrs_upd symtab) xs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = gs; global_acc_valid g_hrs g_hrs_upd; D \<inter> global_data_region symtab x1 = {}; \<forall>y\<in>set xs. global_data_swappable x1 y; distinct_prop global_data_swappable xs; global_data_valid g_hrs g_hrs_upd x1; \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x; global_data_ok symtab x1; \<forall>x\<in>set xs. global_data_ok symtab x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; \<forall>y\<in>set xs. global_data_region symtab x1 \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs)\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) xs (global_swap g_hrs g_hrs_upd symtab x1 (global_swap g_hrs g_hrs_upd symtab x1 (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs))) = gs proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>foldr (global_swap g_hrs g_hrs_upd symtab) xs (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs) = gs; global_acc_valid g_hrs g_hrs_upd; D \<inter> global_data_region symtab x1 = {}; \<forall>y\<in>set xs. global_data_swappable x1 y; distinct_prop global_data_swappable xs; global_data_valid g_hrs g_hrs_upd x1; \<forall>x\<in>set xs. global_data_valid g_hrs g_hrs_upd x; global_data_ok symtab x1; \<forall>x\<in>set xs. global_data_ok symtab x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; \<forall>y\<in>set xs. global_data_region symtab x1 \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs)\<rbrakk> \<Longrightarrow> foldr (global_swap g_hrs g_hrs_upd symtab) xs (global_swap g_hrs g_hrs_upd symtab x1 (global_swap g_hrs g_hrs_upd symtab x1 (foldr (global_swap g_hrs g_hrs_upd symtab) xs gs))) = gs proof (prove)
goal:
No subgoals!