summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kleing |

Sun, 19 Feb 2006 13:21:32 +0100 | |

changeset 19106 | 6e6b5b1fdc06 |

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/)

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex/ex/ASeries_Complex.thy Sun Feb 19 13:21:32 2006 +0100 @@ -0,0 +1,24 @@ +(* Title: HOL/Library/ASeries.thy + ID: $Id$ + Author: Benjamin Porter, 2006 +*) + + +header {* Arithmetic Series for Reals *} + +theory ASeries_Complex +imports Complex_Main ASeries +begin + +lemma arith_series_real: + "(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = + of_nat n * (a + (a + of_nat(n - 1)*d))" +proof - + have + "((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) = + of_nat(n) * (a + (a + of_nat(n - 1)*d))" + by (rule arith_series_general) + thus ?thesis by simp +qed + +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex/ex/HarmonicSeries.thy Sun Feb 19 13:21:32 2006 +0100 @@ -0,0 +1,323 @@ +(* Title: HOL/Library/HarmonicSeries.thy + ID: $Id$ + Author: Benjamin Porter, 2006 +*) + +header {* Divergence of the Harmonic Series *} + +theory HarmonicSeries +imports Complex_Main +begin + +section {* Abstract *} + +text {* The following document presents a proof of the Divergence of +Harmonic Series theorem formalised in the Isabelle/Isar theorem +proving system. + +{\em Theorem:} The series $\sum_{n=1}^{\infty} \frac{1}{n}$ does not +converge to any number. + +{\em Informal Proof:} + The informal proof is based on the following auxillary lemmas: + \begin{itemize} + \item{aux: $\sum_{n=2^m-1}^{2^m} \frac{1}{n} \geq \frac{1}{2}$} + \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}$} + \end{itemize} + + From {\em aux} and {\em aux2} we can deduce that $\sum_{n=1}^{2^M} + \frac{1}{n} \geq 1 + \frac{M}{2}$ for all $M$. + Now for contradiction, assume that $\sum_{n=1}^{\infty} \frac{1}{n} + = s$ for some $s$. Because $\forall n. \frac{1}{n} > 0$ all the + partial sums in the series must be less than $s$. However with our + deduction above we can choose $N > 2*s - 2$ and thus + $\sum_{n=1}^{2^N} \frac{1}{n} > s$. This leads to a contradiction + and hence $\sum_{n=1}^{\infty} \frac{1}{n}$ is not summable. + QED. +*} + +section {* Formal Proof *} + +lemma two_pow_sub: + "0 < m \<Longrightarrow> (2::nat)^m - 2^(m - 1) = 2^(m - 1)" + by (induct m) auto + +text {* We first prove the following auxillary lemma. This lemma +simply states that the finite sums: $\frac{1}{2}$, $\frac{1}{3} + +\frac{1}{4}$, $\frac{1}{5} + \frac{1}{6} + \frac{1}{7} + \frac{1}{8}$ +etc. are all greater than or equal to $\frac{1}{2}$. We do this by +observing that each term in the sum is greater than or equal to the +last term, e.g. $\frac{1}{3} > \frac{1}{4}$ and thus $\frac{1}{3} + +\frac{1}{4} > \frac{1}{4} + \frac{1}{4} = \frac{1}{2}$. *} + +lemma harmonic_aux: + "\<forall>m>0. (\<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) \<ge> 1/2" + (is "\<forall>m>0. (\<Sum>n\<in>(?S m). 1/real n) \<ge> 1/2") +proof + fix m::nat + obtain tm where tmdef: "tm = (2::nat)^m" by simp + { + assume mgt0: "0 < m" + have "\<And>x. x\<in>(?S m) \<Longrightarrow> 1/(real x) \<ge> 1/(real tm)" + proof - + fix x::nat + assume xs: "x\<in>(?S m)" + have xgt0: "x>0" + proof - + from xs have + "x \<ge> 2^(m - 1) + 1" by auto + moreover with mgt0 have + "2^(m - 1) + 1 \<ge> (1::nat)" by auto + ultimately have + "x \<ge> 1" by (rule xtrans) + thus ?thesis by simp + qed + moreover from xs have "x \<le> 2^m" by auto + ultimately have + "inverse (real x) \<ge> inverse (real ((2::nat)^m))" by simp + moreover + from xgt0 have "real x \<noteq> 0" by simp + then have + "inverse (real x) = 1 / (real x)" + by (rule nonzero_inverse_eq_divide) + moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef) + then have + "inverse (real tm) = 1 / (real tm)" + by (rule nonzero_inverse_eq_divide) + ultimately show + "1/(real x) \<ge> 1/(real tm)" by (auto simp add: tmdef) + qed + then have + "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> (\<Sum>n\<in>(?S m). 1/(real tm))" + by (rule setsum_mono) + moreover have + "(\<Sum>n\<in>(?S m). 1/(real tm)) = 1/2" + proof - + have + "(\<Sum>n\<in>(?S m). 1/(real tm)) = + (1/(real tm))*(\<Sum>n\<in>(?S m). 1)" + by simp + also have + "\<dots> = ((1/(real tm)) * real (card (?S m)))" + by (simp add: real_of_card real_of_nat_def) + also have + "\<dots> = ((1/(real tm)) * real (tm - (2^(m - 1))))" + by (simp add: tmdef) + also from mgt0 have + "\<dots> = ((1/(real tm)) * real ((2::nat)^(m - 1)))" + by (auto simp: tmdef dest: two_pow_sub) + also have + "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m" + by (simp add: tmdef realpow_real_of_nat [symmetric]) + also from mgt0 have + "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)" + by auto + also have "\<dots> = 1/2" by simp + finally show ?thesis . + qed + ultimately have + "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> 1/2" + by - (erule subst) + } + thus "0 < m \<longrightarrow> 1 / 2 \<le> (\<Sum>n\<in>(?S m). 1 / real n)" by simp +qed + +text {* We then show that the sum of a finite number of terms from the +harmonic series can be regrouped in increasing powers of 2. For +example: $1 + \frac{1}{2} + \frac{1}{3} + \frac{1}{4} + \frac{1}{5} + +\frac{1}{6} + \frac{1}{7} + \frac{1}{8} = 1 + (\frac{1}{2}) + +(\frac{1}{3} + \frac{1}{4}) + (\frac{1}{5} + \frac{1}{6} + \frac{1}{7} ++ \frac{1}{8})$. *} + +lemma harmonic_aux2 [rule_format]: + "0<M \<Longrightarrow> (\<Sum>n\<in>{1..(2::nat)^M}. 1/real n) = + (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))" + (is "0<M \<Longrightarrow> ?LHS M = ?RHS M") +proof (induct M) + case 0 show ?case by simp +next + case (Suc M) + have ant: "0 < Suc M" . + { + have suc: "?LHS (Suc M) = ?RHS (Suc M)" + proof cases -- "show that LHS = c and RHS = c, and thus LHS = RHS" + assume mz: "M=0" + { + then have + "?LHS (Suc M) = ?LHS 1" by simp + also have + "\<dots> = (\<Sum>n\<in>{(1::nat)..2}. 1/real n)" by simp + also have + "\<dots> = ((\<Sum>n\<in>{Suc 1..2}. 1/real n) + 1/(real (1::nat)))" + by (subst setsum_head) + (auto simp: atLeastSucAtMost_greaterThanAtMost) + also have + "\<dots> = ((\<Sum>n\<in>{2..2::nat}. 1/real n) + 1/(real (1::nat)))" + by (simp add: nat_number) + also have + "\<dots> = 1/(real (2::nat)) + 1/(real (1::nat))" by simp + finally have + "?LHS (Suc M) = 1/2 + 1" by simp + } + moreover + { + from mz have + "?RHS (Suc M) = ?RHS 1" by simp + also have + "\<dots> = (\<Sum>n\<in>{((2::nat)^0)+1..2^1}. 1/real n) + 1" + by simp + also have + "\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1" + proof - + have "(2::nat)^0 = 1" by simp + then have "(2::nat)^0+1 = 2" by simp + moreover have "(2::nat)^1 = 2" by simp + ultimately have "{((2::nat)^0)+1..2^1} = {2::nat..2}" by auto + thus ?thesis by simp + qed + also have + "\<dots> = 1/2 + 1" + by simp + finally have + "?RHS (Suc M) = 1/2 + 1" by simp + } + ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp + next + assume mnz: "M\<noteq>0" + then have mgtz: "M>0" by simp + with Suc have suc: + "(?LHS M) = (?RHS M)" by blast + have + "(?LHS (Suc M)) = + ((?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1 / real n))" + proof - + have + "{1..(2::nat)^(Suc M)} = + {1..(2::nat)^M}\<union>{(2::nat)^M+1..(2::nat)^(Suc M)}" + by auto + moreover have + "{1..(2::nat)^M}\<inter>{(2::nat)^M+1..(2::nat)^(Suc M)} = {}" + by auto + moreover have + "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}" + by auto + ultimately show ?thesis + by (auto intro: setsum_Un_disjoint) + qed + moreover + { + have + "(?RHS (Suc M)) = + (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) + + (\<Sum>n\<in>{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp + also have + "\<dots> = (?RHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)" + by simp + also from suc have + "\<dots> = (?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)" + by simp + finally have + "(?RHS (Suc M)) = \<dots>" by simp + } + ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp + qed + } + thus ?case by simp +qed + +text {* Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show +that each group sum is greater than or equal to $\frac{1}{2}$ and thus +the finite sum is bounded below by a value proportional to the number +of elements we choose. *} + +lemma harmonic_aux3 [rule_format]: + shows "\<forall>(M::nat). (\<Sum>n\<in>{1..(2::nat)^M}. 1 / real n) \<ge> 1 + (real M)/2" + (is "\<forall>M. ?P M \<ge> _") +proof (rule allI, cases) + fix M::nat + assume "M=0" + then show "?P M \<ge> 1 + (real M)/2" by simp +next + fix M::nat + assume "M\<noteq>0" + then have "M > 0" by simp + then have + "(?P M) = + (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))" + by (rule harmonic_aux2) + also have + "\<dots> \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" + proof - + let ?f = "(\<lambda>x. 1/2)" + let ?g = "(\<lambda>x. (\<Sum>n\<in>{(2::nat)^(x - 1)+1..2^x}. 1/real n))" + from harmonic_aux have "\<And>x. x\<in>{1..M} \<Longrightarrow> ?f x \<le> ?g x" by simp + then have "(\<Sum>m\<in>{1..M}. ?g m) \<ge> (\<Sum>m\<in>{1..M}. ?f m)" by (rule setsum_mono) + thus ?thesis by simp + qed + finally have "(?P M) \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" . + moreover + { + have + "(\<Sum>m\<in>{1..M}. (1::real)/2) = 1/2 * (\<Sum>m\<in>{1..M}. 1)" + by auto + also have + "\<dots> = 1/2*(real (card {1..M}))" + by (simp only: real_of_card[symmetric]) + also have + "\<dots> = 1/2*(real M)" by simp + also have + "\<dots> = (real M)/2" by simp + finally have "(\<Sum>m\<in>{1..M}. (1::real)/2) = (real M)/2" . + } + ultimately show "(?P M) \<ge> (1 + (real M)/2)" by simp +qed + +text {* The final theorem shows that as we take more and more elements +(see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming +the sum converges, the lemma @{thm [source] series_pos_less} ( @{thm +series_pos_less} ) states that each sum is bounded above by the +series' limit. This contradicts our first statement and thus we prove +that the harmonic series is divergent. *} + +theorem DivergenceOfHarmonicSeries: + shows "\<not>summable (\<lambda>n. 1/real (Suc n))" + (is "\<not>summable ?f") +proof -- "by contradiction" + let ?s = "suminf ?f" -- "let ?s equal the sum of the harmonic series" + assume sf: "summable ?f" + then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp + then have ngt: "1 + real n/2 > ?s" + proof - + have "\<forall>n. 0 \<le> ?f n" by simp + with sf have "?s \<ge> 0" + by - (rule suminf_0_le, simp_all) + then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp + + from ndef have "n = nat \<lceil>(2*?s)\<rceil>" . + then have "real n = real (nat \<lceil>2*?s\<rceil>)" by simp + with cgt0 have "real n = real \<lceil>2*?s\<rceil>" + by (auto dest: real_nat_eq_real) + then have "real n \<ge> 2*(?s)" by simp + then have "real n/2 \<ge> (?s)" by simp + then show "1 + real n/2 > (?s)" by simp + qed + + obtain j where jdef: "j = (2::nat)^n" by simp + have "\<forall>m\<ge>j. 0 < ?f m" by simp + with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" by (rule series_pos_less) + then have "(\<Sum>i\<in>{1..<Suc j}. 1/(real i)) < ?s" + apply - + apply (subst(asm) setsum_shift_bounds_Suc_ivl [symmetric]) + by simp + with jdef have + "(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp + then have + "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) < ?s" + by (simp only: atLeastLessThanSuc_atLeastAtMost) + moreover from harmonic_aux3 have + "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) \<ge> 1 + real n/2" by simp + moreover from ngt have "1 + real n/2 > ?s" by simp + ultimately show False by simp +qed + +end \ No newline at end of file

