19 by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1); |
19 by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1); |
20 by (resolve_tac [exI] 1); |
20 by (resolve_tac [exI] 1); |
21 by (resolve_tac [conjI] 1); |
21 by (resolve_tac [conjI] 1); |
22 by (eresolve_tac [well_ord_Memrel RSN (2, subset_refl RSN (2, |
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 |
23 restrict_bij RS bij_converse_bij) RS bij_is_inj RS well_ord_rvimage)] 1 |
24 THEN (atac 1)); |
24 THEN (assume_tac 1)); |
25 by (resolve_tac [subset_refl RSN (2, restrict_bij RS bij_converse_bij) RS |
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 |
26 (well_ord_Memrel RSN (2, bij_ordertype_vimage)) RS |
27 (ordertype_Memrel RSN (2, trans))] 1 |
27 (ordertype_Memrel RSN (2, trans))] 1 |
28 THEN (REPEAT (atac 1))); |
28 THEN (REPEAT (assume_tac 1))); |
29 val Ord_lepoll_imp_ex_well_ord = result(); |
29 val Ord_lepoll_imp_ex_well_ord = result(); |
30 |
30 |
31 goal thy "!!X. [| Ord(a); a lepoll X |] ==> \ |
31 goal thy "!!X. [| Ord(a); a lepoll X |] ==> \ |
32 \ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)"; |
32 \ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)"; |
33 by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (atac 1)); |
33 by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (assume_tac 1)); |
34 by (step_tac AC_cs 1); |
34 by (step_tac AC_cs 1); |
35 by (REPEAT (ares_tac [exI, conjI] 1)); |
35 by (REPEAT (ares_tac [exI, conjI] 1)); |
36 by (eresolve_tac [ordertype_Int] 2); |
36 by (eresolve_tac [ordertype_Int] 2); |
37 by (fast_tac AC_cs 1); |
37 by (fast_tac AC_cs 1); |
38 val Ord_lepoll_imp_eq_ordertype = result(); |
38 val Ord_lepoll_imp_eq_ordertype = result(); |
40 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> \ |
40 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> \ |
41 \ ALL a. Ord(a) --> \ |
41 \ ALL a. Ord(a) --> \ |
42 \ a:{a. Z:Pow(X)*Pow(X*X), EX Y R. Z=<Y,R> & ordertype(Y,R)=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)); |
43 by (REPEAT (resolve_tac [allI,impI] 1)); |
44 by (REPEAT (eresolve_tac [allE, impE] 1)); |
44 by (REPEAT (eresolve_tac [allE, impE] 1)); |
45 by (atac 1); |
45 by (assume_tac 1); |
46 by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (atac 1)); |
46 by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (assume_tac 1)); |
47 by (fast_tac (AC_cs addSIs [ReplaceI] addEs [sym]) 1); |
47 by (fast_tac (AC_cs addSIs [ReplaceI] addEs [sym]) 1); |
48 val Ords_lepoll_set_lemma = result(); |
48 val Ords_lepoll_set_lemma = result(); |
49 |
49 |
50 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P"; |
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); |
51 by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1); |