44 |
44 |
45 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; |
45 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; |
46 |
46 |
47 |
47 |
48 theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)" |
48 theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)" |
49 (is "??P n" is "??S n = _"); |
49 (is "?P n" is "?S n = _"); |
50 proof (induct n); |
50 proof (induct n); |
51 show "??P 0"; by simp; |
51 show "?P 0"; by simp; |
52 |
52 |
53 fix n; |
53 fix n; |
54 have "??S (n + 1) = ??S n + 2 * (n + 1)"; by simp; |
54 have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp; |
55 also; assume "??S n = n * (n + 1)"; |
55 also; assume "?S n = n * (n + 1)"; |
56 also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp; |
56 also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp; |
57 finally; show "??P (Suc n)"; by simp; |
57 finally; show "?P (Suc n)"; by simp; |
58 qed; |
58 qed; |
59 |
59 |
60 theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2" |
60 theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2" |
61 (is "??P n" is "??S n = _"); |
61 (is "?P n" is "?S n = _"); |
62 proof (induct n); |
62 proof (induct n); |
63 show "??P 0"; by simp; |
63 show "?P 0"; by simp; |
64 |
64 |
65 fix n; |
65 fix n; |
66 have "??S (n + 1) = ??S n + 2 * n + 1"; by simp; |
66 have "?S (n + 1) = ?S n + 2 * n + 1"; by simp; |
67 also; assume "??S n = n^2"; |
67 also; assume "?S n = n^2"; |
68 also; have "... + 2 * n + 1 = (n + 1)^2"; by simp; |
68 also; have "... + 2 * n + 1 = (n + 1)^2"; by simp; |
69 finally; show "??P (Suc n)"; by simp; |
69 finally; show "?P (Suc n)"; by simp; |
70 qed; |
70 qed; |
71 |
71 |
72 theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" |
72 theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" |
73 (is "??P n" is "??S n = _"); |
73 (is "?P n" is "?S n = _"); |
74 proof (induct n); |
74 proof (induct n); |
75 show "??P 0"; by simp; |
75 show "?P 0"; by simp; |
76 |
76 |
77 fix n; |
77 fix n; |
78 have "??S (n + 1) = ??S n + 6 * (n + 1)^2"; by simp; |
78 have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp; |
79 also; assume "??S n = n * (n + 1) * (2 * n + 1)"; |
79 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)"; by simp; |
80 also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp; |
81 finally; show "??P (Suc n)"; by simp; |
81 finally; show "?P (Suc n)"; by simp; |
82 qed; |
82 qed; |
83 |
83 |
84 theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" |
84 theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" |
85 (is "??P n" is "??S n = _"); |
85 (is "?P n" is "?S n = _"); |
86 proof (induct n); |
86 proof (induct n); |
87 show "??P 0"; by simp; |
87 show "?P 0"; by simp; |
88 |
88 |
89 fix n; |
89 fix n; |
90 have "??S (n + 1) = ??S n + 4 * (n + 1)^3"; by simp; |
90 have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp; |
91 also; assume "??S n = (n * (n + 1))^2"; |
91 also; assume "?S n = (n * (n + 1))^2"; |
92 also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp; |
92 also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp; |
93 finally; show "??P (Suc n)"; by simp; |
93 finally; show "?P (Suc n)"; by simp; |
94 qed; |
94 qed; |
95 |
95 |
96 |
96 |
97 end; |
97 end; |