1123
|
1 |
(* Title: ZF/AC/WO1-WO6.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Krzysztof Gr`abczewski
|
|
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 |
|
|
8 |
Every proofs (exept one) presented in this file are referred as clear
|
|
9 |
by Rubin & Rubin (page 2).
|
|
10 |
They refer reader to a book by G"odel to see the proof WO1 ==> WO2.
|
|
11 |
Fortunately order types made this proof also very easy.
|
|
12 |
*)
|
|
13 |
|
|
14 |
(* ********************************************************************** *)
|
|
15 |
|
|
16 |
goalw thy WO_defs "!!Z. WO2 ==> WO3";
|
|
17 |
by (fast_tac ZF_cs 1);
|
|
18 |
result();
|
|
19 |
|
|
20 |
(* ********************************************************************** *)
|
|
21 |
|
|
22 |
goalw thy (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1";
|
|
23 |
by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage,
|
|
24 |
well_ord_Memrel RS well_ord_subset]) 1);
|
|
25 |
result();
|
|
26 |
|
|
27 |
(* ********************************************************************** *)
|
|
28 |
|
|
29 |
goalw thy (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2";
|
|
30 |
by (fast_tac (ZF_cs addSIs [Ord_ordertype, ordermap_bij]) 1);
|
|
31 |
result();
|
|
32 |
|
|
33 |
(* ********************************************************************** *)
|
|
34 |
|
|
35 |
goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}";
|
|
36 |
by (fast_tac (ZF_cs addSIs [lam_type, RepFunI, apply_type]) 1);
|
|
37 |
val lam_sets = result();
|
|
38 |
|
|
39 |
goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
|
|
40 |
by (fast_tac (ZF_cs addSIs [equalityI] addSEs [singletonE, apply_type]) 1);
|
|
41 |
val surj_imp_eq_ = result();
|
|
42 |
|
|
43 |
goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
|
|
44 |
by (fast_tac (AC_cs addSDs [surj_imp_eq_]
|
|
45 |
addSIs [equalityI, ltI] addSEs [ltE]) 1);
|
|
46 |
val surj_imp_eq = result();
|
|
47 |
|
|
48 |
goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
|
|
49 |
by (resolve_tac [allI] 1);
|
|
50 |
by (eres_inst_tac [("x","A")] allE 1);
|
|
51 |
by (eresolve_tac [exE] 1);
|
|
52 |
by (REPEAT (resolve_tac [exI, conjI] 1));
|
|
53 |
by (eresolve_tac [Ord_ordertype] 1);
|
|
54 |
by (resolve_tac [conjI] 1);
|
|
55 |
by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS
|
|
56 |
lam_sets RS domain_of_fun] 1);
|
|
57 |
by (asm_simp_tac (AC_ss addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
|
|
58 |
Ord_ordertype RSN (2, ordermap_bij RS bij_converse_bij RS
|
|
59 |
bij_is_surj RS surj_imp_eq)]) 1);
|
|
60 |
result();
|
|
61 |
|
|
62 |
(* ********************************************************************** *)
|
|
63 |
|
|
64 |
goalw thy WO_defs "!!Z. [| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)";
|
|
65 |
by (fast_tac (AC_cs addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1);
|
|
66 |
result();
|
|
67 |
|
|
68 |
(* ********************************************************************** *)
|
|
69 |
|
|
70 |
val prems = goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5";
|
|
71 |
by (fast_tac ZF_cs 1);
|
|
72 |
result();
|
|
73 |
|
|
74 |
(* ********************************************************************** *)
|
|
75 |
|
|
76 |
val prems = goalw thy WO_defs "!!Z. WO5 ==> WO6";
|
|
77 |
by (fast_tac ZF_cs 1);
|
|
78 |
result();
|
|
79 |
|