# HG changeset patch
# User paulson
# Date 905442606 -7200
# Node ID 4abb47b79b86a0d93d00c8cffa243a919121175a
# Parent  746cd24ee3acce88aad6d80dd1d687b3bfb37fff
added proof of final result...

diff -r 746cd24ee3ac -r 4abb47b79b86 src/ZF/AC/WO1_WO7.ML
--- a/src/ZF/AC/WO1_WO7.ML	Thu Sep 10 17:49:36 1998 +0200
+++ b/src/ZF/AC/WO1_WO7.ML	Thu Sep 10 17:50:06 1998 +0200
@@ -10,8 +10,8 @@
 (* It is easy to see, that WO7 is equivallent to (**)                     *)
 (* ********************************************************************** *)
 
-Goalw [WO7_def] "WO7 <-> (ALL X. ~Finite(X) -->  \
-\                       (EX R. well_ord(X,R) & ~well_ord(X,converse(R))))";
+Goalw [WO7_def, LEMMA_def] 
+  "WO7 <-> LEMMA";
 by (fast_tac (claset() addSEs [Finite_well_ord_converse]) 1);
 qed "WO7_iff_LEMMA";
 
@@ -19,8 +19,7 @@
 (* It is also easy to show that LEMMA implies WO1.                        *)
 (* ********************************************************************** *)
 
-Goalw [WO1_def] "ALL X. ~Finite(X) -->  \
-\               (EX R. well_ord(X,R) & ~well_ord(X,converse(R))) ==> WO1";
+Goalw [WO1_def, LEMMA_def] "LEMMA ==> WO1";
 by (rtac allI 1);
 by (etac allE 1);
 by (excluded_middle_tac "Finite(A)" 1);
@@ -44,16 +43,16 @@
 (* ********************************************************************** *)
 
 Goalw [wf_on_def, wf_def] 
-    "!!a. [| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))";
+    "[| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))";
 by (dresolve_tac [nat_le_infinite_Ord RS le_imp_subset] 1 
     THEN (assume_tac 1));
 by (rtac notI 1);
 by (eres_inst_tac [("x","nat")] allE 1);
-by (blast_tac (claset() addSEs [nat_0I RSN (2,equals0E)]) 1);
+by (Blast_tac 1);
 qed "converse_Memrel_not_wf_on";
 
 Goalw [well_ord_def] 
-    "!!a. [| Ord(a); ~Finite(a) |] ==> ~well_ord(a,converse(Memrel(a)))";
+    "[| Ord(a); ~Finite(a) |] ==> ~well_ord(a,converse(Memrel(a)))";
 by (fast_tac (claset() addSDs [converse_Memrel_not_wf_on]) 1);
 qed "converse_Memrel_not_well_ord";
 
@@ -69,8 +68,7 @@
         THEN (assume_tac 1));
 qed "well_ord_converse_Memrel";
 
-Goalw [WO1_def] "WO1 ==> ALL X. ~Finite(X) -->  \
-\                       (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))";
+Goalw [WO1_def, LEMMA_def] "WO1 ==> LEMMA";
 by (REPEAT (resolve_tac [allI,impI] 1));
 by (REPEAT (eresolve_tac [allE,exE] 1));
 by (REPEAT (ares_tac [exI,conjI,notI] 1));
@@ -83,3 +81,8 @@
                 addSIs [notI] addEs [notE]) 1);
 qed "WO1_imp_LEMMA";
 
+
+Goal "WO1 <-> WO7";
+by (simp_tac (simpset() addsimps [WO7_iff_LEMMA]) 1);
+by (blast_tac (claset() addIs [LEMMA_imp_WO1, WO1_imp_LEMMA]) 1);
+qed "WO1_iff_WO7";