author | wenzelm |
Tue, 13 Sep 2022 09:38:02 +0200 | |
changeset 76129 | 5979f73b9db1 |
parent 71460 | 8f628d216ea1 |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
65386
diff
changeset
|
1 |
(* Title: ZF/ZF_Base.thy |
0 | 2 |
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
3 |
Copyright 1993 University of Cambridge |
|
14076 | 4 |
*) |
0 | 5 |
|
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
65386
diff
changeset
|
6 |
section \<open>Base of Zermelo-Fraenkel Set Theory\<close> |
0 | 7 |
|
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
65386
diff
changeset
|
8 |
theory ZF_Base |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
65449
diff
changeset
|
9 |
imports FOL |
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37405
diff
changeset
|
10 |
begin |
0 | 11 |
|
62149 | 12 |
subsection \<open>Signature\<close> |
13 |
||
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
38798
diff
changeset
|
14 |
declare [[eta_contract = false]] |
23168 | 15 |
|
14076 | 16 |
typedecl i |
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
48733
diff
changeset
|
17 |
instance i :: "term" .. |
0 | 18 |
|
69587 | 19 |
axiomatization mem :: "[i, i] \<Rightarrow> o" (infixl \<open>\<in>\<close> 50) \<comment> \<open>membership relation\<close> |
20 |
and zero :: "i" (\<open>0\<close>) \<comment> \<open>the empty set\<close> |
|
62149 | 21 |
and Pow :: "i \<Rightarrow> i" \<comment> \<open>power sets\<close> |
22 |
and Inf :: "i" \<comment> \<open>infinite set\<close> |
|
69587 | 23 |
and Union :: "i \<Rightarrow> i" (\<open>\<Union>_\<close> [90] 90) |
62149 | 24 |
and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" |
25 |
||
69587 | 26 |
abbreviation not_mem :: "[i, i] \<Rightarrow> o" (infixl \<open>\<notin>\<close> 50) \<comment> \<open>negated membership relation\<close> |
62149 | 27 |
where "x \<notin> y \<equiv> \<not> (x \<in> y)" |
28 |
||
29 |
||
30 |
subsection \<open>Bounded Quantifiers\<close> |
|
31 |
||
32 |
definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o" |
|
33 |
where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)" |
|
0 | 34 |
|
62149 | 35 |
definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o" |
36 |
where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)" |
|
0 | 37 |
|
62149 | 38 |
syntax |
69587 | 39 |
"_Ball" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<forall>_\<in>_./ _)\<close> 10) |
40 |
"_Bex" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<exists>_\<in>_./ _)\<close> 10) |
|
62149 | 41 |
translations |
42 |
"\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)" |
|
43 |
"\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)" |
|
44 |
||
45 |
||
46 |
subsection \<open>Variations on Replacement\<close> |
|
47 |
||
48 |
(* Derived form of replacement, restricting P to its functional part. |
|
49 |
The resulting set (for functional P) is the same as with |
|
50 |
PrimReplace, but the rules are simpler. *) |
|
51 |
definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" |
|
63901 | 52 |
where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))" |
0 | 53 |
|
62149 | 54 |
syntax |
69587 | 55 |
"_Replace" :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _ \<in> _, _})\<close>) |
62149 | 56 |
translations |
57 |
"{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)" |
|
58 |
||
59 |
||
60 |
(* Functional form of replacement -- analgous to ML's map functional *) |
|
61 |
||
62 |
definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
|
63 |
where "RepFun(A,f) == {y . x\<in>A, y=f(x)}" |
|
64 |
||
65 |
syntax |
|
69587 | 66 |
"_RepFun" :: "[i, pttrn, i] => i" (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51]) |
62149 | 67 |
translations |
68 |
"{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)" |
|
69 |
||
0 | 70 |
|
62149 | 71 |
(* Separation and Pairing can be derived from the Replacement |
72 |
and Powerset Axioms using the following definitions. *) |
|
73 |
definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i" |
|
74 |
where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}" |
|
75 |
||
76 |
syntax |
|
69587 | 77 |
"_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ \<in> _ ./ _})\<close>) |
62149 | 78 |
translations |
79 |
"{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)" |
|
80 |
||
6068 | 81 |
|
62149 | 82 |
subsection \<open>General union and intersection\<close> |
83 |
||
69587 | 84 |
definition Inter :: "i => i" (\<open>\<Inter>_\<close> [90] 90) |
62149 | 85 |
where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}" |
86 |
||
87 |
syntax |
|
69587 | 88 |
"_UNION" :: "[pttrn, i, i] => i" (\<open>(3\<Union>_\<in>_./ _)\<close> 10) |
89 |
"_INTER" :: "[pttrn, i, i] => i" (\<open>(3\<Inter>_\<in>_./ _)\<close> 10) |
|
62149 | 90 |
translations |
91 |
"\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})" |
|
92 |
"\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})" |
|
6068 | 93 |
|
94 |
||
62149 | 95 |
subsection \<open>Finite sets and binary operations\<close> |
96 |
||
97 |
(*Unordered pairs (Upair) express binary union/intersection and cons; |
|
98 |
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) |
|
99 |
||
100 |
definition Upair :: "[i, i] => i" |
|
101 |
where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}" |
|
0 | 102 |
|
69587 | 103 |
definition Subset :: "[i, i] \<Rightarrow> o" (infixl \<open>\<subseteq>\<close> 50) \<comment> \<open>subset relation\<close> |
62149 | 104 |
where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B" |
105 |
||
69587 | 106 |
definition Diff :: "[i, i] \<Rightarrow> i" (infixl \<open>-\<close> 65) \<comment> \<open>set difference\<close> |
62149 | 107 |
where "A - B == { x\<in>A . ~(x\<in>B) }" |
0 | 108 |
|
69587 | 109 |
definition Un :: "[i, i] \<Rightarrow> i" (infixl \<open>\<union>\<close> 65) \<comment> \<open>binary union\<close> |
62149 | 110 |
where "A \<union> B == \<Union>(Upair(A,B))" |
111 |
||
69587 | 112 |
definition Int :: "[i, i] \<Rightarrow> i" (infixl \<open>\<inter>\<close> 70) \<comment> \<open>binary intersection\<close> |
62149 | 113 |
where "A \<inter> B == \<Inter>(Upair(A,B))" |
0 | 114 |
|
62149 | 115 |
definition cons :: "[i, i] => i" |
116 |
where "cons(a,A) == Upair(a,a) \<union> A" |
|
117 |
||
118 |
definition succ :: "i => i" |
|
119 |
where "succ(i) == cons(i, i)" |
|
0 | 120 |
|
62149 | 121 |
nonterminal "is" |
122 |
syntax |
|
69587 | 123 |
"" :: "i \<Rightarrow> is" (\<open>_\<close>) |
124 |
"_Enum" :: "[i, is] \<Rightarrow> is" (\<open>_,/ _\<close>) |
|
125 |
"_Finset" :: "is \<Rightarrow> i" (\<open>{(_)}\<close>) |
|
62149 | 126 |
translations |
127 |
"{x, xs}" == "CONST cons(x, {xs})" |
|
128 |
"{x}" == "CONST cons(x, 0)" |
|
129 |
||
130 |
||
131 |
subsection \<open>Axioms\<close> |
|
132 |
||
133 |
(* ZF axioms -- see Suppes p.238 |
|
134 |
Axioms for Union, Pow and Replace state existence only, |
|
135 |
uniqueness is derivable using extensionality. *) |
|
48733
18e76e2db6d4
proper axiomatization of "mem" -- do not leave it formally unspecified;
wenzelm
parents:
48462
diff
changeset
|
136 |
|
18e76e2db6d4
proper axiomatization of "mem" -- do not leave it formally unspecified;
wenzelm
parents:
48462
diff
changeset
|
137 |
axiomatization |
62149 | 138 |
where |
139 |
extension: "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and |
|
140 |
Union_iff: "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and |
|
141 |
Pow_iff: "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and |
|
24826 | 142 |
|
62149 | 143 |
(*We may name this set, though it is not uniquely defined.*) |
144 |
infinity: "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and |
|
24826 | 145 |
|
62149 | 146 |
(*This formulation facilitates case analysis on A.*) |
147 |
foundation: "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and |
|
148 |
||
149 |
(*Schema axiom since predicate P is a higher-order variable*) |
|
150 |
replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow> |
|
151 |
b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))" |
|
0 | 152 |
|
153 |
||
62149 | 154 |
subsection \<open>Definite descriptions -- via Replace over the set "1"\<close> |
155 |
||
69587 | 156 |
definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder \<open>THE \<close> 10) |
62149 | 157 |
where the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})" |
615 | 158 |
|
69587 | 159 |
definition If :: "[o, i, i] \<Rightarrow> i" (\<open>(if (_)/ then (_)/ else (_))\<close> [10] 10) |
62149 | 160 |
where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b" |
161 |
||
162 |
abbreviation (input) |
|
69587 | 163 |
old_if :: "[o, i, i] => i" (\<open>if '(_,_,_')\<close>) |
62149 | 164 |
where "if(P,a,b) == If(P,a,b)" |
165 |
||
166 |
||
167 |
subsection \<open>Ordered Pairing\<close> |
|
24826 | 168 |
|
62149 | 169 |
(* this "symmetric" definition works better than {{a}, {a,b}} *) |
170 |
definition Pair :: "[i, i] => i" |
|
171 |
where "Pair(a,b) == {{a,a}, {a,b}}" |
|
172 |
||
173 |
definition fst :: "i \<Rightarrow> i" |
|
174 |
where "fst(p) == THE a. \<exists>b. p = Pair(a, b)" |
|
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
175 |
|
62149 | 176 |
definition snd :: "i \<Rightarrow> i" |
177 |
where "snd(p) == THE b. \<exists>a. p = Pair(a, b)" |
|
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
178 |
|
62149 | 179 |
definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}" \<comment> \<open>for pattern-matching\<close> |
180 |
where "split(c) == \<lambda>p. c(fst(p), snd(p))" |
|
181 |
||
182 |
(* Patterns -- extends pre-defined type "pttrn" used in abstractions *) |
|
183 |
nonterminal patterns |
|
184 |
syntax |
|
69587 | 185 |
"_pattern" :: "patterns => pttrn" (\<open>\<langle>_\<rangle>\<close>) |
186 |
"" :: "pttrn => patterns" (\<open>_\<close>) |
|
187 |
"_patterns" :: "[pttrn, patterns] => patterns" (\<open>_,/_\<close>) |
|
188 |
"_Tuple" :: "[i, is] => i" (\<open>\<langle>(_,/ _)\<rangle>\<close>) |
|
0 | 189 |
translations |
61979 | 190 |
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>" |
191 |
"\<langle>x, y\<rangle>" == "CONST Pair(x, y)" |
|
192 |
"\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)" |
|
193 |
"\<lambda>\<langle>x,y\<rangle>.b" == "CONST split(\<lambda>x y. b)" |
|
2286 | 194 |
|
62149 | 195 |
definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
196 |
where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}" |
|
197 |
||
69587 | 198 |
abbreviation cart_prod :: "[i, i] => i" (infixr \<open>\<times>\<close> 80) \<comment> \<open>Cartesian product\<close> |
62149 | 199 |
where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)" |
200 |
||
201 |
||
202 |
subsection \<open>Relations and Functions\<close> |
|
203 |
||
204 |
(*converse of relation r, inverse of function*) |
|
205 |
definition converse :: "i \<Rightarrow> i" |
|
206 |
where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}" |
|
207 |
||
208 |
definition domain :: "i \<Rightarrow> i" |
|
209 |
where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}" |
|
210 |
||
211 |
definition range :: "i \<Rightarrow> i" |
|
212 |
where "range(r) == domain(converse(r))" |
|
213 |
||
214 |
definition field :: "i \<Rightarrow> i" |
|
215 |
where "field(r) == domain(r) \<union> range(r)" |
|
216 |
||
217 |
definition relation :: "i \<Rightarrow> o" \<comment> \<open>recognizes sets of pairs\<close> |
|
218 |
where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>" |
|
219 |
||
65386 | 220 |
definition "function" :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close> |
62149 | 221 |
where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')" |
222 |
||
69587 | 223 |
definition Image :: "[i, i] \<Rightarrow> i" (infixl \<open>``\<close> 90) \<comment> \<open>image\<close> |
62149 | 224 |
where image_def: "r `` A == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}" |
225 |
||
69587 | 226 |
definition vimage :: "[i, i] \<Rightarrow> i" (infixl \<open>-``\<close> 90) \<comment> \<open>inverse image\<close> |
62149 | 227 |
where vimage_def: "r -`` A == converse(r)``A" |
228 |
||
229 |
(* Restrict the relation r to the domain A *) |
|
230 |
definition restrict :: "[i, i] \<Rightarrow> i" |
|
231 |
where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}" |
|
232 |
||
233 |
||
234 |
(* Abstraction, application and Cartesian product of a family of sets *) |
|
235 |
||
236 |
definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
|
237 |
where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}" |
|
238 |
||
69587 | 239 |
definition "apply" :: "[i, i] \<Rightarrow> i" (infixl \<open>`\<close> 90) \<comment> \<open>function application\<close> |
62149 | 240 |
where "f`a == \<Union>(f``{a})" |
241 |
||
242 |
definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
|
243 |
where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}" |
|
244 |
||
71460
8f628d216ea1
proper print mode for function_space notation (amending d68b705719ce);
wenzelm
parents:
69593
diff
changeset
|
245 |
abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr \<open>\<rightarrow>\<close> 60) \<comment> \<open>function space\<close> |
8f628d216ea1
proper print mode for function_space notation (amending d68b705719ce);
wenzelm
parents:
69593
diff
changeset
|
246 |
where "A \<rightarrow> B \<equiv> Pi(A, \<lambda>_. B)" |
62149 | 247 |
|
248 |
||
249 |
(* binder syntax *) |
|
250 |
||
251 |
syntax |
|
69587 | 252 |
"_PROD" :: "[pttrn, i, i] => i" (\<open>(3\<Prod>_\<in>_./ _)\<close> 10) |
253 |
"_SUM" :: "[pttrn, i, i] => i" (\<open>(3\<Sum>_\<in>_./ _)\<close> 10) |
|
254 |
"_lam" :: "[pttrn, i, i] => i" (\<open>(3\<lambda>_\<in>_./ _)\<close> 10) |
|
62149 | 255 |
translations |
256 |
"\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)" |
|
257 |
"\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)" |
|
258 |
"\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)" |
|
259 |
||
260 |
||
261 |
subsection \<open>ASCII syntax\<close> |
|
0 | 262 |
|
61979 | 263 |
notation (ASCII) |
69587 | 264 |
cart_prod (infixr \<open>*\<close> 80) and |
265 |
Int (infixl \<open>Int\<close> 70) and |
|
266 |
Un (infixl \<open>Un\<close> 65) and |
|
71460
8f628d216ea1
proper print mode for function_space notation (amending d68b705719ce);
wenzelm
parents:
69593
diff
changeset
|
267 |
function_space (infixr \<open>->\<close> 60) and |
69587 | 268 |
Subset (infixl \<open><=\<close> 50) and |
269 |
mem (infixl \<open>:\<close> 50) and |
|
270 |
not_mem (infixl \<open>~:\<close> 50) |
|
24826 | 271 |
|
61979 | 272 |
syntax (ASCII) |
69587 | 273 |
"_Ball" :: "[pttrn, i, o] => o" (\<open>(3ALL _:_./ _)\<close> 10) |
274 |
"_Bex" :: "[pttrn, i, o] => o" (\<open>(3EX _:_./ _)\<close> 10) |
|
275 |
"_Collect" :: "[pttrn, i, o] => i" (\<open>(1{_: _ ./ _})\<close>) |
|
276 |
"_Replace" :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _: _, _})\<close>) |
|
277 |
"_RepFun" :: "[i, pttrn, i] => i" (\<open>(1{_ ./ _: _})\<close> [51,0,51]) |
|
278 |
"_UNION" :: "[pttrn, i, i] => i" (\<open>(3UN _:_./ _)\<close> 10) |
|
279 |
"_INTER" :: "[pttrn, i, i] => i" (\<open>(3INT _:_./ _)\<close> 10) |
|
280 |
"_PROD" :: "[pttrn, i, i] => i" (\<open>(3PROD _:_./ _)\<close> 10) |
|
281 |
"_SUM" :: "[pttrn, i, i] => i" (\<open>(3SUM _:_./ _)\<close> 10) |
|
282 |
"_lam" :: "[pttrn, i, i] => i" (\<open>(3lam _:_./ _)\<close> 10) |
|
283 |
"_Tuple" :: "[i, is] => i" (\<open><(_,/ _)>\<close>) |
|
284 |
"_pattern" :: "patterns => pttrn" (\<open><_>\<close>) |
|
2540 | 285 |
|
13780 | 286 |
|
60770 | 287 |
subsection \<open>Substitution\<close> |
13780 | 288 |
|
289 |
(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) |
|
14227 | 290 |
lemma subst_elem: "[| b\<in>A; a=b |] ==> a\<in>A" |
13780 | 291 |
by (erule ssubst, assumption) |
292 |
||
293 |
||
60770 | 294 |
subsection\<open>Bounded universal quantifier\<close> |
13780 | 295 |
|
14227 | 296 |
lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)" |
13780 | 297 |
by (simp add: Ball_def) |
298 |
||
15481 | 299 |
lemmas strip = impI allI ballI |
300 |
||
14227 | 301 |
lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x); x: A |] ==> P(x)" |
13780 | 302 |
by (simp add: Ball_def) |
303 |
||
304 |
(*Instantiates x first: better for automatic theorem proving?*) |
|
46820 | 305 |
lemma rev_ballE [elim]: |
306 |
"[| \<forall>x\<in>A. P(x); x\<notin>A ==> Q; P(x) ==> Q |] ==> Q" |
|
307 |
by (simp add: Ball_def, blast) |
|
13780 | 308 |
|
46820 | 309 |
lemma ballE: "[| \<forall>x\<in>A. P(x); P(x) ==> Q; x\<notin>A ==> Q |] ==> Q" |
13780 | 310 |
by blast |
311 |
||
312 |
(*Used in the datatype package*) |
|
14227 | 313 |
lemma rev_bspec: "[| x: A; \<forall>x\<in>A. P(x) |] ==> P(x)" |
13780 | 314 |
by (simp add: Ball_def) |
315 |
||
46820 | 316 |
(*Trival rewrite rule; @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*) |
317 |
lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)" |
|
13780 | 318 |
by (simp add: Ball_def) |
319 |
||
320 |
(*Congruence rule for rewriting*) |
|
321 |
lemma ball_cong [cong]: |
|
14227 | 322 |
"[| A=A'; !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))" |
13780 | 323 |
by (simp add: Ball_def) |
324 |
||
18845 | 325 |
lemma atomize_ball: |
326 |
"(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))" |
|
327 |
by (simp only: Ball_def atomize_all atomize_imp) |
|
328 |
||
329 |
lemmas [symmetric, rulify] = atomize_ball |
|
330 |
and [symmetric, defn] = atomize_ball |
|
331 |
||
13780 | 332 |
|
60770 | 333 |
subsection\<open>Bounded existential quantifier\<close> |
13780 | 334 |
|
14227 | 335 |
lemma bexI [intro]: "[| P(x); x: A |] ==> \<exists>x\<in>A. P(x)" |
13780 | 336 |
by (simp add: Bex_def, blast) |
337 |
||
46820 | 338 |
(*The best argument order when there is only one @{term"x\<in>A"}*) |
14227 | 339 |
lemma rev_bexI: "[| x\<in>A; P(x) |] ==> \<exists>x\<in>A. P(x)" |
13780 | 340 |
by blast |
341 |
||
46820 | 342 |
(*Not of the general form for such rules. The existential quanitifer becomes universal. *) |
14227 | 343 |
lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a); a: A |] ==> \<exists>x\<in>A. P(x)" |
13780 | 344 |
by blast |
345 |
||
14227 | 346 |
lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x); !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q" |
13780 | 347 |
by (simp add: Bex_def, blast) |
348 |
||
46820 | 349 |
(*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*) |
14227 | 350 |
lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)" |
13780 | 351 |
by (simp add: Bex_def) |
352 |
||
353 |
lemma bex_cong [cong]: |
|
46820 | 354 |
"[| A=A'; !!x. x\<in>A' ==> P(x) <-> P'(x) |] |
14227 | 355 |
==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))" |
13780 | 356 |
by (simp add: Bex_def cong: conj_cong) |
357 |
||
358 |
||
359 |
||
60770 | 360 |
subsection\<open>Rules for subsets\<close> |
13780 | 361 |
|
362 |
lemma subsetI [intro!]: |
|
46820 | 363 |
"(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B" |
364 |
by (simp add: subset_def) |
|
13780 | 365 |
|
366 |
(*Rule in Modus Ponens style [was called subsetE] *) |
|
46820 | 367 |
lemma subsetD [elim]: "[| A \<subseteq> B; c\<in>A |] ==> c\<in>B" |
13780 | 368 |
apply (unfold subset_def) |
369 |
apply (erule bspec, assumption) |
|
370 |
done |
|
371 |
||
372 |
(*Classical elimination rule*) |
|
373 |
lemma subsetCE [elim]: |
|
46820 | 374 |
"[| A \<subseteq> B; c\<notin>A ==> P; c\<in>B ==> P |] ==> P" |
375 |
by (simp add: subset_def, blast) |
|
13780 | 376 |
|
377 |
(*Sometimes useful with premises in this order*) |
|
14227 | 378 |
lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B" |
13780 | 379 |
by blast |
380 |
||
46820 | 381 |
lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A" |
13780 | 382 |
by blast |
383 |
||
46820 | 384 |
lemma rev_contra_subsetD: "[| c \<notin> B; A \<subseteq> B |] ==> c \<notin> A" |
13780 | 385 |
by blast |
386 |
||
46820 | 387 |
lemma subset_refl [simp]: "A \<subseteq> A" |
13780 | 388 |
by blast |
389 |
||
390 |
lemma subset_trans: "[| A<=B; B<=C |] ==> A<=C" |
|
391 |
by blast |
|
392 |
||
393 |
(*Useful for proving A<=B by rewriting in some cases*) |
|
46820 | 394 |
lemma subset_iff: |
395 |
"A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)" |
|
13780 | 396 |
apply (unfold subset_def Ball_def) |
397 |
apply (rule iff_refl) |
|
398 |
done |
|
399 |
||
60770 | 400 |
text\<open>For calculations\<close> |
46907
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46820
diff
changeset
|
401 |
declare subsetD [trans] rev_subsetD [trans] subset_trans [trans] |
eea3eb057fea
Structured proofs concerning the square of an infinite cardinal
paulson
parents:
46820
diff
changeset
|
402 |
|
13780 | 403 |
|
60770 | 404 |
subsection\<open>Rules for equality\<close> |
13780 | 405 |
|
406 |
(*Anti-symmetry of the subset relation*) |
|
46820 | 407 |
lemma equalityI [intro]: "[| A \<subseteq> B; B \<subseteq> A |] ==> A = B" |
408 |
by (rule extension [THEN iffD2], rule conjI) |
|
13780 | 409 |
|
410 |
||
14227 | 411 |
lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B" |
13780 | 412 |
by (rule equalityI, blast+) |
413 |
||
45602 | 414 |
lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1] |
415 |
lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2] |
|
13780 | 416 |
|
417 |
lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" |
|
46820 | 418 |
by (blast dest: equalityD1 equalityD2) |
13780 | 419 |
|
420 |
lemma equalityCE: |
|
46820 | 421 |
"[| A = B; [| c\<in>A; c\<in>B |] ==> P; [| c\<notin>A; c\<notin>B |] ==> P |] ==> P" |
422 |
by (erule equalityE, blast) |
|
13780 | 423 |
|
27702 | 424 |
lemma equality_iffD: |
46820 | 425 |
"A = B ==> (!!x. x \<in> A <-> x \<in> B)" |
27702 | 426 |
by auto |
427 |
||
13780 | 428 |
|
60770 | 429 |
subsection\<open>Rules for Replace -- the derived form of replacement\<close> |
13780 | 430 |
|
46820 | 431 |
lemma Replace_iff: |
432 |
"b \<in> {y. x\<in>A, P(x,y)} <-> (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))" |
|
13780 | 433 |
apply (unfold Replace_def) |
434 |
apply (rule replacement [THEN iff_trans], blast+) |
|
435 |
done |
|
436 |
||
437 |
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *) |
|
46820 | 438 |
lemma ReplaceI [intro]: |
439 |
"[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==> |
|
440 |
b \<in> {y. x\<in>A, P(x,y)}" |
|
441 |
by (rule Replace_iff [THEN iffD2], blast) |
|
13780 | 442 |
|
443 |
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *) |
|
46820 | 444 |
lemma ReplaceE: |
445 |
"[| b \<in> {y. x\<in>A, P(x,y)}; |
|
446 |
!!x. [| x: A; P(x,b); \<forall>y. P(x,y)\<longrightarrow>y=b |] ==> R |
|
13780 | 447 |
|] ==> R" |
448 |
by (rule Replace_iff [THEN iffD1, THEN bexE], simp+) |
|
449 |
||
450 |
(*As above but without the (generally useless) 3rd assumption*) |
|
46820 | 451 |
lemma ReplaceE2 [elim!]: |
452 |
"[| b \<in> {y. x\<in>A, P(x,y)}; |
|
453 |
!!x. [| x: A; P(x,b) |] ==> R |
|
13780 | 454 |
|] ==> R" |
46820 | 455 |
by (erule ReplaceE, blast) |
13780 | 456 |
|
457 |
lemma Replace_cong [cong]: |
|
46820 | 458 |
"[| A=B; !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==> |
13780 | 459 |
Replace(A,P) = Replace(B,Q)" |
46820 | 460 |
apply (rule equality_iffI) |
461 |
apply (simp add: Replace_iff) |
|
13780 | 462 |
done |
463 |
||
464 |
||
60770 | 465 |
subsection\<open>Rules for RepFun\<close> |
13780 | 466 |
|
46820 | 467 |
lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}" |
13780 | 468 |
by (simp add: RepFun_def Replace_iff, blast) |
469 |
||
470 |
(*Useful for coinduction proofs*) |
|
46820 | 471 |
lemma RepFun_eqI [intro]: "[| b=f(a); a \<in> A |] ==> b \<in> {f(x). x\<in>A}" |
13780 | 472 |
apply (erule ssubst) |
473 |
apply (erule RepFunI) |
|
474 |
done |
|
475 |
||
476 |
lemma RepFunE [elim!]: |
|
46820 | 477 |
"[| b \<in> {f(x). x\<in>A}; |
478 |
!!x.[| x\<in>A; b=f(x) |] ==> P |] ==> |
|
13780 | 479 |
P" |
46820 | 480 |
by (simp add: RepFun_def Replace_iff, blast) |
13780 | 481 |
|
46820 | 482 |
lemma RepFun_cong [cong]: |
14227 | 483 |
"[| A=B; !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)" |
13780 | 484 |
by (simp add: RepFun_def) |
485 |
||
46820 | 486 |
lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))" |
13780 | 487 |
by (unfold Bex_def, blast) |
488 |
||
14227 | 489 |
lemma triv_RepFun [simp]: "{x. x\<in>A} = A" |
13780 | 490 |
by blast |
491 |
||
492 |
||
60770 | 493 |
subsection\<open>Rules for Collect -- forming a subset by separation\<close> |
13780 | 494 |
|
495 |
(*Separation is derivable from Replacement*) |
|
46820 | 496 |
lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)" |
13780 | 497 |
by (unfold Collect_def, blast) |
498 |
||
46820 | 499 |
lemma CollectI [intro!]: "[| a\<in>A; P(a) |] ==> a \<in> {x\<in>A. P(x)}" |
13780 | 500 |
by simp |
501 |
||
46820 | 502 |
lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)}; [| a\<in>A; P(a) |] ==> R |] ==> R" |
13780 | 503 |
by simp |
504 |
||
46820 | 505 |
lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A" |
13780 | 506 |
by (erule CollectE, assumption) |
507 |
||
46820 | 508 |
lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)" |
13780 | 509 |
by (erule CollectE, assumption) |
510 |
||
511 |
lemma Collect_cong [cong]: |
|
46820 | 512 |
"[| A=B; !!x. x\<in>B ==> P(x) <-> Q(x) |] |
13780 | 513 |
==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))" |
514 |
by (simp add: Collect_def) |
|
515 |
||
516 |
||
60770 | 517 |
subsection\<open>Rules for Unions\<close> |
13780 | 518 |
|
519 |
declare Union_iff [simp] |
|
520 |
||
521 |
(*The order of the premises presupposes that C is rigid; A may be flexible*) |
|
46820 | 522 |
lemma UnionI [intro]: "[| B: C; A: B |] ==> A: \<Union>(C)" |
13780 | 523 |
by (simp, blast) |
524 |
||
46820 | 525 |
lemma UnionE [elim!]: "[| A \<in> \<Union>(C); !!B.[| A: B; B: C |] ==> R |] ==> R" |
13780 | 526 |
by (simp, blast) |
527 |
||
528 |
||
60770 | 529 |
subsection\<open>Rules for Unions of families\<close> |
46820 | 530 |
(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *) |
13780 | 531 |
|
46820 | 532 |
lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))" |
13780 | 533 |
by (simp add: Bex_def, blast) |
534 |
||
535 |
(*The order of the premises presupposes that A is rigid; b may be flexible*) |
|
14227 | 536 |
lemma UN_I: "[| a: A; b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))" |
13780 | 537 |
by (simp, blast) |
538 |
||
539 |
||
46820 | 540 |
lemma UN_E [elim!]: |
541 |
"[| b \<in> (\<Union>x\<in>A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R" |
|
542 |
by blast |
|
13780 | 543 |
|
46820 | 544 |
lemma UN_cong: |
14227 | 545 |
"[| A=B; !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))" |
46820 | 546 |
by simp |
13780 | 547 |
|
548 |
||
46820 | 549 |
(*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*) |
13780 | 550 |
|
551 |
(* UN_E appears before UnionE so that it is tried first, to avoid expensive |
|
552 |
calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge |
|
553 |
the search space.*) |
|
554 |
||
555 |
||
60770 | 556 |
subsection\<open>Rules for the empty set\<close> |
13780 | 557 |
|
46820 | 558 |
(*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0 |
13780 | 559 |
See Suppes, page 21.*) |
46820 | 560 |
lemma not_mem_empty [simp]: "a \<notin> 0" |
13780 | 561 |
apply (cut_tac foundation) |
562 |
apply (best dest: equalityD2) |
|
563 |
done |
|
564 |
||
45602 | 565 |
lemmas emptyE [elim!] = not_mem_empty [THEN notE] |
13780 | 566 |
|
567 |
||
46820 | 568 |
lemma empty_subsetI [simp]: "0 \<subseteq> A" |
569 |
by blast |
|
13780 | 570 |
|
14227 | 571 |
lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0" |
13780 | 572 |
by blast |
573 |
||
46820 | 574 |
lemma equals0D [dest]: "A=0 ==> a \<notin> A" |
13780 | 575 |
by blast |
576 |
||
577 |
declare sym [THEN equals0D, dest] |
|
578 |
||
46820 | 579 |
lemma not_emptyI: "a\<in>A ==> A \<noteq> 0" |
13780 | 580 |
by blast |
581 |
||
46820 | 582 |
lemma not_emptyE: "[| A \<noteq> 0; !!x. x\<in>A ==> R |] ==> R" |
13780 | 583 |
by blast |
584 |
||
585 |
||
60770 | 586 |
subsection\<open>Rules for Inter\<close> |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
587 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
588 |
(*Not obviously useful for proving InterI, InterD, InterE*) |
46820 | 589 |
lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0" |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
590 |
by (simp add: Inter_def Ball_def, blast) |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
591 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
592 |
(* Intersection is well-behaved only if the family is non-empty! *) |
46820 | 593 |
lemma InterI [intro!]: |
594 |
"[| !!x. x: C ==> A: x; C\<noteq>0 |] ==> A \<in> \<Inter>(C)" |
|
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
595 |
by (simp add: Inter_iff) |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
596 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
597 |
(*A "destruct" rule -- every B in C contains A as an element, but |
14227 | 598 |
A\<in>B can hold when B\<in>C does not! This rule is analogous to "spec". *) |
46820 | 599 |
lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C); B \<in> C |] ==> A \<in> B" |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
600 |
by (unfold Inter_def, blast) |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
601 |
|
46820 | 602 |
(*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *) |
603 |
lemma InterE [elim]: |
|
604 |
"[| A \<in> \<Inter>(C); B\<notin>C ==> R; A\<in>B ==> R |] ==> R" |
|
605 |
by (simp add: Inter_def, blast) |
|
606 |
||
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
607 |
|
60770 | 608 |
subsection\<open>Rules for Intersections of families\<close> |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
609 |
|
46820 | 610 |
(* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *) |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
611 |
|
46820 | 612 |
lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0" |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
613 |
by (force simp add: Inter_def) |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
614 |
|
14227 | 615 |
lemma INT_I: "[| !!x. x: A ==> b: B(x); A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))" |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
616 |
by blast |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
617 |
|
46820 | 618 |
lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x)); a: A |] ==> b \<in> B(a)" |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
619 |
by blast |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
620 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
621 |
lemma INT_cong: |
14227 | 622 |
"[| A=B; !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))" |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
623 |
by simp |
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
624 |
|
46820 | 625 |
(*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*) |
14095
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
626 |
|
a1ba833d6b61
Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents:
14076
diff
changeset
|
627 |
|
60770 | 628 |
subsection\<open>Rules for Powersets\<close> |
13780 | 629 |
|
46820 | 630 |
lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)" |
13780 | 631 |
by (erule Pow_iff [THEN iffD2]) |
632 |
||
14227 | 633 |
lemma PowD: "A \<in> Pow(B) ==> A<=B" |
13780 | 634 |
by (erule Pow_iff [THEN iffD1]) |
635 |
||
636 |
declare Pow_iff [iff] |
|
637 |
||
69593 | 638 |
lemmas Pow_bottom = empty_subsetI [THEN PowI] \<comment> \<open>\<^term>\<open>0 \<in> Pow(B)\<close>\<close> |
639 |
lemmas Pow_top = subset_refl [THEN PowI] \<comment> \<open>\<^term>\<open>A \<in> Pow(A)\<close>\<close> |
|
13780 | 640 |
|
641 |
||
60770 | 642 |
subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close> |
13780 | 643 |
|
46820 | 644 |
(*The search is undirected. Allowing redundant introduction rules may |
13780 | 645 |
make it diverge. Variable b represents ANY map, such as |
14227 | 646 |
(lam x\<in>A.b(x)): A->Pow(A). *) |
46820 | 647 |
lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S" |
13780 | 648 |
by (best elim!: equalityCE del: ReplaceI RepFun_eqI) |
649 |
||
0 | 650 |
end |