1 (* Title: ZF/ZF.thy |
1 section\<open>Main ZF Theory: Everything Except AC\<close> |
2 Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
|
3 Copyright 1993 University of Cambridge |
|
4 *) |
|
5 |
2 |
6 section \<open>Zermelo-Fraenkel Set Theory\<close> |
3 theory ZF imports List_ZF IntDiv_ZF CardinalArith begin |
7 |
4 |
8 theory ZF |
5 (*The theory of "iterates" logically belongs to Nat, but can't go there because |
9 imports "~~/src/FOL/FOL" |
6 primrec isn't available into after Datatype.*) |
10 begin |
|
11 |
7 |
12 subsection \<open>Signature\<close> |
8 subsection\<open>Iteration of the function @{term F}\<close> |
13 |
9 |
14 declare [[eta_contract = false]] |
10 consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) |
15 |
11 |
16 typedecl i |
12 primrec |
17 instance i :: "term" .. |
13 "F^0 (x) = x" |
|
14 "F^(succ(n)) (x) = F(F^n (x))" |
18 |
15 |
19 axiomatization mem :: "[i, i] \<Rightarrow> o" (infixl "\<in>" 50) \<comment> \<open>membership relation\<close> |
16 definition |
20 and zero :: "i" ("0") \<comment> \<open>the empty set\<close> |
17 iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where |
21 and Pow :: "i \<Rightarrow> i" \<comment> \<open>power sets\<close> |
18 "F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)" |
22 and Inf :: "i" \<comment> \<open>infinite set\<close> |
|
23 and Union :: "i \<Rightarrow> i" ("\<Union>_" [90] 90) |
|
24 and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" |
|
25 |
19 |
26 abbreviation not_mem :: "[i, i] \<Rightarrow> o" (infixl "\<notin>" 50) \<comment> \<open>negated membership relation\<close> |
20 lemma iterates_triv: |
27 where "x \<notin> y \<equiv> \<not> (x \<in> y)" |
21 "[| n\<in>nat; F(x) = x |] ==> F^n (x) = x" |
|
22 by (induct n rule: nat_induct, simp_all) |
|
23 |
|
24 lemma iterates_type [TC]: |
|
25 "[| n \<in> nat; a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |] |
|
26 ==> F^n (a) \<in> A" |
|
27 by (induct n rule: nat_induct, simp_all) |
|
28 |
|
29 lemma iterates_omega_triv: |
|
30 "F(x) = x ==> F^\<omega> (x) = x" |
|
31 by (simp add: iterates_omega_def iterates_triv) |
|
32 |
|
33 lemma Ord_iterates [simp]: |
|
34 "[| n\<in>nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] |
|
35 ==> Ord(F^n (x))" |
|
36 by (induct n rule: nat_induct, simp_all) |
|
37 |
|
38 lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))" |
|
39 by (induct_tac n, simp_all) |
28 |
40 |
29 |
41 |
30 subsection \<open>Bounded Quantifiers\<close> |
42 subsection\<open>Transfinite Recursion\<close> |
31 |
43 |
32 definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o" |
44 text\<open>Transfinite recursion for definitions based on the |
33 where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)" |
45 three cases of ordinals\<close> |
34 |
46 |
35 definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o" |
47 definition |
36 where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)" |
48 transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where |
|
49 "transrec3(k, a, b, c) == |
|
50 transrec(k, \<lambda>x r. |
|
51 if x=0 then a |
|
52 else if Limit(x) then c(x, \<lambda>y\<in>x. r`y) |
|
53 else b(Arith.pred(x), r ` Arith.pred(x)))" |
37 |
54 |
38 syntax |
55 lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a" |
39 "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<forall>_\<in>_./ _)" 10) |
56 by (rule transrec3_def [THEN def_transrec, THEN trans], simp) |
40 "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<exists>_\<in>_./ _)" 10) |
57 |
41 translations |
58 lemma transrec3_succ [simp]: |
42 "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)" |
59 "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))" |
43 "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)" |
60 by (rule transrec3_def [THEN def_transrec, THEN trans], simp) |
|
61 |
|
62 lemma transrec3_Limit: |
|
63 "Limit(i) ==> |
|
64 transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))" |
|
65 by (rule transrec3_def [THEN def_transrec, THEN trans], force) |
44 |
66 |
45 |
67 |
46 subsection \<open>Variations on Replacement\<close> |
68 declaration \<open>fn _ => |
47 |
69 Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => |
48 (* Derived form of replacement, restricting P to its functional part. |
70 map mk_eq o Ord_atomize o Variable.gen_all ctxt)) |
49 The resulting set (for functional P) is the same as with |
71 \<close> |
50 PrimReplace, but the rules are simpler. *) |
|
51 definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" |
|
52 where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))" |
|
53 |
|
54 syntax |
|
55 "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})") |
|
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 |
|
66 "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51]) |
|
67 translations |
|
68 "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)" |
|
69 |
|
70 |
|
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 |
|
77 "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" ("(1{_ \<in> _ ./ _})") |
|
78 translations |
|
79 "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)" |
|
80 |
|
81 |
|
82 subsection \<open>General union and intersection\<close> |
|
83 |
|
84 definition Inter :: "i => i" ("\<Inter>_" [90] 90) |
|
85 where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}" |
|
86 |
|
87 syntax |
|
88 "_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10) |
|
89 "_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10) |
|
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})" |
|
93 |
|
94 |
|
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)}" |
|
102 |
|
103 definition Subset :: "[i, i] \<Rightarrow> o" (infixl "\<subseteq>" 50) \<comment> \<open>subset relation\<close> |
|
104 where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B" |
|
105 |
|
106 definition Diff :: "[i, i] \<Rightarrow> i" (infixl "-" 65) \<comment> \<open>set difference\<close> |
|
107 where "A - B == { x\<in>A . ~(x\<in>B) }" |
|
108 |
|
109 definition Un :: "[i, i] \<Rightarrow> i" (infixl "\<union>" 65) \<comment> \<open>binary union\<close> |
|
110 where "A \<union> B == \<Union>(Upair(A,B))" |
|
111 |
|
112 definition Int :: "[i, i] \<Rightarrow> i" (infixl "\<inter>" 70) \<comment> \<open>binary intersection\<close> |
|
113 where "A \<inter> B == \<Inter>(Upair(A,B))" |
|
114 |
|
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)" |
|
120 |
|
121 nonterminal "is" |
|
122 syntax |
|
123 "" :: "i \<Rightarrow> is" ("_") |
|
124 "_Enum" :: "[i, is] \<Rightarrow> is" ("_,/ _") |
|
125 "_Finset" :: "is \<Rightarrow> i" ("{(_)}") |
|
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. *) |
|
136 |
|
137 axiomatization |
|
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 |
|
142 |
|
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 |
|
145 |
|
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))" |
|
152 |
|
153 |
|
154 subsection \<open>Definite descriptions -- via Replace over the set "1"\<close> |
|
155 |
|
156 definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder "THE " 10) |
|
157 where the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})" |
|
158 |
|
159 definition If :: "[o, i, i] \<Rightarrow> i" ("(if (_)/ then (_)/ else (_))" [10] 10) |
|
160 where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b" |
|
161 |
|
162 abbreviation (input) |
|
163 old_if :: "[o, i, i] => i" ("if '(_,_,_')") |
|
164 where "if(P,a,b) == If(P,a,b)" |
|
165 |
|
166 |
|
167 subsection \<open>Ordered Pairing\<close> |
|
168 |
|
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)" |
|
175 |
|
176 definition snd :: "i \<Rightarrow> i" |
|
177 where "snd(p) == THE b. \<exists>a. p = Pair(a, b)" |
|
178 |
|
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 |
|
185 "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>") |
|
186 "" :: "pttrn => patterns" ("_") |
|
187 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/_") |
|
188 "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>") |
|
189 translations |
|
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)" |
|
194 |
|
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 |
|
198 abbreviation cart_prod :: "[i, i] => i" (infixr "\<times>" 80) \<comment> \<open>Cartesian product\<close> |
|
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 |
|
220 definition "function" :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close> |
|
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 |
|
223 definition Image :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>image\<close> |
|
224 where image_def: "r `` A == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}" |
|
225 |
|
226 definition vimage :: "[i, i] \<Rightarrow> i" (infixl "-``" 90) \<comment> \<open>inverse image\<close> |
|
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 |
|
239 definition "apply" :: "[i, i] \<Rightarrow> i" (infixl "`" 90) \<comment> \<open>function application\<close> |
|
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 |
|
245 abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr "->" 60) \<comment> \<open>function space\<close> |
|
246 where "A -> B \<equiv> Pi(A, \<lambda>_. B)" |
|
247 |
|
248 |
|
249 (* binder syntax *) |
|
250 |
|
251 syntax |
|
252 "_PROD" :: "[pttrn, i, i] => i" ("(3\<Prod>_\<in>_./ _)" 10) |
|
253 "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sum>_\<in>_./ _)" 10) |
|
254 "_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10) |
|
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> |
|
262 |
|
263 notation (ASCII) |
|
264 cart_prod (infixr "*" 80) and |
|
265 Int (infixl "Int" 70) and |
|
266 Un (infixl "Un" 65) and |
|
267 function_space (infixr "\<rightarrow>" 60) and |
|
268 Subset (infixl "<=" 50) and |
|
269 mem (infixl ":" 50) and |
|
270 not_mem (infixl "~:" 50) |
|
271 |
|
272 syntax (ASCII) |
|
273 "_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) |
|
274 "_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) |
|
275 "_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") |
|
276 "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") |
|
277 "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) |
|
278 "_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) |
|
279 "_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) |
|
280 "_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) |
|
281 "_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) |
|
282 "_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) |
|
283 "_Tuple" :: "[i, is] => i" ("<(_,/ _)>") |
|
284 "_pattern" :: "patterns => pttrn" ("<_>") |
|
285 |
|
286 |
|
287 subsection \<open>Substitution\<close> |
|
288 |
|
289 (*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) |
|
290 lemma subst_elem: "[| b\<in>A; a=b |] ==> a\<in>A" |
|
291 by (erule ssubst, assumption) |
|
292 |
|
293 |
|
294 subsection\<open>Bounded universal quantifier\<close> |
|
295 |
|
296 lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)" |
|
297 by (simp add: Ball_def) |
|
298 |
|
299 lemmas strip = impI allI ballI |
|
300 |
|
301 lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x); x: A |] ==> P(x)" |
|
302 by (simp add: Ball_def) |
|
303 |
|
304 (*Instantiates x first: better for automatic theorem proving?*) |
|
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) |
|
308 |
|
309 lemma ballE: "[| \<forall>x\<in>A. P(x); P(x) ==> Q; x\<notin>A ==> Q |] ==> Q" |
|
310 by blast |
|
311 |
|
312 (*Used in the datatype package*) |
|
313 lemma rev_bspec: "[| x: A; \<forall>x\<in>A. P(x) |] ==> P(x)" |
|
314 by (simp add: Ball_def) |
|
315 |
|
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)" |
|
318 by (simp add: Ball_def) |
|
319 |
|
320 (*Congruence rule for rewriting*) |
|
321 lemma ball_cong [cong]: |
|
322 "[| A=A'; !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))" |
|
323 by (simp add: Ball_def) |
|
324 |
|
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 |
|
332 |
|
333 subsection\<open>Bounded existential quantifier\<close> |
|
334 |
|
335 lemma bexI [intro]: "[| P(x); x: A |] ==> \<exists>x\<in>A. P(x)" |
|
336 by (simp add: Bex_def, blast) |
|
337 |
|
338 (*The best argument order when there is only one @{term"x\<in>A"}*) |
|
339 lemma rev_bexI: "[| x\<in>A; P(x) |] ==> \<exists>x\<in>A. P(x)" |
|
340 by blast |
|
341 |
|
342 (*Not of the general form for such rules. The existential quanitifer becomes universal. *) |
|
343 lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a); a: A |] ==> \<exists>x\<in>A. P(x)" |
|
344 by blast |
|
345 |
|
346 lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x); !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q" |
|
347 by (simp add: Bex_def, blast) |
|
348 |
|
349 (*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*) |
|
350 lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)" |
|
351 by (simp add: Bex_def) |
|
352 |
|
353 lemma bex_cong [cong]: |
|
354 "[| A=A'; !!x. x\<in>A' ==> P(x) <-> P'(x) |] |
|
355 ==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))" |
|
356 by (simp add: Bex_def cong: conj_cong) |
|
357 |
|
358 |
|
359 |
|
360 subsection\<open>Rules for subsets\<close> |
|
361 |
|
362 lemma subsetI [intro!]: |
|
363 "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B" |
|
364 by (simp add: subset_def) |
|
365 |
|
366 (*Rule in Modus Ponens style [was called subsetE] *) |
|
367 lemma subsetD [elim]: "[| A \<subseteq> B; c\<in>A |] ==> c\<in>B" |
|
368 apply (unfold subset_def) |
|
369 apply (erule bspec, assumption) |
|
370 done |
|
371 |
|
372 (*Classical elimination rule*) |
|
373 lemma subsetCE [elim]: |
|
374 "[| A \<subseteq> B; c\<notin>A ==> P; c\<in>B ==> P |] ==> P" |
|
375 by (simp add: subset_def, blast) |
|
376 |
|
377 (*Sometimes useful with premises in this order*) |
|
378 lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B" |
|
379 by blast |
|
380 |
|
381 lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A" |
|
382 by blast |
|
383 |
|
384 lemma rev_contra_subsetD: "[| c \<notin> B; A \<subseteq> B |] ==> c \<notin> A" |
|
385 by blast |
|
386 |
|
387 lemma subset_refl [simp]: "A \<subseteq> A" |
|
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*) |
|
394 lemma subset_iff: |
|
395 "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)" |
|
396 apply (unfold subset_def Ball_def) |
|
397 apply (rule iff_refl) |
|
398 done |
|
399 |
|
400 text\<open>For calculations\<close> |
|
401 declare subsetD [trans] rev_subsetD [trans] subset_trans [trans] |
|
402 |
|
403 |
|
404 subsection\<open>Rules for equality\<close> |
|
405 |
|
406 (*Anti-symmetry of the subset relation*) |
|
407 lemma equalityI [intro]: "[| A \<subseteq> B; B \<subseteq> A |] ==> A = B" |
|
408 by (rule extension [THEN iffD2], rule conjI) |
|
409 |
|
410 |
|
411 lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B" |
|
412 by (rule equalityI, blast+) |
|
413 |
|
414 lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1] |
|
415 lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2] |
|
416 |
|
417 lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" |
|
418 by (blast dest: equalityD1 equalityD2) |
|
419 |
|
420 lemma equalityCE: |
|
421 "[| A = B; [| c\<in>A; c\<in>B |] ==> P; [| c\<notin>A; c\<notin>B |] ==> P |] ==> P" |
|
422 by (erule equalityE, blast) |
|
423 |
|
424 lemma equality_iffD: |
|
425 "A = B ==> (!!x. x \<in> A <-> x \<in> B)" |
|
426 by auto |
|
427 |
|
428 |
|
429 subsection\<open>Rules for Replace -- the derived form of replacement\<close> |
|
430 |
|
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))" |
|
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. *) |
|
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) |
|
442 |
|
443 (*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *) |
|
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 |
|
447 |] ==> R" |
|
448 by (rule Replace_iff [THEN iffD1, THEN bexE], simp+) |
|
449 |
|
450 (*As above but without the (generally useless) 3rd assumption*) |
|
451 lemma ReplaceE2 [elim!]: |
|
452 "[| b \<in> {y. x\<in>A, P(x,y)}; |
|
453 !!x. [| x: A; P(x,b) |] ==> R |
|
454 |] ==> R" |
|
455 by (erule ReplaceE, blast) |
|
456 |
|
457 lemma Replace_cong [cong]: |
|
458 "[| A=B; !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==> |
|
459 Replace(A,P) = Replace(B,Q)" |
|
460 apply (rule equality_iffI) |
|
461 apply (simp add: Replace_iff) |
|
462 done |
|
463 |
|
464 |
|
465 subsection\<open>Rules for RepFun\<close> |
|
466 |
|
467 lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}" |
|
468 by (simp add: RepFun_def Replace_iff, blast) |
|
469 |
|
470 (*Useful for coinduction proofs*) |
|
471 lemma RepFun_eqI [intro]: "[| b=f(a); a \<in> A |] ==> b \<in> {f(x). x\<in>A}" |
|
472 apply (erule ssubst) |
|
473 apply (erule RepFunI) |
|
474 done |
|
475 |
|
476 lemma RepFunE [elim!]: |
|
477 "[| b \<in> {f(x). x\<in>A}; |
|
478 !!x.[| x\<in>A; b=f(x) |] ==> P |] ==> |
|
479 P" |
|
480 by (simp add: RepFun_def Replace_iff, blast) |
|
481 |
|
482 lemma RepFun_cong [cong]: |
|
483 "[| A=B; !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)" |
|
484 by (simp add: RepFun_def) |
|
485 |
|
486 lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))" |
|
487 by (unfold Bex_def, blast) |
|
488 |
|
489 lemma triv_RepFun [simp]: "{x. x\<in>A} = A" |
|
490 by blast |
|
491 |
|
492 |
|
493 subsection\<open>Rules for Collect -- forming a subset by separation\<close> |
|
494 |
|
495 (*Separation is derivable from Replacement*) |
|
496 lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)" |
|
497 by (unfold Collect_def, blast) |
|
498 |
|
499 lemma CollectI [intro!]: "[| a\<in>A; P(a) |] ==> a \<in> {x\<in>A. P(x)}" |
|
500 by simp |
|
501 |
|
502 lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)}; [| a\<in>A; P(a) |] ==> R |] ==> R" |
|
503 by simp |
|
504 |
|
505 lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A" |
|
506 by (erule CollectE, assumption) |
|
507 |
|
508 lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)" |
|
509 by (erule CollectE, assumption) |
|
510 |
|
511 lemma Collect_cong [cong]: |
|
512 "[| A=B; !!x. x\<in>B ==> P(x) <-> Q(x) |] |
|
513 ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))" |
|
514 by (simp add: Collect_def) |
|
515 |
|
516 |
|
517 subsection\<open>Rules for Unions\<close> |
|
518 |
|
519 declare Union_iff [simp] |
|
520 |
|
521 (*The order of the premises presupposes that C is rigid; A may be flexible*) |
|
522 lemma UnionI [intro]: "[| B: C; A: B |] ==> A: \<Union>(C)" |
|
523 by (simp, blast) |
|
524 |
|
525 lemma UnionE [elim!]: "[| A \<in> \<Union>(C); !!B.[| A: B; B: C |] ==> R |] ==> R" |
|
526 by (simp, blast) |
|
527 |
|
528 |
|
529 subsection\<open>Rules for Unions of families\<close> |
|
530 (* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *) |
|
531 |
|
532 lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))" |
|
533 by (simp add: Bex_def, blast) |
|
534 |
|
535 (*The order of the premises presupposes that A is rigid; b may be flexible*) |
|
536 lemma UN_I: "[| a: A; b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))" |
|
537 by (simp, blast) |
|
538 |
|
539 |
|
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 |
|
543 |
|
544 lemma UN_cong: |
|
545 "[| A=B; !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))" |
|
546 by simp |
|
547 |
|
548 |
|
549 (*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*) |
|
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 |
|
556 subsection\<open>Rules for the empty set\<close> |
|
557 |
|
558 (*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0 |
|
559 See Suppes, page 21.*) |
|
560 lemma not_mem_empty [simp]: "a \<notin> 0" |
|
561 apply (cut_tac foundation) |
|
562 apply (best dest: equalityD2) |
|
563 done |
|
564 |
|
565 lemmas emptyE [elim!] = not_mem_empty [THEN notE] |
|
566 |
|
567 |
|
568 lemma empty_subsetI [simp]: "0 \<subseteq> A" |
|
569 by blast |
|
570 |
|
571 lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0" |
|
572 by blast |
|
573 |
|
574 lemma equals0D [dest]: "A=0 ==> a \<notin> A" |
|
575 by blast |
|
576 |
|
577 declare sym [THEN equals0D, dest] |
|
578 |
|
579 lemma not_emptyI: "a\<in>A ==> A \<noteq> 0" |
|
580 by blast |
|
581 |
|
582 lemma not_emptyE: "[| A \<noteq> 0; !!x. x\<in>A ==> R |] ==> R" |
|
583 by blast |
|
584 |
|
585 |
|
586 subsection\<open>Rules for Inter\<close> |
|
587 |
|
588 (*Not obviously useful for proving InterI, InterD, InterE*) |
|
589 lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0" |
|
590 by (simp add: Inter_def Ball_def, blast) |
|
591 |
|
592 (* Intersection is well-behaved only if the family is non-empty! *) |
|
593 lemma InterI [intro!]: |
|
594 "[| !!x. x: C ==> A: x; C\<noteq>0 |] ==> A \<in> \<Inter>(C)" |
|
595 by (simp add: Inter_iff) |
|
596 |
|
597 (*A "destruct" rule -- every B in C contains A as an element, but |
|
598 A\<in>B can hold when B\<in>C does not! This rule is analogous to "spec". *) |
|
599 lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C); B \<in> C |] ==> A \<in> B" |
|
600 by (unfold Inter_def, blast) |
|
601 |
|
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 |
|
607 |
|
608 subsection\<open>Rules for Intersections of families\<close> |
|
609 |
|
610 (* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *) |
|
611 |
|
612 lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0" |
|
613 by (force simp add: Inter_def) |
|
614 |
|
615 lemma INT_I: "[| !!x. x: A ==> b: B(x); A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))" |
|
616 by blast |
|
617 |
|
618 lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x)); a: A |] ==> b \<in> B(a)" |
|
619 by blast |
|
620 |
|
621 lemma INT_cong: |
|
622 "[| A=B; !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))" |
|
623 by simp |
|
624 |
|
625 (*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*) |
|
626 |
|
627 |
|
628 subsection\<open>Rules for Powersets\<close> |
|
629 |
|
630 lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)" |
|
631 by (erule Pow_iff [THEN iffD2]) |
|
632 |
|
633 lemma PowD: "A \<in> Pow(B) ==> A<=B" |
|
634 by (erule Pow_iff [THEN iffD1]) |
|
635 |
|
636 declare Pow_iff [iff] |
|
637 |
|
638 lemmas Pow_bottom = empty_subsetI [THEN PowI] \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close> |
|
639 lemmas Pow_top = subset_refl [THEN PowI] \<comment>\<open>@{term"A \<in> Pow(A)"}\<close> |
|
640 |
|
641 |
|
642 subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close> |
|
643 |
|
644 (*The search is undirected. Allowing redundant introduction rules may |
|
645 make it diverge. Variable b represents ANY map, such as |
|
646 (lam x\<in>A.b(x)): A->Pow(A). *) |
|
647 lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S" |
|
648 by (best elim!: equalityCE del: ReplaceI RepFun_eqI) |
|
649 |
72 |
650 end |
73 end |