--- 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
--- /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;
--- 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";
+