19351
|
1 |
(* Title: HOL/Library/Arithmetic_Series.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Benjamin Porter, 2006
|
|
4 |
*)
|
|
5 |
|
|
6 |
|
|
7 |
header {* Arithmetic Series *}
|
|
8 |
|
|
9 |
theory Arithmetic_Series
|
|
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{tabular}{ll}
|
|
28 |
$S$ &$= a + (a+d) + (a+2d) + ... a_n$ \\
|
|
29 |
&$= n*a + d (0 + 1 + 2 + ... n-1)$ \\
|
|
30 |
&$= n*a + d (\frac{1}{2} * (n-1) * n)$ ..using a simple sum identity \\
|
|
31 |
&$= \frac{n}{2} (2a + d(n-1))$ \\
|
|
32 |
& ..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so \\
|
|
33 |
$S$ &$= \frac{n}{2} (a + a_n)$
|
|
34 |
\end{tabular}
|
|
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_right_distrib 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
|