9 Classical Theorems of Set Theory. |
9 Classical Theorems of Set Theory. |
10 |
10 |
11 Union_in_Pow is proved in ZF.ML |
11 Union_in_Pow is proved in ZF.ML |
12 *) |
12 *) |
13 |
13 |
14 Zorn = OrderArith + AC + Inductive + |
14 theory Zorn = OrderArith + AC + Inductive: |
15 |
15 |
16 consts |
16 constdefs |
17 Subset_rel :: i=>i |
17 Subset_rel :: "i=>i" |
18 chain, maxchain :: i=>i |
18 "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}" |
19 super :: [i,i]=>i |
19 |
20 |
20 chain :: "i=>i" |
21 defs |
21 "chain(A) == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}" |
22 Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}" |
22 |
23 |
23 maxchain :: "i=>i" |
24 chain_def "chain(A) == {F: Pow(A). ALL X:F. ALL Y:F. X<=Y | Y<=X}" |
24 "maxchain(A) == {c: chain(A). super(A,c)=0}" |
25 super_def "super(A,c) == {d: chain(A). c<=d & c~=d}" |
25 |
26 maxchain_def "maxchain(A) == {c: chain(A). super(A,c)=0}" |
26 super :: "[i,i]=>i" |
27 |
27 "super(A,c) == {d: chain(A). c<=d & c~=d}" |
|
28 |
|
29 |
|
30 constdefs |
|
31 increasing :: "i=>i" |
|
32 "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}" |
28 |
33 |
29 (** We could make the inductive definition conditional on next: increasing(S) |
34 (** We could make the inductive definition conditional on next: increasing(S) |
30 but instead we make this a side-condition of an introduction rule. Thus |
35 but instead we make this a side-condition of an introduction rule. Thus |
31 the induction rule lets us assume that condition! Many inductive proofs |
36 the induction rule lets us assume that condition! Many inductive proofs |
32 are therefore unconditional. |
37 are therefore unconditional. |
33 **) |
38 **) |
34 consts |
39 consts |
35 "TFin" :: [i,i]=>i |
40 "TFin" :: "[i,i]=>i" |
36 |
41 |
37 inductive |
42 inductive |
38 domains "TFin(S,next)" <= "Pow(S)" |
43 domains "TFin(S,next)" <= "Pow(S)" |
39 intrs |
44 intros |
40 nextI "[| x : TFin(S,next); next: increasing(S) |
45 nextI: "[| x : TFin(S,next); next: increasing(S) |] |
41 |] ==> next`x : TFin(S,next)" |
46 ==> next`x : TFin(S,next)" |
42 |
47 |
43 Pow_UnionI "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)" |
48 Pow_UnionI: "Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)" |
44 |
49 |
45 monos Pow_mono |
50 monos Pow_mono |
46 con_defs increasing_def |
51 con_defs increasing_def |
47 type_intrs "[CollectD1 RS apply_funtype, Union_in_Pow]" |
52 type_intros CollectD1 [THEN apply_funtype] Union_in_Pow |
|
53 |
|
54 |
|
55 (*** Section 1. Mathematical Preamble ***) |
|
56 |
|
57 lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)" |
|
58 apply blast |
|
59 done |
|
60 |
|
61 lemma Inter_lemma0: "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B" |
|
62 apply blast |
|
63 done |
|
64 |
|
65 |
|
66 (*** Section 2. The Transfinite Construction ***) |
|
67 |
|
68 lemma increasingD1: "f: increasing(A) ==> f: Pow(A)->Pow(A)" |
|
69 apply (unfold increasing_def) |
|
70 apply (erule CollectD1) |
|
71 done |
|
72 |
|
73 lemma increasingD2: "[| f: increasing(A); x<=A |] ==> x <= f`x" |
|
74 apply (unfold increasing_def) |
|
75 apply (blast intro: elim:); |
|
76 done |
|
77 |
|
78 lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard] |
|
79 |
|
80 lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard] |
|
81 |
|
82 |
|
83 (** Structural induction on TFin(S,next) **) |
|
84 |
|
85 lemma TFin_induct: |
|
86 "[| n: TFin(S,next); |
|
87 !!x. [| x : TFin(S,next); P(x); next: increasing(S) |] ==> P(next`x); |
|
88 !!Y. [| Y <= TFin(S,next); ALL y:Y. P(y) |] ==> P(Union(Y)) |
|
89 |] ==> P(n)" |
|
90 apply (erule TFin.induct) |
|
91 apply blast+ |
|
92 done |
|
93 |
|
94 |
|
95 (*** Section 3. Some Properties of the Transfinite Construction ***) |
|
96 |
|
97 lemmas increasing_trans = subset_trans [OF _ increasingD2, |
|
98 OF _ _ TFin_is_subset] |
|
99 |
|
100 (*Lemma 1 of section 3.1*) |
|
101 lemma TFin_linear_lemma1: |
|
102 "[| n: TFin(S,next); m: TFin(S,next); |
|
103 ALL x: TFin(S,next) . x<=m --> x=m | next`x<=m |] |
|
104 ==> n<=m | next`m<=n" |
|
105 apply (erule TFin_induct) |
|
106 apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*) |
|
107 (*downgrade subsetI from intro! to intro*) |
|
108 apply (blast dest: increasing_trans) |
|
109 done |
|
110 |
|
111 (*Lemma 2 of section 3.2. Interesting in its own right! |
|
112 Requires next: increasing(S) in the second induction step. *) |
|
113 lemma TFin_linear_lemma2: |
|
114 "[| m: TFin(S,next); next: increasing(S) |] |
|
115 ==> ALL n: TFin(S,next) . n<=m --> n=m | next`n<=m" |
|
116 apply (erule TFin_induct) |
|
117 apply (rule impI [THEN ballI]) |
|
118 (*case split using TFin_linear_lemma1*) |
|
119 apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE], |
|
120 assumption+) |
|
121 apply (blast del: subsetI |
|
122 intro: increasing_trans subsetI) |
|
123 apply (blast intro: elim:); |
|
124 (*second induction step*) |
|
125 apply (rule impI [THEN ballI]) |
|
126 apply (rule Union_lemma0 [THEN disjE]) |
|
127 apply (erule_tac [3] disjI2) |
|
128 prefer 2 apply (blast intro: elim:); |
|
129 apply (rule ballI) |
|
130 apply (drule bspec, assumption) |
|
131 apply (drule subsetD, assumption) |
|
132 apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE], |
|
133 assumption+) |
|
134 apply (blast intro: elim:); |
|
135 apply (erule increasingD2 [THEN subset_trans, THEN disjI1]) |
|
136 apply (blast dest: TFin_is_subset)+ |
|
137 done |
|
138 |
|
139 (*a more convenient form for Lemma 2*) |
|
140 lemma TFin_subsetD: |
|
141 "[| n<=m; m: TFin(S,next); n: TFin(S,next); next: increasing(S) |] |
|
142 ==> n=m | next`n<=m" |
|
143 by (blast dest: TFin_linear_lemma2 [rule_format]) |
|
144 |
|
145 (*Consequences from section 3.3 -- Property 3.2, the ordering is total*) |
|
146 lemma TFin_subset_linear: |
|
147 "[| m: TFin(S,next); n: TFin(S,next); next: increasing(S) |] |
|
148 ==> n<=m | m<=n" |
|
149 apply (rule disjE) |
|
150 apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2]) |
|
151 apply (assumption+, erule disjI2) |
|
152 apply (blast del: subsetI |
|
153 intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset) |
|
154 done |
|
155 |
|
156 |
|
157 (*Lemma 3 of section 3.3*) |
|
158 lemma equal_next_upper: |
|
159 "[| n: TFin(S,next); m: TFin(S,next); m = next`m |] ==> n<=m" |
|
160 apply (erule TFin_induct) |
|
161 apply (drule TFin_subsetD) |
|
162 apply (assumption+) |
|
163 apply (force ); |
|
164 apply (blast) |
|
165 done |
|
166 |
|
167 (*Property 3.3 of section 3.3*) |
|
168 lemma equal_next_Union: "[| m: TFin(S,next); next: increasing(S) |] |
|
169 ==> m = next`m <-> m = Union(TFin(S,next))" |
|
170 apply (rule iffI) |
|
171 apply (rule Union_upper [THEN equalityI]) |
|
172 apply (rule_tac [2] equal_next_upper [THEN Union_least]) |
|
173 apply (assumption+) |
|
174 apply (erule ssubst) |
|
175 apply (rule increasingD2 [THEN equalityI] , assumption) |
|
176 apply (blast del: subsetI |
|
177 intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+ |
|
178 done |
|
179 |
|
180 |
|
181 (*** Section 4. Hausdorff's Theorem: every set contains a maximal chain ***) |
|
182 (*** NB: We assume the partial ordering is <=, the subset relation! **) |
|
183 |
|
184 (** Defining the "next" operation for Hausdorff's Theorem **) |
|
185 |
|
186 lemma chain_subset_Pow: "chain(A) <= Pow(A)" |
|
187 apply (unfold chain_def) |
|
188 apply (rule Collect_subset) |
|
189 done |
|
190 |
|
191 lemma super_subset_chain: "super(A,c) <= chain(A)" |
|
192 apply (unfold super_def) |
|
193 apply (rule Collect_subset) |
|
194 done |
|
195 |
|
196 lemma maxchain_subset_chain: "maxchain(A) <= chain(A)" |
|
197 apply (unfold maxchain_def) |
|
198 apply (rule Collect_subset) |
|
199 done |
|
200 |
|
201 lemma choice_super: "[| ch : (PROD X:Pow(chain(S)) - {0}. X); |
|
202 X : chain(S); X ~: maxchain(S) |] |
|
203 ==> ch ` super(S,X) : super(S,X)" |
|
204 apply (erule apply_type) |
|
205 apply (unfold super_def maxchain_def) |
|
206 apply blast |
|
207 done |
|
208 |
|
209 lemma choice_not_equals: |
|
210 "[| ch : (PROD X:Pow(chain(S)) - {0}. X); |
|
211 X : chain(S); X ~: maxchain(S) |] |
|
212 ==> ch ` super(S,X) ~= X" |
|
213 apply (rule notI) |
|
214 apply (drule choice_super) |
|
215 apply assumption |
|
216 apply assumption |
|
217 apply (simp add: super_def) |
|
218 done |
|
219 |
|
220 (*This justifies Definition 4.4*) |
|
221 lemma Hausdorff_next_exists: |
|
222 "ch: (PROD X: Pow(chain(S))-{0}. X) ==> |
|
223 EX next: increasing(S). ALL X: Pow(S). |
|
224 next`X = if(X: chain(S)-maxchain(S), ch`super(S,X), X)" |
|
225 apply (rule bexI) |
|
226 apply (rule ballI) |
|
227 apply (rule beta) |
|
228 apply assumption |
|
229 apply (unfold increasing_def) |
|
230 apply (rule CollectI) |
|
231 apply (rule lam_type) |
|
232 apply (simp (no_asm_simp)) |
|
233 apply (blast dest: super_subset_chain [THEN subsetD] chain_subset_Pow [THEN subsetD] choice_super) |
|
234 (*Now, verify that it increases*) |
|
235 apply (simp (no_asm_simp) add: Pow_iff subset_refl) |
|
236 apply safe |
|
237 apply (drule choice_super) |
|
238 apply (assumption+) |
|
239 apply (unfold super_def) |
|
240 apply blast |
|
241 done |
|
242 |
|
243 (*Lemma 4*) |
|
244 lemma TFin_chain_lemma4: |
|
245 "[| c: TFin(S,next); |
|
246 ch: (PROD X: Pow(chain(S))-{0}. X); |
|
247 next: increasing(S); |
|
248 ALL X: Pow(S). next`X = |
|
249 if(X: chain(S)-maxchain(S), ch`super(S,X), X) |] |
|
250 ==> c: chain(S)" |
|
251 apply (erule TFin_induct) |
|
252 apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD] |
|
253 choice_super [THEN super_subset_chain [THEN subsetD]]) |
|
254 apply (unfold chain_def) |
|
255 apply (rule CollectI , blast) |
|
256 apply safe |
|
257 apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE]) |
|
258 apply fast+ (*Blast_tac's slow*) |
|
259 done |
|
260 |
|
261 lemma Hausdorff: "EX c. c : maxchain(S)" |
|
262 apply (rule AC_Pi_Pow [THEN exE]) |
|
263 apply (rule Hausdorff_next_exists [THEN bexE]) |
|
264 apply assumption |
|
265 apply (rename_tac ch "next") |
|
266 apply (subgoal_tac "Union (TFin (S,next)) : chain (S) ") |
|
267 prefer 2 |
|
268 apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI]) |
|
269 apply (rule_tac x = "Union (TFin (S,next))" in exI) |
|
270 apply (rule classical) |
|
271 apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))") |
|
272 apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric]) |
|
273 apply (rule_tac [2] subset_refl [THEN TFin_UnionI]) |
|
274 prefer 2 apply (assumption) |
|
275 apply (rule_tac [2] refl) |
|
276 apply (simp add: subset_refl [THEN TFin_UnionI, |
|
277 THEN TFin.dom_subset [THEN subsetD, THEN PowD]]) |
|
278 apply (erule choice_not_equals [THEN notE]) |
|
279 apply (assumption+) |
|
280 done |
|
281 |
|
282 |
|
283 (*** Section 5. Zorn's Lemma: if all chains in S have upper bounds in S |
|
284 then S contains a maximal element ***) |
|
285 |
|
286 (*Used in the proof of Zorn's Lemma*) |
|
287 lemma chain_extend: |
|
288 "[| c: chain(A); z: A; ALL x:c. x<=z |] ==> cons(z,c) : chain(A)" |
|
289 apply (unfold chain_def) |
|
290 apply blast |
|
291 done |
|
292 |
|
293 lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z" |
|
294 apply (rule Hausdorff [THEN exE]) |
|
295 apply (simp add: maxchain_def) |
|
296 apply (rename_tac c) |
|
297 apply (rule_tac x = "Union (c)" in bexI) |
|
298 prefer 2 apply (blast) |
|
299 apply safe |
|
300 apply (rename_tac z) |
|
301 apply (rule classical) |
|
302 apply (subgoal_tac "cons (z,c) : super (S,c) ") |
|
303 apply (blast elim: equalityE) |
|
304 apply (unfold super_def) |
|
305 apply safe |
|
306 apply (fast elim: chain_extend) |
|
307 apply (fast elim: equalityE) |
|
308 done |
|
309 |
|
310 |
|
311 (*** Section 6. Zermelo's Theorem: every set can be well-ordered ***) |
|
312 |
|
313 (*Lemma 5*) |
|
314 lemma TFin_well_lemma5: |
|
315 "[| n: TFin(S,next); Z <= TFin(S,next); z:Z; ~ Inter(Z) : Z |] |
|
316 ==> ALL m:Z. n<=m" |
|
317 apply (erule TFin_induct) |
|
318 prefer 2 apply (blast) (*second induction step is easy*) |
|
319 apply (rule ballI) |
|
320 apply (rule bspec [THEN TFin_subsetD, THEN disjE]) |
|
321 apply (auto ); |
|
322 apply (subgoal_tac "m = Inter (Z) ") |
|
323 apply blast+ |
|
324 done |
|
325 |
|
326 (*Well-ordering of TFin(S,next)*) |
|
327 lemma well_ord_TFin_lemma: "[| Z <= TFin(S,next); z:Z |] ==> Inter(Z) : Z" |
|
328 apply (rule classical) |
|
329 apply (subgoal_tac "Z = {Union (TFin (S,next))}") |
|
330 apply (simp (no_asm_simp) add: Inter_singleton) |
|
331 apply (erule equal_singleton) |
|
332 apply (rule Union_upper [THEN equalityI]) |
|
333 apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec]) |
|
334 apply (blast intro: elim:)+ |
|
335 done |
|
336 |
|
337 (*This theorem just packages the previous result*) |
|
338 lemma well_ord_TFin: |
|
339 "next: increasing(S) ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))" |
|
340 apply (rule well_ordI) |
|
341 apply (unfold Subset_rel_def linear_def) |
|
342 (*Prove the well-foundedness goal*) |
|
343 apply (rule wf_onI) |
|
344 apply (frule well_ord_TFin_lemma , assumption) |
|
345 apply (drule_tac x = "Inter (Z) " in bspec , assumption) |
|
346 apply blast |
|
347 (*Now prove the linearity goal*) |
|
348 apply (intro ballI) |
|
349 apply (case_tac "x=y") |
|
350 apply (blast) |
|
351 (*The x~=y case remains*) |
|
352 apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE], |
|
353 assumption+) |
|
354 apply (blast intro: elim:)+ |
|
355 done |
|
356 |
|
357 (** Defining the "next" operation for Zermelo's Theorem **) |
|
358 |
|
359 lemma choice_Diff: |
|
360 "[| ch \<in> (\<Pi>X \<in> Pow(S) - {0}. X); X \<subseteq> S; X\<noteq>S |] ==> ch ` (S-X) \<in> S-X" |
|
361 apply (erule apply_type) |
|
362 apply (blast elim!: equalityE) |
|
363 done |
|
364 |
|
365 (*This justifies Definition 6.1*) |
|
366 lemma Zermelo_next_exists: |
|
367 "ch: (PROD X: Pow(S)-{0}. X) ==> |
|
368 EX next: increasing(S). ALL X: Pow(S). |
|
369 next`X = if(X=S, S, cons(ch`(S-X), X))" |
|
370 apply (rule bexI) |
|
371 apply (rule ballI) |
|
372 apply (rule beta) |
|
373 apply assumption |
|
374 apply (unfold increasing_def) |
|
375 apply (rule CollectI) |
|
376 apply (rule lam_type) |
|
377 (*Type checking is surprisingly hard!*) |
|
378 apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl) |
|
379 apply (blast intro!: choice_Diff [THEN DiffD1]) |
|
380 (*Verify that it increases*) |
|
381 apply (intro allI impI) |
|
382 apply (simp add: Pow_iff subset_consI subset_refl) |
|
383 done |
|
384 |
|
385 |
|
386 (*The construction of the injection*) |
|
387 lemma choice_imp_injection: |
|
388 "[| ch: (PROD X: Pow(S)-{0}. X); |
|
389 next: increasing(S); |
|
390 ALL X: Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |] |
|
391 ==> (lam x:S. Union({y: TFin(S,next). x~: y})) |
|
392 : inj(S, TFin(S,next) - {S})" |
|
393 apply (rule_tac d = "%y. ch` (S-y) " in lam_injective) |
|
394 apply (rule DiffI) |
|
395 apply (rule Collect_subset [THEN TFin_UnionI]) |
|
396 apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE) |
|
397 apply (subgoal_tac "x ~: Union ({y: TFin (S,next) . x~: y}) ") |
|
398 prefer 2 apply (blast elim: equalityE) |
|
399 apply (subgoal_tac "Union ({y: TFin (S,next) . x~: y}) ~= S") |
|
400 prefer 2 apply (blast elim: equalityE) |
|
401 (*For proving x : next`Union(...) |
|
402 Abrial & Laffitte's justification appears to be faulty.*) |
|
403 apply (subgoal_tac "~ next ` Union ({y: TFin (S,next) . x~: y}) <= Union ({y: TFin (S,next) . x~: y}) ") |
|
404 prefer 2 |
|
405 apply (simp del: Union_iff |
|
406 add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset] |
|
407 Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2]) |
|
408 apply (subgoal_tac "x : next ` Union ({y: TFin (S,next) . x~: y}) ") |
|
409 prefer 2 |
|
410 apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI) |
|
411 (*End of the lemmas!*) |
|
412 apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]) |
|
413 done |
|
414 |
|
415 (*The wellordering theorem*) |
|
416 lemma AC_well_ord: "EX r. well_ord(S,r)" |
|
417 apply (rule AC_Pi_Pow [THEN exE]) |
|
418 apply (rule Zermelo_next_exists [THEN bexE]) |
|
419 apply assumption |
|
420 apply (rule exI) |
|
421 apply (rule well_ord_rvimage) |
|
422 apply (erule_tac [2] well_ord_TFin) |
|
423 apply (rule choice_imp_injection [THEN inj_weaken_type]) |
|
424 apply (blast intro: elim:)+ |
|
425 done |
48 |
426 |
49 end |
427 end |