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