src/HOL/ex/NatSum.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8976 340d306f0118
child 10698 dc5e984dfe13
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1805
10494d0241cd Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents: 1783
diff changeset
     1
(*  Title:      HOL/ex/NatSum.ML
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1266
diff changeset
     3
    Author:     Tobias Nipkow
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
8836
32fe62227ff0 new example
paulson
parents: 8780
diff changeset
     6
Summing natural numbers, squares, cubes, etc.
8415
paulson
parents: 8356
diff changeset
     7
paulson
parents: 8356
diff changeset
     8
Originally demonstrated permutative rewriting, but add_ac is no longer needed
paulson
parents: 8356
diff changeset
     9
  thanks to new simprocs.
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    10
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    11
Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    12
  http://www.research.att.com/~njas/sequences/
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    13
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    14
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    15
Addsimps [lessThan_Suc, atMost_Suc];
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    16
Addsimps [add_mult_distrib, add_mult_distrib2];
8869
9ba7ef8a765b new simprules needed because of new subtraction rewriting
paulson
parents: 8842
diff changeset
    17
Addsimps [diff_mult_distrib, diff_mult_distrib2];
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    18
8493
60c2f892b1d9 re-ordered the theorems
paulson
parents: 8415
diff changeset
    19
(*The sum of the first n odd numbers equals n squared.*)
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    20
Goal "setsum (%i. Suc(i+i)) (lessThan n) = n*n";
8493
60c2f892b1d9 re-ordered the theorems
paulson
parents: 8415
diff changeset
    21
by (induct_tac "n" 1);
60c2f892b1d9 re-ordered the theorems
paulson
parents: 8415
diff changeset
    22
by Auto_tac;
60c2f892b1d9 re-ordered the theorems
paulson
parents: 8415
diff changeset
    23
qed "sum_of_odds";
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    24
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    25
(*The sum of the first n odd squares*)
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    26
Goal "#3 * setsum (%i. Suc(i+i)*Suc(i+i)) (lessThan n) = n * (#4*n*n - #1)";
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    27
by (induct_tac "n" 1);
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    28
(*This removes the -#1 from the inductive step*)
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    29
by (case_tac "n" 2);
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    30
by Auto_tac;
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    31
qed "sum_of_odd_squares";
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    32
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    33
(*The sum of the first n odd cubes*)
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    34
Goal "setsum (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) (lessThan n) = n * n * (#2*n*n - #1)";
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    35
by (induct_tac "n" 1);
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    36
(*This removes the -#1 from the inductive step*)
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    37
by (case_tac "n" 2);
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    38
by Auto_tac;
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    39
qed "sum_of_odd_cubes";
8493
60c2f892b1d9 re-ordered the theorems
paulson
parents: 8415
diff changeset
    40
8770
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    41
(*The sum of the first n positive integers equals n(n+1)/2.*)
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    42
Goal "#2 * setsum id (atMost n) = n*Suc(n)";
8770
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    43
by (induct_tac "n" 1);
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    44
by Auto_tac;
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    45
qed "sum_of_naturals";
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    46
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    47
Goal "#6 * setsum (%i. i*i) (atMost n) = n * Suc(n) * Suc(#2*n)";
8770
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    48
by (induct_tac "n" 1);
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    49
by Auto_tac;
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    50
qed "sum_of_squares";
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    51
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    52
Goal "#4 * setsum (%i. i*i*i) (atMost n) = n * n * Suc(n) * Suc(n)";
8770
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    53
by (induct_tac "n" 1);
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    54
by Auto_tac;
bfab4d4b7516 new, but still slow, proofs using binary numerals
paulson
parents: 8493
diff changeset
    55
qed "sum_of_cubes";
8836
32fe62227ff0 new example
paulson
parents: 8780
diff changeset
    56
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    57
(** Sum of fourth powers: two versions **)
8836
32fe62227ff0 new example
paulson
parents: 8780
diff changeset
    58
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    59
Goal "#30 * setsum (%i. i*i*i*i) (atMost n) = \
8836
32fe62227ff0 new example
paulson
parents: 8780
diff changeset
    60
\     n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n - #1)";
32fe62227ff0 new example
paulson
parents: 8780
diff changeset
    61
by (induct_tac "n" 1);
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    62
by Auto_tac;
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    63
(*Eliminates the subtraction*)
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    64
by (case_tac "n" 1);
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    65
by (ALLGOALS Asm_simp_tac);
8836
32fe62227ff0 new example
paulson
parents: 8780
diff changeset
    66
qed "sum_of_fourth_powers";
32fe62227ff0 new example
paulson
parents: 8780
diff changeset
    67
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    68
(*Alternative proof, with a change of variables and much more subtraction, 
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    69
  performed using the integers.*)
8836
32fe62227ff0 new example
paulson
parents: 8780
diff changeset
    70
8837
9ee87bdcba05 yet another example
paulson
parents: 8836
diff changeset
    71
Addsimps [zmult_int RS sym, zadd_zmult_distrib, zadd_zmult_distrib2, 
9ee87bdcba05 yet another example
paulson
parents: 8836
diff changeset
    72
	  zdiff_zmult_distrib, zdiff_zmult_distrib2];
9ee87bdcba05 yet another example
paulson
parents: 8836
diff changeset
    73
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    74
Goal "#30 * int (setsum (%i. i*i*i*i) (lessThan m)) = \
8842
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    75
\         int m * (int m - #1) * (int (#2*m) - #1) * \
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    76
\         (int (#3*m*m) - int(#3*m) - #1)";
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    77
by (induct_tac "m" 1);
b90d653bd089 more examples
paulson
parents: 8837
diff changeset
    78
by (ALLGOALS Asm_simp_tac);
8837
9ee87bdcba05 yet another example
paulson
parents: 8836
diff changeset
    79
qed "int_sum_of_fourth_powers";
8932
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    80
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    81
(** Sums of geometric series: 2, 3 and the general case **)
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    82
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    83
Goal "setsum (%i. #2^i) (lessThan n) = #2^n - 1";
8932
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    84
by (induct_tac "n" 1);
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    85
by Auto_tac;
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    86
qed "sum_of_2_powers";
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    87
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    88
Goal "#2 * setsum (%i. #3^i) (lessThan n) = #3^n - 1";
8932
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    89
by (induct_tac "n" 1);
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    90
by Auto_tac;
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    91
qed "sum_of_3_powers";
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    92
8976
340d306f0118 setsum replaces sum_below
paulson
parents: 8932
diff changeset
    93
Goal "0<k ==> (k-1) * setsum (%i. k^i) (lessThan n) = k^n - 1";
8932
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    94
by (induct_tac "n" 1);
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    95
by Auto_tac;
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    96
by (subgoal_tac "1*k^n <= k * k^n" 1);
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    97
by (Asm_full_simp_tac 1);
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    98
by (rtac mult_le_mono1 1);
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
    99
by Auto_tac;
c1d0f7495714 Sums of geometric series
paulson
parents: 8869
diff changeset
   100
qed "sum_of_powers";