author | paulson |
Fri, 12 May 2000 15:20:46 +0200 | |
changeset 8869 | 9ba7ef8a765b |
parent 8842 | b90d653bd089 |
child 8932 | c1d0f7495714 |
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]; |
8869
9ba7ef8a765b
new simprules needed because of new subtraction rewriting
paulson
parents:
8842
diff
changeset
|
16 |
Addsimps [diff_mult_distrib, diff_mult_distrib2]; |
8842 | 17 |
|
8493 | 18 |
(*The sum of the first n odd numbers equals n squared.*) |
19 |
Goal "sum (%i. Suc(i+i)) n = n*n"; |
|
20 |
by (induct_tac "n" 1); |
|
21 |
by Auto_tac; |
|
22 |
qed "sum_of_odds"; |
|
969 | 23 |
|
8842 | 24 |
(*The sum of the first n odd squares*) |
25 |
Goal "#3 * sum (%i. Suc(i+i)*Suc(i+i)) n = n * (#4*n*n - #1)"; |
|
26 |
by (induct_tac "n" 1); |
|
27 |
(*This removes the -#1 from the inductive step*) |
|
28 |
by (case_tac "n" 2); |
|
29 |
by Auto_tac; |
|
30 |
qed "sum_of_odd_squares"; |
|
31 |
||
32 |
(*The sum of the first n odd cubes*) |
|
33 |
Goal "sum (%i. Suc(i+i)*Suc(i+i)*Suc(i+i)) n = n * n * (#2*n*n - #1)"; |
|
34 |
by (induct_tac "n" 1); |
|
35 |
(*This removes the -#1 from the inductive step*) |
|
36 |
by (case_tac "n" 2); |
|
37 |
by Auto_tac; |
|
38 |
qed "sum_of_odd_cubes"; |
|
8493 | 39 |
|
8770 | 40 |
(*The sum of the first n positive integers equals n(n+1)/2.*) |
41 |
Goal "#2 * sum id (Suc n) = n*Suc(n)"; |
|
42 |
by (induct_tac "n" 1); |
|
43 |
by Auto_tac; |
|
44 |
qed "sum_of_naturals"; |
|
45 |
||
46 |
Goal "#6 * sum (%i. i*i) (Suc n) = n * Suc(n) * Suc(#2*n)"; |
|
47 |
by (induct_tac "n" 1); |
|
48 |
by Auto_tac; |
|
49 |
qed "sum_of_squares"; |
|
50 |
||
51 |
Goal "#4 * sum (%i. i*i*i) (Suc n) = n * n * Suc(n) * Suc(n)"; |
|
52 |
by (induct_tac "n" 1); |
|
53 |
by Auto_tac; |
|
54 |
qed "sum_of_cubes"; |
|
8836 | 55 |
|
8842 | 56 |
(** Sum of fourth powers: two versions **) |
8836 | 57 |
|
58 |
Goal "#30 * sum (%i. i*i*i*i) (Suc n) = \ |
|
59 |
\ n * Suc(n) * Suc(#2*n) * (#3*n*n + #3*n - #1)"; |
|
60 |
by (induct_tac "n" 1); |
|
61 |
by (Simp_tac 1); |
|
62 |
(*In simplifying we want only the outer Suc argument to be unfolded. |
|
63 |
Thus the result matches the induction hypothesis (also with Suc). *) |
|
64 |
by (asm_simp_tac (simpset() delsimps [sum_Suc] |
|
65 |
addsimps [inst "n" "Suc ?m" sum_Suc]) 1); |
|
8842 | 66 |
(*Eliminates the subtraction*) |
67 |
by (case_tac "n" 1); |
|
68 |
by (ALLGOALS Asm_simp_tac); |
|
8836 | 69 |
qed "sum_of_fourth_powers"; |
70 |
||
8842 | 71 |
(*Alternative proof. The change of variables n |-> m-#1 eliminates the tricky |
72 |
rewriting of Suc (Suc n). Because it involves much more subtraction, we |
|
73 |
switch to the integers. *) |
|
8836 | 74 |
|
8837 | 75 |
Addsimps [zmult_int RS sym, zadd_zmult_distrib, zadd_zmult_distrib2, |
76 |
zdiff_zmult_distrib, zdiff_zmult_distrib2]; |
|
77 |
||
8842 | 78 |
Goal "#30 * int (sum (%i. i*i*i*i) m) = \ |
79 |
\ int m * (int m - #1) * (int (#2*m) - #1) * \ |
|
80 |
\ (int (#3*m*m) - int(#3*m) - #1)"; |
|
81 |
by (induct_tac "m" 1); |
|
82 |
by (ALLGOALS Asm_simp_tac); |
|
8837 | 83 |
qed "int_sum_of_fourth_powers"; |