theory GlobalsSwap

lemma globals_list_distinct_filter_member:
  "x \<in> set xs \<Longrightarrow> globals_list_distinct D symtab xs
    \<Longrightarrow> \<not> P x
    \<Longrightarrow> globals_list_distinct (global_data_region symtab x) symtab
        (filter P xs)" apply (clarsimp simp: globals_list_distinct_def) apply (rule conjI) apply (clarsimp simp: in_set_conv_decomp[where x="x"]
                         distinct_prop_append) apply auto[1] apply (simp add: distinct_prop_map distinct_prop_filter) apply (erule distinct_prop_weaken, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; globals_list_distinct D symtab xs; \<not> P x\<rbrakk> \<Longrightarrow> globals_list_distinct (global_data_region symtab x) symtab (filter P xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; \<not> P x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs)\<rbrakk> \<Longrightarrow> (\<forall>y. y \<in> set xs \<and> P y \<longrightarrow> global_data_region symtab x \<inter> global_data_region symtab y = {}) \<and> distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter P xs)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set xs; \<not> P x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs)\<rbrakk> \<Longrightarrow> \<forall>y. y \<in> set xs \<and> P y \<longrightarrow> global_data_region symtab x \<inter> global_data_region symtab y = {}
 2. \<lbrakk>x \<in> set xs; \<not> P x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs)\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter P xs)) proof (prove)
goal (2 subgoals):
 1. \<And>ys zs y. \<lbrakk>\<not> P x; xs = ys @ x # zs; y = x \<or> y \<in> set ys \<or> y \<in> set zs; P y; D \<inter> global_data_region symtab x = {}; \<forall>y\<in>set ys \<union> set zs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) ys); \<forall>y\<in>set zs. global_data_region symtab x \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) zs); \<forall>xa\<in>set ys. global_data_region symtab xa \<inter> global_data_region symtab x = {} \<and> (\<forall>y\<in>set zs. global_data_region symtab xa \<inter> global_data_region symtab y = {})\<rbrakk> \<Longrightarrow> global_data_region symtab x \<inter> global_data_region symtab y = {}
 2. \<lbrakk>x \<in> set xs; \<not> P x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs)\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter P xs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; \<not> P x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) xs)\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) (filter P xs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; \<not> P x; \<forall>y\<in>set xs. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>x y. global_data_region symtab x \<inter> global_data_region symtab y = {}) xs\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. P x \<and> P y \<longrightarrow> global_data_region symtab x \<inter> global_data_region symtab y = {}) xs proof (prove)
goal:
No subgoals!