src/HOL/Isar_examples/Summation.thy

--- a/src/HOL/Isar_examples/Summation.thy	Fri May 05 22:29:02 2000 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Fri May 05 22:30:14 2000 +0200
@@ -34,35 +34,20 @@
 *};
 
 consts
-  sum :: "[nat => nat, nat] => nat";
+  sum :: "(nat => nat) => nat => nat";
 
 primrec
   "sum f 0 = 0"
   "sum f (Suc n) = f n + sum f n";
 
 syntax
-  "_SUM" :: "[idt, nat, nat] => nat"
+  "_SUM" :: "idt => nat => nat => nat"
     ("SUM _ < _. _" [0, 0, 10] 10);
 translations
   "SUM i < k. b" == "sum (\\<lambda>i. b) k";
 
 
 subsection {* Summation laws *};
-(*<*)
-(* FIXME binary arithmetic does not yet work here *)
-
-syntax
-  "3" :: nat  ("3")
-  "4" :: nat  ("4")
-  "6" :: nat  ("6");
-
-translations
-  "3" == "Suc 2"
-  "4" == "Suc 3"
-  "6" == "Suc (Suc 4)";
-
-theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
-(*>*)
 
 text {*
  The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
@@ -139,31 +124,39 @@
   finally; show "?P (Suc n)"; by simp;
 qed;
 
+text {*
+ Subsequently we require some additional tweaking of Isabelle built-in
+ arithmetic simplifications, such as bringing in distributivity by
+ hand.
+*};
+
+lemmas distrib = add_mult_distrib add_mult_distrib2;
+
 theorem sum_of_squares:
-  "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
+  "#6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
   (is "?P n" is "?S n = _");
 proof (induct n);
   show "?P 0"; by simp;
 
   fix n;
-  have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
+  have "?S (n + 1) = ?S n + #6 * (n + 1)^2"; by (simp add: distrib);
   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 add: distrib);
   finally; show "?P (Suc n)"; by simp;
 qed;
 
 theorem sum_of_cubes:
-  "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
+  "#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;
+  show "?P 0"; by (simp add: power_eq_if);
 
   fix n;
-  have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
+  have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"; by (simp add: power_eq_if distrib);
   also; assume "?S n = (n * (n + 1))^2";
-  also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2";
-    by simp;
+  also; have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2";
+    by (simp add: power_eq_if distrib);
   finally; show "?P (Suc n)"; by simp;
 qed;