theory GlobalsSwap

lemma globals_swap_reorder_append:
  "\<lbrakk> globals_list_valid symtab g_hrs g_hrs_upd (xs @ ys);
        global_acc_valid g_hrs g_hrs_upd;
        globals_list_distinct D symtab (xs @ ys) \<rbrakk>
    \<Longrightarrow> globals_swap g_hrs g_hrs_upd symtab (xs @ ys) = globals_swap g_hrs g_hrs_upd symtab (ys @ xs)" apply (induct xs) apply simp apply (rule ext) apply (clarsimp simp: globals_swap_def foldr_hrs_htd_global_swap
                        fun_eq_iff) apply (drule meta_mp, simp add: globals_list_valid_def) apply (clarsimp simp: globals_list_distinct_def) apply (rule foldr_update_commutes) apply (clarsimp simp: ball_Un globals_list_valid_def) apply (rule global_swap_swap, simp_all) done

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