|
1 (* Title: ZF/Zorn0.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Preamble to proofs from the paper |
|
7 Abrial & Laffitte, |
|
8 Towards the Mechanization of the Proofs of Some |
|
9 Classical Theorems of Set Theory. |
|
10 *) |
|
11 |
|
12 |
|
13 (*** Section 1. Mathematical Preamble ***) |
|
14 |
|
15 goal ZF.thy "!!A B C. (ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"; |
|
16 by (fast_tac ZF_cs 1); |
|
17 val Union_lemma0 = result(); |
|
18 |
|
19 goal ZF.thy |
|
20 "!!A B C. [| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"; |
|
21 by (fast_tac ZF_cs 1); |
|
22 val Inter_lemma0 = result(); |
|
23 |
|
24 open Zorn0; |
|
25 |
|
26 (*** Section 2. The Transfinite Construction ***) |
|
27 |
|
28 goalw Zorn0.thy [increasing_def] |
|
29 "!!f A. f: increasing(A) ==> f: Pow(A)->Pow(A)"; |
|
30 by (eresolve_tac [CollectD1] 1); |
|
31 val increasingD1 = result(); |
|
32 |
|
33 goalw Zorn0.thy [increasing_def] |
|
34 "!!f A. [| f: increasing(A); x<=A |] ==> x <= f`x"; |
|
35 by (eresolve_tac [CollectD2 RS spec RS mp] 1); |
|
36 by (assume_tac 1); |
|
37 val increasingD2 = result(); |
|
38 |
|
39 goal Zorn0.thy |
|
40 "!!next S. [| X : Pow(S); next: increasing(S) |] ==> next`X : Pow(S)"; |
|
41 by (eresolve_tac [increasingD1 RS apply_type] 1); |
|
42 by (assume_tac 1); |
|
43 val next_bounded = result(); |
|
44 |
|
45 (*Trivial to prove here; hard to prove within Inductive_Fun*) |
|
46 goal ZF.thy "!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"; |
|
47 by (fast_tac ZF_cs 1); |
|
48 val Union_in_Pow = result(); |
|
49 |
|
50 (** We could make the inductive definition conditional on next: increasing(S) |
|
51 but instead we make this a side-condition of an introduction rule. Thus |
|
52 the induction rule lets us assume that condition! Many inductive proofs |
|
53 are therefore unconditional. |
|
54 **) |
|
55 |
|
56 |