24895
|
1 |
theory Support
|
25751
|
2 |
imports "../Nominal"
|
24895
|
3 |
begin
|
|
4 |
|
|
5 |
text {*
|
|
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 |
|
26262
|
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.
|
24895
|
14 |
*}
|
|
15 |
|
|
16 |
atom_decl atom
|
|
17 |
|
25751
|
18 |
text {* The set of even atoms. *}
|
24895
|
19 |
abbreviation
|
|
20 |
EVEN :: "atom set"
|
|
21 |
where
|
|
22 |
"EVEN \<equiv> {atom n | n. \<exists>i. n=2*i}"
|
|
23 |
|
25751
|
24 |
text {* The set of odd atoms: *}
|
24895
|
25 |
abbreviation
|
|
26 |
ODD :: "atom set"
|
|
27 |
where
|
|
28 |
"ODD \<equiv> {atom n | n. \<exists>i. n=2*i+1}"
|
|
29 |
|
25751
|
30 |
text {* An atom is either even or odd. *}
|
24895
|
31 |
lemma even_or_odd:
|
37388
|
32 |
fixes n :: nat
|
24895
|
33 |
shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)"
|
|
34 |
by (induct n) (presburger)+
|
|
35 |
|
26055
|
36 |
text {*
|
|
37 |
The union of even and odd atoms is the set of all atoms.
|
26262
|
38 |
(Unfortunately I do not know a simpler proof of this fact.) *}
|
24895
|
39 |
lemma EVEN_union_ODD:
|
|
40 |
shows "EVEN \<union> ODD = UNIV"
|
25139
|
41 |
using even_or_odd
|
24895
|
42 |
proof -
|
|
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
|
40702
|
48 |
by (auto simp add: surj_def)
|
24895
|
49 |
finally show "EVEN \<union> ODD = UNIV" by simp
|
|
50 |
qed
|
|
51 |
|
25751
|
52 |
text {* The sets of even and odd atoms are disjunct. *}
|
24895
|
53 |
lemma EVEN_intersect_ODD:
|
|
54 |
shows "EVEN \<inter> ODD = {}"
|
|
55 |
using even_or_odd
|
|
56 |
by (auto) (presburger)
|
|
57 |
|
25751
|
58 |
text {*
|
|
59 |
The preceeding two lemmas help us to prove
|
26055
|
60 |
the following two useful equalities: *}
|
|
61 |
|
24895
|
62 |
lemma UNIV_subtract:
|
|
63 |
shows "UNIV - EVEN = ODD"
|
|
64 |
and "UNIV - ODD = EVEN"
|
|
65 |
using EVEN_union_ODD EVEN_intersect_ODD
|
|
66 |
by (blast)+
|
|
67 |
|
25751
|
68 |
text {* The sets EVEN and ODD are infinite. *}
|
24895
|
69 |
lemma EVEN_ODD_infinite:
|
|
70 |
shows "infinite EVEN"
|
|
71 |
and "infinite ODD"
|
25751
|
72 |
unfolding infinite_iff_countable_subset
|
|
73 |
proof -
|
|
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)
|
|
77 |
next
|
|
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)
|
|
81 |
qed
|
24895
|
82 |
|
25139
|
83 |
text {*
|
26262
|
84 |
A general fact about a set S of atoms that is both infinite and
|
27360
|
85 |
coinfinite. Then S has all atoms as its support. Steve Zdancewic
|
26055
|
86 |
helped with proving this fact. *}
|
|
87 |
|
24895
|
88 |
lemma supp_infinite_coinfinite:
|
|
89 |
fixes S::"atom set"
|
25867
|
90 |
assumes asm1: "infinite S"
|
|
91 |
and asm2: "infinite (UNIV-S)"
|
24895
|
92 |
shows "(supp S) = (UNIV::atom set)"
|
|
93 |
proof -
|
|
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
|
26806
|
101 |
hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
|
25867
|
102 |
with asm2 have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
|
24895
|
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
|
26806
|
108 |
hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
|
25867
|
109 |
with asm1 have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
|
24895
|
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
|
|
115 |
qed
|
|
116 |
|
25751
|
117 |
text {* As a corollary we get that EVEN and ODD have infinite support. *}
|
24895
|
118 |
lemma 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 |
|
25751
|
124 |
text {*
|
|
125 |
The set of all atoms has empty support, since any swappings leaves
|
26055
|
126 |
this set unchanged. *}
|
|
127 |
|
24895
|
128 |
lemma UNIV_supp:
|
|
129 |
shows "supp (UNIV::atom set) = ({}::atom set)"
|
|
130 |
proof -
|
|
131 |
have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
|
26806
|
132 |
by (auto simp add: perm_set_eq calc_atm)
|
25751
|
133 |
then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def)
|
24895
|
134 |
qed
|
|
135 |
|
25751
|
136 |
text {* Putting everything together. *}
|
24895
|
137 |
theorem 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 |
|
26055
|
144 |
text {* Moral: support is a sublte notion. *}
|
|
145 |
|
24895
|
146 |
end |