|
1 (* Title: HOL/Library/ASeries.thy |
|
2 ID: $Id$ |
|
3 Author: Benjamin Porter, 2006 |
|
4 *) |
|
5 |
|
6 |
|
7 header {* Arithmetic Series *} |
|
8 |
|
9 theory ASeries |
|
10 imports Main |
|
11 begin |
|
12 |
|
13 section {* Abstract *} |
|
14 |
|
15 text {* The following document presents a proof of the Arithmetic |
|
16 Series Sum formalised in Isabelle/Isar. |
|
17 |
|
18 {\em Theorem:} The series $\sum_{i=1}^{n} a_i$ where $a_{i+1} = a_i + |
|
19 d$ for some constant $d$ has the sum $\frac{n}{2} (a_1 + a_n)$ |
|
20 (i.e. $n$ multiplied by the arithmetic mean of the first and last |
|
21 element). |
|
22 |
|
23 {\em Informal Proof:} (from |
|
24 "http://mathworld.wolfram.com/ArithmeticSeries.html") |
|
25 The proof is a simple forward proof. Let $S$ equal the sum above and |
|
26 $a$ the first element, then we have |
|
27 \begin{align} |
|
28 \nonumber S &= a + (a+d) + (a+2d) + ... a_n \\ |
|
29 \nonumber &= n*a + d (0 + 1 + 2 + ... n-1) \\ |
|
30 \nonumber &= n*a + d (\frac{1}{2} * (n-1) * n) \mbox{..using a simple sum identity} \\ |
|
31 \nonumber &= \frac{n}{2} (2a + d(n-1)) \\ |
|
32 \nonumber & \mbox{..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so} \\ |
|
33 \nonumber S &= \frac{n}{2} (a + a_n) |
|
34 \end{align} |
|
35 *} |
|
36 |
|
37 section {* Formal Proof *} |
|
38 |
|
39 text {* We present a proof for the abstract case of a commutative ring, |
|
40 we then instantiate for three common types nats, ints and reals. The |
|
41 function @{text "of_nat"} maps the natural numbers into any |
|
42 commutative ring. |
|
43 *} |
|
44 |
|
45 lemmas comm_simp [simp] = left_distrib right_distrib add_assoc mult_ac |
|
46 |
|
47 text {* Next we prove the following simple summation law $\sum_{i=1}^n |
|
48 i = \frac {n * (n+1)}{2}$. *} |
|
49 |
|
50 lemma sum_ident: |
|
51 "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) = |
|
52 of_nat n*((of_nat n)+1)" |
|
53 proof (induct n) |
|
54 case 0 |
|
55 show ?case by simp |
|
56 next |
|
57 case (Suc n) |
|
58 then show ?case by simp |
|
59 qed |
|
60 |
|
61 text {* The abstract theorem follows. Note that $2$ is displayed as |
|
62 $1+1$ to keep the structure as abstract as possible. *} |
|
63 |
|
64 theorem arith_series_general: |
|
65 "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
|
66 of_nat n * (a + (a + of_nat(n - 1)*d))" |
|
67 proof cases |
|
68 assume ngt1: "n > 1" |
|
69 let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n" |
|
70 have |
|
71 "(\<Sum>i\<in>{..<n}. a+?I i*d) = |
|
72 ((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" |
|
73 by (rule setsum_addf) |
|
74 also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp |
|
75 also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" |
|
76 by (simp add: setsum_mult setsum_head_upt) |
|
77 also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" |
|
78 by simp |
|
79 also from ngt1 have "{1..<n} = {1..n - 1}" |
|
80 by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) |
|
81 also from ngt1 |
|
82 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)" |
|
83 by (simp only: mult_ac sum_ident [of "n - 1"]) (simp add: of_nat_Suc [symmetric]) |
|
84 finally show ?thesis by simp |
|
85 next |
|
86 assume "\<not>(n > 1)" |
|
87 hence "n = 1 \<or> n = 0" by auto |
|
88 thus ?thesis by auto |
|
89 qed |
|
90 |
|
91 subsection {* Instantiation *} |
|
92 |
|
93 lemma arith_series_nat: |
|
94 "(2::nat) * (\<Sum>i\<in>{..<n}. a+i*d) = n * (a + (a+(n - 1)*d))" |
|
95 proof - |
|
96 have |
|
97 "((1::nat) + 1) * (\<Sum>i\<in>{..<n::nat}. a + of_nat(i)*d) = |
|
98 of_nat(n) * (a + (a + of_nat(n - 1)*d))" |
|
99 by (rule arith_series_general) |
|
100 thus ?thesis by (auto simp add: of_nat_id) |
|
101 qed |
|
102 |
|
103 lemma arith_series_int: |
|
104 "(2::int) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
|
105 of_nat n * (a + (a + of_nat(n - 1)*d))" |
|
106 proof - |
|
107 have |
|
108 "((1::int) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
|
109 of_nat(n) * (a + (a + of_nat(n - 1)*d))" |
|
110 by (rule arith_series_general) |
|
111 thus ?thesis by simp |
|
112 qed |
|
113 |
|
114 end |