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