src/HOL/Isar_examples/Summation.thy
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 7443 e5356e73f57a
child 7748 5b9c45b21782
permissions -rw-r--r--
replaced ?? by ?;
     1 (*  Title:      HOL/Isar_examples/Summation.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel
     4 
     5 Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the
     6 original scripts).  Demonstrates mathematical induction together with
     7 calculational proof.
     8 *)
     9 
    10 
    11 theory Summation = Main:;
    12 
    13 
    14 section {* Summing natural numbers *};
    15 
    16 text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *};
    17 
    18 consts
    19   sum   :: "[nat => nat, nat] => nat";
    20 
    21 primrec
    22   "sum f 0 = 0"
    23   "sum f (Suc n) = f n + sum f n";
    24 
    25 syntax
    26   "_SUM" :: "idt => nat => nat => nat"       ("SUM _ < _. _" [0, 0, 10] 10);
    27 translations
    28   "SUM i < k. b" == "sum (%i. b) k";
    29 
    30 
    31 subsection {* Summation laws *};
    32 
    33 (* FIXME binary arithmetic does not yet work here *)
    34 
    35 syntax
    36   "3" :: nat  ("3")
    37   "4" :: nat  ("4")
    38   "6" :: nat  ("6");
    39 
    40 translations
    41   "3" == "Suc 2"
    42   "4" == "Suc 3"
    43   "6" == "Suc (Suc 4)";
    44 
    45 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
    46 
    47 
    48 theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"
    49   (is "?P n" is "?S n = _");
    50 proof (induct n);
    51   show "?P 0"; by simp;
    52 
    53   fix n;
    54   have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp;
    55   also; assume "?S n = n * (n + 1)";
    56   also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
    57   finally; show "?P (Suc n)"; by simp;
    58 qed;
    59 
    60 theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"
    61   (is "?P n" is "?S n = _");
    62 proof (induct n);
    63   show "?P 0"; by simp;
    64 
    65   fix n;
    66   have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;
    67   also; assume "?S n = n^2";
    68   also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
    69   finally; show "?P (Suc n)"; by simp;
    70 qed;
    71 
    72 theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
    73   (is "?P n" is "?S n = _");
    74 proof (induct n);
    75   show "?P 0"; by simp;
    76 
    77   fix n;
    78   have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
    79   also; assume "?S n = n * (n + 1) * (2 * n + 1)";
    80   also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
    81   finally; show "?P (Suc n)"; by simp;
    82 qed;
    83 
    84 theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
    85   (is "?P n" is "?S n = _");
    86 proof (induct n);
    87   show "?P 0"; by simp;
    88 
    89   fix n;
    90   have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
    91   also; assume "?S n = (n * (n + 1))^2";
    92   also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;
    93   finally; show "?P (Suc n)"; by simp;
    94 qed;
    95 
    96 
    97 end;