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