equal
deleted
inserted
replaced
5 Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the |
5 Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the |
6 original scripts). Demonstrates mathematical induction together with |
6 original scripts). Demonstrates mathematical induction together with |
7 calculational proof. |
7 calculational proof. |
8 *) |
8 *) |
9 |
9 |
|
10 header {* Summing natural numbers *}; |
10 |
11 |
11 theory Summation = Main:; |
12 theory Summation = Main:; |
12 |
13 |
13 |
14 subsection {* A summation operator *}; |
14 section {* Summing natural numbers *}; |
|
15 |
|
16 text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *}; |
|
17 |
15 |
18 consts |
16 consts |
19 sum :: "[nat => nat, nat] => nat"; |
17 sum :: "[nat => nat, nat] => nat"; |
20 |
18 |
21 primrec |
19 primrec |
28 "SUM i < k. b" == "sum (%i. b) k"; |
26 "SUM i < k. b" == "sum (%i. b) k"; |
29 |
27 |
30 |
28 |
31 subsection {* Summation laws *}; |
29 subsection {* Summation laws *}; |
32 |
30 |
33 (* FIXME binary arithmetic does not yet work here *) |
31 syntax (* FIXME binary arithmetic does not yet work here *) |
34 |
|
35 syntax |
|
36 "3" :: nat ("3") |
32 "3" :: nat ("3") |
37 "4" :: nat ("4") |
33 "4" :: nat ("4") |
38 "6" :: nat ("6"); |
34 "6" :: nat ("6"); |
39 |
35 |
40 translations |
36 translations |
91 also; assume "?S n = (n * (n + 1))^2"; |
87 also; assume "?S n = (n * (n + 1))^2"; |
92 also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp; |
88 also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp; |
93 finally; show "?P (Suc n)"; by simp; |
89 finally; show "?P (Suc n)"; by simp; |
94 qed; |
90 qed; |
95 |
91 |
96 |
|
97 end; |
92 end; |