src/HOL/ex/NatSum.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 40077 c8a9eaaa2f59
child 54703 499f92dc6e45
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
haftmann@28952
     1
(*  Title:  HOL/ex/NatSum.thy
haftmann@28952
     2
    Author: Tobias Nipkow
wenzelm@11024
     3
*)
wenzelm@11024
     4
wenzelm@11024
     5
header {* Summing natural numbers *}
wenzelm@11024
     6
wenzelm@21256
     7
theory NatSum imports Main Parity begin
wenzelm@11024
     8
wenzelm@11786
     9
text {*
wenzelm@11786
    10
  Summing natural numbers, squares, cubes, etc.
wenzelm@11786
    11
wenzelm@11786
    12
  Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
wenzelm@11786
    13
  \url{http://www.research.att.com/~njas/sequences/}.
wenzelm@11786
    14
*}
wenzelm@11786
    15
nipkow@15561
    16
lemmas [simp] =
nipkow@23477
    17
  ring_distribs
nipkow@15561
    18
  diff_mult_distrib diff_mult_distrib2 --{*for type nat*}
wenzelm@11024
    19
wenzelm@11024
    20
text {*
wenzelm@12023
    21
  \medskip The sum of the first @{text n} odd numbers equals @{text n}
wenzelm@11024
    22
  squared.
wenzelm@11024
    23
*}
wenzelm@11024
    24
paulson@16593
    25
lemma sum_of_odds: "(\<Sum>i=0..<n. Suc (i + i)) = n * n"
wenzelm@16993
    26
  by (induct n) auto
wenzelm@11024
    27
wenzelm@11024
    28
wenzelm@11024
    29
text {*
wenzelm@11024
    30
  \medskip The sum of the first @{text n} odd squares.
wenzelm@11024
    31
*}
wenzelm@11024
    32
wenzelm@11024
    33
lemma sum_of_odd_squares:
nipkow@15561
    34
  "3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)"
wenzelm@16993
    35
  by (induct n) auto
wenzelm@11024
    36
wenzelm@11024
    37
wenzelm@11024
    38
text {*
wenzelm@12023
    39
  \medskip The sum of the first @{text n} odd cubes
wenzelm@11024
    40
*}
wenzelm@11024
    41
wenzelm@11024
    42
lemma sum_of_odd_cubes:
nipkow@15561
    43
  "(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
wenzelm@11786
    44
    n * n * (2 * n * n - 1)"
wenzelm@16993
    45
  by (induct n) auto
wenzelm@11024
    46
wenzelm@11024
    47
text {*
wenzelm@12023
    48
  \medskip The sum of the first @{text n} positive integers equals
wenzelm@11024
    49
  @{text "n (n + 1) / 2"}.*}
wenzelm@11024
    50
wenzelm@11586
    51
lemma sum_of_naturals:
nipkow@15561
    52
    "2 * (\<Sum>i=0..n. i) = n * Suc n"
wenzelm@16993
    53
  by (induct n) auto
wenzelm@11024
    54
wenzelm@11586
    55
lemma sum_of_squares:
nipkow@15561
    56
    "6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)"
wenzelm@16993
    57
  by (induct n) auto
wenzelm@11024
    58
wenzelm@11586
    59
lemma sum_of_cubes:
nipkow@15561
    60
    "4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
wenzelm@16993
    61
  by (induct n) auto
wenzelm@11024
    62
nipkow@21144
    63
text{* \medskip A cute identity: *}
nipkow@21144
    64
nipkow@21144
    65
lemma sum_squared: "(\<Sum>i=0..n. i)^2 = (\<Sum>i=0..n::nat. i^3)"
nipkow@21144
    66
proof(induct n)
nipkow@21144
    67
  case 0 show ?case by simp
nipkow@21144
    68
next
nipkow@21144
    69
  case (Suc n)
nipkow@21144
    70
  have "(\<Sum>i = 0..Suc n. i)^2 =
nipkow@21144
    71
        (\<Sum>i = 0..n. i^3) + (2*(\<Sum>i = 0..n. i)*(n+1) + (n+1)^2)"
nipkow@21144
    72
    (is "_ = ?A + ?B")
nipkow@40077
    73
    using Suc by(simp add:eval_nat_numeral)
nipkow@21144
    74
  also have "?B = (n+1)^3"
nipkow@40077
    75
    using sum_of_naturals by(simp add:eval_nat_numeral)
nipkow@21144
    76
  also have "?A + (n+1)^3 = (\<Sum>i=0..Suc n. i^3)" by simp
nipkow@21144
    77
  finally show ?case .
nipkow@21144
    78
qed
wenzelm@11024
    79
wenzelm@11024
    80
text {*
nipkow@15561
    81
  \medskip Sum of fourth powers: three versions.
wenzelm@11024
    82
*}
wenzelm@11024
    83
wenzelm@11024
    84
lemma sum_of_fourth_powers:
nipkow@15561
    85
  "30 * (\<Sum>i=0..n. i * i * i * i) =
wenzelm@11786
    86
    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
wenzelm@11024
    87
  apply (induct n)
wenzelm@11024
    88
   apply simp_all
paulson@12196
    89
  apply (case_tac n)  -- {* eliminates the subtraction *} 
paulson@12196
    90
   apply (simp_all (no_asm_simp))
wenzelm@11024
    91
  done
wenzelm@11024
    92
wenzelm@11024
    93
text {*
paulson@16593
    94
  Two alternative proofs, with a change of variables and much more
wenzelm@11024
    95
  subtraction, performed using the integers. *}
wenzelm@11024
    96
wenzelm@11024
    97
lemma int_sum_of_fourth_powers:
nipkow@15561
    98
  "30 * int (\<Sum>i=0..<m. i * i * i * i) =
nipkow@15561
    99
    int m * (int m - 1) * (int(2 * m) - 1) *
nipkow@15561
   100
    (int(3 * m * m) - int(3 * m) - 1)"
wenzelm@16993
   101
  by (induct m) (simp_all add: int_mult)
nipkow@15561
   102
nipkow@15561
   103
lemma of_nat_sum_of_fourth_powers:
nipkow@15561
   104
  "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
paulson@15114
   105
    of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
paulson@15114
   106
    (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
huffman@23431
   107
  by (induct m) (simp_all add: of_nat_mult)
wenzelm@11024
   108
wenzelm@11024
   109
wenzelm@11024
   110
text {*
wenzelm@12023
   111
  \medskip Sums of geometric series: @{text 2}, @{text 3} and the
wenzelm@11786
   112
  general case.
wenzelm@11786
   113
*}
wenzelm@11024
   114
nipkow@15561
   115
lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
wenzelm@16993
   116
  by (induct n) (auto split: nat_diff_split)
wenzelm@11024
   117
nipkow@15561
   118
lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
wenzelm@16993
   119
  by (induct n) auto
wenzelm@11024
   120
nipkow@15561
   121
lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
wenzelm@16993
   122
  by (induct n) auto
wenzelm@11024
   123
wenzelm@11024
   124
end