src/HOL/ex/NatSum.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 16993 2ec0b8159e8e child 21144 17b0b4c6491b permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     1 (*  Title: HOL/ex/NatSum.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Tobias Nipkow
```
```     4 *)
```
```     5
```
```     6 header {* Summing natural numbers *}
```
```     7
```
```     8 theory NatSum imports Main begin
```
```     9
```
```    10 text {*
```
```    11   Summing natural numbers, squares, cubes, etc.
```
```    12
```
```    13   Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
```
```    14   \url{http://www.research.att.com/~njas/sequences/}.
```
```    15 *}
```
```    16
```
```    17 lemmas [simp] =
```
```    18   left_distrib right_distrib
```
```    19   left_diff_distrib right_diff_distrib --{*for true subtraction*}
```
```    20   diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
```
```    21
```
```    22 text {*
```
```    23   \medskip The sum of the first @{text n} odd numbers equals @{text n}
```
```    24   squared.
```
```    25 *}
```
```    26
```
```    27 lemma sum_of_odds: "(\<Sum>i=0..<n. Suc (i + i)) = n * n"
```
```    28   by (induct n) auto
```
```    29
```
```    30
```
```    31 text {*
```
```    32   \medskip The sum of the first @{text n} odd squares.
```
```    33 *}
```
```    34
```
```    35 lemma sum_of_odd_squares:
```
```    36   "3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)"
```
```    37   by (induct n) auto
```
```    38
```
```    39
```
```    40 text {*
```
```    41   \medskip The sum of the first @{text n} odd cubes
```
```    42 *}
```
```    43
```
```    44 lemma sum_of_odd_cubes:
```
```    45   "(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
```
```    46     n * n * (2 * n * n - 1)"
```
```    47   by (induct n) auto
```
```    48
```
```    49 text {*
```
```    50   \medskip The sum of the first @{text n} positive integers equals
```
```    51   @{text "n (n + 1) / 2"}.*}
```
```    52
```
```    53 lemma sum_of_naturals:
```
```    54     "2 * (\<Sum>i=0..n. i) = n * Suc n"
```
```    55   by (induct n) auto
```
```    56
```
```    57 lemma sum_of_squares:
```
```    58     "6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)"
```
```    59   by (induct n) auto
```
```    60
```
```    61 lemma sum_of_cubes:
```
```    62     "4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
```
```    63   by (induct n) auto
```
```    64
```
```    65
```
```    66 text {*
```
```    67   \medskip Sum of fourth powers: three versions.
```
```    68 *}
```
```    69
```
```    70 lemma sum_of_fourth_powers:
```
```    71   "30 * (\<Sum>i=0..n. i * i * i * i) =
```
```    72     n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
```
```    73   apply (induct n)
```
```    74    apply simp_all
```
```    75   apply (case_tac n)  -- {* eliminates the subtraction *}
```
```    76    apply (simp_all (no_asm_simp))
```
```    77   done
```
```    78
```
```    79 text {*
```
```    80   Two alternative proofs, with a change of variables and much more
```
```    81   subtraction, performed using the integers. *}
```
```    82
```
```    83 lemma int_sum_of_fourth_powers:
```
```    84   "30 * int (\<Sum>i=0..<m. i * i * i * i) =
```
```    85     int m * (int m - 1) * (int(2 * m) - 1) *
```
```    86     (int(3 * m * m) - int(3 * m) - 1)"
```
```    87   by (induct m) (simp_all add: int_mult)
```
```    88
```
```    89 lemma of_nat_sum_of_fourth_powers:
```
```    90   "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
```
```    91     of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
```
```    92     (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
```
```    93   by (induct m) simp_all
```
```    94
```
```    95
```
```    96 text {*
```
```    97   \medskip Sums of geometric series: @{text 2}, @{text 3} and the
```
```    98   general case.
```
```    99 *}
```
```   100
```
```   101 lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
```
```   102   by (induct n) (auto split: nat_diff_split)
```
```   103
```
```   104 lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
```
```   105   by (induct n) auto
```
```   106
```
```   107 lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
```
```   108   by (induct n) auto
```
```   109
```
```   110 end
```