--- a/src/HOL/Complex/ex/ROOT.ML Sun Feb 19 02:11:27 2006 +0100 +++ b/src/HOL/Complex/ex/ROOT.ML Sun Feb 19 13:21:32 2006 +0100 @@ -14,3 +14,6 @@ no_document use_thy "BigO"; use_thy "BigO_Complex"; + +use_thy "ASeries_Complex"; +use_thy "HarmonicSeries";

--- a/src/HOL/Hyperreal/Series.thy Sun Feb 19 02:11:27 2006 +0100 +++ b/src/HOL/Hyperreal/Series.thy Sun Feb 19 13:21:32 2006 +0100 @@ -280,7 +280,6 @@ apply simp done - lemma sumr_pos_lt_pair: "[|summable f; \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|] @@ -409,6 +408,21 @@ apply (simp add: abs_le_interval_iff) done +(* specialisation for the common 0 case *) +lemma suminf_0_le: + fixes f::"nat\<Rightarrow>real" + assumes gt0: "\<forall>n. 0 \<le> f n" and sm: "summable f" + shows "0 \<le> suminf f" +proof - + let ?g = "(\<lambda>n. (0::real))" + from gt0 have "\<forall>n. ?g n \<le> f n" by simp + moreover have "summable ?g" by (rule summable_zero) + moreover from sm have "summable f" . + ultimately have "suminf ?g \<le> suminf f" by (rule summable_le) + then show "0 \<le> suminf f" by (simp add: suminf_zero) +qed + + text{*Absolute convergence imples normal convergence*} lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f" apply (auto simp add: summable_Cauchy)

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/ASeries.thy Sun Feb 19 13:21:32 2006 +0100 @@ -0,0 +1,114 @@ +(* Title: HOL/Library/ASeries.thy + ID: $Id$ + Author: Benjamin Porter, 2006 +*) + + +header {* Arithmetic Series *} + +theory ASeries +imports Main +begin + +section {* Abstract *} + +text {* The following document presents a proof of the Arithmetic +Series Sum formalised in Isabelle/Isar. + +{\em Theorem:} The series $\sum_{i=1}^{n} a_i$ where $a_{i+1} = a_i + +d$ for some constant $d$ has the sum $\frac{n}{2} (a_1 + a_n)$ +(i.e. $n$ multiplied by the arithmetic mean of the first and last +element). + +{\em Informal Proof:} (from +"http://mathworld.wolfram.com/ArithmeticSeries.html") + The proof is a simple forward proof. Let $S$ equal the sum above and + $a$ the first element, then we have +\begin{align} +\nonumber S &= a + (a+d) + (a+2d) + ... a_n \\ +\nonumber &= n*a + d (0 + 1 + 2 + ... n-1) \\ +\nonumber &= n*a + d (\frac{1}{2} * (n-1) * n) \mbox{..using a simple sum identity} \\ +\nonumber &= \frac{n}{2} (2a + d(n-1)) \\ +\nonumber & \mbox{..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so} \\ +\nonumber S &= \frac{n}{2} (a + a_n) +\end{align} +*} + +section {* Formal Proof *} + +text {* We present a proof for the abstract case of a commutative ring, +we then instantiate for three common types nats, ints and reals. The +function @{text "of_nat"} maps the natural numbers into any +commutative ring. +*} + +lemmas comm_simp [simp] = left_distrib right_distrib add_assoc mult_ac + +text {* Next we prove the following simple summation law $\sum_{i=1}^n +i = \frac {n * (n+1)}{2}$. *} + +lemma sum_ident: + "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) = + of_nat n*((of_nat n)+1)" +proof (induct n) + case 0 + show ?case by simp +next + case (Suc n) + then show ?case by simp +qed + +text {* The abstract theorem follows. Note that $2$ is displayed as +$1+1$ to keep the structure as abstract as possible. *} + +theorem arith_series_general: + "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = + of_nat n * (a + (a + of_nat(n - 1)*d))" +proof cases + assume ngt1: "n > 1" + let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n" + have + "(\<Sum>i\<in>{..<n}. a+?I i*d) = + ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" + by (rule setsum_addf) + also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp + also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" + by (simp add: setsum_mult setsum_head_upt) + also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" + by simp + also from ngt1 have "{1..<n} = {1..n - 1}" + by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) + also from ngt1 + 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)" + by (simp only: mult_ac sum_ident [of "n - 1"]) (simp add: of_nat_Suc [symmetric]) + finally show ?thesis by simp +next + assume "\<not>(n > 1)" + hence "n = 1 \<or> n = 0" by auto + thus ?thesis by auto +qed + +subsection {* Instantiation *} + +lemma arith_series_nat: + "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))" +proof - + have + "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) = + of_nat(n) * (a + (a + of_nat(n - 1)*d))" + by (rule arith_series_general) + thus ?thesis by (auto simp add: of_nat_id) +qed + +lemma arith_series_int: + "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = + of_nat n * (a + (a + of_nat(n - 1)*d))" +proof - + have + "((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = + of_nat(n) * (a + (a + of_nat(n - 1)*d))" + by (rule arith_series_general) + thus ?thesis by simp +qed + +end

