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

author | kleing |

Fri, 07 Apr 2006 03:20:34 +0200 | |

changeset 19351 | c33563c7c14c |

parent 19350 | 2e1c7ca05ee0 |

child 19352 | 1a07f6cf1e6c |

renamed ASeries to Arithmetic_Series, removed the ^M

src/HOL/Library/ASeries.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Arithmetic_Series.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Library.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/ASeries.thy Thu Apr 06 17:29:40 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,114 +0,0 @@ -(* 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{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

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Arithmetic_Series.thy Fri Apr 07 03:20:34 2006 +0200 @@ -0,0 +1,114 @@ +(* 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