1(* Title: ZF/AC/WO2_AC16.thy 2 Author: Krzysztof Grabczewski 3 4The proof of WO2 ==> AC16(k #+ m, k) 5 6The main part of the proof is the inductive reasoning concerning 7properties of constructed family T_gamma. 8The proof deals with three cases for ordinals: 0, succ and limit ordinal. 9The first instance is trivial, the third not difficult, but the second 10is very complicated requiring many lemmas. 11We also need to prove that at any stage gamma the set 12(s - \<Union>(...) - k_gamma) (Rubin & Rubin page 15) 13contains m distinct elements (in fact is equipollent to s) 14*) 15 16theory WO2_AC16 imports AC_Equiv AC16_lemmas Cardinal_aux begin 17 18(**** A recursive definition used in the proof of WO2 ==> AC16 ****) 19 20definition 21 recfunAC16 :: "[i,i,i,i] => i" where 22 "recfunAC16(f,h,i,a) == 23 transrec2(i, 0, 24 %g r. if (\<exists>y \<in> r. h`g \<subseteq> y) then r 25 else r \<union> {f`(\<mu> i. h`g \<subseteq> f`i & 26 (\<forall>b<a. (h`b \<subseteq> f`i \<longrightarrow> (\<forall>t \<in> r. ~ h`b \<subseteq> t))))})" 27 28(* ********************************************************************** *) 29(* Basic properties of recfunAC16 *) 30(* ********************************************************************** *) 31 32lemma recfunAC16_0: "recfunAC16(f,h,0,a) = 0" 33by (simp add: recfunAC16_def) 34 35lemma recfunAC16_succ: 36 "recfunAC16(f,h,succ(i),a) = 37 (if (\<exists>y \<in> recfunAC16(f,h,i,a). h ` i \<subseteq> y) then recfunAC16(f,h,i,a) 38 else recfunAC16(f,h,i,a) \<union> 39 {f ` (\<mu> j. h ` i \<subseteq> f ` j & 40 (\<forall>b<a. (h`b \<subseteq> f`j 41 \<longrightarrow> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})" 42apply (simp add: recfunAC16_def) 43done 44 45lemma recfunAC16_Limit: "Limit(i) 46 ==> recfunAC16(f,h,i,a) = (\<Union>j<i. recfunAC16(f,h,j,a))" 47by (simp add: recfunAC16_def transrec2_Limit) 48 49(* ********************************************************************** *) 50(* Monotonicity of transrec2 *) 51(* ********************************************************************** *) 52 53lemma transrec2_mono_lemma [rule_format]: 54 "[| !!g r. r \<subseteq> B(g,r); Ord(i) |] 55 ==> j<i \<longrightarrow> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)" 56apply (erule trans_induct) 57apply (rule Ord_cases, assumption+, fast) 58apply (simp (no_asm_simp)) 59apply (blast elim!: leE) 60apply (simp add: transrec2_Limit) 61apply (blast intro: OUN_I ltI Ord_in_Ord [THEN le_refl] 62 elim!: Limit_has_succ [THEN ltE]) 63done 64 65lemma transrec2_mono: 66 "[| !!g r. r \<subseteq> B(g,r); j\<le>i |] 67 ==> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)" 68apply (erule leE) 69apply (rule transrec2_mono_lemma) 70apply (auto intro: lt_Ord2 ) 71done 72 73(* ********************************************************************** *) 74(* Monotonicity of recfunAC16 *) 75(* ********************************************************************** *) 76 77lemma recfunAC16_mono: 78 "i\<le>j ==> recfunAC16(f, g, i, a) \<subseteq> recfunAC16(f, g, j, a)" 79apply (unfold recfunAC16_def) 80apply (rule transrec2_mono, auto) 81done 82 83(* ********************************************************************** *) 84(* case of limit ordinal *) 85(* ********************************************************************** *) 86 87 88lemma lemma3_1: 89 "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y); 90 \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); j\<le>i; i<x; z<a; 91 V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |] 92 ==> V = W" 93apply (erule asm_rl allE impE)+ 94apply (drule subsetD, assumption, blast) 95done 96 97 98lemma lemma3: 99 "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y); 100 \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); i<x; j<x; z<a; 101 V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |] 102 ==> V = W" 103apply (rule_tac j=j in Ord_linear_le [OF lt_Ord lt_Ord], assumption+) 104apply (erule lemma3_1 [symmetric], assumption+) 105apply (erule lemma3_1, assumption+) 106done 107 108lemma lemma4: 109 "[| \<forall>y<x. F(y) \<subseteq> X & 110 (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow> 111 (\<exists>! Y. Y \<in> F(y) & h(x) \<subseteq> Y)); 112 x < a |] 113 ==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) \<longrightarrow> 114 (\<exists>! Y. Y \<in> F(y) & h(z) \<subseteq> Y)" 115apply (intro oallI impI) 116apply (drule ospec, assumption, clarify) 117apply (blast elim!: oallE ) 118done 119 120lemma lemma5: 121 "[| \<forall>y<x. F(y) \<subseteq> X & 122 (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow> 123 (\<exists>! Y. Y \<in> F(y) & h(x) \<subseteq> Y)); 124 x < a; Limit(x); \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j) |] 125 ==> (\<Union>x<x. F(x)) \<subseteq> X & 126 (\<forall>xa<a. xa < x | (\<exists>x \<in> \<Union>x<x. F(x). h(xa) \<subseteq> x) 127 \<longrightarrow> (\<exists>! Y. Y \<in> (\<Union>x<x. F(x)) & h(xa) \<subseteq> Y))" 128apply (rule conjI) 129apply (rule subsetI) 130apply (erule OUN_E) 131apply (drule ospec, assumption, fast) 132apply (drule lemma4, assumption) 133apply (rule oallI) 134apply (rule impI) 135apply (erule disjE) 136apply (frule ospec, erule Limit_has_succ, assumption) 137apply (drule_tac A = a and x = xa in ospec, assumption) 138apply (erule impE, rule le_refl [THEN disjI1], erule lt_Ord) 139apply (blast intro: lemma3 Limit_has_succ) 140apply (blast intro: lemma3) 141done 142 143(* ********************************************************************** *) 144(* case of successor ordinal *) 145(* ********************************************************************** *) 146 147(* 148 First quite complicated proof of the fact used in the recursive construction 149 of the family T_gamma (WO2 ==> AC16(k #+ m, k)) - the fact that at any stage 150 gamma the set (s - \<Union>(...) - k_gamma) is equipollent to s 151 (Rubin & Rubin page 15). 152*) 153 154(* ********************************************************************** *) 155(* dbl_Diff_eqpoll_Card *) 156(* ********************************************************************** *) 157 158 159lemma dbl_Diff_eqpoll_Card: 160 "[| A\<approx>a; Card(a); ~Finite(a); B\<prec>a; C\<prec>a |] ==> A - B - C\<approx>a" 161by (blast intro: Diff_lesspoll_eqpoll_Card) 162 163(* ********************************************************************** *) 164(* Case of finite ordinals *) 165(* ********************************************************************** *) 166 167 168lemma Finite_lesspoll_infinite_Ord: 169 "[| Finite(X); ~Finite(a); Ord(a) |] ==> X\<prec>a" 170apply (unfold lesspoll_def) 171apply (rule conjI) 172apply (drule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption) 173apply (unfold Finite_def) 174apply (blast intro: leI [THEN le_imp_subset, THEN subset_imp_lepoll] 175 ltI eqpoll_imp_lepoll lepoll_trans) 176apply (blast intro: eqpoll_sym [THEN eqpoll_trans]) 177done 178 179lemma Union_lesspoll: 180 "[| \<forall>x \<in> X. x \<lesssim> n & x \<subseteq> T; well_ord(T, R); X \<lesssim> b; 181 b<a; ~Finite(a); Card(a); n \<in> nat |] 182 ==> \<Union>(X)\<prec>a" 183apply (case_tac "Finite (X)") 184apply (blast intro: Card_is_Ord Finite_lesspoll_infinite_Ord 185 lepoll_nat_imp_Finite Finite_Union) 186apply (drule lepoll_imp_ex_le_eqpoll) 187apply (erule lt_Ord) 188apply (elim exE conjE) 189apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption) 190apply (erule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], 191 THEN exE]) 192apply (frule bij_is_surj [THEN surj_image_eq]) 193apply (drule image_fun [OF bij_is_fun subset_refl]) 194apply (drule sym [THEN trans], assumption) 195apply (blast intro: lt_Ord UN_lepoll lt_Card_imp_lesspoll 196 lt_trans1 lesspoll_trans1) 197done 198 199(* ********************************************************************** *) 200(* recfunAC16_lepoll_index *) 201(* ********************************************************************** *) 202 203lemma Un_sing_eq_cons: "A \<union> {a} = cons(a, A)" 204by fast 205 206lemma Un_lepoll_succ: "A \<lesssim> B ==> A \<union> {a} \<lesssim> succ(B)" 207apply (simp add: Un_sing_eq_cons succ_def) 208apply (blast elim!: mem_irrefl intro: cons_lepoll_cong) 209done 210 211lemma Diff_UN_succ_empty: "Ord(a) ==> F(a) - (\<Union>b<succ(a). F(b)) = 0" 212by (fast intro!: le_refl) 213 214lemma Diff_UN_succ_subset: "Ord(a) ==> F(a) \<union> X - (\<Union>b<succ(a). F(b)) \<subseteq> X" 215by blast 216 217lemma recfunAC16_Diff_lepoll_1: 218 "Ord(x) 219 ==> recfunAC16(f, g, x, a) - (\<Union>i<x. recfunAC16(f, g, i, a)) \<lesssim> 1" 220apply (erule Ord_cases) 221 apply (simp add: recfunAC16_0 empty_subsetI [THEN subset_imp_lepoll]) 222(*Limit case*) 223prefer 2 apply (simp add: recfunAC16_Limit Diff_cancel 224 empty_subsetI [THEN subset_imp_lepoll]) 225(*succ case*) 226apply (simp add: recfunAC16_succ 227 Diff_UN_succ_empty [of _ "%j. recfunAC16(f,g,j,a)"] 228 empty_subsetI [THEN subset_imp_lepoll]) 229apply (best intro: Diff_UN_succ_subset [THEN subset_imp_lepoll] 230 singleton_eqpoll_1 [THEN eqpoll_imp_lepoll] lepoll_trans) 231done 232 233lemma in_Least_Diff: 234 "[| z \<in> F(x); Ord(x) |] 235 ==> z \<in> F(\<mu> i. z \<in> F(i)) - (\<Union>j<(\<mu> i. z \<in> F(i)). F(j))" 236by (fast elim: less_LeastE elim!: LeastI) 237 238lemma Least_eq_imp_ex: 239 "[| (\<mu> i. w \<in> F(i)) = (\<mu> i. z \<in> F(i)); 240 w \<in> (\<Union>i<a. F(i)); z \<in> (\<Union>i<a. F(i)) |] 241 ==> \<exists>b<a. w \<in> (F(b) - (\<Union>c<b. F(c))) & z \<in> (F(b) - (\<Union>c<b. F(c)))" 242apply (elim OUN_E) 243apply (drule in_Least_Diff, erule lt_Ord) 244apply (frule in_Least_Diff, erule lt_Ord) 245apply (rule oexI, force) 246apply (blast intro: lt_Ord Least_le [THEN lt_trans1]) 247done 248 249 250lemma two_in_lepoll_1: "[| A \<lesssim> 1; a \<in> A; b \<in> A |] ==> a=b" 251by (fast dest!: lepoll_1_is_sing) 252 253 254lemma UN_lepoll_index: 255 "[| \<forall>i<a. F(i)-(\<Union>j<i. F(j)) \<lesssim> 1; Limit(a) |] 256 ==> (\<Union>x<a. F(x)) \<lesssim> a" 257apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]]) 258apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). \<mu> i. z \<in> F (i) " in exI) 259apply (unfold inj_def) 260apply (rule CollectI) 261apply (rule lam_type) 262apply (erule OUN_E) 263apply (erule Least_in_Ord) 264apply (erule ltD) 265apply (erule lt_Ord2) 266apply (intro ballI) 267apply (simp (no_asm_simp)) 268apply (rule impI) 269apply (drule Least_eq_imp_ex, assumption+) 270apply (fast elim!: two_in_lepoll_1) 271done 272 273 274lemma recfunAC16_lepoll_index: "Ord(y) ==> recfunAC16(f, h, y, a) \<lesssim> y" 275apply (erule trans_induct3) 276(*0 case*) 277apply (simp (no_asm_simp) add: recfunAC16_0 lepoll_refl) 278(*succ case*) 279apply (simp (no_asm_simp) add: recfunAC16_succ) 280apply (blast dest!: succI1 [THEN rev_bspec] 281 intro: subset_succI [THEN subset_imp_lepoll] Un_lepoll_succ 282 lepoll_trans) 283apply (simp (no_asm_simp) add: recfunAC16_Limit) 284apply (blast intro: lt_Ord [THEN recfunAC16_Diff_lepoll_1] UN_lepoll_index) 285done 286 287 288lemma Union_recfunAC16_lesspoll: 289 "[| recfunAC16(f,g,y,a) \<subseteq> {X \<in> Pow(A). X\<approx>n}; 290 A\<approx>a; y<a; ~Finite(a); Card(a); n \<in> nat |] 291 ==> \<Union>(recfunAC16(f,g,y,a))\<prec>a" 292apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE]) 293apply (rule_tac T=A in Union_lesspoll, simp_all) 294apply (blast intro!: eqpoll_imp_lepoll) 295apply (blast intro: bij_is_inj Card_is_Ord [THEN well_ord_Memrel] 296 well_ord_rvimage) 297apply (erule lt_Ord [THEN recfunAC16_lepoll_index]) 298done 299 300lemma dbl_Diff_eqpoll: 301 "[| recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)}; 302 Card(a); ~ Finite(a); A\<approx>a; 303 k \<in> nat; y<a; 304 h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)}) |] 305 ==> A - \<Union>(recfunAC16(f, h, y, a)) - h`y\<approx>a" 306apply (rule dbl_Diff_eqpoll_Card, simp_all) 307apply (simp add: Union_recfunAC16_lesspoll) 308apply (rule Finite_lesspoll_infinite_Ord) 309apply (rule Finite_def [THEN def_imp_iff, THEN iffD2]) 310apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption) 311apply (blast intro: Card_is_Ord) 312done 313 314(* back to the proof *) 315 316lemmas disj_Un_eqpoll_nat_sum = 317 eqpoll_trans [THEN eqpoll_trans, 318 OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum] 319 320 321lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m; 322 h \<in> bij(a, {x \<in> Pow(A) . x\<approx>k}); i<a; k \<in> nat; m \<in> nat |] 323 ==> h ` i \<union> x \<in> {x \<in> Pow(A) . x\<approx>k #+ m}" 324by (blast intro: disj_Un_eqpoll_nat_sum 325 dest: ltD bij_is_fun [THEN apply_type]) 326 327 328(* ********************************************************************** *) 329(* Lemmas simplifying assumptions *) 330(* ********************************************************************** *) 331 332lemma lemma6: 333 "[| \<forall>y<succ(j). F(y)<=X & (\<forall>x<a. x<y | P(x,y) \<longrightarrow> Q(x,y)); succ(j)<a |] 334 ==> F(j)<=X & (\<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j))" 335by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]) 336 337 338lemma lemma7: 339 "[| \<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j); succ(j)<a |] 340 ==> P(j,j) \<longrightarrow> (\<forall>x<a. x\<le>j | P(x,j) \<longrightarrow> Q(x,j))" 341by (fast elim!: leE) 342 343(* ********************************************************************** *) 344(* Lemmas needed to prove ex_next_set, which means that for any successor *) 345(* ordinal there is a set satisfying certain properties *) 346(* ********************************************************************** *) 347 348lemma ex_subset_eqpoll: 349 "[| A\<approx>a; ~ Finite(a); Ord(a); m \<in> nat |] ==> \<exists>X \<in> Pow(A). X\<approx>m" 350apply (rule lepoll_imp_eqpoll_subset [of m A, THEN exE]) 351 apply (rule lepoll_trans, rule leI [THEN le_imp_lepoll]) 352 apply (blast intro: lt_trans2 [OF ltI nat_le_infinite_Ord] Ord_nat) 353apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) 354apply (fast elim!: eqpoll_sym) 355done 356 357lemma subset_Un_disjoint: "[| A \<subseteq> B \<union> C; A \<inter> C = 0 |] ==> A \<subseteq> B" 358by blast 359 360 361lemma Int_empty: 362 "[| X \<in> Pow(A - \<Union>(B) -C); T \<in> B; F \<subseteq> T |] ==> F \<inter> X = 0" 363by blast 364 365 366(* ********************************************************************** *) 367(* equipollent subset (and finite) is the whole set *) 368(* ********************************************************************** *) 369 370 371lemma subset_imp_eq_lemma: 372 "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m \<lesssim> A & B \<lesssim> m \<longrightarrow> A=B" 373apply (induct_tac "m") 374apply (fast dest!: lepoll_0_is_0) 375apply (intro allI impI) 376apply (elim conjE) 377apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], assumption) 378apply (frule subsetD [THEN Diff_sing_lepoll], assumption+) 379apply (frule lepoll_Diff_sing) 380apply (erule allE impE)+ 381apply (rule conjI) 382prefer 2 apply fast 383apply fast 384apply (blast elim: equalityE) 385done 386 387 388lemma subset_imp_eq: "[| A \<subseteq> B; m \<lesssim> A; B \<lesssim> m; m \<in> nat |] ==> A=B" 389by (blast dest!: subset_imp_eq_lemma) 390 391 392lemma bij_imp_arg_eq: 393 "[| f \<in> bij(a, {Y \<in> X. Y\<approx>succ(k)}); k \<in> nat; f`b \<subseteq> f`y; b<a; y<a |] 394 ==> b=y" 395apply (drule subset_imp_eq) 396apply (erule_tac [3] nat_succI) 397apply (unfold bij_def inj_def) 398apply (blast intro: eqpoll_sym eqpoll_imp_lepoll 399 dest: ltD apply_type)+ 400done 401 402 403lemma ex_next_set: 404 "[| recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)}; 405 Card(a); ~ Finite(a); A\<approx>a; 406 k \<in> nat; m \<in> nat; y<a; 407 h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)}); 408 ~ (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y) |] 409 ==> \<exists>X \<in> {Y \<in> Pow(A). Y\<approx>succ(k #+ m)}. h`y \<subseteq> X & 410 (\<forall>b<a. h`b \<subseteq> X \<longrightarrow> 411 (\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))" 412apply (erule_tac m1=m in dbl_Diff_eqpoll [THEN ex_subset_eqpoll, THEN bexE], 413 assumption+) 414apply (erule Card_is_Ord, assumption) 415apply (frule Un_in_Collect, (erule asm_rl nat_succI)+) 416apply (erule CollectE) 417apply (rule rev_bexI, simp) 418apply (rule conjI, blast) 419apply (intro ballI impI oallI notI) 420apply (drule subset_Un_disjoint, rule Int_empty, assumption+) 421apply (blast dest: bij_imp_arg_eq) 422done 423 424(* ********************************************************************** *) 425(* Lemma ex_next_Ord states that for any successor *) 426(* ordinal there is a number of the set satisfying certain properties *) 427(* ********************************************************************** *) 428 429lemma ex_next_Ord: 430 "[| recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)}; 431 Card(a); ~ Finite(a); A\<approx>a; 432 k \<in> nat; m \<in> nat; y<a; 433 h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)}); 434 f \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k #+ m)}); 435 ~ (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y) |] 436 ==> \<exists>c<a. h`y \<subseteq> f`c & 437 (\<forall>b<a. h`b \<subseteq> f`c \<longrightarrow> 438 (\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))" 439apply (drule ex_next_set, assumption+) 440apply (erule bexE) 441apply (rule_tac x="converse(f)`X" in oexI) 442apply (simp add: right_inverse_bij) 443apply (blast intro: bij_converse_bij bij_is_fun [THEN apply_type] ltI 444 Card_is_Ord) 445done 446 447 448(* ********************************************************************** *) 449(* Lemma simplifying assumptions *) 450(* ********************************************************************** *) 451 452lemma lemma8: 453 "[| \<forall>x<a. x<j | (\<exists>xa \<in> F(j). P(x, xa)) 454 \<longrightarrow> (\<exists>! Y. Y \<in> F(j) & P(x, Y)); F(j) \<subseteq> X; 455 L \<in> X; P(j, L) & (\<forall>x<a. P(x, L) \<longrightarrow> (\<forall>xa \<in> F(j). ~P(x, xa))) |] 456 ==> F(j) \<union> {L} \<subseteq> X & 457 (\<forall>x<a. x\<le>j | (\<exists>xa \<in> (F(j) \<union> {L}). P(x, xa)) \<longrightarrow> 458 (\<exists>! Y. Y \<in> (F(j) \<union> {L}) & P(x, Y)))" 459apply (rule conjI) 460apply (fast intro!: singleton_subsetI) 461apply (rule oallI) 462apply (blast elim!: leE oallE) 463done 464 465(* ********************************************************************** *) 466(* The main part of the proof: inductive proof of the property of T_gamma *) 467(* lemma main_induct *) 468(* ********************************************************************** *) 469 470lemma main_induct: 471 "[| b < a; f \<in> bij(a, {Y \<in> Pow(A) . Y\<approx>succ(k #+ m)}); 472 h \<in> bij(a, {Y \<in> Pow(A) . Y\<approx>succ(k)}); 473 ~Finite(a); Card(a); A\<approx>a; k \<in> nat; m \<in> nat |] 474 ==> recfunAC16(f, h, b, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)} & 475 (\<forall>x<a. x < b | (\<exists>Y \<in> recfunAC16(f, h, b, a). h ` x \<subseteq> Y) \<longrightarrow> 476 (\<exists>! Y. Y \<in> recfunAC16(f, h, b, a) & h ` x \<subseteq> Y))" 477apply (erule lt_induct) 478apply (frule lt_Ord) 479apply (erule Ord_cases) 480(* case 0 *) 481apply (simp add: recfunAC16_0) 482(* case Limit *) 483prefer 2 apply (simp add: recfunAC16_Limit) 484 apply (rule lemma5, assumption+) 485 apply (blast dest!: recfunAC16_mono) 486(* case succ *) 487apply clarify 488apply (erule lemma6 [THEN conjE], assumption) 489apply (simp (no_asm_simp) split del: split_if add: recfunAC16_succ) 490apply (rule conjI [THEN split_if [THEN iffD2]]) 491 apply (simp, erule lemma7, assumption) 492apply (rule impI) 493apply (rule ex_next_Ord [THEN oexE], 494 assumption+, rule le_refl [THEN lt_trans], assumption+) 495apply (erule lemma8, assumption) 496 apply (rule bij_is_fun [THEN apply_type], assumption) 497 apply (erule Least_le [THEN lt_trans2, THEN ltD]) 498 apply (erule lt_Ord) 499 apply (erule succ_leI) 500apply (erule LeastI) 501apply (erule lt_Ord) 502done 503 504(* ********************************************************************** *) 505(* Lemma to simplify the inductive proof *) 506(* - the desired property is a consequence of the inductive assumption *) 507(* ********************************************************************** *) 508 509lemma lemma_simp_induct: 510 "[| \<forall>b. b<a \<longrightarrow> F(b) \<subseteq> S & (\<forall>x<a. (x<b | (\<exists>Y \<in> F(b). f`x \<subseteq> Y)) 511 \<longrightarrow> (\<exists>! Y. Y \<in> F(b) & f`x \<subseteq> Y)); 512 f \<in> a->f``(a); Limit(a); 513 \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j) |] 514 ==> (\<Union>j<a. F(j)) \<subseteq> S & 515 (\<forall>x \<in> f``a. \<exists>! Y. Y \<in> (\<Union>j<a. F(j)) & x \<subseteq> Y)" 516apply (rule conjI) 517apply (rule subsetI) 518apply (erule OUN_E, blast) 519apply (rule ballI) 520apply (erule imageE) 521apply (drule ltI, erule Limit_is_Ord) 522apply (drule Limit_has_succ, assumption) 523apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption) 524apply (erule conjE) 525apply (drule ospec) 526(** LEVEL 10 **) 527apply (erule leI [THEN succ_leE]) 528apply (erule impE) 529apply (fast elim!: leI [THEN succ_leE, THEN lt_Ord, THEN le_refl]) 530apply (drule apply_equality, assumption) 531apply (elim conjE ex1E) 532(** LEVEL 15 **) 533apply (rule ex1I, blast) 534apply (elim conjE OUN_E) 535apply (erule_tac i="succ(xa)" and j=aa 536 in Ord_linear_le [OF lt_Ord lt_Ord], assumption) 537prefer 2 538apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 539(** LEVEL 20 **) 540apply (drule_tac x1=aa in spec [THEN mp], assumption) 541apply (frule succ_leE) 542apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 543done 544 545(* ********************************************************************** *) 546(* The target theorem *) 547(* ********************************************************************** *) 548 549theorem WO2_AC16: "[| WO2; 0<m; k \<in> nat; m \<in> nat |] ==> AC16(k #+ m,k)" 550apply (unfold AC16_def) 551apply (rule allI) 552apply (rule impI) 553apply (frule WO2_infinite_subsets_eqpoll_X, assumption+) 554apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp, simp) 555apply (frule WO2_imp_ex_Card) 556apply (elim exE conjE) 557apply (drule eqpoll_trans [THEN eqpoll_sym, 558 THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]], 559 assumption) 560apply (drule eqpoll_trans [THEN eqpoll_sym, 561 THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]], 562 assumption+) 563apply (elim exE) 564apply (rename_tac h) 565apply (rule_tac x = "\<Union>j<a. recfunAC16 (h,f,j,a) " in exI) 566apply (rule_tac P="%z. Y & (\<forall>x \<in> z. Z(x))" for Y Z 567 in bij_is_surj [THEN surj_image_eq, THEN subst], assumption) 568apply (rule lemma_simp_induct) 569apply (blast del: conjI notI 570 intro!: main_induct eqpoll_imp_lepoll [THEN lepoll_infinite] ) 571apply (blast intro: bij_is_fun [THEN surj_image, THEN surj_is_fun]) 572apply (erule eqpoll_imp_lepoll [THEN lepoll_infinite, 573 THEN infinite_Card_is_InfCard, 574 THEN InfCard_is_Limit], 575 assumption+) 576apply (blast dest!: recfunAC16_mono) 577done 578 579end 580