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