--- a/src/HOL/Library/Library.thy Sun Feb 19 02:11:27 2006 +0100 +++ b/src/HOL/Library/Library.thy Sun Feb 19 13:21:32 2006 +0100 @@ -21,6 +21,7 @@ Char_ord Commutative_Ring Coinductive_List + ASeries begin end (*>*)

--- a/src/HOL/SetInterval.thy Sun Feb 19 02:11:27 2006 +0100 +++ b/src/HOL/SetInterval.thy Sun Feb 19 13:21:32 2006 +0100 @@ -715,24 +715,39 @@ "setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){m..<n}" by (simp add:setsum_shift_bounds_nat_ivl[where k=1,simplified]) -lemma setsum_rmv_head: +lemma setsum_head: + fixes n :: nat + assumes mn: "m <= n" + shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs") +proof - + from mn + have "{m..n} = {m} \<union> {m<..n}" + by (auto intro: ivl_disj_un_singleton) + hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)" + by (simp add: atLeast0LessThan) + also have "\<dots> = ?rhs" by simp + finally show ?thesis . +qed + +lemma setsum_head_upt: fixes m::nat assumes m: "0 < m" - shows "P 0 + (\<Sum>x\<in>{1..<m}. P x) = (\<Sum>x<m. P x)" - (is "?lhs = ?rhs") + shows "(\<Sum>x<m. P x) = P 0 + (\<Sum>x\<in>{1..<m}. P x)" proof - - let ?a = "\<Sum>x\<in>({0} \<union> {0<..<m}). P x" - from m - have "{0..<m} = {0} \<union> {0<..<m}" - by (simp only: ivl_disj_un_singleton) - hence "?rhs = ?a" + have "(\<Sum>x<m. P x) = (\<Sum>x\<in>{0..<m}. P x)" by (simp add: atLeast0LessThan) - moreover - have "?a = ?lhs" - by (simp add: setsum_Un ivl_disj_int - atLeastSucLessThan_greaterThanLessThan) - ultimately - show ?thesis by simp + also + from m + have "\<dots> = (\<Sum>x\<in>{0..m - 1}. P x)" + by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) + also + have "\<dots> = P 0 + (\<Sum>x\<in>{0<..m - 1}. P x)" + by (simp add: setsum_head) + also + from m + have "{0<..m - 1} = {1..<m}" + by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) + finally show ?thesis . qed subsection {* The formula for geometric sums *}

--- a/src/HOL/ex/ThreeDivides.thy Sun Feb 19 02:11:27 2006 +0100 +++ b/src/HOL/ex/ThreeDivides.thy Sun Feb 19 13:21:32 2006 +0100 @@ -207,7 +207,7 @@ (simp add: atLeast0LessThan) also have "\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)" - by (simp add: setsum_rmv_head [symmetric] cdef) + by (simp add: setsum_rmv_upt cdef) also note `Suc nd = nlen m` finally show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .