author | wenzelm |
Tue, 07 Sep 1999 10:40:58 +0200 | |
changeset 7499 | 23e090051cb8 |
parent 5473 | 4abb47b79b86 |
child 11317 | 7f9e4c389318 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/WO1_WO7.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5) |
|
6 |
LEMMA is the sentence denoted by (**) |
|
7 |
*) |
|
8 |
||
9 |
(* ********************************************************************** *) |
|
1461 | 10 |
(* It is easy to see, that WO7 is equivallent to (**) *) |
1123 | 11 |
(* ********************************************************************** *) |
12 |
||
5473 | 13 |
Goalw [WO7_def, LEMMA_def] |
14 |
"WO7 <-> LEMMA"; |
|
4091 | 15 |
by (fast_tac (claset() addSEs [Finite_well_ord_converse]) 1); |
3731 | 16 |
qed "WO7_iff_LEMMA"; |
1123 | 17 |
|
18 |
(* ********************************************************************** *) |
|
1461 | 19 |
(* It is also easy to show that LEMMA implies WO1. *) |
1123 | 20 |
(* ********************************************************************** *) |
21 |
||
5473 | 22 |
Goalw [WO1_def, LEMMA_def] "LEMMA ==> WO1"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
23 |
by (rtac allI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
24 |
by (etac allE 1); |
1123 | 25 |
by (excluded_middle_tac "Finite(A)" 1); |
2469 | 26 |
by (Fast_tac 1); |
1123 | 27 |
by (rewrite_goals_tac [Finite_def, eqpoll_def]); |
4091 | 28 |
by (fast_tac (claset() addSIs [[bij_is_inj, nat_implies_well_ord] MRS |
1461 | 29 |
well_ord_rvimage]) 1); |
3731 | 30 |
qed "LEMMA_imp_WO1"; |
1123 | 31 |
|
32 |
(* ********************************************************************** *) |
|
1461 | 33 |
(* The Rubins' proof of the other implication is contained within the *) |
34 |
(* following sentence : *) |
|
35 |
(* "... each infinite ordinal is well ordered by < but not by >." *) |
|
36 |
(* This statement can be proved by the following two theorems. *) |
|
37 |
(* But moreover we need to show similar property for any well ordered *) |
|
1123 | 38 |
(* infinite set. It is not very difficult thanks to Isabelle order types *) |
5137 | 39 |
(* We show that if a set is well ordered by some relation and by its *) |
1123 | 40 |
(* converse, then apropriate order type is well ordered by the converse *) |
1461 | 41 |
(* of it's membership relation, which in connection with the previous *) |
42 |
(* gives the conclusion. *) |
|
1123 | 43 |
(* ********************************************************************** *) |
44 |
||
5068 | 45 |
Goalw [wf_on_def, wf_def] |
5473 | 46 |
"[| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"; |
1123 | 47 |
by (dresolve_tac [nat_le_infinite_Ord RS le_imp_subset] 1 |
1196 | 48 |
THEN (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
49 |
by (rtac notI 1); |
1123 | 50 |
by (eres_inst_tac [("x","nat")] allE 1); |
5473 | 51 |
by (Blast_tac 1); |
3731 | 52 |
qed "converse_Memrel_not_wf_on"; |
1123 | 53 |
|
5068 | 54 |
Goalw [well_ord_def] |
5473 | 55 |
"[| Ord(a); ~Finite(a) |] ==> ~well_ord(a,converse(Memrel(a)))"; |
4091 | 56 |
by (fast_tac (claset() addSDs [converse_Memrel_not_wf_on]) 1); |
3731 | 57 |
qed "converse_Memrel_not_well_ord"; |
1123 | 58 |
|
5137 | 59 |
Goal "[| well_ord(A,r); well_ord(A,converse(r)) |] \ |
1461 | 60 |
\ ==> well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))"; |
1123 | 61 |
by (rtac ([ordertype_ord_iso RS ord_iso_sym RS ord_iso_rvimage_eq, |
1461 | 62 |
Memrel_type RS (subset_Int_iff RS iffD1)] |
63 |
MRS trans RS subst) 1 |
|
64 |
THEN (assume_tac 1)); |
|
1123 | 65 |
by (rtac (rvimage_converse RS subst) 1); |
66 |
by (etac (ordertype_ord_iso RS ord_iso_sym RS ord_iso_is_bij RS |
|
1461 | 67 |
bij_is_inj RS well_ord_rvimage) 1 |
68 |
THEN (assume_tac 1)); |
|
3731 | 69 |
qed "well_ord_converse_Memrel"; |
1123 | 70 |
|
5473 | 71 |
Goalw [WO1_def, LEMMA_def] "WO1 ==> LEMMA"; |
1123 | 72 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
73 |
by (REPEAT (eresolve_tac [allE,exE] 1)); |
|
74 |
by (REPEAT (ares_tac [exI,conjI,notI] 1)); |
|
7499 | 75 |
by (ftac well_ord_converse_Memrel 1 THEN (assume_tac 1)); |
1123 | 76 |
by (forward_tac [Ord_ordertype RS converse_Memrel_not_well_ord] 1); |
77 |
by (contr_tac 2); |
|
78 |
by (fast_tac (empty_cs addSEs [ordertype_ord_iso RS ord_iso_is_bij RS |
|
1461 | 79 |
bij_is_inj RS (exI RS (lepoll_def RS def_imp_iff RS iffD2)) |
80 |
RS lepoll_Finite] |
|
81 |
addSIs [notI] addEs [notE]) 1); |
|
3731 | 82 |
qed "WO1_imp_LEMMA"; |
1123 | 83 |
|
5473 | 84 |
|
85 |
Goal "WO1 <-> WO7"; |
|
86 |
by (simp_tac (simpset() addsimps [WO7_iff_LEMMA]) 1); |
|
87 |
by (blast_tac (claset() addIs [LEMMA_imp_WO1, WO1_imp_LEMMA]) 1); |
|
88 |
qed "WO1_iff_WO7"; |