src/HOL/ex/NatSum.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 21256 47195501ecf7
child 23431 25ca91279a9b
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
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
wenzelm@21256
     8
theory NatSum imports Main Parity 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
nipkow@21144
    65
text{* \medskip A cute identity: *}
nipkow@21144
    66
nipkow@21144
    67
lemma sum_squared: "(\<Sum>i=0..n. i)^2 = (\<Sum>i=0..n::nat. i^3)"
nipkow@21144
    68
proof(induct n)
nipkow@21144
    69
  case 0 show ?case by simp
nipkow@21144
    70
next
nipkow@21144
    71
  case (Suc n)
nipkow@21144
    72
  have "(\<Sum>i = 0..Suc n. i)^2 =
nipkow@21144
    73
        (\<Sum>i = 0..n. i^3) + (2*(\<Sum>i = 0..n. i)*(n+1) + (n+1)^2)"
nipkow@21144
    74
    (is "_ = ?A + ?B")
nipkow@21144
    75
    using Suc by(simp add:nat_number)
nipkow@21144
    76
  also have "?B = (n+1)^3"
nipkow@21144
    77
    using sum_of_naturals by(simp add:nat_number)
nipkow@21144
    78
  also have "?A + (n+1)^3 = (\<Sum>i=0..Suc n. i^3)" by simp
nipkow@21144
    79
  finally show ?case .
nipkow@21144
    80
qed
wenzelm@11024
    81
wenzelm@11024
    82
text {*
nipkow@15561
    83
  \medskip Sum of fourth powers: three versions.
wenzelm@11024
    84
*}
wenzelm@11024
    85
wenzelm@11024
    86
lemma sum_of_fourth_powers:
nipkow@15561
    87
  "30 * (\<Sum>i=0..n. i * i * i * i) =
wenzelm@11786
    88
    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
wenzelm@11024
    89
  apply (induct n)
wenzelm@11024
    90
   apply simp_all
paulson@12196
    91
  apply (case_tac n)  -- {* eliminates the subtraction *} 
paulson@12196
    92
   apply (simp_all (no_asm_simp))
wenzelm@11024
    93
  done
wenzelm@11024
    94
wenzelm@11024
    95
text {*
paulson@16593
    96
  Two alternative proofs, with a change of variables and much more
wenzelm@11024
    97
  subtraction, performed using the integers. *}
wenzelm@11024
    98
wenzelm@11024
    99
lemma int_sum_of_fourth_powers:
nipkow@15561
   100
  "30 * int (\<Sum>i=0..<m. i * i * i * i) =
nipkow@15561
   101
    int m * (int m - 1) * (int(2 * m) - 1) *
nipkow@15561
   102
    (int(3 * m * m) - int(3 * m) - 1)"
wenzelm@16993
   103
  by (induct m) (simp_all add: int_mult)
nipkow@15561
   104
nipkow@15561
   105
lemma of_nat_sum_of_fourth_powers:
nipkow@15561
   106
  "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
paulson@15114
   107
    of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
paulson@15114
   108
    (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
wenzelm@16993
   109
  by (induct m) simp_all
wenzelm@11024
   110
wenzelm@11024
   111
wenzelm@11024
   112
text {*
wenzelm@12023
   113
  \medskip Sums of geometric series: @{text 2}, @{text 3} and the
wenzelm@11786
   114
  general case.
wenzelm@11786
   115
*}
wenzelm@11024
   116
nipkow@15561
   117
lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
wenzelm@16993
   118
  by (induct n) (auto split: nat_diff_split)
wenzelm@11024
   119
nipkow@15561
   120
lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
wenzelm@16993
   121
  by (induct n) auto
wenzelm@11024
   122
nipkow@15561
   123
lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
wenzelm@16993
   124
  by (induct n) auto
wenzelm@11024
   125
wenzelm@11024
   126
end