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