1(* Title: ZF/AC/DC.thy 2 Author: Krzysztof Grabczewski 3 4The proofs concerning the Axiom of Dependent Choice. 5*) 6 7theory DC 8imports AC_Equiv Hartog Cardinal_aux 9begin 10 11lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a" 12apply (unfold lepoll_def) 13apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . \<mu> i. z=P (i) " in exI) 14apply (rule_tac d="%z. P (z)" in lam_injective) 15 apply (fast intro!: Least_in_Ord) 16apply (rule sym) 17apply (fast intro: LeastI Ord_in_Ord) 18done 19 20text\<open>Trivial in the presence of AC, but here we need a wellordering of X\<close> 21lemma image_Ord_lepoll: "[| f \<in> X->Y; Ord(X) |] ==> f``X \<lesssim> X" 22apply (unfold lepoll_def) 23apply (rule_tac x = "\<lambda>x \<in> f``X. \<mu> y. f`y = x" in exI) 24apply (rule_tac d = "%z. f`z" in lam_injective) 25apply (fast intro!: Least_in_Ord apply_equality, clarify) 26apply (rule LeastI) 27 apply (erule apply_equality, assumption+) 28apply (blast intro: Ord_in_Ord) 29done 30 31lemma range_subset_domain: 32 "[| R \<subseteq> X*X; !!g. g \<in> X ==> \<exists>u. <g,u> \<in> R |] 33 ==> range(R) \<subseteq> domain(R)" 34by blast 35 36lemma cons_fun_type: "g \<in> n->X ==> cons(<n,x>, g) \<in> succ(n) -> cons(x, X)" 37apply (unfold succ_def) 38apply (fast intro!: fun_extend elim!: mem_irrefl) 39done 40 41lemma cons_fun_type2: 42 "[| g \<in> n->X; x \<in> X |] ==> cons(<n,x>, g) \<in> succ(n) -> X" 43by (erule cons_absorb [THEN subst], erule cons_fun_type) 44 45lemma cons_image_n: "n \<in> nat ==> cons(<n,x>, g)``n = g``n" 46by (fast elim!: mem_irrefl) 47 48lemma cons_val_n: "g \<in> n->X ==> cons(<n,x>, g)`n = x" 49by (fast intro!: apply_equality elim!: cons_fun_type) 50 51lemma cons_image_k: "k \<in> n ==> cons(<n,x>, g)``k = g``k" 52by (fast elim: mem_asym) 53 54lemma cons_val_k: "[| k \<in> n; g \<in> n->X |] ==> cons(<n,x>, g)`k = g`k" 55by (fast intro!: apply_equality consI2 elim!: cons_fun_type apply_Pair) 56 57lemma domain_cons_eq_succ: "domain(f)=x ==> domain(cons(<x,y>, f)) = succ(x)" 58by (simp add: domain_cons succ_def) 59 60lemma restrict_cons_eq: "g \<in> n->X ==> restrict(cons(<n,x>, g), n) = g" 61apply (simp add: restrict_def Pi_iff) 62apply (blast intro: elim: mem_irrefl) 63done 64 65lemma succ_in_succ: "[| Ord(k); i \<in> k |] ==> succ(i) \<in> succ(k)" 66apply (rule Ord_linear [of "succ(i)" "succ(k)", THEN disjE]) 67apply (fast elim: Ord_in_Ord mem_irrefl mem_asym)+ 68done 69 70lemma restrict_eq_imp_val_eq: 71 "[|restrict(f, domain(g)) = g; x \<in> domain(g)|] 72 ==> f`x = g`x" 73by (erule subst, simp add: restrict) 74 75lemma domain_eq_imp_fun_type: "[| domain(f)=A; f \<in> B->C |] ==> f \<in> A->C" 76by (frule domain_of_fun, fast) 77 78lemma ex_in_domain: "[| R \<subseteq> A * B; R \<noteq> 0 |] ==> \<exists>x. x \<in> domain(R)" 79by (fast elim!: not_emptyE) 80 81 82definition 83 DC :: "i => o" where 84 "DC(a) == \<forall>X R. R \<subseteq> Pow(X)*X & 85 (\<forall>Y \<in> Pow(X). Y \<prec> a \<longrightarrow> (\<exists>x \<in> X. <Y,x> \<in> R)) 86 \<longrightarrow> (\<exists>f \<in> a->X. \<forall>b<a. <f``b,f`b> \<in> R)" 87 88definition 89 DC0 :: o where 90 "DC0 == \<forall>A B R. R \<subseteq> A*B & R\<noteq>0 & range(R) \<subseteq> domain(R) 91 \<longrightarrow> (\<exists>f \<in> nat->domain(R). \<forall>n \<in> nat. <f`n,f`succ(n)>:R)" 92 93definition 94 ff :: "[i, i, i, i] => i" where 95 "ff(b, X, Q, R) == 96 transrec(b, %c r. THE x. first(x, {x \<in> X. <r``c, x> \<in> R}, Q))" 97 98 99locale DC0_imp = 100 fixes XX and RR and X and R 101 102 assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R)" 103 104 defines XX_def: "XX == (\<Union>n \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R})" 105 and RR_def: "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1)) 106 & restrict(z2, domain(z1)) = z1}" 107begin 108 109(* ********************************************************************** *) 110(* DC ==> DC(omega) *) 111(* *) 112(* The scheme of the proof: *) 113(* *) 114(* Assume DC. Let R and X satisfy the premise of DC(omega). *) 115(* *) 116(* Define XX and RR as follows: *) 117(* *) 118(* XX = (\<Union>n \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R}) *) 119(* f RR g iff domain(g)=succ(domain(f)) & *) 120(* restrict(g, domain(f)) = f *) 121(* *) 122(* Then RR satisfies the hypotheses of DC. *) 123(* So applying DC: *) 124(* *) 125(* \<exists>f \<in> nat->XX. \<forall>n \<in> nat. f`n RR f`succ(n) *) 126(* *) 127(* Thence *) 128(* *) 129(* ff = {<n, f`succ(n)`n>. n \<in> nat} *) 130(* *) 131(* is the desired function. *) 132(* *) 133(* ********************************************************************** *) 134 135lemma lemma1_1: "RR \<subseteq> XX*XX" 136by (unfold RR_def, fast) 137 138lemma lemma1_2: "RR \<noteq> 0" 139apply (unfold RR_def XX_def) 140apply (rule all_ex [THEN ballE]) 141apply (erule_tac [2] notE [OF _ empty_subsetI [THEN PowI]]) 142apply (erule_tac impE [OF _ nat_0I [THEN n_lesspoll_nat]]) 143apply (erule bexE) 144apply (rule_tac a = "<0, {<0, x>}>" in not_emptyI) 145apply (rule CollectI) 146apply (rule SigmaI) 147apply (rule nat_0I [THEN UN_I]) 148apply (simp (no_asm_simp) add: nat_0I [THEN UN_I]) 149apply (rule nat_1I [THEN UN_I]) 150apply (force intro!: singleton_fun [THEN Pi_type] 151 simp add: singleton_0 [symmetric]) 152apply (simp add: singleton_0) 153done 154 155lemma lemma1_3: "range(RR) \<subseteq> domain(RR)" 156apply (unfold RR_def XX_def) 157apply (rule range_subset_domain, blast, clarify) 158apply (frule fun_is_rel [THEN image_subset, THEN PowI, 159 THEN all_ex [THEN bspec]]) 160apply (erule impE[OF _ lesspoll_trans1[OF image_Ord_lepoll 161 [OF _ nat_into_Ord] n_lesspoll_nat]], 162 assumption+) 163apply (erule bexE) 164apply (rule_tac x = "cons (<n,x>, g) " in exI) 165apply (rule CollectI) 166apply (force elim!: cons_fun_type2 167 simp add: cons_image_n cons_val_n cons_image_k cons_val_k) 168apply (simp add: domain_of_fun succ_def restrict_cons_eq) 169done 170 171lemma lemma2: 172 "[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR; f \<in> nat -> XX; n \<in> nat |] 173 ==> \<exists>k \<in> nat. f`succ(n) \<in> k -> X & n \<in> k 174 & <f`succ(n)``n, f`succ(n)`n> \<in> R" 175apply (induct_tac "n") 176apply (drule apply_type [OF _ nat_1I]) 177apply (drule bspec [OF _ nat_0I]) 178apply (simp add: XX_def, safe) 179apply (rule rev_bexI, assumption) 180apply (subgoal_tac "0 \<in> y", force) 181apply (force simp add: RR_def 182 intro: ltD elim!: nat_0_le [THEN leE]) 183(** LEVEL 7, other subgoal **) 184apply (drule bspec [OF _ nat_succI], assumption) 185apply (subgoal_tac "f ` succ (succ (x)) \<in> succ (k) ->X") 186apply (drule apply_type [OF _ nat_succI [THEN nat_succI]], assumption) 187apply (simp (no_asm_use) add: XX_def RR_def) 188apply safe 189apply (frule_tac a="succ(k)" in domain_of_fun [symmetric, THEN trans], 190 assumption) 191apply (frule_tac a=y in domain_of_fun [symmetric, THEN trans], 192 assumption) 193apply (fast elim!: nat_into_Ord [THEN succ_in_succ] 194 dest!: bspec [OF _ nat_into_Ord [THEN succ_in_succ]]) 195apply (drule domain_of_fun) 196apply (simp add: XX_def RR_def, clarify) 197apply (blast dest: domain_of_fun [symmetric, THEN trans] ) 198done 199 200lemma lemma3_1: 201 "[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR; f \<in> nat -> XX; m \<in> nat |] 202 ==> {f`succ(x)`x. x \<in> m} = {f`succ(m)`x. x \<in> m}" 203apply (subgoal_tac "\<forall>x \<in> m. f`succ (m) `x = f`succ (x) `x") 204apply simp 205apply (induct_tac "m", blast) 206apply (rule ballI) 207apply (erule succE) 208 apply (rule restrict_eq_imp_val_eq) 209 apply (drule bspec [OF _ nat_succI], assumption) 210 apply (simp add: RR_def) 211 apply (drule lemma2, assumption+) 212 apply (fast dest!: domain_of_fun) 213apply (drule_tac x = xa in bspec, assumption) 214apply (erule sym [THEN trans, symmetric]) 215apply (rule restrict_eq_imp_val_eq [symmetric]) 216 apply (drule bspec [OF _ nat_succI], assumption) 217 apply (simp add: RR_def) 218apply (drule lemma2, assumption+) 219apply (blast dest!: domain_of_fun 220 intro: nat_into_Ord OrdmemD [THEN subsetD]) 221done 222 223lemma lemma3: 224 "[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR; f \<in> nat -> XX; m \<in> nat |] 225 ==> (\<lambda>x \<in> nat. f`succ(x)`x) `` m = f`succ(m)``m" 226apply (erule natE, simp) 227apply (subst image_lam) 228 apply (fast elim!: OrdmemD [OF nat_succI Ord_nat]) 229apply (subst lemma3_1, assumption+) 230 apply fast 231apply (fast dest!: lemma2 232 elim!: image_fun [symmetric, OF _ OrdmemD [OF _ nat_into_Ord]]) 233done 234 235end 236 237theorem DC0_imp_DC_nat: "DC0 ==> DC(nat)" 238apply (unfold DC_def DC0_def, clarify) 239apply (elim allE) 240apply (erule impE) 241 (*these three results comprise Lemma 1*) 242apply (blast intro!: DC0_imp.lemma1_1 [OF DC0_imp.intro] DC0_imp.lemma1_2 [OF DC0_imp.intro] DC0_imp.lemma1_3 [OF DC0_imp.intro]) 243apply (erule bexE) 244apply (rule_tac x = "\<lambda>n \<in> nat. f`succ (n) `n" in rev_bexI) 245 apply (rule lam_type, blast dest!: DC0_imp.lemma2 [OF DC0_imp.intro] intro: fun_weaken_type) 246apply (rule oallI) 247apply (frule DC0_imp.lemma2 [OF DC0_imp.intro], assumption) 248 apply (blast intro: fun_weaken_type) 249 apply (erule ltD) 250(** LEVEL 11: last subgoal **) 251apply (subst DC0_imp.lemma3 [OF DC0_imp.intro], assumption+) 252 apply (fast elim!: fun_weaken_type) 253 apply (erule ltD) 254apply (force simp add: lt_def) 255done 256 257 258(* ************************************************************************ 259 DC(omega) ==> DC 260 261 The scheme of the proof: 262 263 Assume DC(omega). Let R and x satisfy the premise of DC. 264 265 Define XX and RR as follows: 266 267 XX = (\<Union>n \<in> nat. {f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R}) 268 269 RR = {<z1,z2>:Fin(XX)*XX. 270 (domain(z2)=succ(\<Union>f \<in> z1. domain(f)) & 271 (\<forall>f \<in> z1. restrict(z2, domain(f)) = f)) | 272 (~ (\<exists>g \<in> XX. domain(g)=succ(\<Union>f \<in> z1. domain(f)) & 273 (\<forall>f \<in> z1. restrict(g, domain(f)) = f)) & 274 z2={<0,x>})} 275 276 Then XX and RR satisfy the hypotheses of DC(omega). 277 So applying DC: 278 279 \<exists>f \<in> nat->XX. \<forall>n \<in> nat. f``n RR f`n 280 281 Thence 282 283 ff = {<n, f`n`n>. n \<in> nat} 284 285 is the desired function. 286 287************************************************************************* *) 288 289lemma singleton_in_funs: 290 "x \<in> X ==> {<0,x>} \<in> 291 (\<Union>n \<in> nat. {f \<in> succ(n)->X. \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})" 292apply (rule nat_0I [THEN UN_I]) 293apply (force simp add: singleton_0 [symmetric] 294 intro!: singleton_fun [THEN Pi_type]) 295done 296 297 298locale imp_DC0 = 299 fixes XX and RR and x and R and f and allRR 300 defines XX_def: "XX == (\<Union>n \<in> nat. 301 {f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})" 302 and RR_def: 303 "RR == {<z1,z2>:Fin(XX)*XX. 304 (domain(z2)=succ(\<Union>f \<in> z1. domain(f)) 305 & (\<forall>f \<in> z1. restrict(z2, domain(f)) = f)) 306 | (~ (\<exists>g \<in> XX. domain(g)=succ(\<Union>f \<in> z1. domain(f)) 307 & (\<forall>f \<in> z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}" 308 and allRR_def: 309 "allRR == \<forall>b<nat. 310 <f``b, f`b> \<in> 311 {<z1,z2>\<in>Fin(XX)*XX. (domain(z2)=succ(\<Union>f \<in> z1. domain(f)) 312 & (\<Union>f \<in> z1. domain(f)) = b 313 & (\<forall>f \<in> z1. restrict(z2,domain(f)) = f))}" 314begin 315 316lemma lemma4: 317 "[| range(R) \<subseteq> domain(R); x \<in> domain(R) |] 318 ==> RR \<subseteq> Pow(XX)*XX & 319 (\<forall>Y \<in> Pow(XX). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> XX. <Y,x>:RR))" 320apply (rule conjI) 321apply (force dest!: FinD [THEN PowI] simp add: RR_def) 322apply (rule impI [THEN ballI]) 323apply (drule Finite_Fin [OF lesspoll_nat_is_Finite PowD], assumption) 324apply (case_tac 325 "\<exists>g \<in> XX. domain (g) = 326 succ(\<Union>f \<in> Y. domain(f)) & (\<forall>f\<in>Y. restrict(g, domain(f)) = f)") 327apply (simp add: RR_def, blast) 328apply (safe del: domainE) 329apply (unfold XX_def RR_def) 330apply (rule rev_bexI, erule singleton_in_funs) 331apply (simp add: nat_0I [THEN rev_bexI] cons_fun_type2) 332done 333 334lemma UN_image_succ_eq: 335 "[| f \<in> nat->X; n \<in> nat |] 336 ==> (\<Union>x \<in> f``succ(n). P(x)) = P(f`n) \<union> (\<Union>x \<in> f``n. P(x))" 337by (simp add: image_fun OrdmemD) 338 339lemma UN_image_succ_eq_succ: 340 "[| (\<Union>x \<in> f``n. P(x)) = y; P(f`n) = succ(y); 341 f \<in> nat -> X; n \<in> nat |] ==> (\<Union>x \<in> f``succ(n). P(x)) = succ(y)" 342by (simp add: UN_image_succ_eq, blast) 343 344lemma apply_domain_type: 345 "[| h \<in> succ(n) -> D; n \<in> nat; domain(h)=succ(y) |] ==> h`y \<in> D" 346by (fast elim: apply_type dest!: trans [OF sym domain_of_fun]) 347 348lemma image_fun_succ: 349 "[| h \<in> nat -> X; n \<in> nat |] ==> h``succ(n) = cons(h`n, h``n)" 350by (simp add: image_fun OrdmemD) 351 352lemma f_n_type: 353 "[| domain(f`n) = succ(k); f \<in> nat -> XX; n \<in> nat |] 354 ==> f`n \<in> succ(k) -> domain(R)" 355apply (unfold XX_def) 356apply (drule apply_type, assumption) 357apply (fast elim: domain_eq_imp_fun_type) 358done 359 360lemma f_n_pairs_in_R [rule_format]: 361 "[| h \<in> nat -> XX; domain(h`n) = succ(k); n \<in> nat |] 362 ==> \<forall>i \<in> k. <h`n`i, h`n`succ(i)> \<in> R" 363apply (unfold XX_def) 364apply (drule apply_type, assumption) 365apply (elim UN_E CollectE) 366apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp) 367done 368 369lemma restrict_cons_eq_restrict: 370 "[| restrict(h, domain(u))=u; h \<in> n->X; domain(u) \<subseteq> n |] 371 ==> restrict(cons(<n, y>, h), domain(u)) = u" 372apply (unfold restrict_def) 373apply (simp add: restrict_def Pi_iff) 374apply (erule sym [THEN trans, symmetric]) 375apply (blast elim: mem_irrefl) 376done 377 378lemma all_in_image_restrict_eq: 379 "[| \<forall>x \<in> f``n. restrict(f`n, domain(x))=x; 380 f \<in> nat -> XX; 381 n \<in> nat; domain(f`n) = succ(n); 382 (\<Union>x \<in> f``n. domain(x)) \<subseteq> n |] 383 ==> \<forall>x \<in> f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x)) = x" 384apply (rule ballI) 385apply (simp add: image_fun_succ) 386apply (drule f_n_type, assumption+) 387apply (erule disjE) 388 apply (simp add: domain_of_fun restrict_cons_eq) 389apply (blast intro!: restrict_cons_eq_restrict) 390done 391 392lemma simplify_recursion: 393 "[| \<forall>b<nat. <f``b, f`b> \<in> RR; 394 f \<in> nat -> XX; range(R) \<subseteq> domain(R); x \<in> domain(R)|] 395 ==> allRR" 396apply (unfold RR_def allRR_def) 397apply (rule oallI, drule ltD) 398apply (erule nat_induct) 399apply (drule_tac x=0 in ospec, blast intro: Limit_has_0) 400apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs) 401(*induction step*) (** LEVEL 5 **) 402(*prevent simplification of ~\<exists> to \<forall>~ *) 403apply (simp only: separation split) 404apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI) 405apply (elim conjE disjE) 406apply (force elim!: trans subst_context 407 intro!: UN_image_succ_eq_succ) 408apply (erule notE) 409apply (simp add: XX_def UN_image_succ_eq_succ) 410apply (elim conjE bexE) 411apply (drule apply_domain_type, assumption+) 412apply (erule domainE)+ 413apply (frule f_n_type) 414apply (simp add: XX_def, assumption+) 415apply (rule rev_bexI, erule nat_succI) 416apply (rename_tac m i j y z) 417apply (rule_tac x = "cons(<succ(m), z>, f`m)" in bexI) 418prefer 2 apply (blast intro: cons_fun_type2) 419apply (rule conjI) 420prefer 2 apply (fast del: ballI subsetI 421 elim: trans [OF _ subst_context, THEN domain_cons_eq_succ] 422 subst_context 423 all_in_image_restrict_eq [simplified XX_def] 424 trans equalityD1) 425(*one remaining subgoal*) 426apply (rule ballI) 427apply (erule succE) 428(** LEVEL 25 **) 429 apply (simp add: cons_val_n cons_val_k) 430(*assumption+ will not perform the required backtracking!*) 431apply (drule f_n_pairs_in_R [simplified XX_def, OF _ domain_of_fun], 432 assumption, assumption, assumption) 433apply (simp add: nat_into_Ord [THEN succ_in_succ] succI2 cons_val_k) 434done 435 436 437lemma lemma2: 438 "[| allRR; f \<in> nat->XX; range(R) \<subseteq> domain(R); x \<in> domain(R); n \<in> nat |] 439 ==> f`n \<in> succ(n) -> domain(R) & (\<forall>i \<in> n. <f`n`i, f`n`succ(i)>:R)" 440apply (unfold allRR_def) 441apply (drule ospec) 442apply (erule ltI [OF _ Ord_nat]) 443apply (erule CollectE, simp) 444apply (rule conjI) 445prefer 2 apply (fast elim!: f_n_pairs_in_R trans subst_context) 446apply (unfold XX_def) 447apply (fast elim!: trans [THEN domain_eq_imp_fun_type] subst_context) 448done 449 450lemma lemma3: 451 "[| allRR; f \<in> nat->XX; n\<in>nat; range(R) \<subseteq> domain(R); x \<in> domain(R) |] 452 ==> f`n`n = f`succ(n)`n" 453apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+) 454apply (unfold allRR_def) 455apply (drule ospec) 456apply (drule ltI [OF nat_succI Ord_nat], assumption, simp) 457apply (elim conjE ballE) 458apply (erule restrict_eq_imp_val_eq [symmetric], force) 459apply (simp add: image_fun OrdmemD) 460done 461 462end 463 464 465theorem DC_nat_imp_DC0: "DC(nat) ==> DC0" 466apply (unfold DC_def DC0_def) 467apply (intro allI impI) 468apply (erule asm_rl conjE ex_in_domain [THEN exE] allE)+ 469apply (erule impE [OF _ imp_DC0.lemma4], assumption+) 470apply (erule bexE) 471apply (drule imp_DC0.simplify_recursion, assumption+) 472apply (rule_tac x = "\<lambda>n \<in> nat. f`n`n" in bexI) 473apply (rule_tac [2] lam_type) 474apply (erule_tac [2] apply_type [OF imp_DC0.lemma2 [THEN conjunct1] succI1]) 475apply (rule ballI) 476apply (frule_tac n="succ(n)" in imp_DC0.lemma2, 477 (assumption|erule nat_succI)+) 478apply (drule imp_DC0.lemma3, auto) 479done 480 481(* ********************************************************************** *) 482(* \<forall>K. Card(K) \<longrightarrow> DC(K) ==> WO3 *) 483(* ********************************************************************** *) 484 485lemma fun_Ord_inj: 486 "[| f \<in> a->X; Ord(a); 487 !!b c. [| b<c; c \<in> a |] ==> f`b\<noteq>f`c |] 488 ==> f \<in> inj(a, X)" 489apply (unfold inj_def, simp) 490apply (intro ballI impI) 491apply (rule_tac j=x in Ord_in_Ord [THEN Ord_linear_lt], assumption+) 492apply (blast intro: Ord_in_Ord, auto) 493apply (atomize, blast dest: not_sym) 494done 495 496lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A" 497by (fast elim!: image_fun [THEN ssubst]) 498 499lemma lesspoll_lemma: "[| ~ A \<prec> B; C \<prec> B |] ==> A - C \<noteq> 0" 500apply (unfold lesspoll_def) 501apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll] 502 intro!: eqpollI elim: notE 503 elim!: eqpollE lepoll_trans) 504done 505 506theorem DC_WO3: "(\<forall>K. Card(K) \<longrightarrow> DC(K)) ==> WO3" 507apply (unfold DC_def WO3_def) 508apply (rule allI) 509apply (case_tac "A \<prec> Hartog (A)") 510apply (fast dest!: lesspoll_imp_ex_lt_eqpoll 511 intro!: Ord_Hartog leI [THEN le_imp_subset]) 512apply (erule allE impE)+ 513apply (rule Card_Hartog) 514apply (erule_tac x = A in allE) 515apply (erule_tac x = "{<z1,z2> \<in> Pow (A) *A . z1 \<prec> Hartog (A) & z2 \<notin> z1}" 516 in allE) 517apply simp 518apply (erule impE, fast elim: lesspoll_lemma [THEN not_emptyE]) 519apply (erule bexE) 520apply (rule Hartog_lepoll_selfE) 521apply (rule lepoll_def [THEN def_imp_iff, THEN iffD2]) 522apply (rule exI, rule fun_Ord_inj, assumption, rule Ord_Hartog) 523apply (drule value_in_image) 524apply (drule OrdmemD, rule Ord_Hartog, assumption+, erule ltD) 525apply (drule ospec) 526apply (blast intro: ltI Ord_Hartog, force) 527done 528 529(* ********************************************************************** *) 530(* WO1 ==> \<forall>K. Card(K) \<longrightarrow> DC(K) *) 531(* ********************************************************************** *) 532 533lemma images_eq: 534 "[| \<forall>x \<in> A. f`x=g`x; f \<in> Df->Cf; g \<in> Dg->Cg; A \<subseteq> Df; A \<subseteq> Dg |] 535 ==> f``A = g``A" 536apply (simp (no_asm_simp) add: image_fun) 537done 538 539lemma lam_images_eq: 540 "[| Ord(a); b \<in> a |] ==> (\<lambda>x \<in> a. h(x))``b = (\<lambda>x \<in> b. h(x))``b" 541apply (rule images_eq) 542 apply (rule ballI) 543 apply (drule OrdmemD [THEN subsetD], assumption+) 544 apply simp 545 apply (fast elim!: RepFunI OrdmemD intro!: lam_type)+ 546done 547 548lemma lam_type_RepFun: "(\<lambda>b \<in> a. h(b)) \<in> a -> {h(b). b \<in> a}" 549by (fast intro!: lam_type RepFunI) 550 551lemma lemmaX: 552 "[| \<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R); 553 b \<in> K; Z \<in> Pow(X); Z \<prec> K |] 554 ==> {x \<in> X. <Z,x> \<in> R} \<noteq> 0" 555by blast 556 557 558lemma WO1_DC_lemma: 559 "[| Card(K); well_ord(X,Q); 560 \<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R); b \<in> K |] 561 ==> ff(b, X, Q, R) \<in> {x \<in> X. <(\<lambda>c \<in> b. ff(c, X, Q, R))``b, x> \<in> R}" 562apply (rule_tac P = "b \<in> K" in impE, (erule_tac [2] asm_rl)+) 563apply (rule_tac i=b in Card_is_Ord [THEN Ord_in_Ord, THEN trans_induct], 564 assumption+) 565apply (rule impI) 566apply (rule ff_def [THEN def_transrec, THEN ssubst]) 567apply (erule the_first_in, fast) 568apply (simp add: image_fun [OF lam_type_RepFun subset_refl]) 569apply (erule lemmaX, assumption) 570 apply (blast intro: Card_is_Ord OrdmemD [THEN subsetD]) 571apply (blast intro: lesspoll_trans1 in_Card_imp_lesspoll RepFun_lepoll) 572done 573 574theorem WO1_DC_Card: "WO1 ==> \<forall>K. Card(K) \<longrightarrow> DC(K)" 575apply (unfold DC_def WO1_def) 576apply (rule allI impI)+ 577apply (erule allE exE conjE)+ 578apply (rule_tac x = "\<lambda>b \<in> K. ff (b, X, Ra, R) " in bexI) 579 apply (simp add: lam_images_eq [OF Card_is_Ord ltD]) 580 apply (fast elim!: ltE WO1_DC_lemma [THEN CollectD2]) 581apply (rule_tac lam_type) 582apply (rule WO1_DC_lemma [THEN CollectD1], assumption+) 583done 584 585end 586