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;
```