# HG changeset patch
# User wenzelm
# Date 925218636 -7200
# Node ID 6b64d1454ee34b8da31e93d2c22bd4acc8ec07f7
# Parent  bb2c4ddd8e5e1182d13585edb13460e2d35d9044
added Isar_examples/NatSum.thy;

diff -r bb2c4ddd8e5e -r 6b64d1454ee3 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Apr 27 13:05:52 1999 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 27 15:10:36 1999 +0200
@@ -326,8 +326,8 @@
 
 $(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
-  Isar_examples/ExprCompiler.thy Isar_examples/Peirce.thy \
-  Isar_examples/ROOT.ML
+  Isar_examples/ExprCompiler.thy Isar_examples/NatSum.thy \
+  Isar_examples/Peirce.thy Isar_examples/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
 
 
diff -r bb2c4ddd8e5e -r 6b64d1454ee3 src/HOL/Isar_examples/NatSum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/NatSum.thy	Tue Apr 27 15:10:36 1999 +0200
@@ -0,0 +1,80 @@
+(*  Title:      HOL/Isar_examples/NatSum.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow and Markus Wenzel
+*)
+
+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";
+
+
+(*theorems [simp] = add_assoc add_commute add_left_commute add_mult_distrib add_mult_distrib2;*)
+
+
+subsection "The sum of the first n positive integers equals n(n+1)/2";
+
+text "Emulate Isabelle proof script:";
+
+(*
+  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";
+*)
+
+theorem "2 * sum (%i. i) (Suc n) = n * Suc n";
+proof same;
+  refine simp_tac;
+  refine (induct n);
+  refine simp_tac;
+  refine asm_simp_tac;
+qed_with sum_of_naturals;
+
+
+text "Proper Isabelle/Isar proof expressing the same reasoning (which
+  is apparently not the most natural one):";
+
+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;
+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");
+proof (induct n);
+  show "??P 0"; by simp;
+  fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp add: hyp);
+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");
+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);
+qed;
+
+
+end;
diff -r bb2c4ddd8e5e -r 6b64d1454ee3 src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Tue Apr 27 13:05:52 1999 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Tue Apr 27 15:10:36 1999 +0200
@@ -9,3 +9,5 @@
 use_thy "Peirce";
 use_thy "Cantor";
 use_thy "ExprCompiler";
+use_thy "NatSum";
+