# HG changeset patch
# User wenzelm
# Date 936278719 -7200
# Node ID e5356e73f57ab49cdfbdd4e4cd5340325486939d
# Parent  2d2849258e3fa960b8e205f419ef9f54e8a42bf2
renamed NatSum to Summation;

diff -r 2d2849258e3f -r e5356e73f57a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Sep 02 15:24:56 1999 +0200
+++ b/src/HOL/IsaMakefile	Thu Sep 02 15:25:19 1999 +0200
@@ -342,8 +342,8 @@
   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \
   Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \
-  Isar_examples/MutilatedCheckerboard.thy Isar_examples/NatSum.thy \
-  Isar_examples/Peirce.thy Isar_examples/ROOT.ML
+  Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
+  Isar_examples/Summation.thy Isar_examples/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
 
 
diff -r 2d2849258e3f -r e5356e73f57a src/HOL/Isar_examples/NatSum.thy
--- a/src/HOL/Isar_examples/NatSum.thy	Thu Sep 02 15:24:56 1999 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(*  Title:      HOL/Isar_examples/NatSum.thy
-    ID:         $Id$
-    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";
-
-primrec
-  "sum f 0 = 0"
-  "sum f (Suc n) = f n + sum f n";
-
-syntax
-  "_SUM" :: "idt => nat => nat => nat"       ("SUM _ < _. _" [0, 0, 10] 10);
-translations
-  "SUM i < k. b" == "sum (%i. b) k";
-
-
-subsection {* Summation laws *};
-
-(* FIXME fails with binary numeral (why!?) *)
-
-syntax
-  "3" :: nat  ("3")
-  "4" :: nat  ("4")
-  "6" :: nat  ("6");
-
-translations
-  "3" == "Suc 2"
-  "4" == "Suc 3"
-  "6" == "Suc (Suc 4)";
-
-
-(* 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;
-
-
-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;
-
-  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;
-
-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 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;
-
-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"; 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;
-
-
-end;
diff -r 2d2849258e3f -r e5356e73f57a src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Thu Sep 02 15:24:56 1999 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Thu Sep 02 15:25:19 1999 +0200
@@ -10,9 +10,7 @@
 time_use_thy "Cantor";
 time_use_thy "ExprCompiler";
 time_use_thy "Group";
-time_use_thy "NatSum";
+time_use_thy "Summation";
 time_use_thy "KnasterTarski";
 time_use_thy "MutilatedCheckerboard";
-
-add_path "../Induct";
-time_use_thy "MultisetOrder";
+with_path "../Induct" time_use_thy "MultisetOrder";
diff -r 2d2849258e3f -r e5356e73f57a src/HOL/Isar_examples/Summation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Summation.thy	Thu Sep 02 15:25:19 1999 +0200
@@ -0,0 +1,97 @@
+(*  Title:      HOL/Isar_examples/Summation.thy
+    ID:         $Id$
+    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 Summation = 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";
+
+primrec
+  "sum f 0 = 0"
+  "sum f (Suc n) = f n + sum f n";
+
+syntax
+  "_SUM" :: "idt => nat => nat => nat"       ("SUM _ < _. _" [0, 0, 10] 10);
+translations
+  "SUM i < k. b" == "sum (%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;
+
+
+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;
+
+  fix n;
+  have "??S (n + 1) = ??S n + 2 * (n + 1)"; by simp;
+  also; assume "??S 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 "??S n = _");
+proof (induct n);
+  show "??P 0"; by simp;
+
+  fix n;
+  have "??S (n + 1) = ??S n + 2 * n + 1"; by simp;
+  also; assume "??S n = n^2";
+  also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
+  finally; show "??P (Suc n)"; by simp;
+qed;
+
+theorem sum_of_squares: "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;
+  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;
+  finally; show "??P (Suc n)"; by simp;
+qed;
+
+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;
+
+  fix n;
+  have "??S (n + 1) = ??S n + 4 * (n + 1)^3"; by simp;
+  also; assume "??S 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;
+
+
+end;