1123
|
1 |
(* Title: ZF/AC/Hartog.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Krzysztof Gr`abczewski
|
|
4 |
|
|
5 |
Some proofs on the Hartogs function.
|
|
6 |
*)
|
|
7 |
|
|
8 |
open Hartog;
|
|
9 |
|
|
10 |
goal thy "!!X. ALL a. Ord(a) --> a:X ==> P";
|
|
11 |
by (res_inst_tac [("X1","{y:X. Ord(y)}")] (ON_class RS revcut_rl) 1);
|
1200
|
12 |
by (fast_tac ZF_cs 1);
|
1123
|
13 |
val Ords_in_set = result();
|
|
14 |
|
|
15 |
goalw thy [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==> \
|
|
16 |
\ EX Y. Y<=X & (EX R. well_ord(Y,R) & ordertype(Y,R)=a)";
|
|
17 |
by (eresolve_tac [exE] 1);
|
|
18 |
by (REPEAT (resolve_tac [exI, conjI] 1));
|
|
19 |
by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1);
|
|
20 |
by (resolve_tac [exI] 1);
|
|
21 |
by (resolve_tac [conjI] 1);
|
|
22 |
by (eresolve_tac [well_ord_Memrel RSN (2, subset_refl RSN (2,
|
|
23 |
restrict_bij RS bij_converse_bij) RS bij_is_inj RS well_ord_rvimage)] 1
|
1196
|
24 |
THEN (assume_tac 1));
|
1123
|
25 |
by (resolve_tac [subset_refl RSN (2, restrict_bij RS bij_converse_bij) RS
|
|
26 |
(well_ord_Memrel RSN (2, bij_ordertype_vimage)) RS
|
|
27 |
(ordertype_Memrel RSN (2, trans))] 1
|
1196
|
28 |
THEN (REPEAT (assume_tac 1)));
|
1123
|
29 |
val Ord_lepoll_imp_ex_well_ord = result();
|
|
30 |
|
|
31 |
goal thy "!!X. [| Ord(a); a lepoll X |] ==> \
|
|
32 |
\ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)";
|
1196
|
33 |
by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (assume_tac 1));
|
1200
|
34 |
by (step_tac ZF_cs 1);
|
1123
|
35 |
by (REPEAT (ares_tac [exI, conjI] 1));
|
|
36 |
by (eresolve_tac [ordertype_Int] 2);
|
1200
|
37 |
by (fast_tac ZF_cs 1);
|
1123
|
38 |
val Ord_lepoll_imp_eq_ordertype = result();
|
|
39 |
|
|
40 |
goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> \
|
|
41 |
\ ALL a. Ord(a) --> \
|
|
42 |
\ a:{a. Z:Pow(X)*Pow(X*X), EX Y R. Z=<Y,R> & ordertype(Y,R)=a}";
|
|
43 |
by (REPEAT (resolve_tac [allI,impI] 1));
|
|
44 |
by (REPEAT (eresolve_tac [allE, impE] 1));
|
1196
|
45 |
by (assume_tac 1);
|
|
46 |
by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (assume_tac 1));
|
1200
|
47 |
by (fast_tac (ZF_cs addSIs [ReplaceI] addEs [sym]) 1);
|
1123
|
48 |
val Ords_lepoll_set_lemma = result();
|
|
49 |
|
|
50 |
goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P";
|
|
51 |
by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1);
|
|
52 |
val Ords_lepoll_set = result();
|
|
53 |
|
|
54 |
goal thy "EX a. Ord(a) & ~a lepoll X";
|
|
55 |
by (resolve_tac [swap] 1);
|
1200
|
56 |
by (fast_tac ZF_cs 1);
|
1123
|
57 |
by (resolve_tac [Ords_lepoll_set] 1);
|
1200
|
58 |
by (fast_tac ZF_cs 1);
|
1123
|
59 |
val ex_Ord_not_lepoll = result();
|
|
60 |
|
|
61 |
goalw thy [Hartog_def] "~ Hartog(A) lepoll A";
|
|
62 |
by (resolve_tac [ex_Ord_not_lepoll RS exE] 1);
|
|
63 |
by (resolve_tac [LeastI] 1);
|
1200
|
64 |
by (REPEAT (fast_tac ZF_cs 1));
|
1123
|
65 |
val HartogI = result();
|
|
66 |
|
|
67 |
val HartogE = HartogI RS notE;
|
|
68 |
|
|
69 |
goalw thy [Hartog_def] "Ord(Hartog(A))";
|
|
70 |
by (resolve_tac [Ord_Least] 1);
|
|
71 |
val Ord_Hartog = result();
|
|
72 |
|
|
73 |
goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P";
|
1200
|
74 |
by (fast_tac (ZF_cs addEs [less_LeastE]) 1);
|
1123
|
75 |
val less_HartogE1 = result();
|
|
76 |
|
|
77 |
goal thy "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P";
|
1200
|
78 |
by (fast_tac (ZF_cs addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll
|
1123
|
79 |
RS lepoll_trans RS HartogE]) 1);
|
|
80 |
val less_HartogE = result();
|
|
81 |
|
|
82 |
goal thy "Card(Hartog(A))";
|
1200
|
83 |
by (fast_tac (ZF_cs addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1);
|
1196
|
84 |
val Card_Hartog = result();
|