author | paulson |
Fri, 28 Jul 1995 17:21:44 +0200 | |
changeset 1208 | bc3093616ba4 |
parent 1200 | d4551b1a6da7 |
child 1299 | e74f694ca1da |
permissions | -rw-r--r-- |
1123 | 1 |
(* Title: ZF/AC/Hartog.ML |
2 |
ID: $Id$ |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
3 |
Author: Krzysztof Grabczewski |
1123 | 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)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
17 |
by (etac exE 1); |
1123 | 18 |
by (REPEAT (resolve_tac [exI, conjI] 1)); |
19 |
by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
20 |
by (rtac exI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
21 |
by (rtac conjI 1); |
1123 | 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)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
33 |
by (dtac 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)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
36 |
by (etac 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); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
46 |
by (dtac 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"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
55 |
by (rtac swap 1); |
1200 | 56 |
by (fast_tac ZF_cs 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
57 |
by (rtac 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); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
63 |
by (rtac 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))"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
70 |
by (rtac Ord_Least 1); |
1123 | 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(); |