equal
deleted
inserted
replaced
361 "[| h \<in> nat -> XX; domain(h`n) = succ(k); n \<in> nat |] |
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" |
362 ==> \<forall>i \<in> k. <h`n`i, h`n`succ(i)> \<in> R" |
363 apply (unfold XX_def) |
363 apply (unfold XX_def) |
364 apply (drule apply_type, assumption) |
364 apply (drule apply_type, assumption) |
365 apply (elim UN_E CollectE) |
365 apply (elim UN_E CollectE) |
366 apply (drule domain_of_fun [symmetric, THEN trans], assumption) |
366 apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp) |
367 apply simp |
|
368 done |
367 done |
369 |
368 |
370 lemma (in imp_DC0) restrict_cons_eq_restrict: |
369 lemma (in imp_DC0) restrict_cons_eq_restrict: |
371 "[| restrict(h, domain(u))=u; h \<in> n->X; domain(u) \<subseteq> n |] |
370 "[| restrict(h, domain(u))=u; h \<in> n->X; domain(u) \<subseteq> n |] |
372 ==> restrict(cons(<n, y>, h), domain(u)) = u" |
371 ==> restrict(cons(<n, y>, h), domain(u)) = u" |
402 apply (drule_tac x="0" in ospec, blast intro: Limit_has_0) |
401 apply (drule_tac x="0" in ospec, blast intro: Limit_has_0) |
403 apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs) |
402 apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs) |
404 (*induction step*) (** LEVEL 5 **) |
403 (*induction step*) (** LEVEL 5 **) |
405 (*prevent simplification of ~\<exists> to \<forall>~ *) |
404 (*prevent simplification of ~\<exists> to \<forall>~ *) |
406 apply (simp only: separation split) |
405 apply (simp only: separation split) |
407 apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI); |
406 apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI) |
408 apply (elim conjE disjE) |
407 apply (elim conjE disjE) |
409 apply (force elim!: trans subst_context |
408 apply (force elim!: trans subst_context |
410 intro!: UN_image_succ_eq_succ) |
409 intro!: UN_image_succ_eq_succ) |
411 apply (erule notE) |
410 apply (erule notE) |
412 apply (simp add: XX_def UN_image_succ_eq_succ) |
411 apply (simp add: XX_def UN_image_succ_eq_succ) |
453 "[| allRR; f \<in> nat->XX; n\<in>nat; range(R) \<subseteq> domain(R); x \<in> domain(R) |] |
452 "[| allRR; f \<in> nat->XX; n\<in>nat; range(R) \<subseteq> domain(R); x \<in> domain(R) |] |
454 ==> f`n`n = f`succ(n)`n" |
453 ==> f`n`n = f`succ(n)`n" |
455 apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+) |
454 apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+) |
456 apply (unfold allRR_def) |
455 apply (unfold allRR_def) |
457 apply (drule ospec) |
456 apply (drule ospec) |
458 apply (drule ltI [OF nat_succI Ord_nat], assumption) |
457 apply (drule ltI [OF nat_succI Ord_nat], assumption, simp) |
459 apply simp |
|
460 apply (elim conjE ballE) |
458 apply (elim conjE ballE) |
461 apply (erule restrict_eq_imp_val_eq [symmetric], force) |
459 apply (erule restrict_eq_imp_val_eq [symmetric], force) |
462 apply (simp add: image_fun OrdmemD) |
460 apply (simp add: image_fun OrdmemD) |
463 done |
461 done |
464 |
462 |
498 by (fast elim!: image_fun [THEN ssubst]); |
496 by (fast elim!: image_fun [THEN ssubst]); |
499 |
497 |
500 theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3" |
498 theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3" |
501 apply (unfold DC_def WO3_def) |
499 apply (unfold DC_def WO3_def) |
502 apply (rule allI) |
500 apply (rule allI) |
503 apply (case_tac "A \<prec> Hartog (A)"); |
501 apply (case_tac "A \<prec> Hartog (A)") |
504 apply (fast dest!: lesspoll_imp_ex_lt_eqpoll |
502 apply (fast dest!: lesspoll_imp_ex_lt_eqpoll |
505 intro!: Ord_Hartog leI [THEN le_imp_subset]) |
503 intro!: Ord_Hartog leI [THEN le_imp_subset]) |
506 apply (erule allE impE)+ |
504 apply (erule allE impE)+ |
507 apply (rule Card_Hartog) |
505 apply (rule Card_Hartog) |
508 apply (erule_tac x = "A" in allE) |
506 apply (erule_tac x = "A" in allE) |