renamed NatSum to Summation;
authorwenzelm
Thu Sep 02 15:25:19 1999 +0200 (1999-09-02)
changeset 7443e5356e73f57a
parent 7442 2d2849258e3f
child 7444 ee17ad649c26
renamed NatSum to Summation;
src/HOL/IsaMakefile
src/HOL/Isar_examples/NatSum.thy
src/HOL/Isar_examples/ROOT.ML
src/HOL/Isar_examples/Summation.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 02 15:24:56 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Sep 02 15:25:19 1999 +0200
     1.3 @@ -342,8 +342,8 @@
     1.4    Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
     1.5    Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \
     1.6    Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \
     1.7 -  Isar_examples/MutilatedCheckerboard.thy Isar_examples/NatSum.thy \
     1.8 -  Isar_examples/Peirce.thy Isar_examples/ROOT.ML
     1.9 +  Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
    1.10 +  Isar_examples/Summation.thy Isar_examples/ROOT.ML
    1.11  	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
    1.12  
    1.13  
     2.1 --- a/src/HOL/Isar_examples/NatSum.thy	Thu Sep 02 15:24:56 1999 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,102 +0,0 @@
     2.4 -(*  Title:      HOL/Isar_examples/NatSum.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Markus Wenzel
     2.7 -
     2.8 -Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the
     2.9 -original scripts).
    2.10 -
    2.11 -Demonstrates mathematical induction together with calculational proof.
    2.12 -*)
    2.13 -
    2.14 -
    2.15 -theory NatSum = Main:;
    2.16 -
    2.17 -
    2.18 -section {* Summing natural numbers *};
    2.19 -
    2.20 -text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *};
    2.21 -
    2.22 -consts
    2.23 -  sum   :: "[nat => nat, nat] => nat";
    2.24 -
    2.25 -primrec
    2.26 -  "sum f 0 = 0"
    2.27 -  "sum f (Suc n) = f n + sum f n";
    2.28 -
    2.29 -syntax
    2.30 -  "_SUM" :: "idt => nat => nat => nat"       ("SUM _ < _. _" [0, 0, 10] 10);
    2.31 -translations
    2.32 -  "SUM i < k. b" == "sum (%i. b) k";
    2.33 -
    2.34 -
    2.35 -subsection {* Summation laws *};
    2.36 -
    2.37 -(* FIXME fails with binary numeral (why!?) *)
    2.38 -
    2.39 -syntax
    2.40 -  "3" :: nat  ("3")
    2.41 -  "4" :: nat  ("4")
    2.42 -  "6" :: nat  ("6");
    2.43 -
    2.44 -translations
    2.45 -  "3" == "Suc 2"
    2.46 -  "4" == "Suc 3"
    2.47 -  "6" == "Suc (Suc 4)";
    2.48 -
    2.49 -
    2.50 -(* FIXME bind_thms in Arith.ML *)
    2.51 -theorems mult_distrib [simp] = add_mult_distrib add_mult_distrib2;
    2.52 -theorems mult_ac [simp] = mult_assoc mult_commute mult_left_commute;
    2.53 -
    2.54 -
    2.55 -theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
    2.56 -  (is "??P n" is "??L n = _");
    2.57 -proof (induct n);
    2.58 -  show "??P 0"; by simp;
    2.59 -
    2.60 -  fix n;
    2.61 -  have "??L (n + 1) = ??L n + 2 * (n + 1)"; by simp;
    2.62 -  also; assume "??L n = n * (n + 1)";
    2.63 -  also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
    2.64 -  finally; show "??P (Suc n)"; by simp;
    2.65 -qed;
    2.66 -
    2.67 -theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
    2.68 -  (is "??P n" is "??L n = _");
    2.69 -proof (induct n);
    2.70 -  show "??P 0"; by simp;
    2.71 -
    2.72 -  fix n;
    2.73 -  have "??L (n + 1) = ??L n + 2 * n + 1"; by simp;
    2.74 -  also; assume "??L n = n^2";
    2.75 -  also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
    2.76 -  finally; show "??P (Suc n)"; by simp;
    2.77 -qed;
    2.78 -
    2.79 -theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
    2.80 -  (is "??P n" is "??L n = _");
    2.81 -proof (induct n);
    2.82 -  show "??P 0"; by simp;
    2.83 -
    2.84 -  fix n;
    2.85 -  have "??L (n + 1) = ??L n + 6 * (n + 1)^2"; by simp;
    2.86 -  also; assume "??L n = n * (n + 1) * (2 * n + 1)";
    2.87 -  also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
    2.88 -     (* FIXME #6: arith and simp fail!! *)
    2.89 -  finally; show "??P (Suc n)"; by simp;
    2.90 -qed;
    2.91 -
    2.92 -theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
    2.93 -  (is "??P n" is "??L n = _");
    2.94 -proof (induct n);
    2.95 -  show "??P 0"; by simp;
    2.96 -
    2.97 -  fix n;
    2.98 -  have "??L (n + 1) = ??L n + 4 * (n + 1)^3"; by simp;
    2.99 -  also; assume "??L n = (n * (n + 1))^2";
   2.100 -  also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
   2.101 -  finally; show "??P (Suc n)"; by simp;
   2.102 -qed;
   2.103 -
   2.104 -
   2.105 -end;
     3.1 --- a/src/HOL/Isar_examples/ROOT.ML	Thu Sep 02 15:24:56 1999 +0200
     3.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Thu Sep 02 15:25:19 1999 +0200
     3.3 @@ -10,9 +10,7 @@
     3.4  time_use_thy "Cantor";
     3.5  time_use_thy "ExprCompiler";
     3.6  time_use_thy "Group";
     3.7 -time_use_thy "NatSum";
     3.8 +time_use_thy "Summation";
     3.9  time_use_thy "KnasterTarski";
    3.10  time_use_thy "MutilatedCheckerboard";
    3.11 -
    3.12 -add_path "../Induct";
    3.13 -time_use_thy "MultisetOrder";
    3.14 +with_path "../Induct" time_use_thy "MultisetOrder";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Isar_examples/Summation.thy	Thu Sep 02 15:25:19 1999 +0200
     4.3 @@ -0,0 +1,97 @@
     4.4 +(*  Title:      HOL/Isar_examples/Summation.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Markus Wenzel
     4.7 +
     4.8 +Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the
     4.9 +original scripts).  Demonstrates mathematical induction together with
    4.10 +calculational proof.
    4.11 +*)
    4.12 +
    4.13 +
    4.14 +theory Summation = Main:;
    4.15 +
    4.16 +
    4.17 +section {* Summing natural numbers *};
    4.18 +
    4.19 +text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *};
    4.20 +
    4.21 +consts
    4.22 +  sum   :: "[nat => nat, nat] => nat";
    4.23 +
    4.24 +primrec
    4.25 +  "sum f 0 = 0"
    4.26 +  "sum f (Suc n) = f n + sum f n";
    4.27 +
    4.28 +syntax
    4.29 +  "_SUM" :: "idt => nat => nat => nat"       ("SUM _ < _. _" [0, 0, 10] 10);
    4.30 +translations
    4.31 +  "SUM i < k. b" == "sum (%i. b) k";
    4.32 +
    4.33 +
    4.34 +subsection {* Summation laws *};
    4.35 +
    4.36 +(* FIXME binary arithmetic does not yet work here *)
    4.37 +
    4.38 +syntax
    4.39 +  "3" :: nat  ("3")
    4.40 +  "4" :: nat  ("4")
    4.41 +  "6" :: nat  ("6");
    4.42 +
    4.43 +translations
    4.44 +  "3" == "Suc 2"
    4.45 +  "4" == "Suc 3"
    4.46 +  "6" == "Suc (Suc 4)";
    4.47 +
    4.48 +theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
    4.49 +
    4.50 +
    4.51 +theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
    4.52 +  (is "??P n" is "??S n = _");
    4.53 +proof (induct n);
    4.54 +  show "??P 0"; by simp;
    4.55 +
    4.56 +  fix n;
    4.57 +  have "??S (n + 1) = ??S n + 2 * (n + 1)"; by simp;
    4.58 +  also; assume "??S n = n * (n + 1)";
    4.59 +  also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
    4.60 +  finally; show "??P (Suc n)"; by simp;
    4.61 +qed;
    4.62 +
    4.63 +theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
    4.64 +  (is "??P n" is "??S n = _");
    4.65 +proof (induct n);
    4.66 +  show "??P 0"; by simp;
    4.67 +
    4.68 +  fix n;
    4.69 +  have "??S (n + 1) = ??S n + 2 * n + 1"; by simp;
    4.70 +  also; assume "??S n = n^2";
    4.71 +  also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
    4.72 +  finally; show "??P (Suc n)"; by simp;
    4.73 +qed;
    4.74 +
    4.75 +theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
    4.76 +  (is "??P n" is "??S n = _");
    4.77 +proof (induct n);
    4.78 +  show "??P 0"; by simp;
    4.79 +
    4.80 +  fix n;
    4.81 +  have "??S (n + 1) = ??S n + 6 * (n + 1)^2"; by simp;
    4.82 +  also; assume "??S n = n * (n + 1) * (2 * n + 1)";
    4.83 +  also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
    4.84 +  finally; show "??P (Suc n)"; by simp;
    4.85 +qed;
    4.86 +
    4.87 +theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
    4.88 +  (is "??P n" is "??S n = _");
    4.89 +proof (induct n);
    4.90 +  show "??P 0"; by simp;
    4.91 +
    4.92 +  fix n;
    4.93 +  have "??S (n + 1) = ??S n + 4 * (n + 1)^3"; by simp;
    4.94 +  also; assume "??S n = (n * (n + 1))^2";
    4.95 +  also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
    4.96 +  finally; show "??P (Suc n)"; by simp;
    4.97 +qed;
    4.98 +
    4.99 +
   4.100 +end;