author | paulson |
Mon, 29 Sep 1997 11:48:48 +0200 | |
changeset 3731 | 71366483323b |
parent 2496 | 40efb87985b5 |
child 4091 | 771b1f6422a8 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/WO1-WO6.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
Proofs needed to state that formulations WO1,...,WO6 are all equivalent. |
|
6 |
All but one WO6 ==> WO1 (placed in separate file WO6_WO1.ML) |
|
7 |
||
2469 | 8 |
Every proof (exept one) presented in this file are referred as "clear" |
1123 | 9 |
by Rubin & Rubin (page 2). |
2469 | 10 |
They refer reader to a book by Gödel to see the proof WO1 ==> WO2. |
1123 | 11 |
Fortunately order types made this proof also very easy. |
12 |
*) |
|
13 |
||
14 |
(* ********************************************************************** *) |
|
15 |
||
16 |
goalw thy WO_defs "!!Z. WO2 ==> WO3"; |
|
2469 | 17 |
by (Fast_tac 1); |
1196 | 18 |
qed "WO2_WO3"; |
1123 | 19 |
|
20 |
(* ********************************************************************** *) |
|
21 |
||
22 |
goalw thy (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1"; |
|
2469 | 23 |
by (fast_tac (!claset addSEs [bij_is_inj RS well_ord_rvimage, |
24 |
well_ord_Memrel RS well_ord_subset]) 1); |
|
1196 | 25 |
qed "WO3_WO1"; |
1123 | 26 |
|
27 |
(* ********************************************************************** *) |
|
28 |
||
29 |
goalw thy (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2"; |
|
2469 | 30 |
by (fast_tac (!claset addSIs [Ord_ordertype, ordermap_bij]) 1); |
1196 | 31 |
qed "WO1_WO2"; |
1123 | 32 |
|
33 |
(* ********************************************************************** *) |
|
34 |
||
35 |
goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}"; |
|
2469 | 36 |
by (fast_tac (!claset addSIs [lam_type, apply_type]) 1); |
3731 | 37 |
qed "lam_sets"; |
1123 | 38 |
|
39 |
goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B"; |
|
2496 | 40 |
by (fast_tac (!claset addSEs [apply_type]) 1); |
3731 | 41 |
qed "surj_imp_eq_"; |
1123 | 42 |
|
43 |
goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B"; |
|
2469 | 44 |
by (fast_tac (!claset addSDs [surj_imp_eq_] |
2496 | 45 |
addSIs [ltI] addSEs [ltE]) 1); |
3731 | 46 |
qed "surj_imp_eq"; |
1123 | 47 |
|
48 |
goalw thy WO_defs "!!Z. WO1 ==> WO4(1)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
49 |
by (rtac allI 1); |
1123 | 50 |
by (eres_inst_tac [("x","A")] allE 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
51 |
by (etac exE 1); |
1123 | 52 |
by (REPEAT (resolve_tac [exI, conjI] 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
53 |
by (etac Ord_ordertype 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
54 |
by (rtac conjI 1); |
1123 | 55 |
by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS |
1461 | 56 |
lam_sets RS domain_of_fun] 1); |
2469 | 57 |
by (asm_simp_tac (!simpset addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll, |
1123 | 58 |
Ord_ordertype RSN (2, ordermap_bij RS bij_converse_bij RS |
1461 | 59 |
bij_is_surj RS surj_imp_eq)]) 1); |
1196 | 60 |
qed "WO1_WO4"; |
1123 | 61 |
|
62 |
(* ********************************************************************** *) |
|
63 |
||
64 |
goalw thy WO_defs "!!Z. [| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)"; |
|
2469 | 65 |
by (fast_tac (!claset addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1); |
1196 | 66 |
qed "WO4_mono"; |
1123 | 67 |
|
68 |
(* ********************************************************************** *) |
|
69 |
||
1196 | 70 |
goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5"; |
2469 | 71 |
(*ZF_cs is essential: default claset's too slow*) |
1123 | 72 |
by (fast_tac ZF_cs 1); |
1196 | 73 |
qed "WO4_WO5"; |
1123 | 74 |
|
75 |
(* ********************************************************************** *) |
|
76 |
||
1196 | 77 |
goalw thy WO_defs "!!Z. WO5 ==> WO6"; |
2469 | 78 |
(*ZF_cs is essential: default claset's too slow*) |
1123 | 79 |
by (fast_tac ZF_cs 1); |
1196 | 80 |
qed "WO5_WO6"; |
1123 | 81 |