635 lemma Limit_has_0: "Limit(i) ==> 0 < i" |
635 lemma Limit_has_0: "Limit(i) ==> 0 < i" |
636 apply (unfold Limit_def) |
636 apply (unfold Limit_def) |
637 apply (erule conjunct2 [THEN conjunct1]) |
637 apply (erule conjunct2 [THEN conjunct1]) |
638 done |
638 done |
639 |
639 |
|
640 lemma Limit_nonzero: "Limit(i) ==> i ~= 0" |
|
641 by (drule Limit_has_0, blast) |
|
642 |
640 lemma Limit_has_succ: "[| Limit(i); j<i |] ==> succ(j) < i" |
643 lemma Limit_has_succ: "[| Limit(i); j<i |] ==> succ(j) < i" |
641 by (unfold Limit_def, blast) |
644 by (unfold Limit_def, blast) |
642 |
645 |
|
646 lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <-> (j<i)" |
|
647 apply (safe intro!: Limit_has_succ) |
|
648 apply (frule lt_Ord) |
|
649 apply (blast intro: lt_trans) |
|
650 done |
|
651 |
643 lemma zero_not_Limit [iff]: "~ Limit(0)" |
652 lemma zero_not_Limit [iff]: "~ Limit(0)" |
644 by (simp add: Limit_def) |
653 by (simp add: Limit_def) |
645 |
654 |
646 lemma Limit_has_1: "Limit(i) ==> 1 < i" |
655 lemma Limit_has_1: "Limit(i) ==> 1 < i" |
647 by (blast intro: Limit_has_0 Limit_has_succ) |
656 by (blast intro: Limit_has_0 Limit_has_succ) |
648 |
657 |
649 lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)" |
658 lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)" |
650 apply (simp add: Limit_def lt_Ord2, clarify) |
659 apply (unfold Limit_def, simp add: lt_Ord2, clarify) |
651 apply (drule_tac i=y in ltD) |
660 apply (drule_tac i=y in ltD) |
652 apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2) |
661 apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2) |
653 done |
662 done |
654 |
663 |
655 lemma non_succ_LimitI: |
664 lemma non_succ_LimitI: |