1theory Support 2 imports "HOL-Nominal.Nominal" 3begin 4 5text \<open> 6 An example showing that in general 7 8 x\<sharp>(A \<union> B) does not imply x\<sharp>A and x\<sharp>B 9 10 For this we set A to the set of even atoms and B to 11 the set of odd atoms. Then A \<union> B, that is the set of 12 all atoms, has empty support. The sets A, respectively B, 13 however have the set of all atoms as their support. 14\<close> 15 16atom_decl atom 17 18text \<open>The set of even atoms.\<close> 19abbreviation 20 EVEN :: "atom set" 21where 22 "EVEN \<equiv> {atom n | n. \<exists>i. n=2*i}" 23 24text \<open>The set of odd atoms:\<close> 25abbreviation 26 ODD :: "atom set" 27where 28 "ODD \<equiv> {atom n | n. \<exists>i. n=2*i+1}" 29 30text \<open>An atom is either even or odd.\<close> 31lemma even_or_odd: 32 fixes n :: nat 33 shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)" 34 by (induct n) (presburger)+ 35 36text \<open> 37 The union of even and odd atoms is the set of all atoms. 38 (Unfortunately I do not know a simpler proof of this fact.)\<close> 39lemma EVEN_union_ODD: 40 shows "EVEN \<union> ODD = UNIV" 41 using even_or_odd 42proof - 43 have "EVEN \<union> ODD = (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i} \<union> (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i+1}" by auto 44 also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i} \<union> {n. \<exists>i. n = 2*i+1})" by auto 45 also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto 46 also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto 47 also have "\<dots> = (UNIV::atom set)" using atom.exhaust 48 by (auto simp add: surj_def) 49 finally show "EVEN \<union> ODD = UNIV" by simp 50qed 51 52text \<open>The sets of even and odd atoms are disjunct.\<close> 53lemma EVEN_intersect_ODD: 54 shows "EVEN \<inter> ODD = {}" 55 using even_or_odd 56 by (auto) (presburger) 57 58text \<open> 59 The preceeding two lemmas help us to prove 60 the following two useful equalities:\<close> 61 62lemma UNIV_subtract: 63 shows "UNIV - EVEN = ODD" 64 and "UNIV - ODD = EVEN" 65 using EVEN_union_ODD EVEN_intersect_ODD 66 by (blast)+ 67 68text \<open>The sets EVEN and ODD are infinite.\<close> 69lemma EVEN_ODD_infinite: 70 shows "infinite EVEN" 71 and "infinite ODD" 72unfolding infinite_iff_countable_subset 73proof - 74 let ?f = "\<lambda>n. atom (2*n)" 75 have "inj ?f \<and> range ?f \<subseteq> EVEN" by (auto simp add: inj_on_def) 76 then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> EVEN" by (rule_tac exI) 77next 78 let ?f = "\<lambda>n. atom (2*n+1)" 79 have "inj ?f \<and> range ?f \<subseteq> ODD" by (auto simp add: inj_on_def) 80 then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> ODD" by (rule_tac exI) 81qed 82 83text \<open> 84 A general fact about a set S of atoms that is both infinite and 85 coinfinite. Then S has all atoms as its support. Steve Zdancewic 86 helped with proving this fact.\<close> 87 88lemma supp_infinite_coinfinite: 89 fixes S::"atom set" 90 assumes asm1: "infinite S" 91 and asm2: "infinite (UNIV-S)" 92 shows "(supp S) = (UNIV::atom set)" 93proof - 94 have "\<forall>(x::atom). x\<in>(supp S)" 95 proof 96 fix x::"atom" 97 show "x\<in>(supp S)" 98 proof (cases "x\<in>S") 99 case True 100 have "x\<in>S" by fact 101 hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm) 102 with asm2 have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection) 103 hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto) 104 then show "x\<in>(supp S)" by (simp add: supp_def) 105 next 106 case False 107 have "x\<notin>S" by fact 108 hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm) 109 with asm1 have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection) 110 hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto) 111 then show "x\<in>(supp S)" by (simp add: supp_def) 112 qed 113 qed 114 then show "(supp S) = (UNIV::atom set)" by auto 115qed 116 117text \<open>As a corollary we get that EVEN and ODD have infinite support.\<close> 118lemma EVEN_ODD_supp: 119 shows "supp EVEN = (UNIV::atom set)" 120 and "supp ODD = (UNIV::atom set)" 121 using supp_infinite_coinfinite UNIV_subtract EVEN_ODD_infinite 122 by simp_all 123 124text \<open> 125 The set of all atoms has empty support, since any swappings leaves 126 this set unchanged.\<close> 127 128lemma UNIV_supp: 129 shows "supp (UNIV::atom set) = ({}::atom set)" 130proof - 131 have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)" 132 by (auto simp add: perm_set_def calc_atm) 133 then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def) 134qed 135 136text \<open>Putting everything together.\<close> 137theorem EVEN_ODD_freshness: 138 fixes x::"atom" 139 shows "x\<sharp>(EVEN \<union> ODD)" 140 and "\<not>x\<sharp>EVEN" 141 and "\<not>x\<sharp>ODD" 142 by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp) 143 144text \<open>Moral: support is a sublte notion.\<close> 145 146end 147