author | paulson |
Tue, 09 May 2000 11:29:13 +0200 | |
changeset 8842 | b90d653bd089 |
parent 8837 | 9ee87bdcba05 |
child 8869 | 9ba7ef8a765b |
permissions | -rw-r--r-- |
1805
10494d0241cd
Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents:
1783
diff
changeset
|
1 |
(* Title: HOL/ex/NatSum.ML |
969 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
969 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
8836 | 6 |
Summing natural numbers, squares, cubes, etc. |
8415 | 7 |
|
8 |
Originally demonstrated permutative rewriting, but add_ac is no longer needed |
|
9 |
thanks to new simprocs. |
|
8842 | 10 |
|
11 |
Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, |
|
12 |
http://www.research.att.com/~njas/sequences/ |
|
969 | 13 |
*) |
14 |
||
8842 | 15 |
Addsimps [add_mult_distrib, add_mult_distrib2]; |
16 |
||
8493 | 17 |
(*The sum of the first n odd numbers equals n squared.*) |
18 |
Goal "sum (%i. Suc(i+i)) n = n*n"; |
|
19 |
by (induct_tac "n" 1); |
|
20 |
by Auto_tac; |
|
21 |
qed "sum_of_odds"; |
|
969 | 22 |
|
8842 | 23 |
(*The sum of the first n odd squares*) |
24 |
Goal "#3 * sum (%i. Suc(i+i)*Suc(i+i)) n = n * (#4*n*n - #1)"; |
|
25 |
by (induct_tac "n" 1); |
|
26 |
(*This removes the -#1 from the inductive step*) |
|
27 |
by (case_tac "n" 2); |
|
28 |
by Auto_tac; |
|
29 |
qed "sum_of_odd_squares"; |
|
30 |
||
31 |
(*The sum of the first n odd cubes*) |
|
32 |
Goal "sum (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) n = n * n * (#2*n*n - #1)"; |
|
33 |
by (induct_tac "n" 1); |
|
34 |
(*This removes the -#1 from the inductive step*) |
|
35 |
by (case_tac "n" 2); |
|
36 |
by Auto_tac; |
|
37 |
qed "sum_of_odd_cubes"; |
|
8493 | 38 |
|
8770 | 39 |
(*The sum of the first n positive integers equals n(n+1)/2.*) |
40 |
Goal "#2 * sum id (Suc n) = n*Suc(n)"; |
|
41 |
by (induct_tac "n" 1); |
|
42 |
by Auto_tac; |
|
43 |
qed "sum_of_naturals"; |
|
44 |
||
45 |
Goal "#6 * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(#2*n)"; |
|
46 |
by (induct_tac "n" 1); |
|
47 |
by Auto_tac; |
|
48 |
qed "sum_of_squares"; |
|
49 |
||
50 |
Goal "#4 * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
|
51 |
by (induct_tac "n" 1); |
|
52 |
by Auto_tac; |
|
53 |
qed "sum_of_cubes"; |
|
8836 | 54 |
|
8842 | 55 |
(** Sum of fourth powers: two versions **) |
8836 | 56 |
|
57 |
Goal "#30 * sum (%i. i*i*i*i) (Suc n) = \ |
|
58 |
\ n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n - #1)"; |
|
59 |
by (induct_tac "n" 1); |
|
60 |
by (Simp_tac 1); |
|
61 |
(*In simplifying we want only the outer Suc argument to be unfolded. |
|
62 |
Thus the result matches the induction hypothesis (also with Suc). *) |
|
63 |
by (asm_simp_tac (simpset() delsimps [sum_Suc] |
|
64 |
addsimps [inst "n" "Suc ?m" sum_Suc]) 1); |
|
8842 | 65 |
(*Eliminates the subtraction*) |
66 |
by (case_tac "n" 1); |
|
67 |
by (ALLGOALS Asm_simp_tac); |
|
8836 | 68 |
qed "sum_of_fourth_powers"; |
69 |
||
8842 | 70 |
(*Alternative proof. The change of variables n |-> m-#1 eliminates the tricky |
71 |
rewriting of Suc (Suc n). Because it involves much more subtraction, we |
|
72 |
switch to the integers. *) |
|
8836 | 73 |
|
8837 | 74 |
Addsimps [zmult_int RS sym, zadd_zmult_distrib, zadd_zmult_distrib2, |
75 |
zdiff_zmult_distrib, zdiff_zmult_distrib2]; |
|
76 |
||
8842 | 77 |
Goal "#30 * int (sum (%i. i*i*i*i) m) = \ |
78 |
\ int m * (int m - #1) * (int (#2*m) - #1) * \ |
|
79 |
\ (int (#3*m*m) - int(#3*m) - #1)"; |
|
80 |
by (induct_tac "m" 1); |
|
81 |
by (ALLGOALS Asm_simp_tac); |
|
8837 | 82 |
qed "int_sum_of_fourth_powers"; |