7443
|
1 |
(* Title: HOL/Isar_examples/Summation.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel
|
|
4 |
|
|
5 |
Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the
|
|
6 |
original scripts). Demonstrates mathematical induction together with
|
|
7 |
calculational proof.
|
|
8 |
*)
|
|
9 |
|
7748
|
10 |
header {* Summing natural numbers *};
|
7443
|
11 |
|
|
12 |
theory Summation = Main:;
|
|
13 |
|
7761
|
14 |
|
7748
|
15 |
subsection {* A summation operator *};
|
7443
|
16 |
|
|
17 |
consts
|
|
18 |
sum :: "[nat => nat, nat] => nat";
|
|
19 |
|
|
20 |
primrec
|
|
21 |
"sum f 0 = 0"
|
|
22 |
"sum f (Suc n) = f n + sum f n";
|
|
23 |
|
|
24 |
syntax
|
7800
|
25 |
"_SUM" :: "idt => nat => nat => nat"
|
|
26 |
("SUM _ < _. _" [0, 0, 10] 10);
|
7443
|
27 |
translations
|
|
28 |
"SUM i < k. b" == "sum (%i. b) k";
|
|
29 |
|
|
30 |
|
|
31 |
subsection {* Summation laws *};
|
|
32 |
|
7800
|
33 |
verbatim {* \begin{comment} *};
|
|
34 |
|
7761
|
35 |
(* FIXME binary arithmetic does not yet work here *)
|
|
36 |
|
|
37 |
syntax
|
7443
|
38 |
"3" :: nat ("3")
|
|
39 |
"4" :: nat ("4")
|
|
40 |
"6" :: nat ("6");
|
|
41 |
|
|
42 |
translations
|
|
43 |
"3" == "Suc 2"
|
|
44 |
"4" == "Suc 3"
|
|
45 |
"6" == "Suc (Suc 4)";
|
|
46 |
|
|
47 |
theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
|
|
48 |
|
7800
|
49 |
verbatim {* \end{comment} *};
|
7443
|
50 |
|
7800
|
51 |
|
|
52 |
theorem sum_of_naturals:
|
|
53 |
"2 * (SUM i < n + 1. i) = n * (n + 1)"
|
7480
|
54 |
(is "?P n" is "?S n = _");
|
7443
|
55 |
proof (induct n);
|
7480
|
56 |
show "?P 0"; by simp;
|
7443
|
57 |
|
|
58 |
fix n;
|
7480
|
59 |
have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp;
|
|
60 |
also; assume "?S n = n * (n + 1)";
|
7443
|
61 |
also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
|
7480
|
62 |
finally; show "?P (Suc n)"; by simp;
|
7443
|
63 |
qed;
|
|
64 |
|
7800
|
65 |
theorem sum_of_odds:
|
|
66 |
"(SUM i < n. 2 * i + 1) = n^2"
|
7480
|
67 |
(is "?P n" is "?S n = _");
|
7443
|
68 |
proof (induct n);
|
7480
|
69 |
show "?P 0"; by simp;
|
7443
|
70 |
|
|
71 |
fix n;
|
7480
|
72 |
have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;
|
|
73 |
also; assume "?S n = n^2";
|
7443
|
74 |
also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
|
7480
|
75 |
finally; show "?P (Suc n)"; by simp;
|
7443
|
76 |
qed;
|
|
77 |
|
7761
|
78 |
theorem sum_of_squares:
|
|
79 |
"6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
|
7480
|
80 |
(is "?P n" is "?S n = _");
|
7443
|
81 |
proof (induct n);
|
7480
|
82 |
show "?P 0"; by simp;
|
7443
|
83 |
|
|
84 |
fix n;
|
7480
|
85 |
have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
|
|
86 |
also; assume "?S n = n * (n + 1) * (2 * n + 1)";
|
7800
|
87 |
also; have "... + 6 * (n + 1)^2 =
|
|
88 |
(n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
|
7480
|
89 |
finally; show "?P (Suc n)"; by simp;
|
7443
|
90 |
qed;
|
|
91 |
|
7800
|
92 |
theorem sum_of_cubes:
|
|
93 |
"4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
|
7480
|
94 |
(is "?P n" is "?S n = _");
|
7443
|
95 |
proof (induct n);
|
7480
|
96 |
show "?P 0"; by simp;
|
7443
|
97 |
|
|
98 |
fix n;
|
7480
|
99 |
have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
|
|
100 |
also; assume "?S n = (n * (n + 1))^2";
|
7761
|
101 |
also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2";
|
|
102 |
by simp;
|
7480
|
103 |
finally; show "?P (Suc n)"; by simp;
|
7443
|
104 |
qed;
|
|
105 |
|
|
106 |
end;
|