author | paulson |
Thu, 10 Sep 1998 17:49:36 +0200 | |
changeset 5472 | 746cd24ee3ac |
parent 5147 | 825877190618 |
child 6068 | 2d8f3e1f1151 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/WO1-WO6.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 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 |
||
2469 | 8 |
Every proof (exept one) presented in this file are referred as "clear" |
1123 | 9 |
by Rubin & Rubin (page 2). |
2469 | 10 |
They refer reader to a book by Gödel to see the proof WO1 ==> WO2. |
1123 | 11 |
Fortunately order types made this proof also very easy. |
12 |
*) |
|
13 |
||
14 |
(* ********************************************************************** *) |
|
15 |
||
5137 | 16 |
Goalw WO_defs "WO2 ==> WO3"; |
2469 | 17 |
by (Fast_tac 1); |
1196 | 18 |
qed "WO2_WO3"; |
1123 | 19 |
|
20 |
(* ********************************************************************** *) |
|
21 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
22 |
Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1"; |
4091 | 23 |
by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, |
2469 | 24 |
well_ord_Memrel RS well_ord_subset]) 1); |
1196 | 25 |
qed "WO3_WO1"; |
1123 | 26 |
|
27 |
(* ********************************************************************** *) |
|
28 |
||
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
29 |
Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2"; |
4091 | 30 |
by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); |
1196 | 31 |
qed "WO1_WO2"; |
1123 | 32 |
|
33 |
(* ********************************************************************** *) |
|
34 |
||
5137 | 35 |
Goal "f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}"; |
4091 | 36 |
by (fast_tac (claset() addSIs [lam_type, apply_type]) 1); |
3731 | 37 |
qed "lam_sets"; |
1123 | 38 |
|
5137 | 39 |
Goalw [surj_def] "f:surj(A,B) ==> (UN a:A. {f`a}) = B"; |
4091 | 40 |
by (fast_tac (claset() addSEs [apply_type]) 1); |
3731 | 41 |
qed "surj_imp_eq_"; |
1123 | 42 |
|
5137 | 43 |
Goal "[| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B"; |
4091 | 44 |
by (fast_tac (claset() addSDs [surj_imp_eq_] |
2496 | 45 |
addSIs [ltI] addSEs [ltE]) 1); |
3731 | 46 |
qed "surj_imp_eq"; |
1123 | 47 |
|
5137 | 48 |
Goalw WO_defs "WO1 ==> WO4(1)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
49 |
by (rtac allI 1); |
1123 | 50 |
by (eres_inst_tac [("x","A")] allE 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
51 |
by (etac exE 1); |
1123 | 52 |
by (REPEAT (resolve_tac [exI, conjI] 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
53 |
by (etac Ord_ordertype 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
54 |
by (rtac conjI 1); |
1123 | 55 |
by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS |
1461 | 56 |
lam_sets RS domain_of_fun] 1); |
4091 | 57 |
by (asm_simp_tac (simpset() addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll, |
1123 | 58 |
Ord_ordertype RSN (2, ordermap_bij RS bij_converse_bij RS |
1461 | 59 |
bij_is_surj RS surj_imp_eq)]) 1); |
1196 | 60 |
qed "WO1_WO4"; |
1123 | 61 |
|
62 |
(* ********************************************************************** *) |
|
63 |
||
5137 | 64 |
Goalw WO_defs "[| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)"; |
5472 | 65 |
by (rtac allI 1); |
66 |
by (dtac spec 1); |
|
67 |
by (blast_tac (claset() addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1); |
|
1196 | 68 |
qed "WO4_mono"; |
1123 | 69 |
|
70 |
(* ********************************************************************** *) |
|
71 |
||
5137 | 72 |
Goalw WO_defs "[| m:nat; 1 le m; WO4(m) |] ==> WO5"; |
5472 | 73 |
by (Blast_tac 1); |
1196 | 74 |
qed "WO4_WO5"; |
1123 | 75 |
|
76 |
(* ********************************************************************** *) |
|
77 |
||
5137 | 78 |
Goalw WO_defs "WO5 ==> WO6"; |
5472 | 79 |
by (Blast_tac 1); |
1196 | 80 |
qed "WO5_WO6"; |
1123 | 81 |