added Isar_examples/NatSum.thy;
authorwenzelm
Tue Apr 27 15:10:36 1999 +0200 (1999-04-27)
changeset 65266b64d1454ee3
parent 6525 bb2c4ddd8e5e
child 6527 f7a7ac2b9926
added Isar_examples/NatSum.thy;
src/HOL/IsaMakefile
src/HOL/Isar_examples/NatSum.thy
src/HOL/Isar_examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Apr 27 13:05:52 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Apr 27 15:10:36 1999 +0200
     1.3 @@ -326,8 +326,8 @@
     1.4  
     1.5  $(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
     1.6    Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
     1.7 -  Isar_examples/ExprCompiler.thy Isar_examples/Peirce.thy \
     1.8 -  Isar_examples/ROOT.ML
     1.9 +  Isar_examples/ExprCompiler.thy Isar_examples/NatSum.thy \
    1.10 +  Isar_examples/Peirce.thy Isar_examples/ROOT.ML
    1.11  	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
    1.12  
    1.13  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Isar_examples/NatSum.thy	Tue Apr 27 15:10:36 1999 +0200
     2.3 @@ -0,0 +1,80 @@
     2.4 +(*  Title:      HOL/Isar_examples/NatSum.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow and Markus Wenzel
     2.7 +*)
     2.8 +
     2.9 +theory NatSum = Main:;
    2.10 +
    2.11 +section "Summing natural numbers";
    2.12 +
    2.13 +text "A summation operator: sum f (n+1) is the sum of all f(i), i=0...n.";
    2.14 +
    2.15 +consts
    2.16 +  sum	:: "[nat => nat, nat] => nat";
    2.17 +
    2.18 +primrec 
    2.19 +  "sum f 0 = 0"
    2.20 +  "sum f (Suc n) = f n + sum f n";
    2.21 +
    2.22 +
    2.23 +(*theorems [simp] = add_assoc add_commute add_left_commute add_mult_distrib add_mult_distrib2;*)
    2.24 +
    2.25 +
    2.26 +subsection "The sum of the first n positive integers equals n(n+1)/2";
    2.27 +
    2.28 +text "Emulate Isabelle proof script:";
    2.29 +
    2.30 +(*
    2.31 +  Goal "2*sum (%i. i) (Suc n) = n*Suc(n)";
    2.32 +  by (Simp_tac 1);
    2.33 +  by (induct_tac "n" 1);
    2.34 +  by (Simp_tac 1);
    2.35 +  by (Asm_simp_tac 1);
    2.36 +  qed "sum_of_naturals";
    2.37 +*)
    2.38 +
    2.39 +theorem "2 * sum (%i. i) (Suc n) = n * Suc n";
    2.40 +proof same;
    2.41 +  refine simp_tac;
    2.42 +  refine (induct n);
    2.43 +  refine simp_tac;
    2.44 +  refine asm_simp_tac;
    2.45 +qed_with sum_of_naturals;
    2.46 +
    2.47 +
    2.48 +text "Proper Isabelle/Isar proof expressing the same reasoning (which
    2.49 +  is apparently not the most natural one):";
    2.50 +
    2.51 +theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n";
    2.52 +proof simp;
    2.53 +  show "n + (sum (%i. i) n + sum (%i. i) n) = n * n" (is "??P n");
    2.54 +  proof (induct ??P n);
    2.55 +    show "??P 0"; by simp;
    2.56 +    fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp);
    2.57 +  qed;
    2.58 +qed;
    2.59 +
    2.60 +
    2.61 +subsection "The sum of the first n odd numbers equals n squared";
    2.62 +
    2.63 +text "First version: `proof-by-induction'";
    2.64 +
    2.65 +theorem sum_of_odds: "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
    2.66 +proof (induct n);
    2.67 +  show "??P 0"; by simp;
    2.68 +  fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp add: hyp);
    2.69 +qed;
    2.70 +
    2.71 +text "The second version tells more about what is going on during the
    2.72 +induction.";
    2.73 +
    2.74 +theorem sum_of_odds': "sum (%i. Suc (i + i)) n = n * n" (is "??P n");
    2.75 +proof (induct n);
    2.76 +  show "??P 0" (is "sum (%i. Suc (i + i)) 0 = 0 * 0"); by simp;
    2.77 +  fix m; assume hyp: "??P m";
    2.78 +  show "??P (Suc m)" (is "sum (%i. Suc (i + i)) (Suc m) = Suc m * Suc m");
    2.79 +    by (simp, rule hyp);
    2.80 +qed;
    2.81 +
    2.82 +
    2.83 +end;
     3.1 --- a/src/HOL/Isar_examples/ROOT.ML	Tue Apr 27 13:05:52 1999 +0200
     3.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Tue Apr 27 15:10:36 1999 +0200
     3.3 @@ -9,3 +9,5 @@
     3.4  use_thy "Peirce";
     3.5  use_thy "Cantor";
     3.6  use_thy "ExprCompiler";
     3.7 +use_thy "NatSum";
     3.8 +