moved arithmetic series to geometric series in SetInterval
authorkleing
Wed Apr 26 07:01:33 2006 +0200 (2006-04-26)
changeset 19469958d2f2dd8d4
parent 19468 0afdd5023bfc
child 19470 3572af78f114
moved arithmetic series to geometric series in SetInterval
src/HOL/Complex/ex/Arithmetic_Series_Complex.thy
src/HOL/Complex/ex/ROOT.ML
src/HOL/Library/Arithmetic_Series.thy
src/HOL/Library/Library.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Complex/ex/Arithmetic_Series_Complex.thy	Tue Apr 25 22:23:58 2006 +0200
     1.2 +++ b/src/HOL/Complex/ex/Arithmetic_Series_Complex.thy	Wed Apr 26 07:01:33 2006 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Arithmetic Series for Reals *}
     1.5  
     1.6  theory Arithmetic_Series_Complex
     1.7 -imports Complex_Main Arithmetic_Series
     1.8 +imports Complex_Main 
     1.9  begin
    1.10  
    1.11  lemma arith_series_real:
     2.1 --- a/src/HOL/Complex/ex/ROOT.ML	Tue Apr 25 22:23:58 2006 +0200
     2.2 +++ b/src/HOL/Complex/ex/ROOT.ML	Wed Apr 26 07:01:33 2006 +0200
     2.3 @@ -15,7 +15,6 @@
     2.4  no_document use_thy "BigO";
     2.5  use_thy "BigO_Complex";
     2.6  
     2.7 -no_document use_thy "Arithmetic_Series";
     2.8  use_thy "Arithmetic_Series_Complex";
     2.9  use_thy "HarmonicSeries";
    2.10  
     3.1 --- a/src/HOL/Library/Arithmetic_Series.thy	Tue Apr 25 22:23:58 2006 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,114 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Arithmetic_Series.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Benjamin Porter, 2006
     3.7 -*)
     3.8 -
     3.9 -
    3.10 -header {* Arithmetic Series *}
    3.11 -
    3.12 -theory Arithmetic_Series
    3.13 -imports Main
    3.14 -begin
    3.15 -
    3.16 -section {* Abstract *}
    3.17 -
    3.18 -text {* The following document presents a proof of the Arithmetic
    3.19 -Series Sum formalised in Isabelle/Isar.
    3.20 -
    3.21 -{\em Theorem:} The series $\sum_{i=1}^{n} a_i$ where $a_{i+1} = a_i +
    3.22 -d$ for some constant $d$ has the sum $\frac{n}{2} (a_1 + a_n)$
    3.23 -(i.e. $n$ multiplied by the arithmetic mean of the first and last
    3.24 -element).
    3.25 -
    3.26 -{\em Informal Proof:} (from
    3.27 -"http://mathworld.wolfram.com/ArithmeticSeries.html")
    3.28 -  The proof is a simple forward proof. Let $S$ equal the sum above and
    3.29 -  $a$ the first element, then we have
    3.30 -\begin{tabular}{ll}
    3.31 -  $S$ &$= a + (a+d) + (a+2d) + ... a_n$ \\
    3.32 -    &$= n*a + d (0 + 1 + 2 + ... n-1)$ \\
    3.33 -    &$= n*a + d (\frac{1}{2} * (n-1) * n)$   ..using a simple sum identity \\
    3.34 -    &$= \frac{n}{2} (2a + d(n-1))$ \\
    3.35 -    & ..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so \\
    3.36 -  $S$ &$= \frac{n}{2} (a + a_n)$
    3.37 -\end{tabular}
    3.38 -*}
    3.39 -
    3.40 -section {* Formal Proof *}
    3.41 -
    3.42 -text {* We present a proof for the abstract case of a commutative ring,
    3.43 -we then instantiate for three common types nats, ints and reals. The
    3.44 -function @{text "of_nat"} maps the natural numbers into any
    3.45 -commutative ring.
    3.46 -*}
    3.47 -
    3.48 -lemmas comm_simp [simp] = left_distrib right_distrib add_assoc mult_ac
    3.49 -
    3.50 -text {* Next we prove the following simple summation law $\sum_{i=1}^n
    3.51 -i = \frac {n * (n+1)}{2}$. *}
    3.52 -
    3.53 -lemma sum_ident:
    3.54 -  "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
    3.55 -   of_nat n*((of_nat n)+1)"
    3.56 -proof (induct n)
    3.57 -  case 0
    3.58 -  show ?case by simp
    3.59 -next
    3.60 -  case (Suc n)
    3.61 -  then show ?case by simp
    3.62 -qed
    3.63 -
    3.64 -text {* The abstract theorem follows. Note that $2$ is displayed as
    3.65 -$1+1$ to keep the structure as abstract as possible. *}
    3.66 -
    3.67 -theorem arith_series_general:
    3.68 -  "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    3.69 -  of_nat n * (a + (a + of_nat(n - 1)*d))"
    3.70 -proof cases
    3.71 -  assume ngt1: "n > 1"
    3.72 -  let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
    3.73 -  have
    3.74 -    "(\<Sum>i\<in>{..<n}. a+?I i*d) =
    3.75 -     ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
    3.76 -    by (rule setsum_addf)
    3.77 -  also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
    3.78 -  also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
    3.79 -    by (simp add: setsum_right_distrib setsum_head_upt)
    3.80 -  also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
    3.81 -    by simp
    3.82 -  also from ngt1 have "{1..<n} = {1..n - 1}"
    3.83 -    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)    
    3.84 -  also from ngt1 
    3.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)"
    3.86 -    by (simp only: mult_ac sum_ident [of "n - 1"]) (simp add: of_nat_Suc [symmetric])
    3.87 -  finally show ?thesis by simp
    3.88 -next
    3.89 -  assume "\<not>(n > 1)"
    3.90 -  hence "n = 1 \<or> n = 0" by auto
    3.91 -  thus ?thesis by auto
    3.92 -qed
    3.93 -
    3.94 -subsection {* Instantiation *}
    3.95 -
    3.96 -lemma arith_series_nat:
    3.97 -  "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
    3.98 -proof -
    3.99 -  have
   3.100 -    "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
   3.101 -    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
   3.102 -    by (rule arith_series_general)
   3.103 -  thus ?thesis by (auto simp add: of_nat_id)
   3.104 -qed
   3.105 -
   3.106 -lemma arith_series_int:
   3.107 -  "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
   3.108 -  of_nat n * (a + (a + of_nat(n - 1)*d))"
   3.109 -proof -
   3.110 -  have
   3.111 -    "((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
   3.112 -    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
   3.113 -    by (rule arith_series_general)
   3.114 -  thus ?thesis by simp
   3.115 -qed
   3.116 -
   3.117 -end
     4.1 --- a/src/HOL/Library/Library.thy	Tue Apr 25 22:23:58 2006 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Wed Apr 26 07:01:33 2006 +0200
     4.3 @@ -21,7 +21,6 @@
     4.4    Char_ord
     4.5    Commutative_Ring
     4.6    Coinductive_List
     4.7 -  Arithmetic_Series
     4.8    AssocList
     4.9  begin
    4.10  end
     5.1 --- a/src/HOL/SetInterval.thy	Tue Apr 25 22:23:58 2006 +0200
     5.2 +++ b/src/HOL/SetInterval.thy	Wed Apr 26 07:01:33 2006 +0200
     5.3 @@ -762,6 +762,67 @@
     5.4    done
     5.5  
     5.6  
     5.7 +subsection {* The formula for arithmetic sums *}
     5.8 +
     5.9 +lemma gauss_sum:
    5.10 +  "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
    5.11 +   of_nat n*((of_nat n)+1)"
    5.12 +proof (induct n)
    5.13 +  case 0
    5.14 +  show ?case by simp
    5.15 +next
    5.16 +  case (Suc n)
    5.17 +  then show ?case by (simp add: right_distrib add_assoc mult_ac)
    5.18 +qed
    5.19 +
    5.20 +theorem arith_series_general:
    5.21 +  "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    5.22 +  of_nat n * (a + (a + of_nat(n - 1)*d))"
    5.23 +proof cases
    5.24 +  assume ngt1: "n > 1"
    5.25 +  let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n"
    5.26 +  have
    5.27 +    "(\<Sum>i\<in>{..<n}. a+?I i*d) =
    5.28 +     ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))"
    5.29 +    by (rule setsum_addf)
    5.30 +  also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
    5.31 +  also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
    5.32 +    by (simp add: setsum_right_distrib setsum_head_upt mult_ac)
    5.33 +  also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
    5.34 +    by (simp add: left_distrib right_distrib)
    5.35 +  also from ngt1 have "{1..<n} = {1..n - 1}"
    5.36 +    by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost)    
    5.37 +  also from ngt1 
    5.38 +  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.39 +    by (simp only: mult_ac gauss_sum [of "n - 1"])
    5.40 +       (simp add:  mult_ac of_nat_Suc [symmetric])
    5.41 +  finally show ?thesis by (simp add: mult_ac add_ac right_distrib)
    5.42 +next
    5.43 +  assume "\<not>(n > 1)"
    5.44 +  hence "n = 1 \<or> n = 0" by auto
    5.45 +  thus ?thesis by (auto simp: mult_ac right_distrib)
    5.46 +qed
    5.47 +
    5.48 +lemma arith_series_nat:
    5.49 +  "Suc (Suc 0) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))"
    5.50 +proof -
    5.51 +  have
    5.52 +    "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) =
    5.53 +    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    5.54 +    by (rule arith_series_general)
    5.55 +  thus ?thesis by (auto simp add: of_nat_id)
    5.56 +qed
    5.57 +
    5.58 +lemma arith_series_int:
    5.59 +  "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    5.60 +  of_nat n * (a + (a + of_nat(n - 1)*d))"
    5.61 +proof -
    5.62 +  have
    5.63 +    "((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
    5.64 +    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    5.65 +    by (rule arith_series_general)
    5.66 +  thus ?thesis by simp
    5.67 +qed
    5.68  
    5.69  lemma sum_diff_distrib:
    5.70    fixes P::"nat\<Rightarrow>nat"