equal
deleted
inserted
replaced
58 theorem sum_of_naturals: |
58 theorem sum_of_naturals: |
59 "2 * (SUM i < n + 1. i) = n * (n + 1)" |
59 "2 * (SUM i < n + 1. i) = n * (n + 1)" |
60 (is "?P n" is "?S n = _") |
60 (is "?P n" is "?S n = _") |
61 proof (induct n) |
61 proof (induct n) |
62 show "?P 0" by simp |
62 show "?P 0" by simp |
63 |
63 next |
64 fix n |
64 fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp |
65 have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp |
|
66 also assume "?S n = n * (n + 1)" |
65 also assume "?S n = n * (n + 1)" |
67 also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp |
66 also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp |
68 finally show "?P (Suc n)" by simp |
67 finally show "?P (Suc n)" by simp |
69 qed |
68 qed |
70 |
69 |
114 theorem sum_of_odds: |
113 theorem sum_of_odds: |
115 "(SUM i < n. 2 * i + 1) = n^2" |
114 "(SUM i < n. 2 * i + 1) = n^2" |
116 (is "?P n" is "?S n = _") |
115 (is "?P n" is "?S n = _") |
117 proof (induct n) |
116 proof (induct n) |
118 show "?P 0" by simp |
117 show "?P 0" by simp |
119 |
118 next |
120 fix n |
119 fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp |
121 have "?S (n + 1) = ?S n + 2 * n + 1" by simp |
|
122 also assume "?S n = n^2" |
120 also assume "?S n = n^2" |
123 also have "... + 2 * n + 1 = (n + 1)^2" by simp |
121 also have "... + 2 * n + 1 = (n + 1)^2" by simp |
124 finally show "?P (Suc n)" by simp |
122 finally show "?P (Suc n)" by simp |
125 qed |
123 qed |
126 |
124 |
135 theorem sum_of_squares: |
133 theorem sum_of_squares: |
136 "#6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" |
134 "#6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" |
137 (is "?P n" is "?S n = _") |
135 (is "?P n" is "?S n = _") |
138 proof (induct n) |
136 proof (induct n) |
139 show "?P 0" by simp |
137 show "?P 0" by simp |
140 |
138 next |
141 fix n |
139 fix n have "?S (n + 1) = ?S n + #6 * (n + 1)^2" by (simp add: distrib) |
142 have "?S (n + 1) = ?S n + #6 * (n + 1)^2" by (simp add: distrib) |
|
143 also assume "?S n = n * (n + 1) * (2 * n + 1)" |
140 also assume "?S n = n * (n + 1) * (2 * n + 1)" |
144 also have "... + #6 * (n + 1)^2 = |
141 also have "... + #6 * (n + 1)^2 = |
145 (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib) |
142 (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib) |
146 finally show "?P (Suc n)" by simp |
143 finally show "?P (Suc n)" by simp |
147 qed |
144 qed |
149 theorem sum_of_cubes: |
146 theorem sum_of_cubes: |
150 "#4 * (SUM i < n + 1. i^#3) = (n * (n + 1))^2" |
147 "#4 * (SUM i < n + 1. i^#3) = (n * (n + 1))^2" |
151 (is "?P n" is "?S n = _") |
148 (is "?P n" is "?S n = _") |
152 proof (induct n) |
149 proof (induct n) |
153 show "?P 0" by (simp add: power_eq_if) |
150 show "?P 0" by (simp add: power_eq_if) |
154 |
151 next |
155 fix n |
152 fix n have "?S (n + 1) = ?S n + #4 * (n + 1)^#3" |
156 have "?S (n + 1) = ?S n + #4 * (n + 1)^#3" |
|
157 by (simp add: power_eq_if distrib) |
153 by (simp add: power_eq_if distrib) |
158 also assume "?S n = (n * (n + 1))^2" |
154 also assume "?S n = (n * (n + 1))^2" |
159 also have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2" |
155 also have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2" |
160 by (simp add: power_eq_if distrib) |
156 by (simp add: power_eq_if distrib) |
161 finally show "?P (Suc n)" by simp |
157 finally show "?P (Suc n)" by simp |