equal
deleted
inserted
replaced
20 primrec |
20 primrec |
21 "sum f 0 = 0" |
21 "sum f 0 = 0" |
22 "sum f (Suc n) = f n + sum f n"; |
22 "sum f (Suc n) = f n + sum f n"; |
23 |
23 |
24 syntax |
24 syntax |
25 "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10); |
25 "_SUM" :: "idt => nat => nat => nat" |
|
26 ("SUM _ < _. _" [0, 0, 10] 10); |
26 translations |
27 translations |
27 "SUM i < k. b" == "sum (%i. b) k"; |
28 "SUM i < k. b" == "sum (%i. b) k"; |
28 |
29 |
29 |
30 |
30 subsection {* Summation laws *}; |
31 subsection {* Summation laws *}; |
|
32 |
|
33 verbatim {* \begin{comment} *}; |
31 |
34 |
32 (* FIXME binary arithmetic does not yet work here *) |
35 (* FIXME binary arithmetic does not yet work here *) |
33 |
36 |
34 syntax |
37 syntax |
35 "3" :: nat ("3") |
38 "3" :: nat ("3") |
41 "4" == "Suc 3" |
44 "4" == "Suc 3" |
42 "6" == "Suc (Suc 4)"; |
45 "6" == "Suc (Suc 4)"; |
43 |
46 |
44 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; |
47 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; |
45 |
48 |
|
49 verbatim {* \end{comment} *}; |
46 |
50 |
47 theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)" |
51 |
|
52 theorem sum_of_naturals: |
|
53 "2 * (SUM i < n + 1. i) = n * (n + 1)" |
48 (is "?P n" is "?S n = _"); |
54 (is "?P n" is "?S n = _"); |
49 proof (induct n); |
55 proof (induct n); |
50 show "?P 0"; by simp; |
56 show "?P 0"; by simp; |
51 |
57 |
52 fix n; |
58 fix n; |
54 also; assume "?S n = n * (n + 1)"; |
60 also; assume "?S n = n * (n + 1)"; |
55 also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp; |
61 also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp; |
56 finally; show "?P (Suc n)"; by simp; |
62 finally; show "?P (Suc n)"; by simp; |
57 qed; |
63 qed; |
58 |
64 |
59 theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2" |
65 theorem sum_of_odds: |
|
66 "(SUM i < n. 2 * i + 1) = n^2" |
60 (is "?P n" is "?S n = _"); |
67 (is "?P n" is "?S n = _"); |
61 proof (induct n); |
68 proof (induct n); |
62 show "?P 0"; by simp; |
69 show "?P 0"; by simp; |
63 |
70 |
64 fix n; |
71 fix n; |
75 show "?P 0"; by simp; |
82 show "?P 0"; by simp; |
76 |
83 |
77 fix n; |
84 fix n; |
78 have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp; |
85 have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp; |
79 also; assume "?S n = n * (n + 1) * (2 * n + 1)"; |
86 also; assume "?S n = n * (n + 1) * (2 * n + 1)"; |
80 also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; |
87 also; have "... + 6 * (n + 1)^2 = |
81 by simp; |
88 (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp; |
82 finally; show "?P (Suc n)"; by simp; |
89 finally; show "?P (Suc n)"; by simp; |
83 qed; |
90 qed; |
84 |
91 |
85 theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" |
92 theorem sum_of_cubes: |
|
93 "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" |
86 (is "?P n" is "?S n = _"); |
94 (is "?P n" is "?S n = _"); |
87 proof (induct n); |
95 proof (induct n); |
88 show "?P 0"; by simp; |
96 show "?P 0"; by simp; |
89 |
97 |
90 fix n; |
98 fix n; |