* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
authorkleing
Sun Feb 19 13:21:32 2006 +0100 (2006-02-19)
changeset 191066e6b5b1fdc06
parent 19105 3aabd46340e0
child 19107 b16a45c53884
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
* added Complex/ex/ASeries_Complex (instantiation of the above for reals)
* added Complex/ex/HarmonicSeries (should really be in something like Complex/Library)

(these are contributions by Benjamin Porter, numbers 68 and 34 of
http://www.cs.ru.nl/~freek/100/)
src/HOL/Complex/ex/ASeries_Complex.thy
src/HOL/Complex/ex/HarmonicSeries.thy
src/HOL/Complex/ex/ROOT.ML
src/HOL/Hyperreal/Series.thy
src/HOL/Library/ASeries.thy
src/HOL/Library/Library.thy
src/HOL/SetInterval.thy
src/HOL/ex/ThreeDivides.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Complex/ex/ASeries_Complex.thy	Sun Feb 19 13:21:32 2006 +0100
     1.3 @@ -0,0 +1,24 @@
     1.4 +(*  Title:      HOL/Library/ASeries.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Benjamin Porter, 2006
     1.7 +*)
     1.8 +
     1.9 +
    1.10 +header {* Arithmetic Series for Reals *}
    1.11 +
    1.12 +theory ASeries_Complex
    1.13 +imports Complex_Main ASeries
    1.14 +begin
    1.15 +
    1.16 +lemma arith_series_real:
    1.17 +  "(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    1.18 +  of_nat n * (a + (a + of_nat(n - 1)*d))"
    1.19 +proof -
    1.20 +  have
    1.21 +    "((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) =
    1.22 +    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    1.23 +    by (rule arith_series_general)
    1.24 +  thus ?thesis by simp
    1.25 +qed
    1.26 +
    1.27 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Complex/ex/HarmonicSeries.thy	Sun Feb 19 13:21:32 2006 +0100
     2.3 @@ -0,0 +1,323 @@
     2.4 +(*  Title:      HOL/Library/HarmonicSeries.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Benjamin Porter, 2006
     2.7 +*)
     2.8 +
     2.9 +header {* Divergence of the Harmonic Series *}
    2.10 +
    2.11 +theory HarmonicSeries
    2.12 +imports Complex_Main
    2.13 +begin
    2.14 +
    2.15 +section {* Abstract *}
    2.16 +
    2.17 +text {* The following document presents a proof of the Divergence of
    2.18 +Harmonic Series theorem formalised in the Isabelle/Isar theorem
    2.19 +proving system.
    2.20 +
    2.21 +{\em Theorem:} The series $\sum_{n=1}^{\infty} \frac{1}{n}$ does not
    2.22 +converge to any number.
    2.23 +
    2.24 +{\em Informal Proof:}
    2.25 +  The informal proof is based on the following auxillary lemmas:
    2.26 +  \begin{itemize}
    2.27 +  \item{aux: $\sum_{n=2^m-1}^{2^m} \frac{1}{n} \geq \frac{1}{2}$}
    2.28 +  \item{aux2: $\sum_{n=1}^{2^M} \frac{1}{n} = 1 + \sum_{m=1}^{M} \sum_{n=2^m-1}^{2^m} \frac{1}{n}$}
    2.29 +  \end{itemize}
    2.30 +
    2.31 +  From {\em aux} and {\em aux2} we can deduce that $\sum_{n=1}^{2^M}
    2.32 +  \frac{1}{n} \geq 1 + \frac{M}{2}$ for all $M$.
    2.33 +  Now for contradiction, assume that $\sum_{n=1}^{\infty} \frac{1}{n}
    2.34 +  = s$ for some $s$. Because $\forall n. \frac{1}{n} > 0$ all the
    2.35 +  partial sums in the series must be less than $s$. However with our
    2.36 +  deduction above we can choose $N > 2*s - 2$ and thus
    2.37 +  $\sum_{n=1}^{2^N} \frac{1}{n} > s$. This leads to a contradiction
    2.38 +  and hence $\sum_{n=1}^{\infty} \frac{1}{n}$ is not summable.
    2.39 +  QED.
    2.40 +*}
    2.41 +
    2.42 +section {* Formal Proof *}
    2.43 +
    2.44 +lemma two_pow_sub:
    2.45 +  "0 < m \<Longrightarrow> (2::nat)^m - 2^(m - 1) = 2^(m - 1)"
    2.46 +  by (induct m) auto
    2.47 +
    2.48 +text {* We first prove the following auxillary lemma. This lemma
    2.49 +simply states that the finite sums: $\frac{1}{2}$, $\frac{1}{3} +
    2.50 +\frac{1}{4}$, $\frac{1}{5} + \frac{1}{6} + \frac{1}{7} + \frac{1}{8}$
    2.51 +etc. are all greater than or equal to $\frac{1}{2}$. We do this by
    2.52 +observing that each term in the sum is greater than or equal to the
    2.53 +last term, e.g. $\frac{1}{3} > \frac{1}{4}$ and thus $\frac{1}{3} +
    2.54 +\frac{1}{4} > \frac{1}{4} + \frac{1}{4} = \frac{1}{2}$. *}
    2.55 +
    2.56 +lemma harmonic_aux:
    2.57 +  "\<forall>m>0. (\<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) \<ge> 1/2"
    2.58 +  (is "\<forall>m>0. (\<Sum>n\<in>(?S m). 1/real n) \<ge> 1/2")
    2.59 +proof
    2.60 +  fix m::nat
    2.61 +  obtain tm where tmdef: "tm = (2::nat)^m" by simp
    2.62 +  {
    2.63 +    assume mgt0: "0 < m"
    2.64 +    have "\<And>x. x\<in>(?S m) \<Longrightarrow> 1/(real x) \<ge> 1/(real tm)"
    2.65 +    proof -
    2.66 +      fix x::nat
    2.67 +      assume xs: "x\<in>(?S m)"
    2.68 +      have xgt0: "x>0"
    2.69 +      proof -
    2.70 +        from xs have
    2.71 +          "x \<ge> 2^(m - 1) + 1" by auto
    2.72 +        moreover with mgt0 have
    2.73 +          "2^(m - 1) + 1 \<ge> (1::nat)" by auto
    2.74 +        ultimately have
    2.75 +          "x \<ge> 1" by (rule xtrans)
    2.76 +        thus ?thesis by simp
    2.77 +      qed
    2.78 +      moreover from xs have "x \<le> 2^m" by auto
    2.79 +      ultimately have
    2.80 +        "inverse (real x) \<ge> inverse (real ((2::nat)^m))" by simp
    2.81 +      moreover
    2.82 +      from xgt0 have "real x \<noteq> 0" by simp
    2.83 +      then have
    2.84 +        "inverse (real x) = 1 / (real x)"
    2.85 +        by (rule nonzero_inverse_eq_divide)
    2.86 +      moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef)
    2.87 +      then have
    2.88 +        "inverse (real tm) = 1 / (real tm)"
    2.89 +        by (rule nonzero_inverse_eq_divide)
    2.90 +      ultimately show
    2.91 +        "1/(real x) \<ge> 1/(real tm)" by (auto simp add: tmdef)
    2.92 +    qed
    2.93 +    then have
    2.94 +      "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> (\<Sum>n\<in>(?S m). 1/(real tm))"
    2.95 +      by (rule setsum_mono)
    2.96 +    moreover have
    2.97 +      "(\<Sum>n\<in>(?S m). 1/(real tm)) = 1/2"
    2.98 +    proof -
    2.99 +      have
   2.100 +        "(\<Sum>n\<in>(?S m). 1/(real tm)) =
   2.101 +         (1/(real tm))*(\<Sum>n\<in>(?S m). 1)"
   2.102 +        by simp
   2.103 +      also have
   2.104 +        "\<dots> = ((1/(real tm)) * real (card (?S m)))"
   2.105 +        by (simp add: real_of_card real_of_nat_def)
   2.106 +      also have
   2.107 +        "\<dots> = ((1/(real tm)) * real (tm - (2^(m - 1))))"
   2.108 +        by (simp add: tmdef)
   2.109 +      also from mgt0 have
   2.110 +        "\<dots> = ((1/(real tm)) * real ((2::nat)^(m - 1)))"
   2.111 +        by (auto simp: tmdef dest: two_pow_sub)
   2.112 +      also have
   2.113 +        "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m"
   2.114 +        by (simp add: tmdef realpow_real_of_nat [symmetric])
   2.115 +      also from mgt0 have
   2.116 +        "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)"
   2.117 +        by auto
   2.118 +      also have "\<dots> = 1/2" by simp
   2.119 +      finally show ?thesis .
   2.120 +    qed
   2.121 +    ultimately have
   2.122 +      "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> 1/2"
   2.123 +      by - (erule subst)
   2.124 +  }
   2.125 +  thus "0 < m \<longrightarrow> 1 / 2 \<le> (\<Sum>n\<in>(?S m). 1 / real n)" by simp
   2.126 +qed
   2.127 +
   2.128 +text {* We then show that the sum of a finite number of terms from the
   2.129 +harmonic series can be regrouped in increasing powers of 2. For
   2.130 +example: $1 + \frac{1}{2} + \frac{1}{3} + \frac{1}{4} + \frac{1}{5} +
   2.131 +\frac{1}{6} + \frac{1}{7} + \frac{1}{8} = 1 + (\frac{1}{2}) +
   2.132 +(\frac{1}{3} + \frac{1}{4}) + (\frac{1}{5} + \frac{1}{6} + \frac{1}{7}
   2.133 ++ \frac{1}{8})$. *}
   2.134 +
   2.135 +lemma harmonic_aux2 [rule_format]:
   2.136 +  "0<M \<Longrightarrow> (\<Sum>n\<in>{1..(2::nat)^M}. 1/real n) =
   2.137 +   (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))"
   2.138 +  (is "0<M \<Longrightarrow> ?LHS M = ?RHS M")
   2.139 +proof (induct M)
   2.140 +  case 0 show ?case by simp
   2.141 +next
   2.142 +  case (Suc M)
   2.143 +  have ant: "0 < Suc M" .
   2.144 +  {
   2.145 +    have suc: "?LHS (Suc M) = ?RHS (Suc M)"
   2.146 +    proof cases -- "show that LHS = c and RHS = c, and thus LHS = RHS"
   2.147 +      assume mz: "M=0"
   2.148 +      {
   2.149 +        then have
   2.150 +          "?LHS (Suc M) = ?LHS 1" by simp
   2.151 +        also have
   2.152 +          "\<dots> = (\<Sum>n\<in>{(1::nat)..2}. 1/real n)" by simp
   2.153 +        also have
   2.154 +          "\<dots> = ((\<Sum>n\<in>{Suc 1..2}. 1/real n) + 1/(real (1::nat)))"
   2.155 +          by (subst setsum_head)
   2.156 +             (auto simp: atLeastSucAtMost_greaterThanAtMost)
   2.157 +        also have
   2.158 +          "\<dots> = ((\<Sum>n\<in>{2..2::nat}. 1/real n) + 1/(real (1::nat)))"
   2.159 +          by (simp add: nat_number)
   2.160 +        also have
   2.161 +          "\<dots> =  1/(real (2::nat)) + 1/(real (1::nat))" by simp
   2.162 +        finally have
   2.163 +          "?LHS (Suc M) = 1/2 + 1" by simp
   2.164 +      }
   2.165 +      moreover
   2.166 +      {
   2.167 +        from mz have
   2.168 +          "?RHS (Suc M) = ?RHS 1" by simp
   2.169 +        also have
   2.170 +          "\<dots> = (\<Sum>n\<in>{((2::nat)^0)+1..2^1}. 1/real n) + 1"
   2.171 +          by simp
   2.172 +        also have
   2.173 +          "\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1"
   2.174 +        proof -
   2.175 +          have "(2::nat)^0 = 1" by simp
   2.176 +          then have "(2::nat)^0+1 = 2" by simp
   2.177 +          moreover have "(2::nat)^1 = 2" by simp
   2.178 +          ultimately have "{((2::nat)^0)+1..2^1} = {2::nat..2}" by auto
   2.179 +          thus ?thesis by simp
   2.180 +        qed
   2.181 +        also have
   2.182 +          "\<dots> = 1/2 + 1"
   2.183 +          by simp
   2.184 +        finally have
   2.185 +          "?RHS (Suc M) = 1/2 + 1" by simp
   2.186 +      }
   2.187 +      ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp
   2.188 +    next
   2.189 +      assume mnz: "M\<noteq>0"
   2.190 +      then have mgtz: "M>0" by simp
   2.191 +      with Suc have suc:
   2.192 +        "(?LHS M) = (?RHS M)" by blast
   2.193 +      have
   2.194 +        "(?LHS (Suc M)) =
   2.195 +         ((?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1 / real n))"
   2.196 +      proof -
   2.197 +        have
   2.198 +          "{1..(2::nat)^(Suc M)} =
   2.199 +           {1..(2::nat)^M}\<union>{(2::nat)^M+1..(2::nat)^(Suc M)}"
   2.200 +          by auto
   2.201 +        moreover have
   2.202 +          "{1..(2::nat)^M}\<inter>{(2::nat)^M+1..(2::nat)^(Suc M)} = {}"
   2.203 +          by auto
   2.204 +        moreover have
   2.205 +          "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}"
   2.206 +          by auto
   2.207 +        ultimately show ?thesis
   2.208 +          by (auto intro: setsum_Un_disjoint)
   2.209 +      qed
   2.210 +      moreover
   2.211 +      {
   2.212 +        have
   2.213 +          "(?RHS (Suc M)) =
   2.214 +           (1 + (\<Sum>m\<in>{1..M}.  \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) +
   2.215 +           (\<Sum>n\<in>{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp
   2.216 +        also have
   2.217 +          "\<dots> = (?RHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)"
   2.218 +          by simp
   2.219 +        also from suc have
   2.220 +          "\<dots> = (?LHS M) +  (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)"
   2.221 +          by simp
   2.222 +        finally have
   2.223 +          "(?RHS (Suc M)) = \<dots>" by simp
   2.224 +      }
   2.225 +      ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp
   2.226 +    qed
   2.227 +  }
   2.228 +  thus ?case by simp
   2.229 +qed
   2.230 +
   2.231 +text {* Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show
   2.232 +that each group sum is greater than or equal to $\frac{1}{2}$ and thus
   2.233 +the finite sum is bounded below by a value proportional to the number
   2.234 +of elements we choose. *}
   2.235 +
   2.236 +lemma harmonic_aux3 [rule_format]:
   2.237 +  shows "\<forall>(M::nat). (\<Sum>n\<in>{1..(2::nat)^M}. 1 / real n) \<ge> 1 + (real M)/2"
   2.238 +  (is "\<forall>M. ?P M \<ge> _")
   2.239 +proof (rule allI, cases)
   2.240 +  fix M::nat
   2.241 +  assume "M=0"
   2.242 +  then show "?P M \<ge> 1 + (real M)/2" by simp
   2.243 +next
   2.244 +  fix M::nat
   2.245 +  assume "M\<noteq>0"
   2.246 +  then have "M > 0" by simp
   2.247 +  then have
   2.248 +    "(?P M) =
   2.249 +     (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))"
   2.250 +    by (rule harmonic_aux2)
   2.251 +  also have
   2.252 +    "\<dots> \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))"
   2.253 +  proof -
   2.254 +    let ?f = "(\<lambda>x. 1/2)"
   2.255 +    let ?g = "(\<lambda>x. (\<Sum>n\<in>{(2::nat)^(x - 1)+1..2^x}. 1/real n))"
   2.256 +    from harmonic_aux have "\<And>x. x\<in>{1..M} \<Longrightarrow> ?f x \<le> ?g x" by simp
   2.257 +    then have "(\<Sum>m\<in>{1..M}. ?g m) \<ge> (\<Sum>m\<in>{1..M}. ?f m)" by (rule setsum_mono)
   2.258 +    thus ?thesis by simp
   2.259 +  qed
   2.260 +  finally have "(?P M) \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" .
   2.261 +  moreover
   2.262 +  {
   2.263 +    have
   2.264 +      "(\<Sum>m\<in>{1..M}. (1::real)/2) = 1/2 * (\<Sum>m\<in>{1..M}. 1)"
   2.265 +      by auto
   2.266 +    also have
   2.267 +      "\<dots> = 1/2*(real (card {1..M}))"
   2.268 +      by (simp only: real_of_card[symmetric])
   2.269 +    also have
   2.270 +      "\<dots> = 1/2*(real M)" by simp
   2.271 +    also have
   2.272 +      "\<dots> = (real M)/2" by simp
   2.273 +    finally have "(\<Sum>m\<in>{1..M}. (1::real)/2) = (real M)/2" .
   2.274 +  }
   2.275 +  ultimately show "(?P M) \<ge> (1 + (real M)/2)" by simp
   2.276 +qed
   2.277 +
   2.278 +text {* The final theorem shows that as we take more and more elements
   2.279 +(see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming
   2.280 +the sum converges, the lemma @{thm [source] series_pos_less} ( @{thm
   2.281 +series_pos_less} ) states that each sum is bounded above by the
   2.282 +series' limit. This contradicts our first statement and thus we prove
   2.283 +that the harmonic series is divergent. *}
   2.284 +
   2.285 +theorem DivergenceOfHarmonicSeries:
   2.286 +  shows "\<not>summable (\<lambda>n. 1/real (Suc n))"
   2.287 +  (is "\<not>summable ?f")
   2.288 +proof -- "by contradiction"
   2.289 +  let ?s = "suminf ?f" -- "let ?s equal the sum of the harmonic series"
   2.290 +  assume sf: "summable ?f"
   2.291 +  then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp
   2.292 +  then have ngt: "1 + real n/2 > ?s"
   2.293 +  proof -
   2.294 +    have "\<forall>n. 0 \<le> ?f n" by simp
   2.295 +    with sf have "?s \<ge> 0"
   2.296 +      by - (rule suminf_0_le, simp_all)
   2.297 +    then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp
   2.298 +
   2.299 +    from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .
   2.300 +    then have "real n = real (nat \<lceil>2*?s\<rceil>)" by simp
   2.301 +    with cgt0 have "real n = real \<lceil>2*?s\<rceil>"
   2.302 +      by (auto dest: real_nat_eq_real)
   2.303 +    then have "real n \<ge> 2*(?s)" by simp
   2.304 +    then have "real n/2 \<ge> (?s)" by simp
   2.305 +    then show "1 + real n/2 > (?s)" by simp
   2.306 +  qed
   2.307 +
   2.308 +  obtain j where jdef: "j = (2::nat)^n" by simp
   2.309 +  have "\<forall>m\<ge>j. 0 < ?f m" by simp
   2.310 +  with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" by (rule series_pos_less)
   2.311 +  then have "(\<Sum>i\<in>{1..<Suc j}. 1/(real i)) < ?s"
   2.312 +    apply -
   2.313 +    apply (subst(asm) setsum_shift_bounds_Suc_ivl [symmetric])
   2.314 +    by simp
   2.315 +  with jdef have
   2.316 +    "(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp
   2.317 +  then have
   2.318 +    "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) < ?s"
   2.319 +    by (simp only: atLeastLessThanSuc_atLeastAtMost)
   2.320 +  moreover from harmonic_aux3 have
   2.321 +    "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) \<ge> 1 + real n/2" by simp
   2.322 +  moreover from ngt have "1 + real n/2 > ?s" by simp
   2.323 +  ultimately show False by simp
   2.324 +qed
   2.325 +
   2.326 +end
   2.327 \ No newline at end of file
     3.1 --- a/src/HOL/Complex/ex/ROOT.ML	Sun Feb 19 02:11:27 2006 +0100
     3.2 +++ b/src/HOL/Complex/ex/ROOT.ML	Sun Feb 19 13:21:32 2006 +0100
     3.3 @@ -14,3 +14,6 @@
     3.4  
     3.5  no_document use_thy "BigO";
     3.6  use_thy "BigO_Complex";
     3.7 +
     3.8 +use_thy "ASeries_Complex";
     3.9 +use_thy "HarmonicSeries";
     4.1 --- a/src/HOL/Hyperreal/Series.thy	Sun Feb 19 02:11:27 2006 +0100
     4.2 +++ b/src/HOL/Hyperreal/Series.thy	Sun Feb 19 13:21:32 2006 +0100
     4.3 @@ -280,7 +280,6 @@
     4.4  apply simp
     4.5  done
     4.6  
     4.7 -
     4.8  lemma sumr_pos_lt_pair:
     4.9       "[|summable f; 
    4.10          \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
    4.11 @@ -409,6 +408,21 @@
    4.12  apply (simp add: abs_le_interval_iff)
    4.13  done
    4.14  
    4.15 +(* specialisation for the common 0 case *)
    4.16 +lemma suminf_0_le:
    4.17 +  fixes f::"nat\<Rightarrow>real"
    4.18 +  assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f"
    4.19 +  shows "0 \<le> suminf f"
    4.20 +proof -
    4.21 +  let ?g = "(\<lambda>n. (0::real))"
    4.22 +  from gt0 have "\<forall>n. ?g n \<le> f n" by simp
    4.23 +  moreover have "summable ?g" by (rule summable_zero)
    4.24 +  moreover from sm have "summable f" .
    4.25 +  ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
    4.26 +  then show "0 \<le> suminf f" by (simp add: suminf_zero)
    4.27 +qed 
    4.28 +
    4.29 +
    4.30  text{*Absolute convergence imples normal convergence*}
    4.31  lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
    4.32  apply (auto simp add: summable_Cauchy)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/ASeries.thy	Sun Feb 19 13:21:32 2006 +0100
     5.3 @@ -0,0 +1,114 @@
     5.4 +(*  Title:      HOL/Library/ASeries.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Benjamin Porter, 2006
     5.7 +*)
     5.8 +
     5.9 +
    5.10 +header {* Arithmetic Series *}
    5.11 +
    5.12 +theory ASeries
    5.13 +imports Main
    5.14 +begin
    5.15 +
    5.16 +section {* Abstract *}
    5.17 +
    5.18 +text {* The following document presents a proof of the Arithmetic
    5.19 +Series Sum formalised in Isabelle/Isar.
    5.20 +
    5.21 +{\em Theorem:} The series $\sum_{i=1}^{n} a_i$ where $a_{i+1} = a_i +
    5.22 +d$ for some constant $d$ has the sum $\frac{n}{2} (a_1 + a_n)$
    5.23 +(i.e. $n$ multiplied by the arithmetic mean of the first and last
    5.24 +element).
    5.25 +
    5.26 +{\em Informal Proof:} (from
    5.27 +"http://mathworld.wolfram.com/ArithmeticSeries.html")
    5.28 +  The proof is a simple forward proof. Let $S$ equal the sum above and
    5.29 +  $a$ the first element, then we have
    5.30 +\begin{align}
    5.31 +\nonumber  S &= a + (a+d) + (a+2d) + ... a_n \\
    5.32 +\nonumber    &= n*a + d (0 + 1 + 2 + ... n-1) \\
    5.33 +\nonumber    &= n*a + d (\frac{1}{2} * (n-1) * n)    \mbox{..using a simple sum identity} \\
    5.34 +\nonumber    &= \frac{n}{2} (2a + d(n-1)) \\
    5.35 +\nonumber    & \mbox{..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so} \\
    5.36 +\nonumber  S &= \frac{n}{2} (a + a_n)
    5.37 +\end{align}
    5.38 +*}
    5.39 +
    5.40 +section {* Formal Proof *}
    5.41 +
    5.42 +text {* We present a proof for the abstract case of a commutative ring,
    5.43 +we then instantiate for three common types nats, ints and reals. The
    5.44 +function @{text "of_nat"} maps the natural numbers into any
    5.45 +commutative ring.
    5.46 +*}
    5.47 +
    5.48 +lemmas comm_simp [simp] = left_distrib right_distrib add_assoc mult_ac
    5.49 +
    5.50 +text {* Next we prove the following simple summation law $\sum_{i=1}^n
    5.51 +i = \frac {n * (n+1)}{2}$. *}
    5.52 +
    5.53 +lemma sum_ident:
    5.54 +  "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
    5.55 +   of_nat n*((of_nat n)+1)"
    5.56 +proof (induct n)
    5.57 +  case 0
    5.58 +  show ?case by simp
    5.59 +next
    5.60 +  case (Suc n)
    5.61 +  then show ?case by simp
    5.62 +qed
    5.63 +
    5.64 +text {* The abstract theorem follows. Note that $2$ is displayed as
    5.65 +$1+1$ to keep the structure as abstract as possible. *}
    5.66 +
    5.67 +theorem arith_series_general:
    5.68 +  "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    5.69 +  of_nat n * (a + (a + of_nat(n - 1)*d))"
    5.70 +proof cases
    5.71 +  assume ngt1: "n > 1"
    5.72 +  let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
    5.73 +  have
    5.74 +    "(\<Sum>i\<in>{..<n}. a+?I i*d) =
    5.75 +     ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
    5.76 +    by (rule setsum_addf)
    5.77 +  also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
    5.78 +  also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
    5.79 +    by (simp add: setsum_mult setsum_head_upt)
    5.80 +  also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
    5.81 +    by simp
    5.82 +  also from ngt1 have "{1..<n} = {1..n - 1}"
    5.83 +    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)    
    5.84 +  also from ngt1 
    5.85 +  have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)"
    5.86 +    by (simp only: mult_ac sum_ident [of "n - 1"]) (simp add: of_nat_Suc [symmetric])
    5.87 +  finally show ?thesis by simp
    5.88 +next
    5.89 +  assume "\<not>(n > 1)"
    5.90 +  hence "n = 1 \<or> n = 0" by auto
    5.91 +  thus ?thesis by auto
    5.92 +qed
    5.93 +
    5.94 +subsection {* Instantiation *}
    5.95 +
    5.96 +lemma arith_series_nat:
    5.97 +  "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
    5.98 +proof -
    5.99 +  have
   5.100 +    "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
   5.101 +    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
   5.102 +    by (rule arith_series_general)
   5.103 +  thus ?thesis by (auto simp add: of_nat_id)
   5.104 +qed
   5.105 +
   5.106 +lemma arith_series_int:
   5.107 +  "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
   5.108 +  of_nat n * (a + (a + of_nat(n - 1)*d))"
   5.109 +proof -
   5.110 +  have
   5.111 +    "((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
   5.112 +    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
   5.113 +    by (rule arith_series_general)
   5.114 +  thus ?thesis by simp
   5.115 +qed
   5.116 +
   5.117 +end
     6.1 --- a/src/HOL/Library/Library.thy	Sun Feb 19 02:11:27 2006 +0100
     6.2 +++ b/src/HOL/Library/Library.thy	Sun Feb 19 13:21:32 2006 +0100
     6.3 @@ -21,6 +21,7 @@
     6.4    Char_ord
     6.5    Commutative_Ring
     6.6    Coinductive_List
     6.7 +  ASeries
     6.8  begin
     6.9  end
    6.10  (*>*)
     7.1 --- a/src/HOL/SetInterval.thy	Sun Feb 19 02:11:27 2006 +0100
     7.2 +++ b/src/HOL/SetInterval.thy	Sun Feb 19 13:21:32 2006 +0100
     7.3 @@ -715,24 +715,39 @@
     7.4    "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}"
     7.5  by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified])
     7.6  
     7.7 -lemma setsum_rmv_head:
     7.8 +lemma setsum_head:
     7.9 +  fixes n :: nat
    7.10 +  assumes mn: "m <= n" 
    7.11 +  shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
    7.12 +proof -
    7.13 +  from mn
    7.14 +  have "{m..n} = {m} \<union> {m<..n}"
    7.15 +    by (auto intro: ivl_disj_un_singleton)
    7.16 +  hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
    7.17 +    by (simp add: atLeast0LessThan)
    7.18 +  also have "\<dots> = ?rhs" by simp
    7.19 +  finally show ?thesis .
    7.20 +qed
    7.21 +
    7.22 +lemma setsum_head_upt:
    7.23    fixes m::nat
    7.24    assumes m: "0 < m"
    7.25 -  shows "P 0 + (\<Sum>x\<in>{1..<m}. P x) = (\<Sum>x<m. P x)"
    7.26 -  (is "?lhs = ?rhs")
    7.27 +  shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)"
    7.28  proof -
    7.29 -  let ?a = "\<Sum>x\<in>({0} \<union> {0<..<m}). P x"
    7.30 -  from m
    7.31 -  have "{0..<m} = {0} \<union> {0<..<m}"
    7.32 -    by (simp only: ivl_disj_un_singleton)
    7.33 -  hence "?rhs = ?a"
    7.34 +  have "(\<Sum>x<m. P x) = (\<Sum>x\<in>{0..<m}. P x)" 
    7.35      by (simp add: atLeast0LessThan)
    7.36 -  moreover
    7.37 -  have "?a = ?lhs"
    7.38 -    by (simp add: setsum_Un ivl_disj_int 
    7.39 -                  atLeastSucLessThan_greaterThanLessThan)
    7.40 -  ultimately 
    7.41 -  show ?thesis by simp
    7.42 +  also 
    7.43 +  from m 
    7.44 +  have "\<dots> = (\<Sum>x\<in>{0..m - 1}. P x)"
    7.45 +    by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)
    7.46 +  also
    7.47 +  have "\<dots> = P 0 + (\<Sum>x\<in>{0<..m - 1}. P x)"
    7.48 +    by (simp add: setsum_head)
    7.49 +  also 
    7.50 +  from m 
    7.51 +  have "{0<..m - 1} = {1..<m}" 
    7.52 +    by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost)
    7.53 +  finally show ?thesis .
    7.54  qed
    7.55  
    7.56  subsection {* The formula for geometric sums *}
     8.1 --- a/src/HOL/ex/ThreeDivides.thy	Sun Feb 19 02:11:27 2006 +0100
     8.2 +++ b/src/HOL/ex/ThreeDivides.thy	Sun Feb 19 13:21:32 2006 +0100
     8.3 @@ -207,7 +207,7 @@
     8.4           (simp add: atLeast0LessThan)
     8.5      also have
     8.6        "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
     8.7 -      by (simp add: setsum_rmv_head [symmetric] cdef)
     8.8 +      by (simp add: setsum_rmv_upt cdef)
     8.9      also note `Suc nd = nlen m`
    8.10      finally
    8.11      show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .