--- a/src/HOL/Isar_examples/Summation.thy Wed Mar 02 10:33:10 2005 +0100
+++ b/src/HOL/Isar_examples/Summation.thy Wed Mar 02 12:06:15 2005 +0100
@@ -5,7 +5,11 @@
header {* Summing natural numbers *}
-theory Summation = Main:
+theory Summation
+imports Main
+begin
+
+declare setsum_op_ivl_Suc [simp] setsum_cl_ivl_Suc [simp]
text_raw {*
\footnote{This example is somewhat reminiscent of the
@@ -31,7 +35,7 @@
*}
theorem sum_of_naturals:
- "2 * (\<Sum>i::nat < n + 1. i) = n * (n + 1)"
+ "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
@@ -86,7 +90,7 @@
*}
theorem sum_of_odds:
- "(\<Sum>i::nat < n. 2 * i + 1) = n^Suc (Suc 0)"
+ "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
@@ -106,7 +110,7 @@
lemmas distrib = add_mult_distrib add_mult_distrib2
theorem sum_of_squares:
- "6 * (\<Sum>i::nat < n + 1. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
+ "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by simp
@@ -119,7 +123,7 @@
qed
theorem sum_of_cubes:
- "4 * (\<Sum>i::nat < n + 1. i^3) = (n * (n + 1))^Suc (Suc 0)"
+ "4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"
(is "?P n" is "?S n = _")
proof (induct n)
show "?P 0" by (simp add: power_eq_if)