--- a/src/HOL/Isar_examples/Summation.thy Fri Oct 08 15:08:47 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Fri Oct 08 15:09:14 1999 +0200
@@ -22,13 +22,16 @@
"sum f (Suc n) = f n + sum f n";
syntax
- "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10);
+ "_SUM" :: "idt => nat => nat => nat"
+ ("SUM _ < _. _" [0, 0, 10] 10);
translations
"SUM i < k. b" == "sum (%i. b) k";
subsection {* Summation laws *};
+verbatim {* \begin{comment} *};
+
(* FIXME binary arithmetic does not yet work here *)
syntax
@@ -43,8 +46,11 @@
theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
+verbatim {* \end{comment} *};
-theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
+
+theorem sum_of_naturals:
+ "2 * (SUM i < n + 1. i) = n * (n + 1)"
(is "?P n" is "?S n = _");
proof (induct n);
show "?P 0"; by simp;
@@ -56,7 +62,8 @@
finally; show "?P (Suc n)"; by simp;
qed;
-theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
+theorem sum_of_odds:
+ "(SUM i < n. 2 * i + 1) = n^2"
(is "?P n" is "?S n = _");
proof (induct n);
show "?P 0"; by simp;
@@ -77,12 +84,13 @@
fix n;
have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
also; assume "?S n = n * (n + 1) * (2 * n + 1)";
- also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)";
- by simp;
+ also; have "... + 6 * (n + 1)^2 =
+ (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
finally; show "?P (Suc n)"; by simp;
qed;
-theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
+theorem sum_of_cubes:
+ "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
(is "?P n" is "?S n = _");
proof (induct n);
show "?P 0"; by simp;