1(* Title: ZF/AC/WO6_WO1.thy 2 Author: Krzysztof Grabczewski 3 4Proofs needed to state that formulations WO1,...,WO6 are all equivalent. 5The only hard one is WO6 ==> WO1. 6 7Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear" 8by Rubin & Rubin (page 2). 9They refer reader to a book by G��del to see the proof WO1 ==> WO2. 10Fortunately order types made this proof also very easy. 11*) 12 13theory WO6_WO1 14imports Cardinal_aux 15begin 16 17(* Auxiliary definitions used in proof *) 18definition 19 NN :: "i => i" where 20 "NN(y) == {m \<in> nat. \<exists>a. \<exists>f. Ord(a) & domain(f)=a & 21 (\<Union>b<a. f`b) = y & (\<forall>b<a. f`b \<lesssim> m)}" 22 23definition 24 uu :: "[i, i, i, i] => i" where 25 "uu(f, beta, gamma, delta) == (f`beta * f`gamma) \<inter> f`delta" 26 27 28(** Definitions for case 1 **) 29definition 30 vv1 :: "[i, i, i] => i" where 31 "vv1(f,m,b) == 32 let g = \<mu> g. (\<exists>d. Ord(d) & (domain(uu(f,b,g,d)) \<noteq> 0 & 33 domain(uu(f,b,g,d)) \<lesssim> m)); 34 d = \<mu> d. domain(uu(f,b,g,d)) \<noteq> 0 & 35 domain(uu(f,b,g,d)) \<lesssim> m 36 in if f`b \<noteq> 0 then domain(uu(f,b,g,d)) else 0" 37 38definition 39 ww1 :: "[i, i, i] => i" where 40 "ww1(f,m,b) == f`b - vv1(f,m,b)" 41 42definition 43 gg1 :: "[i, i, i] => i" where 44 "gg1(f,a,m) == \<lambda>b \<in> a++a. if b<a then vv1(f,m,b) else ww1(f,m,b--a)" 45 46 47(** Definitions for case 2 **) 48definition 49 vv2 :: "[i, i, i, i] => i" where 50 "vv2(f,b,g,s) == 51 if f`g \<noteq> 0 then {uu(f, b, g, \<mu> d. uu(f,b,g,d) \<noteq> 0)`s} else 0" 52 53definition 54 ww2 :: "[i, i, i, i] => i" where 55 "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)" 56 57definition 58 gg2 :: "[i, i, i, i] => i" where 59 "gg2(f,a,b,s) == 60 \<lambda>g \<in> a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)" 61 62 63lemma WO2_WO3: "WO2 ==> WO3" 64by (unfold WO2_def WO3_def, fast) 65 66(* ********************************************************************** *) 67 68lemma WO3_WO1: "WO3 ==> WO1" 69apply (unfold eqpoll_def WO1_def WO3_def) 70apply (intro allI) 71apply (drule_tac x=A in spec) 72apply (blast intro: bij_is_inj well_ord_rvimage 73 well_ord_Memrel [THEN well_ord_subset]) 74done 75 76(* ********************************************************************** *) 77 78lemma WO1_WO2: "WO1 ==> WO2" 79apply (unfold eqpoll_def WO1_def WO2_def) 80apply (blast intro!: Ord_ordertype ordermap_bij) 81done 82 83(* ********************************************************************** *) 84 85lemma lam_sets: "f \<in> A->B ==> (\<lambda>x \<in> A. {f`x}): A -> {{b}. b \<in> B}" 86by (fast intro!: lam_type apply_type) 87 88lemma surj_imp_eq': "f \<in> surj(A,B) ==> (\<Union>a \<in> A. {f`a}) = B" 89apply (unfold surj_def) 90apply (fast elim!: apply_type) 91done 92 93lemma surj_imp_eq: "[| f \<in> surj(A,B); Ord(A) |] ==> (\<Union>a<A. {f`a}) = B" 94by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE) 95 96lemma WO1_WO4: "WO1 ==> WO4(1)" 97apply (unfold WO1_def WO4_def) 98apply (rule allI) 99apply (erule_tac x = A in allE) 100apply (erule exE) 101apply (intro exI conjI) 102apply (erule Ord_ordertype) 103apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN lam_sets, THEN domain_of_fun]) 104apply (simp_all add: singleton_eqpoll_1 eqpoll_imp_lepoll Ord_ordertype 105 ordermap_bij [THEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq] 106 ltD) 107done 108 109(* ********************************************************************** *) 110 111lemma WO4_mono: "[| m\<le>n; WO4(m) |] ==> WO4(n)" 112apply (unfold WO4_def) 113apply (blast dest!: spec intro: lepoll_trans [OF _ le_imp_lepoll]) 114done 115 116(* ********************************************************************** *) 117 118lemma WO4_WO5: "[| m \<in> nat; 1\<le>m; WO4(m) |] ==> WO5" 119by (unfold WO4_def WO5_def, blast) 120 121(* ********************************************************************** *) 122 123lemma WO5_WO6: "WO5 ==> WO6" 124by (unfold WO4_def WO5_def WO6_def, blast) 125 126 127(* ********************************************************************** 128 The proof of "WO6 ==> WO1". Simplified by L C Paulson. 129 130 From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin, 131 pages 2-5 132************************************************************************* *) 133 134lemma lt_oadd_odiff_disj: 135 "[| k < i++j; Ord(i); Ord(j) |] 136 ==> k < i | (~ k<i & k = i ++ (k--i) & (k--i)<j)" 137apply (rule_tac i = k and j = i in Ord_linear2) 138prefer 4 139 apply (drule odiff_lt_mono2, assumption) 140 apply (simp add: oadd_odiff_inverse odiff_oadd_inverse) 141apply (auto elim!: lt_Ord) 142done 143 144 145(* ********************************************************************** *) 146(* The most complicated part of the proof - lemma ii - p. 2-4 *) 147(* ********************************************************************** *) 148 149(* ********************************************************************** *) 150(* some properties of relation uu(beta, gamma, delta) - p. 2 *) 151(* ********************************************************************** *) 152 153lemma domain_uu_subset: "domain(uu(f,b,g,d)) \<subseteq> f`b" 154by (unfold uu_def, blast) 155 156lemma quant_domain_uu_lepoll_m: 157 "\<forall>b<a. f`b \<lesssim> m ==> \<forall>b<a. \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<lesssim> m" 158by (blast intro: domain_uu_subset [THEN subset_imp_lepoll] lepoll_trans) 159 160lemma uu_subset1: "uu(f,b,g,d) \<subseteq> f`b * f`g" 161by (unfold uu_def, blast) 162 163lemma uu_subset2: "uu(f,b,g,d) \<subseteq> f`d" 164by (unfold uu_def, blast) 165 166lemma uu_lepoll_m: "[| \<forall>b<a. f`b \<lesssim> m; d<a |] ==> uu(f,b,g,d) \<lesssim> m" 167by (blast intro: uu_subset2 [THEN subset_imp_lepoll] lepoll_trans) 168 169(* ********************************************************************** *) 170(* Two cases for lemma ii *) 171(* ********************************************************************** *) 172lemma cases: 173 "\<forall>b<a. \<forall>g<a. \<forall>d<a. u(f,b,g,d) \<lesssim> m 174 ==> (\<forall>b<a. f`b \<noteq> 0 \<longrightarrow> 175 (\<exists>g<a. \<exists>d<a. u(f,b,g,d) \<noteq> 0 & u(f,b,g,d) \<prec> m)) 176 | (\<exists>b<a. f`b \<noteq> 0 & (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 \<longrightarrow> 177 u(f,b,g,d) \<approx> m))" 178apply (unfold lesspoll_def) 179apply (blast del: equalityI) 180done 181 182(* ********************************************************************** *) 183(* Lemmas used in both cases *) 184(* ********************************************************************** *) 185lemma UN_oadd: "Ord(a) ==> (\<Union>b<a++a. C(b)) = (\<Union>b<a. C(b) \<union> C(a++b))" 186by (blast intro: ltI lt_oadd1 oadd_lt_mono2 dest!: lt_oadd_disj) 187 188 189(* ********************************************************************** *) 190(* Case 1: lemmas *) 191(* ********************************************************************** *) 192 193lemma vv1_subset: "vv1(f,m,b) \<subseteq> f`b" 194by (simp add: vv1_def Let_def domain_uu_subset) 195 196(* ********************************************************************** *) 197(* Case 1: Union of images is the whole "y" *) 198(* ********************************************************************** *) 199lemma UN_gg1_eq: 200 "[| Ord(a); m \<in> nat |] ==> (\<Union>b<a++a. gg1(f,a,m)`b) = (\<Union>b<a. f`b)" 201by (simp add: gg1_def UN_oadd lt_oadd1 oadd_le_self [THEN le_imp_not_lt] 202 lt_Ord odiff_oadd_inverse ltD vv1_subset [THEN Diff_partition] 203 ww1_def) 204 205lemma domain_gg1: "domain(gg1(f,a,m)) = a++a" 206by (simp add: lam_funtype [THEN domain_of_fun] gg1_def) 207 208(* ********************************************************************** *) 209(* every value of defined function is less than or equipollent to m *) 210(* ********************************************************************** *) 211lemma nested_LeastI: 212 "[| P(a, b); Ord(a); Ord(b); 213 Least_a = (\<mu> a. \<exists>x. Ord(x) & P(a, x)) |] 214 ==> P(Least_a, \<mu> b. P(Least_a, b))" 215apply (erule ssubst) 216apply (rule_tac Q = "%z. P (z, \<mu> b. P (z, b))" in LeastI2) 217apply (fast elim!: LeastI)+ 218done 219 220lemmas nested_Least_instance = 221 nested_LeastI [of "%g d. domain(uu(f,b,g,d)) \<noteq> 0 & 222 domain(uu(f,b,g,d)) \<lesssim> m"] for f b m 223 224lemma gg1_lepoll_m: 225 "[| Ord(a); m \<in> nat; 226 \<forall>b<a. f`b \<noteq>0 \<longrightarrow> 227 (\<exists>g<a. \<exists>d<a. domain(uu(f,b,g,d)) \<noteq> 0 & 228 domain(uu(f,b,g,d)) \<lesssim> m); 229 \<forall>b<a. f`b \<lesssim> succ(m); b<a++a |] 230 ==> gg1(f,a,m)`b \<lesssim> m" 231apply (simp add: gg1_def empty_lepollI) 232apply (safe dest!: lt_oadd_odiff_disj) 233(*Case b<a \<in> show vv1(f,m,b) \<lesssim> m *) 234 apply (simp add: vv1_def Let_def empty_lepollI) 235 apply (fast intro: nested_Least_instance [THEN conjunct2] 236 elim!: lt_Ord) 237(*Case a\<le>b \<in> show ww1(f,m,b--a) \<lesssim> m *) 238apply (simp add: ww1_def empty_lepollI) 239apply (case_tac "f` (b--a) = 0", simp add: empty_lepollI) 240apply (rule Diff_lepoll, blast) 241apply (rule vv1_subset) 242apply (drule ospec [THEN mp], assumption+) 243apply (elim oexE conjE) 244apply (simp add: vv1_def Let_def lt_Ord nested_Least_instance [THEN conjunct1]) 245done 246 247(* ********************************************************************** *) 248(* Case 2: lemmas *) 249(* ********************************************************************** *) 250 251(* ********************************************************************** *) 252(* Case 2: vv2_subset *) 253(* ********************************************************************** *) 254 255lemma ex_d_uu_not_empty: 256 "[| b<a; g<a; f`b\<noteq>0; f`g\<noteq>0; 257 y*y \<subseteq> y; (\<Union>b<a. f`b)=y |] 258 ==> \<exists>d<a. uu(f,b,g,d) \<noteq> 0" 259by (unfold uu_def, blast) 260 261lemma uu_not_empty: 262 "[| b<a; g<a; f`b\<noteq>0; f`g\<noteq>0; y*y \<subseteq> y; (\<Union>b<a. f`b)=y |] 263 ==> uu(f,b,g,\<mu> d. (uu(f,b,g,d) \<noteq> 0)) \<noteq> 0" 264apply (drule ex_d_uu_not_empty, assumption+) 265apply (fast elim!: LeastI lt_Ord) 266done 267 268lemma not_empty_rel_imp_domain: "[| r \<subseteq> A*B; r\<noteq>0 |] ==> domain(r)\<noteq>0" 269by blast 270 271lemma Least_uu_not_empty_lt_a: 272 "[| b<a; g<a; f`b\<noteq>0; f`g\<noteq>0; y*y \<subseteq> y; (\<Union>b<a. f`b)=y |] 273 ==> (\<mu> d. uu(f,b,g,d) \<noteq> 0) < a" 274apply (erule ex_d_uu_not_empty [THEN oexE], assumption+) 275apply (blast intro: Least_le [THEN lt_trans1] lt_Ord) 276done 277 278lemma subset_Diff_sing: "[| B \<subseteq> A; a\<notin>B |] ==> B \<subseteq> A-{a}" 279by blast 280 281(*Could this be proved more directly?*) 282lemma supset_lepoll_imp_eq: 283 "[| A \<lesssim> m; m \<lesssim> B; B \<subseteq> A; m \<in> nat |] ==> A=B" 284apply (erule natE) 285apply (fast dest!: lepoll_0_is_0 intro!: equalityI) 286apply (safe intro!: equalityI) 287apply (rule ccontr) 288apply (rule succ_lepoll_natE) 289 apply (erule lepoll_trans) 290 apply (rule lepoll_trans) 291 apply (erule subset_Diff_sing [THEN subset_imp_lepoll], assumption) 292 apply (rule Diff_sing_lepoll, assumption+) 293done 294 295lemma uu_Least_is_fun: 296 "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 \<longrightarrow> 297 domain(uu(f, b, g, d)) \<approx> succ(m); 298 \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y; 299 (\<Union>b<a. f`b)=y; b<a; g<a; d<a; 300 f`b\<noteq>0; f`g\<noteq>0; m \<in> nat; s \<in> f`b |] 301 ==> uu(f, b, g, \<mu> d. uu(f,b,g,d)\<noteq>0) \<in> f`b -> f`g" 302apply (drule_tac x2=g in ospec [THEN ospec, THEN mp]) 303 apply (rule_tac [3] not_empty_rel_imp_domain [OF uu_subset1 uu_not_empty]) 304 apply (rule_tac [2] Least_uu_not_empty_lt_a, assumption+) 305apply (rule rel_is_fun) 306 apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) 307 apply (erule uu_lepoll_m) 308 apply (rule Least_uu_not_empty_lt_a, assumption+) 309apply (rule uu_subset1) 310apply (rule supset_lepoll_imp_eq [OF _ eqpoll_sym [THEN eqpoll_imp_lepoll]]) 311apply (fast intro!: domain_uu_subset)+ 312done 313 314lemma vv2_subset: 315 "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 \<longrightarrow> 316 domain(uu(f, b, g, d)) \<approx> succ(m); 317 \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y; 318 (\<Union>b<a. f`b)=y; b<a; g<a; m \<in> nat; s \<in> f`b |] 319 ==> vv2(f,b,g,s) \<subseteq> f`g" 320apply (simp add: vv2_def) 321apply (blast intro: uu_Least_is_fun [THEN apply_type]) 322done 323 324(* ********************************************************************** *) 325(* Case 2: Union of images is the whole "y" *) 326(* ********************************************************************** *) 327lemma UN_gg2_eq: 328 "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<longrightarrow> 329 domain(uu(f,b,g,d)) \<approx> succ(m); 330 \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y; 331 (\<Union>b<a. f`b)=y; Ord(a); m \<in> nat; s \<in> f`b; b<a |] 332 ==> (\<Union>g<a++a. gg2(f,a,b,s) ` g) = y" 333apply (unfold gg2_def) 334apply (drule sym) 335apply (simp add: ltD UN_oadd oadd_le_self [THEN le_imp_not_lt] 336 lt_Ord odiff_oadd_inverse ww2_def 337 vv2_subset [THEN Diff_partition]) 338done 339 340lemma domain_gg2: "domain(gg2(f,a,b,s)) = a++a" 341by (simp add: lam_funtype [THEN domain_of_fun] gg2_def) 342 343 344(* ********************************************************************** *) 345(* every value of defined function is less than or equipollent to m *) 346(* ********************************************************************** *) 347 348lemma vv2_lepoll: "[| m \<in> nat; m\<noteq>0 |] ==> vv2(f,b,g,s) \<lesssim> m" 349apply (unfold vv2_def) 350apply (simp add: empty_lepollI) 351apply (fast dest!: le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_0_is_0] 352 intro!: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 353 not_lt_imp_le [THEN le_imp_subset, THEN subset_imp_lepoll] 354 nat_into_Ord nat_1I) 355done 356 357lemma ww2_lepoll: 358 "[| \<forall>b<a. f`b \<lesssim> succ(m); g<a; m \<in> nat; vv2(f,b,g,d) \<subseteq> f`g |] 359 ==> ww2(f,b,g,d) \<lesssim> m" 360apply (unfold ww2_def) 361apply (case_tac "f`g = 0") 362apply (simp add: empty_lepollI) 363apply (drule ospec, assumption) 364apply (rule Diff_lepoll, assumption+) 365apply (simp add: vv2_def not_emptyI) 366done 367 368lemma gg2_lepoll_m: 369 "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<longrightarrow> 370 domain(uu(f,b,g,d)) \<approx> succ(m); 371 \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y; 372 (\<Union>b<a. f`b)=y; b<a; s \<in> f`b; m \<in> nat; m\<noteq> 0; g<a++a |] 373 ==> gg2(f,a,b,s) ` g \<lesssim> m" 374apply (simp add: gg2_def empty_lepollI) 375apply (safe elim!: lt_Ord2 dest!: lt_oadd_odiff_disj) 376 apply (simp add: vv2_lepoll) 377apply (simp add: ww2_lepoll vv2_subset) 378done 379 380(* ********************************************************************** *) 381(* lemma ii *) 382(* ********************************************************************** *) 383lemma lemma_ii: "[| succ(m) \<in> NN(y); y*y \<subseteq> y; m \<in> nat; m\<noteq>0 |] ==> m \<in> NN(y)" 384apply (unfold NN_def) 385apply (elim CollectE exE conjE) 386apply (rule quant_domain_uu_lepoll_m [THEN cases, THEN disjE], assumption) 387(* case 1 *) 388apply (simp add: lesspoll_succ_iff) 389apply (rule_tac x = "a++a" in exI) 390apply (fast intro!: Ord_oadd domain_gg1 UN_gg1_eq gg1_lepoll_m) 391(* case 2 *) 392apply (elim oexE conjE) 393apply (rule_tac A = "f`B" for B in not_emptyE, assumption) 394apply (rule CollectI) 395apply (erule succ_natD) 396apply (rule_tac x = "a++a" in exI) 397apply (rule_tac x = "gg2 (f,a,b,x) " in exI) 398apply (simp add: Ord_oadd domain_gg2 UN_gg2_eq gg2_lepoll_m) 399done 400 401 402(* ********************************************************************** *) 403(* lemma iv - p. 4: *) 404(* For every set x there is a set y such that x \<union> (y * y) \<subseteq> y *) 405(* ********************************************************************** *) 406 407 408(* The leading \<forall>-quantifier looks odd but makes the proofs shorter 409 (used only in the following two lemmas) *) 410 411lemma z_n_subset_z_succ_n: 412 "\<forall>n \<in> nat. rec(n, x, %k r. r \<union> r*r) \<subseteq> rec(succ(n), x, %k r. r \<union> r*r)" 413by (fast intro: rec_succ [THEN ssubst]) 414 415lemma le_subsets: 416 "[| \<forall>n \<in> nat. f(n)<=f(succ(n)); n\<le>m; n \<in> nat; m \<in> nat |] 417 ==> f(n)<=f(m)" 418apply (erule_tac P = "n\<le>m" in rev_mp) 419apply (rule_tac P = "%z. n\<le>z \<longrightarrow> f (n) \<subseteq> f (z) " in nat_induct) 420apply (auto simp add: le_iff) 421done 422 423lemma le_imp_rec_subset: 424 "[| n\<le>m; m \<in> nat |] 425 ==> rec(n, x, %k r. r \<union> r*r) \<subseteq> rec(m, x, %k r. r \<union> r*r)" 426apply (rule z_n_subset_z_succ_n [THEN le_subsets]) 427apply (blast intro: lt_nat_in_nat)+ 428done 429 430lemma lemma_iv: "\<exists>y. x \<union> y*y \<subseteq> y" 431apply (rule_tac x = "\<Union>n \<in> nat. rec (n, x, %k r. r \<union> r*r) " in exI) 432apply safe 433apply (rule nat_0I [THEN UN_I], simp) 434apply (rule_tac a = "succ (n \<union> na) " in UN_I) 435apply (erule Un_nat_type [THEN nat_succI], assumption) 436apply (auto intro: le_imp_rec_subset [THEN subsetD] 437 intro!: Un_upper1_le Un_upper2_le Un_nat_type 438 elim!: nat_into_Ord) 439done 440 441(* ********************************************************************** *) 442(* Rubin & Rubin wrote, *) 443(* "It follows from (ii) and mathematical induction that if y*y \<subseteq> y then *) 444(* y can be well-ordered" *) 445 446(* In fact we have to prove *) 447(* * WO6 ==> NN(y) \<noteq> 0 *) 448(* * reverse induction which lets us infer that 1 \<in> NN(y) *) 449(* * 1 \<in> NN(y) ==> y can be well-ordered *) 450(* ********************************************************************** *) 451 452(* ********************************************************************** *) 453(* WO6 ==> NN(y) \<noteq> 0 *) 454(* ********************************************************************** *) 455 456lemma WO6_imp_NN_not_empty: "WO6 ==> NN(y) \<noteq> 0" 457by (unfold WO6_def NN_def, clarify, blast) 458 459(* ********************************************************************** *) 460(* 1 \<in> NN(y) ==> y can be well-ordered *) 461(* ********************************************************************** *) 462 463lemma lemma1: 464 "[| (\<Union>b<a. f`b)=y; x \<in> y; \<forall>b<a. f`b \<lesssim> 1; Ord(a) |] ==> \<exists>c<a. f`c = {x}" 465by (fast elim!: lepoll_1_is_sing) 466 467lemma lemma2: 468 "[| (\<Union>b<a. f`b)=y; x \<in> y; \<forall>b<a. f`b \<lesssim> 1; Ord(a) |] 469 ==> f` (\<mu> i. f`i = {x}) = {x}" 470apply (drule lemma1, assumption+) 471apply (fast elim!: lt_Ord intro: LeastI) 472done 473 474lemma NN_imp_ex_inj: "1 \<in> NN(y) ==> \<exists>a f. Ord(a) & f \<in> inj(y, a)" 475apply (unfold NN_def) 476apply (elim CollectE exE conjE) 477apply (rule_tac x = a in exI) 478apply (rule_tac x = "\<lambda>x \<in> y. \<mu> i. f`i = {x}" in exI) 479apply (rule conjI, assumption) 480apply (rule_tac d = "%i. THE x. x \<in> f`i" in lam_injective) 481apply (drule lemma1, assumption+) 482apply (fast elim!: Least_le [THEN lt_trans1, THEN ltD] lt_Ord) 483apply (rule lemma2 [THEN ssubst], assumption+, blast) 484done 485 486lemma y_well_ord: "[| y*y \<subseteq> y; 1 \<in> NN(y) |] ==> \<exists>r. well_ord(y, r)" 487apply (drule NN_imp_ex_inj) 488apply (fast elim!: well_ord_rvimage [OF _ well_ord_Memrel]) 489done 490 491(* ********************************************************************** *) 492(* reverse induction which lets us infer that 1 \<in> NN(y) *) 493(* ********************************************************************** *) 494 495lemma rev_induct_lemma [rule_format]: 496 "[| n \<in> nat; !!m. [| m \<in> nat; m\<noteq>0; P(succ(m)) |] ==> P(m) |] 497 ==> n\<noteq>0 \<longrightarrow> P(n) \<longrightarrow> P(1)" 498by (erule nat_induct, blast+) 499 500lemma rev_induct: 501 "[| n \<in> nat; P(n); n\<noteq>0; 502 !!m. [| m \<in> nat; m\<noteq>0; P(succ(m)) |] ==> P(m) |] 503 ==> P(1)" 504by (rule rev_induct_lemma, blast+) 505 506lemma NN_into_nat: "n \<in> NN(y) ==> n \<in> nat" 507by (simp add: NN_def) 508 509lemma lemma3: "[| n \<in> NN(y); y*y \<subseteq> y; n\<noteq>0 |] ==> 1 \<in> NN(y)" 510apply (rule rev_induct [OF NN_into_nat], assumption+) 511apply (rule lemma_ii, assumption+) 512done 513 514(* ********************************************************************** *) 515(* Main theorem "WO6 ==> WO1" *) 516(* ********************************************************************** *) 517 518(* another helpful lemma *) 519lemma NN_y_0: "0 \<in> NN(y) ==> y=0" 520apply (unfold NN_def) 521apply (fast intro!: equalityI dest!: lepoll_0_is_0 elim: subst) 522done 523 524lemma WO6_imp_WO1: "WO6 ==> WO1" 525apply (unfold WO1_def) 526apply (rule allI) 527apply (case_tac "A=0") 528apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord]) 529apply (rule_tac x = A in lemma_iv [elim_format]) 530apply (erule exE) 531apply (drule WO6_imp_NN_not_empty) 532apply (erule Un_subset_iff [THEN iffD1, THEN conjE]) 533apply (erule_tac A = "NN (y) " in not_emptyE) 534apply (frule y_well_ord) 535 apply (fast intro!: lemma3 dest!: NN_y_0 elim!: not_emptyE) 536apply (fast elim: well_ord_subset) 537done 538 539end 540