145 lemmas Ord_1 = Ord_0 [THEN Ord_succ] |
145 lemmas Ord_1 = Ord_0 [THEN Ord_succ] |
146 |
146 |
147 lemma Ord_succ_iff [iff]: "Ord(succ(i)) <-> Ord(i)" |
147 lemma Ord_succ_iff [iff]: "Ord(succ(i)) <-> Ord(i)" |
148 by (blast intro: Ord_succ dest!: Ord_succD) |
148 by (blast intro: Ord_succ dest!: Ord_succD) |
149 |
149 |
150 lemma Ord_Un [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Un j)" |
150 lemma Ord_Un [intro,simp,TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Un j)" |
151 apply (unfold Ord_def) |
151 apply (unfold Ord_def) |
152 apply (blast intro!: Transset_Un) |
152 apply (blast intro!: Transset_Un) |
153 done |
153 done |
154 |
154 |
155 lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Int j)" |
155 lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Int j)" |
453 |
453 |
454 lemma lt_subset_trans: "[| i <= j; j<k; Ord(i) |] ==> i<k" |
454 lemma lt_subset_trans: "[| i <= j; j<k; Ord(i) |] ==> i<k" |
455 apply (rule subset_imp_le [THEN lt_trans1]) |
455 apply (rule subset_imp_le [THEN lt_trans1]) |
456 apply (blast intro: elim: ltE) + |
456 apply (blast intro: elim: ltE) + |
457 done |
457 done |
|
458 |
|
459 lemma lt_imp_0_lt: "j<i ==> 0<i" |
|
460 by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord]) |
458 |
461 |
459 lemma succ_lt_iff: "succ(i) < j \<longleftrightarrow> i<j & succ(i) \<noteq> j" |
462 lemma succ_lt_iff: "succ(i) < j \<longleftrightarrow> i<j & succ(i) \<noteq> j" |
460 apply auto |
463 apply auto |
461 apply (blast intro: lt_trans le_refl dest: lt_Ord) |
464 apply (blast intro: lt_trans le_refl dest: lt_Ord) |
462 apply (frule lt_Ord) |
465 apply (frule lt_Ord) |
516 |
519 |
517 lemma le_Un_iff: |
520 lemma le_Un_iff: |
518 "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j"; |
521 "[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j"; |
519 by (simp add: succ_Un_distrib lt_Un_iff [symmetric]) |
522 by (simp add: succ_Un_distrib lt_Un_iff [symmetric]) |
520 |
523 |
|
524 lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i Un j" |
|
525 by (simp add: lt_Un_iff lt_Ord2) |
|
526 |
|
527 lemma Un_upper2_lt: "[|k < j; Ord(i)|] ==> k < i Un j" |
|
528 by (simp add: lt_Un_iff lt_Ord2) |
|
529 |
|
530 (*See also Transset_iff_Union_succ*) |
|
531 lemma Ord_Union_succ_eq: "Ord(i) ==> \<Union>(succ(i)) = i" |
|
532 by (blast intro: Ord_trans) |
|
533 |
521 |
534 |
522 (*FIXME: the Intersection duals are missing!*) |
535 (*FIXME: the Intersection duals are missing!*) |
523 |
536 |
524 (*** Results about limits ***) |
537 (*** Results about limits ***) |
525 |
538 |
526 lemma Ord_Union: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))" |
539 lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))" |
527 apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) |
540 apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) |
528 apply (blast intro: Ord_contains_Transset)+ |
541 apply (blast intro: Ord_contains_Transset)+ |
529 done |
542 done |
530 |
543 |
531 lemma Ord_UN: "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))" |
544 lemma Ord_UN [intro,simp,TC]: |
|
545 "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))" |
532 by (rule Ord_Union, blast) |
546 by (rule Ord_Union, blast) |
533 |
547 |
534 (* No < version; consider (UN i:nat.i)=nat *) |
548 (* No < version; consider (UN i:nat.i)=nat *) |
535 lemma UN_least_le: |
549 lemma UN_least_le: |
536 "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i" |
550 "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i" |
543 apply (rule ltE, assumption) |
557 apply (rule ltE, assumption) |
544 apply (rule UN_least_le [THEN lt_trans2]) |
558 apply (rule UN_least_le [THEN lt_trans2]) |
545 apply (blast intro: succ_leI)+ |
559 apply (blast intro: succ_leI)+ |
546 done |
560 done |
547 |
561 |
|
562 lemma UN_upper_lt: |
|
563 "[| a\<in>A; i < b(a); Ord(\<Union>x\<in>A. b(x)) |] ==> i < (\<Union>x\<in>A. b(x))" |
|
564 by (unfold lt_def, blast) |
|
565 |
548 lemma UN_upper_le: |
566 lemma UN_upper_le: |
549 "[| a: A; i le b(a); Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))" |
567 "[| a: A; i le b(a); Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))" |
550 apply (frule ltD) |
568 apply (frule ltD) |
551 apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le]) |
569 apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le]) |
552 apply (blast intro: lt_Ord UN_upper)+ |
570 apply (blast intro: lt_Ord UN_upper)+ |
553 done |
571 done |
554 |
572 |
|
573 lemma lt_Union_iff: "\<forall>i\<in>A. Ord(i) ==> (j < \<Union>(A)) <-> (\<exists>i\<in>A. j<i)" |
|
574 by (auto simp: lt_def Ord_Union) |
|
575 |
|
576 lemma Union_upper_le: |
|
577 "[| j: J; i\<le>j; Ord(\<Union>(J)) |] ==> i \<le> \<Union>J" |
|
578 apply (subst Union_eq_UN) |
|
579 apply (rule UN_upper_le, auto) |
|
580 done |
|
581 |
555 lemma le_implies_UN_le_UN: |
582 lemma le_implies_UN_le_UN: |
556 "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))" |
583 "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))" |
557 apply (rule UN_least_le) |
584 apply (rule UN_least_le) |
558 apply (rule_tac [2] UN_upper_le) |
585 apply (rule_tac [2] UN_upper_le) |
559 apply (blast intro: Ord_UN le_Ord2)+ |
586 apply (blast intro: Ord_UN le_Ord2)+ |
584 apply (erule conjunct2 [THEN conjunct1]) |
611 apply (erule conjunct2 [THEN conjunct1]) |
585 done |
612 done |
586 |
613 |
587 lemma Limit_has_succ: "[| Limit(i); j<i |] ==> succ(j) < i" |
614 lemma Limit_has_succ: "[| Limit(i); j<i |] ==> succ(j) < i" |
588 by (unfold Limit_def, blast) |
615 by (unfold Limit_def, blast) |
|
616 |
|
617 lemma zero_not_Limit [iff]: "~ Limit(0)" |
|
618 by (simp add: Limit_def) |
|
619 |
|
620 lemma Limit_has_1: "Limit(i) ==> 1 < i" |
|
621 by (blast intro: Limit_has_0 Limit_has_succ) |
|
622 |
|
623 lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)" |
|
624 apply (simp add: Limit_def lt_Ord2, clarify) |
|
625 apply (drule_tac i=y in ltD) |
|
626 apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2) |
|
627 done |
589 |
628 |
590 lemma non_succ_LimitI: |
629 lemma non_succ_LimitI: |
591 "[| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)" |
630 "[| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)" |
592 apply (unfold Limit_def) |
631 apply (unfold Limit_def) |
593 apply (safe del: subsetI) |
632 apply (safe del: subsetI) |
605 lemma not_succ_Limit [simp]: "~ Limit(succ(i))" |
644 lemma not_succ_Limit [simp]: "~ Limit(succ(i))" |
606 by blast |
645 by blast |
607 |
646 |
608 lemma Limit_le_succD: "[| Limit(i); i le succ(j) |] ==> i le j" |
647 lemma Limit_le_succD: "[| Limit(i); i le succ(j) |] ==> i le j" |
609 by (blast elim!: leE) |
648 by (blast elim!: leE) |
|
649 |
610 |
650 |
611 (** Traditional 3-way case analysis on ordinals **) |
651 (** Traditional 3-way case analysis on ordinals **) |
612 |
652 |
613 lemma Ord_cases_disj: "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)" |
653 lemma Ord_cases_disj: "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)" |
614 by (blast intro!: non_succ_LimitI Ord_0_lt) |
654 by (blast intro!: non_succ_LimitI Ord_0_lt) |
627 !!x. [| Ord(x); P(x) |] ==> P(succ(x)); |
667 !!x. [| Ord(x); P(x) |] ==> P(succ(x)); |
628 !!x. [| Limit(x); ALL y:x. P(y) |] ==> P(x) |
668 !!x. [| Limit(x); ALL y:x. P(y) |] ==> P(x) |
629 |] ==> P(i)" |
669 |] ==> P(i)" |
630 apply (erule trans_induct) |
670 apply (erule trans_induct) |
631 apply (erule Ord_cases, blast+) |
671 apply (erule Ord_cases, blast+) |
|
672 done |
|
673 |
|
674 text{*A set of ordinals is either empty, contains its own union, or its |
|
675 union is a limit ordinal.*} |
|
676 lemma Ord_set_cases: |
|
677 "\<forall>i\<in>I. Ord(i) ==> I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))" |
|
678 apply (clarify elim!: not_emptyE) |
|
679 apply (cases "\<Union>(I)" rule: Ord_cases) |
|
680 apply (blast intro: Ord_Union) |
|
681 apply (blast intro: subst_elem) |
|
682 apply auto |
|
683 apply (clarify elim!: equalityE succ_subsetE) |
|
684 apply (simp add: Union_subset_iff) |
|
685 apply (subgoal_tac "B = succ(j)", blast) |
|
686 apply (rule le_anti_sym) |
|
687 apply (simp add: le_subset_iff) |
|
688 apply (simp add: ltI) |
|
689 done |
|
690 |
|
691 text{*If the union of a set of ordinals is a successor, then it is |
|
692 an element of that set.*} |
|
693 lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X" |
|
694 by (drule Ord_set_cases, auto) |
|
695 |
|
696 lemma Limit_Union [rule_format]: "[| I \<noteq> 0; \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)" |
|
697 apply (simp add: Limit_def lt_def) |
|
698 apply (blast intro!: equalityI) |
632 done |
699 done |
633 |
700 |
634 (*special induction rules for the "induct" method*) |
701 (*special induction rules for the "induct" method*) |
635 lemmas Ord_induct = Ord_induct [consumes 2] |
702 lemmas Ord_induct = Ord_induct [consumes 2] |
636 and Ord_induct_rule = Ord_induct [rule_format, consumes 2] |
703 and Ord_induct_rule = Ord_induct [rule_format, consumes 2] |