11 Fortunately order types made this proof also very easy. |
11 Fortunately order types made this proof also very easy. |
12 *) |
12 *) |
13 |
13 |
14 (* ********************************************************************** *) |
14 (* ********************************************************************** *) |
15 |
15 |
16 goalw thy WO_defs "!!Z. WO2 ==> WO3"; |
16 Goalw WO_defs "!!Z. WO2 ==> WO3"; |
17 by (Fast_tac 1); |
17 by (Fast_tac 1); |
18 qed "WO2_WO3"; |
18 qed "WO2_WO3"; |
19 |
19 |
20 (* ********************************************************************** *) |
20 (* ********************************************************************** *) |
21 |
21 |
22 goalw thy (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1"; |
22 Goalw (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1"; |
23 by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, |
23 by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, |
24 well_ord_Memrel RS well_ord_subset]) 1); |
24 well_ord_Memrel RS well_ord_subset]) 1); |
25 qed "WO3_WO1"; |
25 qed "WO3_WO1"; |
26 |
26 |
27 (* ********************************************************************** *) |
27 (* ********************************************************************** *) |
28 |
28 |
29 goalw thy (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2"; |
29 Goalw (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2"; |
30 by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); |
30 by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); |
31 qed "WO1_WO2"; |
31 qed "WO1_WO2"; |
32 |
32 |
33 (* ********************************************************************** *) |
33 (* ********************************************************************** *) |
34 |
34 |
35 goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}"; |
35 Goal "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}"; |
36 by (fast_tac (claset() addSIs [lam_type, apply_type]) 1); |
36 by (fast_tac (claset() addSIs [lam_type, apply_type]) 1); |
37 qed "lam_sets"; |
37 qed "lam_sets"; |
38 |
38 |
39 goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B"; |
39 Goalw [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B"; |
40 by (fast_tac (claset() addSEs [apply_type]) 1); |
40 by (fast_tac (claset() addSEs [apply_type]) 1); |
41 qed "surj_imp_eq_"; |
41 qed "surj_imp_eq_"; |
42 |
42 |
43 goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B"; |
43 Goal "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B"; |
44 by (fast_tac (claset() addSDs [surj_imp_eq_] |
44 by (fast_tac (claset() addSDs [surj_imp_eq_] |
45 addSIs [ltI] addSEs [ltE]) 1); |
45 addSIs [ltI] addSEs [ltE]) 1); |
46 qed "surj_imp_eq"; |
46 qed "surj_imp_eq"; |
47 |
47 |
48 goalw thy WO_defs "!!Z. WO1 ==> WO4(1)"; |
48 Goalw WO_defs "!!Z. WO1 ==> WO4(1)"; |
49 by (rtac allI 1); |
49 by (rtac allI 1); |
50 by (eres_inst_tac [("x","A")] allE 1); |
50 by (eres_inst_tac [("x","A")] allE 1); |
51 by (etac exE 1); |
51 by (etac exE 1); |
52 by (REPEAT (resolve_tac [exI, conjI] 1)); |
52 by (REPEAT (resolve_tac [exI, conjI] 1)); |
53 by (etac Ord_ordertype 1); |
53 by (etac Ord_ordertype 1); |
59 bij_is_surj RS surj_imp_eq)]) 1); |
59 bij_is_surj RS surj_imp_eq)]) 1); |
60 qed "WO1_WO4"; |
60 qed "WO1_WO4"; |
61 |
61 |
62 (* ********************************************************************** *) |
62 (* ********************************************************************** *) |
63 |
63 |
64 goalw thy WO_defs "!!Z. [| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)"; |
64 Goalw WO_defs "!!Z. [| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)"; |
65 by (fast_tac (claset() addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1); |
65 by (fast_tac (claset() addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1); |
66 qed "WO4_mono"; |
66 qed "WO4_mono"; |
67 |
67 |
68 (* ********************************************************************** *) |
68 (* ********************************************************************** *) |
69 |
69 |
70 goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5"; |
70 Goalw WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5"; |
71 (*ZF_cs is essential: default claset's too slow*) |
71 (*ZF_cs is essential: default claset's too slow*) |
72 by (fast_tac ZF_cs 1); |
72 by (fast_tac ZF_cs 1); |
73 qed "WO4_WO5"; |
73 qed "WO4_WO5"; |
74 |
74 |
75 (* ********************************************************************** *) |
75 (* ********************************************************************** *) |
76 |
76 |
77 goalw thy WO_defs "!!Z. WO5 ==> WO6"; |
77 Goalw WO_defs "!!Z. WO5 ==> WO6"; |
78 (*ZF_cs is essential: default claset's too slow*) |
78 (*ZF_cs is essential: default claset's too slow*) |
79 by (fast_tac ZF_cs 1); |
79 by (fast_tac ZF_cs 1); |
80 qed "WO5_WO6"; |
80 qed "WO5_WO6"; |
81 |
81 |