author | huffman |
Wed, 20 Jun 2007 05:18:39 +0200 | |
changeset 23431 | 25ca91279a9b |
parent 21256 | 47195501ecf7 |
child 23477 | f4b83f03cac9 |
permissions | -rw-r--r-- |
16993 | 1 |
(* Title: HOL/ex/NatSum.thy |
11024 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow |
|
4 |
*) |
|
5 |
||
6 |
header {* Summing natural numbers *} |
|
7 |
||
21256 | 8 |
theory NatSum imports Main Parity begin |
11024 | 9 |
|
11786 | 10 |
text {* |
11 |
Summing natural numbers, squares, cubes, etc. |
|
12 |
||
13 |
Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, |
|
14 |
\url{http://www.research.att.com/~njas/sequences/}. |
|
15 |
*} |
|
16 |
||
15561 | 17 |
lemmas [simp] = |
18 |
left_distrib right_distrib |
|
19 |
left_diff_distrib right_diff_distrib --{*for true subtraction*} |
|
20 |
diff_mult_distrib diff_mult_distrib2 --{*for type nat*} |
|
11024 | 21 |
|
22 |
text {* |
|
12023 | 23 |
\medskip The sum of the first @{text n} odd numbers equals @{text n} |
11024 | 24 |
squared. |
25 |
*} |
|
26 |
||
16593 | 27 |
lemma sum_of_odds: "(\<Sum>i=0..<n. Suc (i + i)) = n * n" |
16993 | 28 |
by (induct n) auto |
11024 | 29 |
|
30 |
||
31 |
text {* |
|
32 |
\medskip The sum of the first @{text n} odd squares. |
|
33 |
*} |
|
34 |
||
35 |
lemma sum_of_odd_squares: |
|
15561 | 36 |
"3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)" |
16993 | 37 |
by (induct n) auto |
11024 | 38 |
|
39 |
||
40 |
text {* |
|
12023 | 41 |
\medskip The sum of the first @{text n} odd cubes |
11024 | 42 |
*} |
43 |
||
44 |
lemma sum_of_odd_cubes: |
|
15561 | 45 |
"(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) = |
11786 | 46 |
n * n * (2 * n * n - 1)" |
16993 | 47 |
by (induct n) auto |
11024 | 48 |
|
49 |
text {* |
|
12023 | 50 |
\medskip The sum of the first @{text n} positive integers equals |
11024 | 51 |
@{text "n (n + 1) / 2"}.*} |
52 |
||
11586 | 53 |
lemma sum_of_naturals: |
15561 | 54 |
"2 * (\<Sum>i=0..n. i) = n * Suc n" |
16993 | 55 |
by (induct n) auto |
11024 | 56 |
|
11586 | 57 |
lemma sum_of_squares: |
15561 | 58 |
"6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)" |
16993 | 59 |
by (induct n) auto |
11024 | 60 |
|
11586 | 61 |
lemma sum_of_cubes: |
15561 | 62 |
"4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n" |
16993 | 63 |
by (induct n) auto |
11024 | 64 |
|
21144 | 65 |
text{* \medskip A cute identity: *} |
66 |
||
67 |
lemma sum_squared: "(\<Sum>i=0..n. i)^2 = (\<Sum>i=0..n::nat. i^3)" |
|
68 |
proof(induct n) |
|
69 |
case 0 show ?case by simp |
|
70 |
next |
|
71 |
case (Suc n) |
|
72 |
have "(\<Sum>i = 0..Suc n. i)^2 = |
|
73 |
(\<Sum>i = 0..n. i^3) + (2*(\<Sum>i = 0..n. i)*(n+1) + (n+1)^2)" |
|
74 |
(is "_ = ?A + ?B") |
|
75 |
using Suc by(simp add:nat_number) |
|
76 |
also have "?B = (n+1)^3" |
|
77 |
using sum_of_naturals by(simp add:nat_number) |
|
78 |
also have "?A + (n+1)^3 = (\<Sum>i=0..Suc n. i^3)" by simp |
|
79 |
finally show ?case . |
|
80 |
qed |
|
11024 | 81 |
|
82 |
text {* |
|
15561 | 83 |
\medskip Sum of fourth powers: three versions. |
11024 | 84 |
*} |
85 |
||
86 |
lemma sum_of_fourth_powers: |
|
15561 | 87 |
"30 * (\<Sum>i=0..n. i * i * i * i) = |
11786 | 88 |
n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)" |
11024 | 89 |
apply (induct n) |
90 |
apply simp_all |
|
12196 | 91 |
apply (case_tac n) -- {* eliminates the subtraction *} |
92 |
apply (simp_all (no_asm_simp)) |
|
11024 | 93 |
done |
94 |
||
95 |
text {* |
|
16593 | 96 |
Two alternative proofs, with a change of variables and much more |
11024 | 97 |
subtraction, performed using the integers. *} |
98 |
||
99 |
lemma int_sum_of_fourth_powers: |
|
15561 | 100 |
"30 * int (\<Sum>i=0..<m. i * i * i * i) = |
101 |
int m * (int m - 1) * (int(2 * m) - 1) * |
|
102 |
(int(3 * m * m) - int(3 * m) - 1)" |
|
16993 | 103 |
by (induct m) (simp_all add: int_mult) |
15561 | 104 |
|
105 |
lemma of_nat_sum_of_fourth_powers: |
|
106 |
"30 * of_nat (\<Sum>i=0..<m. i * i * i * i) = |
|
15114 | 107 |
of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) * |
108 |
(of_nat (3 * m * m) - of_nat (3 * m) - (1::int))" |
|
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
21256
diff
changeset
|
109 |
by (induct m) (simp_all add: of_nat_mult) |
11024 | 110 |
|
111 |
||
112 |
text {* |
|
12023 | 113 |
\medskip Sums of geometric series: @{text 2}, @{text 3} and the |
11786 | 114 |
general case. |
115 |
*} |
|
11024 | 116 |
|
15561 | 117 |
lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)" |
16993 | 118 |
by (induct n) (auto split: nat_diff_split) |
11024 | 119 |
|
15561 | 120 |
lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)" |
16993 | 121 |
by (induct n) auto |
11024 | 122 |
|
15561 | 123 |
lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)" |
16993 | 124 |
by (induct n) auto |
11024 | 125 |
|
126 |
end |