# HG changeset patch
# User kleing
# Date 1146027693 -7200
# Node ID 958d2f2dd8d4c221c6bac562d63a6ad0871ce534
# Parent  0afdd5023bfcda4626f40c2b9ce9a54bfe51b9a6
moved arithmetic series to geometric series in SetInterval

diff -r 0afdd5023bfc -r 958d2f2dd8d4 src/HOL/Complex/ex/Arithmetic_Series_Complex.thy
--- a/src/HOL/Complex/ex/Arithmetic_Series_Complex.thy	Tue Apr 25 22:23:58 2006 +0200
+++ b/src/HOL/Complex/ex/Arithmetic_Series_Complex.thy	Wed Apr 26 07:01:33 2006 +0200
@@ -7,7 +7,7 @@
 header {* Arithmetic Series for Reals *}
 
 theory Arithmetic_Series_Complex
-imports Complex_Main Arithmetic_Series
+imports Complex_Main 
 begin
 
 lemma arith_series_real:
diff -r 0afdd5023bfc -r 958d2f2dd8d4 src/HOL/Complex/ex/ROOT.ML
--- a/src/HOL/Complex/ex/ROOT.ML	Tue Apr 25 22:23:58 2006 +0200
+++ b/src/HOL/Complex/ex/ROOT.ML	Wed Apr 26 07:01:33 2006 +0200
@@ -15,7 +15,6 @@
 no_document use_thy "BigO";
 use_thy "BigO_Complex";
 
-no_document use_thy "Arithmetic_Series";
 use_thy "Arithmetic_Series_Complex";
 use_thy "HarmonicSeries";
 
diff -r 0afdd5023bfc -r 958d2f2dd8d4 src/HOL/Library/Arithmetic_Series.thy
--- a/src/HOL/Library/Arithmetic_Series.thy	Tue Apr 25 22:23:58 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-(*  Title:      HOL/Library/Arithmetic_Series.thy
-    ID:         $Id$
-    Author:     Benjamin Porter, 2006
-*)
-
-
-header {* Arithmetic Series *}
-
-theory Arithmetic_Series
-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{tabular}{ll}
-  $S$ &$= a + (a+d) + (a+2d) + ... a_n$ \\
-    &$= n*a + d (0 + 1 + 2 + ... n-1)$ \\
-    &$= n*a + d (\frac{1}{2} * (n-1) * n)$   ..using a simple sum identity \\
-    &$= \frac{n}{2} (2a + d(n-1))$ \\
-    & ..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so \\
-  $S$ &$= \frac{n}{2} (a + a_n)$
-\end{tabular}
-*}
-
-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_right_distrib 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
diff -r 0afdd5023bfc -r 958d2f2dd8d4 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Apr 25 22:23:58 2006 +0200
+++ b/src/HOL/Library/Library.thy	Wed Apr 26 07:01:33 2006 +0200
@@ -21,7 +21,6 @@
   Char_ord
   Commutative_Ring
   Coinductive_List
-  Arithmetic_Series
   AssocList
 begin
 end
diff -r 0afdd5023bfc -r 958d2f2dd8d4 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Tue Apr 25 22:23:58 2006 +0200
+++ b/src/HOL/SetInterval.thy	Wed Apr 26 07:01:33 2006 +0200
@@ -762,6 +762,67 @@
   done
 
 
+subsection {* The formula for arithmetic sums *}
+
+lemma gauss_sum:
+  "((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 add: right_distrib add_assoc mult_ac)
+qed
+
+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_right_distrib setsum_head_upt mult_ac)
+  also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
+    by (simp add: left_distrib right_distrib)
+  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 gauss_sum [of "n - 1"])
+       (simp add:  mult_ac of_nat_Suc [symmetric])
+  finally show ?thesis by (simp add: mult_ac add_ac right_distrib)
+next
+  assume "\<not>(n > 1)"
+  hence "n = 1 \<or> n = 0" by auto
+  thus ?thesis by (auto simp: mult_ac right_distrib)
+qed
+
+lemma arith_series_nat:
+  "Suc (Suc 0) * (\<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
 
 lemma sum_diff_distrib:
   fixes P::"nat\<Rightarrow>nat"