--- a/src/ZF/AC/WO6_WO1.ML Wed Jan 16 15:04:37 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,538 +0,0 @@
-(* Title: ZF/AC/WO6_WO1.ML
- ID: $Id$
- Author: Krzysztof Grabczewski
-
- Proofs needed to state that formulations WO1,...,WO6 are all equivalent.
- The only hard one is WO6 ==> WO1.
-
- Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear"
- by Rubin & Rubin (page 2).
- They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
- Fortunately order types made this proof also very easy.
-*)
-
-(* ********************************************************************** *)
-
-Goalw WO_defs "WO2 ==> WO3";
-by (Fast_tac 1);
-qed "WO2_WO3";
-
-(* ********************************************************************** *)
-
-Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1";
-by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage,
- well_ord_Memrel RS well_ord_subset]) 1);
-qed "WO3_WO1";
-
-(* ********************************************************************** *)
-
-Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2";
-by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1);
-qed "WO1_WO2";
-
-(* ********************************************************************** *)
-
-Goal "f \\<in> A->B ==> (\\<lambda>x \\<in> A. {f`x}): A -> {{b}. b \\<in> B}";
-by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
-qed "lam_sets";
-
-Goalw [surj_def] "f \\<in> surj(A,B) ==> (\\<Union>a \\<in> A. {f`a}) = B";
-by (fast_tac (claset() addSEs [apply_type]) 1);
-qed "surj_imp_eq_";
-
-Goal "[| f \\<in> surj(A,B); Ord(A) |] ==> (\\<Union>a<A. {f`a}) = B";
-by (fast_tac (claset() addSDs [surj_imp_eq_]
- addSIs [ltI] addSEs [ltE]) 1);
-qed "surj_imp_eq";
-
-Goalw WO_defs "WO1 ==> WO4(1)";
-by (rtac allI 1);
-by (eres_inst_tac [("x","A")] allE 1);
-by (etac exE 1);
-by (REPEAT (resolve_tac [exI, conjI] 1));
-by (etac Ord_ordertype 1);
-by (rtac conjI 1);
-by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS
- lam_sets RS domain_of_fun] 1);
-by (asm_simp_tac (simpset() addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
- Ord_ordertype RSN (2, ordermap_bij RS bij_converse_bij RS
- bij_is_surj RS surj_imp_eq)]) 1);
-qed "WO1_WO4";
-
-(* ********************************************************************** *)
-
-Goalw WO_defs "[| m le n; WO4(m) |] ==> WO4(n)";
-by (blast_tac (claset() addSDs [spec]
- addIs [le_imp_lepoll RSN (2, lepoll_trans)]) 1);
-qed "WO4_mono";
-
-(* ********************************************************************** *)
-
-Goalw WO_defs "[| m \\<in> nat; 1 le m; WO4(m) |] ==> WO5";
-by (Blast_tac 1);
-qed "WO4_WO5";
-
-(* ********************************************************************** *)
-
-Goalw WO_defs "WO5 ==> WO6";
-by (Blast_tac 1);
-qed "WO5_WO6";
-
-
-(* **********************************************************************
- The proof of "WO6 ==> WO1". Simplified by L C Paulson.
-
- From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
- pages 2-5
-************************************************************************* *)
-
-goal OrderType.thy
- "!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==> \
-\ k < i | (~ k<i & k = i ++ (k--i) & (k--i)<j)";
-by (res_inst_tac [("i","k"),("j","i")] Ord_linear2 1);
-by (dtac odiff_lt_mono2 4 THEN assume_tac 4);
-by (asm_full_simp_tac
- (simpset() addsimps [oadd_odiff_inverse, odiff_oadd_inverse]) 4);
-by (safe_tac (claset() addSEs [lt_Ord]));
-qed "lt_oadd_odiff_disj";
-
-(*The corresponding elimination rule*)
-val lt_oadd_odiff_cases = rule_by_tactic Safe_tac
- (lt_oadd_odiff_disj RS disjE);
-
-(* ********************************************************************** *)
-(* The most complicated part of the proof - lemma ii - p. 2-4 *)
-(* ********************************************************************** *)
-
-(* ********************************************************************** *)
-(* some properties of relation uu(beta, gamma, delta) - p. 2 *)
-(* ********************************************************************** *)
-
-Goalw [uu_def] "domain(uu(f,b,g,d)) \\<subseteq> f`b";
-by (Blast_tac 1);
-qed "domain_uu_subset";
-
-Goal "\\<forall>b<a. f`b lepoll m ==> \
-\ \\<forall>b<a. \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) lepoll m";
-by (fast_tac (claset() addSEs
- [domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1);
-qed "quant_domain_uu_lepoll_m";
-
-Goalw [uu_def] "uu(f,b,g,d) \\<subseteq> f`b * f`g";
-by (Blast_tac 1);
-qed "uu_subset1";
-
-Goalw [uu_def] "uu(f,b,g,d) \\<subseteq> f`d";
-by (Blast_tac 1);
-qed "uu_subset2";
-
-Goal "[| \\<forall>b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m";
-by (fast_tac (claset()
- addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
-qed "uu_lepoll_m";
-
-(* ********************************************************************** *)
-(* Two cases for lemma ii *)
-(* ********************************************************************** *)
-Goalw [lesspoll_def]
- "\\<forall>b<a. \\<forall>g<a. \\<forall>d<a. u(f,b,g,d) lepoll m \
-\ ==> (\\<forall>b<a. f`b \\<noteq> 0 --> \
-\ (\\<exists>g<a. \\<exists>d<a. u(f,b,g,d) \\<noteq> 0 & u(f,b,g,d) lesspoll m)) \
-\ | (\\<exists>b<a. f`b \\<noteq> 0 & (\\<forall>g<a. \\<forall>d<a. u(f,b,g,d) \\<noteq> 0 --> \
-\ u(f,b,g,d) eqpoll m))";
-by (Asm_simp_tac 1);
-by (blast_tac (claset() delrules [equalityI]) 1);
-qed "cases";
-
-(* ********************************************************************** *)
-(* Lemmas used in both cases *)
-(* ********************************************************************** *)
-Goal "Ord(a) ==> (\\<Union>b<a++a. C(b)) = (\\<Union>b<a. C(b) Un C(a++b))";
-by (fast_tac (claset() addSIs [equalityI] addIs [ltI]
- addSDs [lt_oadd_disj]
- addSEs [lt_oadd1, oadd_lt_mono2]) 1);
-qed "UN_oadd";
-
-
-(* ********************************************************************** *)
-(* Case 1 \\<in> lemmas *)
-(* ********************************************************************** *)
-
-Goalw [vv1_def] "vv1(f,m,b) \\<subseteq> f`b";
-by (rtac (LetI RS LetI) 1);
-by (simp_tac (simpset() addsimps [domain_uu_subset]) 1);
-qed "vv1_subset";
-
-(* ********************************************************************** *)
-(* Case 1 \\<in> Union of images is the whole "y" *)
-(* ********************************************************************** *)
-Goalw [gg1_def]
- "!! a f y. [| Ord(a); m \\<in> nat |] ==> \
-\ (\\<Union>b<a++a. gg1(f,a,m)`b) = (\\<Union>b<a. f`b)";
-by (asm_simp_tac
- (simpset() addsimps [UN_oadd, lt_oadd1,
- oadd_le_self RS le_imp_not_lt, lt_Ord,
- odiff_oadd_inverse, ltD,
- vv1_subset RS Diff_partition, ww1_def]) 1);
-qed "UN_gg1_eq";
-
-Goal "domain(gg1(f,a,m)) = a++a";
-by (simp_tac (simpset() addsimps [lam_funtype RS domain_of_fun, gg1_def]) 1);
-qed "domain_gg1";
-
-(* ********************************************************************** *)
-(* every value of defined function is less than or equipollent to m *)
-(* ********************************************************************** *)
-Goal "[| P(a, b); Ord(a); Ord(b); \
-\ Least_a = (LEAST a. \\<exists>x. Ord(x) & P(a, x)) |] \
-\ ==> P(Least_a, LEAST b. P(Least_a, b))";
-by (etac ssubst 1);
-by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1);
-by (REPEAT (fast_tac (claset() addSEs [LeastI]) 1));
-qed "nested_LeastI";
-
-bind_thm ("nested_Least_instance",
- inst "P"
- "%g d. domain(uu(f,b,g,d)) \\<noteq> 0 & domain(uu(f,b,g,d)) lepoll m"
- nested_LeastI);
-
-Goalw [gg1_def]
- "!!a. [| Ord(a); m \\<in> nat; \
-\ \\<forall>b<a. f`b \\<noteq>0 --> \
-\ (\\<exists>g<a. \\<exists>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 & \
-\ domain(uu(f,b,g,d)) lepoll m); \
-\ \\<forall>b<a. f`b lepoll succ(m); b<a++a \
-\ |] ==> gg1(f,a,m)`b lepoll m";
-by (Asm_simp_tac 1);
-by (safe_tac (claset() addSEs [lt_oadd_odiff_cases]));
-(*Case b<a \\<in> show vv1(f,m,b) lepoll m *)
-by (asm_simp_tac (simpset() addsimps [vv1_def, Let_def]) 1);
-by (fast_tac (claset() addIs [nested_Least_instance RS conjunct2]
- addSEs [lt_Ord]
- addSIs [empty_lepollI]) 1);
-(*Case a le b \\<in> show ww1(f,m,b--a) lepoll m *)
-by (asm_simp_tac (simpset() addsimps [ww1_def]) 1);
-by (excluded_middle_tac "f`(b--a) = 0" 1);
-by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2);
-by (rtac Diff_lepoll 1);
-by (Blast_tac 1);
-by (rtac vv1_subset 1);
-by (dtac (ospec RS mp) 1);
-by (REPEAT (eresolve_tac [asm_rl, oexE, conjE] 1));
-by (asm_simp_tac (simpset()
- addsimps [vv1_def, Let_def, lt_Ord,
- nested_Least_instance RS conjunct1]) 1);
-qed "gg1_lepoll_m";
-
-(* ********************************************************************** *)
-(* Case 2 \\<in> lemmas *)
-(* ********************************************************************** *)
-
-(* ********************************************************************** *)
-(* Case 2 \\<in> vv2_subset *)
-(* ********************************************************************** *)
-
-Goalw [uu_def] "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \
-\ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y \
-\ |] ==> \\<exists>d<a. uu(f,b,g,d) \\<noteq> 0";
-by (fast_tac (claset() addSIs [not_emptyI]
- addSDs [SigmaI RSN (2, subsetD)]
- addSEs [not_emptyE]) 1);
-qed "ex_d_uu_not_empty";
-
-Goal "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \
-\ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y |] \
-\ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) \\<noteq> 0)) \\<noteq> 0";
-by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1));
-by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1);
-qed "uu_not_empty";
-
-Goal "[| r \\<subseteq> A*B; r\\<noteq>0 |] ==> domain(r)\\<noteq>0";
-by (Blast_tac 1);
-qed "not_empty_rel_imp_domain";
-
-Goal "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \
-\ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y |] \
-\ ==> (LEAST d. uu(f,b,g,d) \\<noteq> 0) < a";
-by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1
- THEN REPEAT (assume_tac 1));
-by (resolve_tac [Least_le RS lt_trans1] 1
- THEN (REPEAT (ares_tac [lt_Ord] 1)));
-qed "Least_uu_not_empty_lt_a";
-
-Goal "[| B \\<subseteq> A; a\\<notin>B |] ==> B \\<subseteq> A-{a}";
-by (Blast_tac 1);
-qed "subset_Diff_sing";
-
-(*Could this be proved more directly?*)
-Goal "[| A lepoll m; m lepoll B; B \\<subseteq> A; m \\<in> nat |] ==> A=B";
-by (etac natE 1);
-by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
-by (safe_tac (claset() addSIs [equalityI]));
-by (rtac ccontr 1);
-by (etac (subset_Diff_sing RS subset_imp_lepoll
- RSN (2, Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
- succ_lepoll_natE) 1
- THEN REPEAT (assume_tac 1));
-qed "supset_lepoll_imp_eq";
-
-Goal "[| \\<forall>g<a. \\<forall>d<a. domain(uu(f, b, g, d))\\<noteq>0 --> \
-\ domain(uu(f, b, g, d)) eqpoll succ(m); \
-\ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \
-\ (\\<Union>b<a. f`b)=y; b<a; g<a; d<a; \
-\ f`b\\<noteq>0; f`g\\<noteq>0; m \\<in> nat; s \\<in> f`b \
-\ |] ==> uu(f, b, g, LEAST d. uu(f,b,g,d)\\<noteq>0) \\<in> f`b -> f`g";
-by (dres_inst_tac [("x2","g")] (ospec RS ospec RS mp) 1);
-by (rtac ([uu_subset1, uu_not_empty] MRS not_empty_rel_imp_domain) 3);
-by (rtac Least_uu_not_empty_lt_a 2 THEN TRYALL assume_tac);
-by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS
- (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2,
- uu_subset1 RSN (4, rel_is_fun)))] 1
- THEN TRYALL assume_tac);
-by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1);
-by (REPEAT_FIRST assume_tac);
-by (REPEAT (fast_tac (claset() addSIs [domain_uu_subset]) 1));
-qed "uu_Least_is_fun";
-
-Goalw [vv2_def]
- "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f, b, g, d))\\<noteq>0 --> \
-\ domain(uu(f, b, g, d)) eqpoll succ(m); \
-\ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \
-\ (\\<Union>b<a. f`b)=y; b<a; g<a; m \\<in> nat; s \\<in> f`b \
-\ |] ==> vv2(f,b,g,s) \\<subseteq> f`g";
-by (split_tac [split_if] 1);
-by Safe_tac;
-by (etac (uu_Least_is_fun RS apply_type) 1);
-by (REPEAT_SOME (fast_tac (claset() addSIs [not_emptyI, singleton_subsetI])));
-qed "vv2_subset";
-
-(* ********************************************************************** *)
-(* Case 2 \\<in> Union of images is the whole "y" *)
-(* ********************************************************************** *)
-Goalw [gg2_def]
- "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 --> \
-\ domain(uu(f,b,g,d)) eqpoll succ(m); \
-\ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \
-\ (\\<Union>b<a. f`b)=y; Ord(a); m \\<in> nat; s \\<in> f`b; b<a \
-\ |] ==> (\\<Union>g<a++a. gg2(f,a,b,s) ` g) = y";
-by (dtac sym 1);
-by (asm_simp_tac
- (simpset() addsimps [UN_oadd, lt_oadd1,
- oadd_le_self RS le_imp_not_lt, lt_Ord,
- odiff_oadd_inverse, ww2_def,
- vv2_subset RS Diff_partition]) 1);
-qed "UN_gg2_eq";
-
-Goal "domain(gg2(f,a,b,s)) = a++a";
-by (simp_tac (simpset() addsimps [lam_funtype RS domain_of_fun, gg2_def]) 1);
-qed "domain_gg2";
-
-(* ********************************************************************** *)
-(* every value of defined function is less than or equipollent to m *)
-(* ********************************************************************** *)
-
-Goalw [vv2_def] "[| m \\<in> nat; m\\<noteq>0 |] ==> vv2(f,b,g,s) lepoll m";
-by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 1);
-by (fast_tac (claset()
- addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0]
- addSIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
- not_lt_imp_le RS le_imp_subset RS subset_imp_lepoll,
- nat_into_Ord, nat_1I]) 1);
-qed "vv2_lepoll";
-
-Goalw [ww2_def]
- "[| \\<forall>b<a. f`b lepoll succ(m); g<a; m \\<in> nat; vv2(f,b,g,d) \\<subseteq> f`g |] \
-\ ==> ww2(f,b,g,d) lepoll m";
-by (excluded_middle_tac "f`g = 0" 1);
-by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2);
-by (dtac ospec 1 THEN (assume_tac 1));
-by (rtac Diff_lepoll 1 THEN (TRYALL assume_tac));
-by (asm_simp_tac (simpset() addsimps [vv2_def, not_emptyI]) 1);
-qed "ww2_lepoll";
-
-Goalw [gg2_def]
- "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 --> \
-\ domain(uu(f,b,g,d)) eqpoll succ(m); \
-\ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \
-\ (\\<Union>b<a. f`b)=y; b<a; s \\<in> f`b; m \\<in> nat; m\\<noteq> 0; g<a++a \
-\ |] ==> gg2(f,a,b,s) ` g lepoll m";
-by (Asm_simp_tac 1);
-by (safe_tac (claset() addSEs [lt_oadd_odiff_cases, lt_Ord2]));
-by (asm_simp_tac (simpset() addsimps [vv2_lepoll]) 1);
-by (asm_simp_tac (simpset() addsimps [ww2_lepoll, vv2_subset]) 1);
-qed "gg2_lepoll_m";
-
-(* ********************************************************************** *)
-(* lemma ii *)
-(* ********************************************************************** *)
-Goalw [NN_def] "[| succ(m) \\<in> NN(y); y*y \\<subseteq> y; m \\<in> nat; m\\<noteq>0 |] ==> m \\<in> NN(y)";
-by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1));
-by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1
- THEN (assume_tac 1));
-(* case 1 *)
-by (asm_full_simp_tac (simpset() addsimps [lesspoll_succ_iff]) 1);
-by (res_inst_tac [("x","a++a")] exI 1);
-by (fast_tac (claset() addSIs [Ord_oadd, domain_gg1, UN_gg1_eq,
- gg1_lepoll_m]) 1);
-(* case 2 *)
-by (REPEAT (eresolve_tac [oexE, conjE] 1));
-by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (assume_tac 1));
-by (rtac CollectI 1);
-by (etac succ_natD 1);
-by (res_inst_tac [("x","a++a")] exI 1);
-by (res_inst_tac [("x","gg2(f,a,b,x)")] exI 1);
-(*Calling fast_tac might get rid of the res_inst_tac calls, but it
- is just too slow.*)
-by (asm_simp_tac (simpset() addsimps
- [Ord_oadd, domain_gg2, UN_gg2_eq, gg2_lepoll_m]) 1);
-qed "lemma_ii";
-
-
-(* ********************************************************************** *)
-(* lemma iv - p. 4 \\<in> *)
-(* For every set x there is a set y such that x Un (y * y) \\<subseteq> y *)
-(* ********************************************************************** *)
-
-(* the quantifier \\<forall>looks inelegant but makes the proofs shorter *)
-(* (used only in the following two lemmas) *)
-
-Goal "\\<forall>n \\<in> nat. rec(n, x, %k r. r Un r*r) \\<subseteq> \
-\ rec(succ(n), x, %k r. r Un r*r)";
-by (fast_tac (claset() addIs [rec_succ RS ssubst]) 1);
-qed "z_n_subset_z_succ_n";
-
-Goal "[| \\<forall>n \\<in> nat. f(n)<=f(succ(n)); n le m; n \\<in> nat; m \\<in> nat |] \
-\ ==> f(n)<=f(m)";
-by (eres_inst_tac [("P","n le m")] rev_mp 1);
-by (res_inst_tac [("P","%z. n le z --> f(n) \\<subseteq> f(z)")] nat_induct 1);
-by (REPEAT (fast_tac le_cs 1));
-qed "le_subsets";
-
-Goal "[| n le m; m \\<in> nat |] ==> \
-\ rec(n, x, %k r. r Un r*r) \\<subseteq> rec(m, x, %k r. r Un r*r)";
-by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1
- THEN (TRYALL assume_tac));
-by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1
- THEN (assume_tac 1));
-qed "le_imp_rec_subset";
-
-Goal "\\<exists>y. x Un y*y \\<subseteq> y";
-by (res_inst_tac [("x","\\<Union>n \\<in> nat. rec(n, x, %k r. r Un r*r)")] exI 1);
-by Safe_tac;
-by (rtac (nat_0I RS UN_I) 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
-by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (assume_tac 1));
-by (fast_tac (ZF_cs addIs [le_imp_rec_subset RS subsetD]
- addSIs [Un_upper1_le, Un_upper2_le, Un_nat_type]
- addSEs [nat_into_Ord] addss (simpset())) 1);
-qed "lemma_iv";
-
-(* ********************************************************************** *)
-(* Rubin & Rubin wrote \\<in> *)
-(* "It follows from (ii) and mathematical induction that if y*y \\<subseteq> y then *)
-(* y can be well-ordered" *)
-
-(* In fact we have to prove \\<in> *)
-(* * WO6 ==> NN(y) \\<noteq> 0 *)
-(* * reverse induction which lets us infer that 1 \\<in> NN(y) *)
-(* * 1 \\<in> NN(y) ==> y can be well-ordered *)
-(* ********************************************************************** *)
-
-(* ********************************************************************** *)
-(* WO6 ==> NN(y) \\<noteq> 0 *)
-(* ********************************************************************** *)
-
-Goalw [WO6_def, NN_def] "WO6 ==> NN(y) \\<noteq> 0";
-by (fast_tac ZF_cs 1); (*SLOW if current claset is used*)
-qed "WO6_imp_NN_not_empty";
-
-(* ********************************************************************** *)
-(* 1 \\<in> NN(y) ==> y can be well-ordered *)
-(* ********************************************************************** *)
-
-Goal "[| (\\<Union>b<a. f`b)=y; x \\<in> y; \\<forall>b<a. f`b lepoll 1; Ord(a) |] \
-\ ==> \\<exists>c<a. f`c = {x}";
-by (fast_tac (claset() addSEs [lepoll_1_is_sing]) 1);
-val lemma1 = result();
-
-Goal "[| (\\<Union>b<a. f`b)=y; x \\<in> y; \\<forall>b<a. f`b lepoll 1; Ord(a) |] \
-\ ==> f` (LEAST i. f`i = {x}) = {x}";
-by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
-by (fast_tac (claset() addSEs [lt_Ord] addIs [LeastI]) 1);
-val lemma2 = result();
-
-Goalw [NN_def] "1 \\<in> NN(y) ==> \\<exists>a f. Ord(a) & f \\<in> inj(y, a)";
-by (etac CollectE 1);
-by (REPEAT (eresolve_tac [exE, conjE] 1));
-by (res_inst_tac [("x","a")] exI 1);
-by (res_inst_tac [("x","\\<lambda>x \\<in> y. LEAST i. f`i = {x}")] exI 1);
-by (rtac conjI 1 THEN (assume_tac 1));
-by (res_inst_tac [("d","%i. THE x. x \\<in> f`i")] lam_injective 1);
-by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
-by (fast_tac (claset() addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
-by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
-by (Blast_tac 1);
-qed "NN_imp_ex_inj";
-
-Goal "[| y*y \\<subseteq> y; 1 \\<in> NN(y) |] ==> \\<exists>r. well_ord(y, r)";
-by (dtac NN_imp_ex_inj 1);
-by (fast_tac (claset() addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1);
-qed "y_well_ord";
-
-(* ********************************************************************** *)
-(* reverse induction which lets us infer that 1 \\<in> NN(y) *)
-(* ********************************************************************** *)
-
-val [prem1, prem2] = goal thy
- "[| n \\<in> nat; !!m. [| m \\<in> nat; m\\<noteq>0; P(succ(m)) |] ==> P(m) |] \
-\ ==> n\\<noteq>0 --> P(n) --> P(1)";
-by (rtac (prem1 RS nat_induct) 1);
-by (Blast_tac 1);
-by (excluded_middle_tac "x=0" 1);
-by (Blast_tac 2);
-by (fast_tac (claset() addSIs [prem2]) 1);
-qed "rev_induct_lemma";
-
-val prems =
-Goal "[| P(n); n \\<in> nat; n\\<noteq>0; \
-\ !!m. [| m \\<in> nat; m\\<noteq>0; P(succ(m)) |] ==> P(m) |] \
-\ ==> P(1)";
-by (resolve_tac [rev_induct_lemma RS impE] 1);
-by (etac impE 4 THEN (assume_tac 5));
-by (REPEAT (ares_tac prems 1));
-qed "rev_induct";
-
-Goalw [NN_def] "n \\<in> NN(y) ==> n \\<in> nat";
-by (etac CollectD1 1);
-qed "NN_into_nat";
-
-Goal "[| n \\<in> NN(y); y*y \\<subseteq> y; n\\<noteq>0 |] ==> 1 \\<in> NN(y)";
-by (rtac rev_induct 1 THEN REPEAT (ares_tac [NN_into_nat] 1));
-by (rtac lemma_ii 1 THEN REPEAT (assume_tac 1));
-val lemma3 = result();
-
-(* ********************************************************************** *)
-(* Main theorem "WO6 ==> WO1" *)
-(* ********************************************************************** *)
-
-(* another helpful lemma *)
-Goalw [NN_def] "0 \\<in> NN(y) ==> y=0";
-by (fast_tac (claset() addSIs [equalityI]
- addSDs [lepoll_0_is_0] addEs [subst]) 1);
-qed "NN_y_0";
-
-Goalw [WO1_def] "WO6 ==> WO1";
-by (rtac allI 1);
-by (excluded_middle_tac "A=0" 1);
-by (fast_tac (claset() addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2);
-by (res_inst_tac [("x1","A")] (lemma_iv RS revcut_rl) 1);
-by (etac exE 1);
-by (dtac WO6_imp_NN_not_empty 1);
-by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1);
-by (eres_inst_tac [("A","NN(y)")] not_emptyE 1);
-by (ftac y_well_ord 1);
-by (fast_tac (claset() addEs [well_ord_subset]) 2);
-by (fast_tac (claset() addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1);
-qed "WO6_imp_WO1";
-