proper calculation / induction;

--- a/src/HOL/Isar_examples/NatSum.thy	Mon Aug 30 20:30:39 1999 +0200
+++ b/src/HOL/Isar_examples/NatSum.thy	Mon Aug 30 23:19:13 1999 +0200
@@ -1,79 +1,101 @@
 (*  Title:      HOL/Isar_examples/NatSum.thy
     ID:         $Id$
-    Author:     Tobias Nipkow and Markus Wenzel
+    Author:     Markus Wenzel
+
+Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the
+original scripts).
+
+Demonstrates mathematical induction together with calculational proof.
 *)
 
+
 theory NatSum = Main:;
 
+
 section {* Summing natural numbers *};
 
 text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *};
 
 consts
-  sum	:: "[nat => nat, nat] => nat";
+  sum   :: "[nat => nat, nat] => nat";
 
-primrec 
+primrec
   "sum f 0 = 0"
   "sum f (Suc n) = f n + sum f n";
 
-
-(*theorems [simp] = add_assoc add_commute add_left_commute add_mult_distrib add_mult_distrib2;*)
+syntax
+  "_SUM" :: "idt => nat => nat => nat"       ("SUM _ < _. _" [0, 0, 10] 10);
+translations
+  "SUM i < k. b" == "sum (%i. b) k";
 
 
-subsection {* The sum of the first n positive integers equals n(n+1)/2 *};
+subsection {* Summation laws *};
+
+(* FIXME fails with binary numeral (why!?) *)
 
-text {* Emulate Isabelle proof script: *};
+syntax
+  "3" :: nat  ("3")
+  "4" :: nat  ("4")
+  "6" :: nat  ("6");
 
-(*
-  Goal "2*sum (%i. i) (Suc n) = n*Suc(n)";
-  by (Simp_tac 1);
-  by (induct_tac "n" 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
-  qed "sum_of_naturals";
-*)
+translations
+  "3" == "Suc 2"
+  "4" == "Suc 3"
+  "6" == "Suc (Suc 4)";
 
-theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n";
-proof -;
-  apply simp_tac;
-  apply (induct n);
-  apply simp_tac;
-  apply asm_simp_tac;
-qed;
+
+(* FIXME bind_thms in Arith.ML *)
+theorems mult_distrib [simp] = add_mult_distrib add_mult_distrib2;
+theorems mult_ac [simp] = mult_assoc mult_commute mult_left_commute;
 
 
-text {* Proper Isabelle/Isar proof expressing the same reasoning (which
-  is apparently not the most natural one): *};
+theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
+  (is "??P n" is "??L n = _");
+proof (induct n);
+  show "??P 0"; by simp;
 
-theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n";
-proof simp;
-  show "n + (sum (%i. i) n + sum (%i. i) n) = n * n" (is "??P n");
-  proof (induct ??P n);
-    show "??P 0"; by simp;
-    fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp);
-  qed;
+  fix n;
+  have "??L (n + 1) = ??L n + 2 * (n + 1)"; by simp;
+  also; assume "??L n = n * (n + 1)";
+  also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
+  finally; show "??P (Suc n)"; by simp;
+qed;
+
+theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
+  (is "??P n" is "??L n = _");
+proof (induct n);
+  show "??P 0"; by simp;
+
+  fix n;
+  have "??L (n + 1) = ??L n + 2 * n + 1"; by simp;
+  also; assume "??L n = n^2";
+  also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
+  finally; show "??P (Suc n)"; by simp;
 qed;
 
-
-subsection {* The sum of the first n odd numbers equals n squared *};
-
-text {* First version: `proof-by-induction' *};
-
-theorem sum_of_odds: "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
+theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
+  (is "??P n" is "??L n = _");
 proof (induct n);
   show "??P 0"; by simp;
-  fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp);
+
+  fix n;
+  have "??L (n + 1) = ??L n + 6 * (n + 1)^2"; by simp;
+  also; assume "??L n = n * (n + 1) * (2 * n + 1)";
+  also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
+     (* FIXME #6: arith and simp fail!! *)
+  finally; show "??P (Suc n)"; by simp;
 qed;
 
-text {* The second version tells more about what is going on during the
-induction. *};
-
-theorem sum_of_odds': "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
+theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
+  (is "??P n" is "??L n = _");
 proof (induct n);
-  show "??P 0" (is "sum (%i. Suc (i + i)) 0 = 0 * 0"); by simp;
-  fix m; assume hyp: "??P m";
-  show "??P (Suc m)" (is "sum (%i. Suc (i + i)) (Suc m) = Suc m * Suc m");
-    by (simp, rule hyp);
+  show "??P 0"; by simp;
+
+  fix n;
+  have "??L (n + 1) = ??L n + 4 * (n + 1)^3"; by simp;
+  also; assume "??L n = (n * (n + 1))^2";
+  also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
+  finally; show "??P (Suc n)"; by simp;
 qed;