547 by (metis convergent_LIMSEQ_iff f) |
548 by (metis convergent_LIMSEQ_iff f) |
548 thus ?thesis |
549 thus ?thesis |
549 proof (simp add: LIMSEQ_iff) |
550 proof (simp add: LIMSEQ_iff) |
550 assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r" |
551 assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r" |
551 hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x" |
552 hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x" |
552 by (metis 0) |
553 by (metis 0) |
553 from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x" |
554 from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x" |
554 by blast |
555 by blast |
555 thus "lim f \<le> x" |
556 thus "lim f \<le> x" |
556 by (metis add_cancel_end add_minus_cancel diff_def linorder_linear |
557 by (metis add_cancel_end add_minus_cancel diff_def linorder_linear |
557 linorder_not_le minus_diff_eq abs_diff_less_iff fn_le) |
558 linorder_not_le minus_diff_eq abs_diff_less_iff fn_le) |
558 qed |
559 qed |
559 qed |
560 qed |
560 |
561 |
561 text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *} |
562 text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *} |
683 apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) |
684 apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) |
684 unfolding order_le_less by blast |
685 unfolding order_le_less by blast |
685 hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+ |
686 hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+ |
686 {fix n |
687 {fix n |
687 have "?P (f (Suc n)) (f n)" |
688 have "?P (f (Suc n)) (f n)" |
688 unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"] |
689 unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"] |
689 using H apply - |
690 using H apply - |
690 apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) |
691 apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) |
691 unfolding order_le_less by blast |
692 unfolding order_le_less by blast |
692 hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+} |
693 hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+} |
693 note fSuc = this |
694 note fSuc = this |
694 {fix p q assume pq: "p \<ge> f q" |
695 {fix p q assume pq: "p \<ge> f q" |
695 have "s p \<le> s(f(q))" using f0(2)[rule_format, of p] pq fSuc |
696 have "s p \<le> s(f(q))" using f0(2)[rule_format, of p] pq fSuc |
696 by (cases q, simp_all) } |
697 by (cases q, simp_all) } |
697 note pqth = this |
698 note pqth = this |
698 {fix q |
699 {fix q |
699 have "f (Suc q) > f q" apply (induct q) |
700 have "f (Suc q) > f q" apply (induct q) |
700 using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))} |
701 using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))} |
701 note fss = this |
702 note fss = this |
702 from fss have th1: "subseq f" unfolding subseq_Suc_iff .. |
703 from fss have th1: "subseq f" unfolding subseq_Suc_iff .. |
703 {fix a b |
704 {fix a b |
704 have "f a \<le> f (a + b)" |
705 have "f a \<le> f (a + b)" |
705 proof(induct b) |
706 proof(induct b) |
706 case 0 thus ?case by simp |
707 case 0 thus ?case by simp |
707 next |
708 next |
708 case (Suc b) |
709 case (Suc b) |
709 from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp |
710 from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp |
710 qed} |
711 qed} |
711 note fmon0 = this |
712 note fmon0 = this |
712 have "monoseq (\<lambda>n. s (f n))" |
713 have "monoseq (\<lambda>n. s (f n))" |
713 proof- |
714 proof- |
714 {fix n |
715 {fix n |
715 have "s (f n) \<ge> s (f (Suc n))" |
716 have "s (f n) \<ge> s (f (Suc n))" |
716 proof(cases n) |
717 proof(cases n) |
717 case 0 |
718 case 0 |
718 assume n0: "n = 0" |
719 assume n0: "n = 0" |
719 from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp |
720 from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp |
720 from f0(2)[rule_format, OF th0] show ?thesis using n0 by simp |
721 from f0(2)[rule_format, OF th0] show ?thesis using n0 by simp |
721 next |
722 next |
722 case (Suc m) |
723 case (Suc m) |
723 assume m: "n = Suc m" |
724 assume m: "n = Suc m" |
724 from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp |
725 from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp |
725 from m fSuc(2)[rule_format, OF th0] show ?thesis by simp |
726 from m fSuc(2)[rule_format, OF th0] show ?thesis by simp |
726 qed} |
727 qed} |
727 thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast |
728 thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast |
728 qed |
729 qed |
729 with th1 have ?thesis by blast} |
730 with th1 have ?thesis by blast} |
730 moreover |
731 moreover |
731 {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p" |
732 {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p" |
748 apply (rule ccontr, simp) |
749 apply (rule ccontr, simp) |
749 done |
750 done |
750 hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+ |
751 hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+ |
751 {fix n |
752 {fix n |
752 have "f n > N \<and> ?P (f (Suc n)) (f n)" |
753 have "f n > N \<and> ?P (f (Suc n)) (f n)" |
753 unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"] |
754 unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"] |
754 proof (induct n) |
755 proof (induct n) |
755 case 0 thus ?case |
756 case 0 thus ?case |
756 using f0 N apply auto |
757 using f0 N apply auto |
757 apply (erule allE[where x="f 0"], clarsimp) |
758 apply (erule allE[where x="f 0"], clarsimp) |
758 apply (rule_tac x="m" in exI, simp) |
759 apply (rule_tac x="m" in exI, simp) |
759 by (subgoal_tac "f 0 \<noteq> m", auto) |
760 by (subgoal_tac "f 0 \<noteq> m", auto) |
760 next |
761 next |
761 case (Suc n) |
762 case (Suc n) |
762 from Suc.hyps have Nfn: "N < f n" by blast |
763 from Suc.hyps have Nfn: "N < f n" by blast |
763 from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast |
764 from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast |
764 with Nfn have mN: "m > N" by arith |
765 with Nfn have mN: "m > N" by arith |
765 note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]] |
766 note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]] |
766 |
767 |
767 from key have th0: "f (Suc n) > N" by simp |
768 from key have th0: "f (Suc n) > N" by simp |
768 from N[rule_format, OF th0] |
769 from N[rule_format, OF th0] |
769 obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast |
770 obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast |
770 have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto |
771 have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto |
771 hence "m' > f (Suc n)" using m'(1) by simp |
772 hence "m' > f (Suc n)" using m'(1) by simp |
772 with key m'(2) show ?case by auto |
773 with key m'(2) show ?case by auto |
773 qed} |
774 qed} |
774 note fSuc = this |
775 note fSuc = this |
775 {fix n |
776 {fix n |
776 have "f n \<ge> Suc N \<and> f(Suc n) > f n \<and> s(f n) < s(f(Suc n))" using fSuc[of n] by auto |
777 have "f n \<ge> Suc N \<and> f(Suc n) > f n \<and> s(f n) < s(f(Suc n))" using fSuc[of n] by auto |
777 hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+} |
778 hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+} |