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