src/HOL/SEQ.thy
 changeset 32960 69916a850301 parent 32877 6f09346c7c08 child 33042 ddf1f03a9ad9
1.1 --- a/src/HOL/SEQ.thy	Sat Oct 17 01:05:59 2009 +0200
1.2 +++ b/src/HOL/SEQ.thy	Sat Oct 17 14:43:18 2009 +0200
1.3 @@ -1,9 +1,10 @@
1.4 -(*  Title       : SEQ.thy
1.5 -    Author      : Jacques D. Fleuriot
1.6 -    Copyright   : 1998  University of Cambridge
1.7 -    Description : Convergence of sequences and series
1.8 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
1.9 -    Additional contributions by Jeremy Avigad and Brian Huffman
1.10 +(*  Title:      HOL/SEQ.thy
1.11 +    Author:     Jacques D. Fleuriot, University of Cambridge
1.12 +    Author:     Lawrence C Paulson
1.13 +    Author:     Jeremy Avigad
1.14 +    Author:     Brian Huffman
1.15 +
1.16 +Convergence of sequences and series.
1.17  *)
1.19  header {* Sequences and Convergence *}
1.20 @@ -337,10 +338,10 @@
1.21      have "\<bar>f (N+k) - l\<bar> < e"
1.22      proof (induct k)
1.23        case 0 show ?case using N
1.24 -	by simp
1.25 +        by simp
1.26      next
1.27        case (Suc k) thus ?case using N inc [of "N+k"]
1.28 -	by simp
1.29 +        by simp
1.30      qed
1.31    } note 1 = this
1.32    { fix n
1.33 @@ -549,11 +550,11 @@
1.34      proof (simp add: LIMSEQ_iff)
1.35        assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
1.36        hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
1.37 -	by (metis 0)
1.38 +        by (metis 0)
1.39        from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
1.40 -	by blast
1.41 +        by blast
1.42        thus "lim f \<le> x"
1.43 -	by (metis add_cancel_end add_minus_cancel diff_def linorder_linear
1.44 +        by (metis add_cancel_end add_minus_cancel diff_def linorder_linear
1.45                    linorder_not_le minus_diff_eq abs_diff_less_iff fn_le)
1.46      qed
1.47  qed
1.48 @@ -685,45 +686,45 @@
1.49      hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
1.50      {fix n
1.51        have "?P (f (Suc n)) (f n)"
1.52 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
1.53 -	using H apply -
1.54 +        unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
1.55 +        using H apply -
1.56        apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI)
1.57        unfolding order_le_less by blast
1.58      hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
1.59    note fSuc = this
1.60      {fix p q assume pq: "p \<ge> f q"
1.61        have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
1.62 -	by (cases q, simp_all) }
1.63 +        by (cases q, simp_all) }
1.64      note pqth = this
1.65      {fix q
1.66        have "f (Suc q) > f q" apply (induct q)
1.67 -	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
1.68 +        using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
1.69      note fss = this
1.70      from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
1.71      {fix a b
1.72        have "f a \<le> f (a + b)"
1.73        proof(induct b)
1.74 -	case 0 thus ?case by simp
1.75 +        case 0 thus ?case by simp
1.76        next
1.77 -	case (Suc b)
1.78 -	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
1.79 +        case (Suc b)
1.80 +        from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
1.81        qed}
1.82      note fmon0 = this
1.83      have "monoseq (\<lambda>n. s (f n))"
1.84      proof-
1.85        {fix n
1.86 -	have "s (f n) \<ge> s (f (Suc n))"
1.87 -	proof(cases n)
1.88 -	  case 0
1.89 -	  assume n0: "n = 0"
1.90 -	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
1.91 -	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
1.92 -	next
1.93 -	  case (Suc m)
1.94 -	  assume m: "n = Suc m"
1.95 -	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
1.96 -	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
1.97 -	qed}
1.98 +        have "s (f n) \<ge> s (f (Suc n))"
1.99 +        proof(cases n)
1.100 +          case 0
1.101 +          assume n0: "n = 0"
1.102 +          from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
1.103 +          from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
1.104 +        next
1.105 +          case (Suc m)
1.106 +          assume m: "n = Suc m"
1.107 +          from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
1.108 +          from m fSuc(2)[rule_format, OF th0] show ?thesis by simp
1.109 +        qed}
1.110        thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast
1.111      qed
1.112      with th1 have ?thesis by blast}
1.113 @@ -750,26 +751,26 @@
1.114      hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
1.115      {fix n
1.116        have "f n > N \<and> ?P (f (Suc n)) (f n)"
1.117 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
1.118 +        unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
1.119        proof (induct n)
1.120 -	case 0 thus ?case
1.121 -	  using f0 N apply auto
1.122 -	  apply (erule allE[where x="f 0"], clarsimp)
1.123 -	  apply (rule_tac x="m" in exI, simp)
1.124 -	  by (subgoal_tac "f 0 \<noteq> m", auto)
1.125 +        case 0 thus ?case
1.126 +          using f0 N apply auto
1.127 +          apply (erule allE[where x="f 0"], clarsimp)
1.128 +          apply (rule_tac x="m" in exI, simp)
1.129 +          by (subgoal_tac "f 0 \<noteq> m", auto)
1.130        next
1.131 -	case (Suc n)
1.132 -	from Suc.hyps have Nfn: "N < f n" by blast
1.133 -	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
1.134 -	with Nfn have mN: "m > N" by arith
1.135 -	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
1.137 -	from key have th0: "f (Suc n) > N" by simp
1.138 -	from N[rule_format, OF th0]
1.139 -	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
1.140 -	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
1.141 -	hence "m' > f (Suc n)" using m'(1) by simp
1.142 -	with key m'(2) show ?case by auto
1.143 +        case (Suc n)
1.144 +        from Suc.hyps have Nfn: "N < f n" by blast
1.145 +        from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
1.146 +        with Nfn have mN: "m > N" by arith
1.147 +        note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
1.149 +        from key have th0: "f (Suc n) > N" by simp
1.150 +        from N[rule_format, OF th0]
1.151 +        obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
1.152 +        have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
1.153 +        hence "m' > f (Suc n)" using m'(1) by simp
1.154 +        with key m'(2) show ?case by auto
1.155        qed}
1.156      note fSuc = this
1.157      {fix n