Mercurial Mercurial > repos > Old_HOL / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ex/NatSum.ML
author nipkow
Sun, 29 Jan 1995 14:02:17 +0100
changeset 204 21c405b4039f
parent 171 16c4ea954511
permissions -rw-r--r--
Added some simplifications for ? x.

(*  Title: 	HOL/ex/natsum.ML
    ID:         $Id$
    Author: 	Tobias Nipkow
    Copyright   1994 TU Muenchen

Summing natural numbers, squares and cubes. Could be continued...
*)

val natsum_ss = arith_ss addsimps
  ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);

(*The sum of the first n positive integers equals n(n+1)/2.*)
goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
by (simp_tac natsum_ss 1);
by (nat_ind_tac "n" 1);
by (simp_tac natsum_ss 1);
by (asm_simp_tac natsum_ss 1);
qed "sum_of_naturals";

goal NatSum.thy
  "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum(%i.i*i,Suc(n)) = \
\  n*Suc(n)*Suc(Suc(Suc(0))*n)";
by (simp_tac natsum_ss 1);
by (nat_ind_tac "n" 1);
by (simp_tac natsum_ss 1);
by (asm_simp_tac natsum_ss 1);
qed "sum_of_squares";

goal NatSum.thy
  "Suc(Suc(Suc(Suc(0))))*sum(%i.i*i*i,Suc(n)) = n*n*Suc(n)*Suc(n)";
by (simp_tac natsum_ss 1);
by (nat_ind_tac "n" 1);
by (simp_tac natsum_ss 1);
by (asm_simp_tac natsum_ss 1);
qed "sum_of_cubes";

(*The sum of the first n odd numbers equals n squared.*)
goal NatSum.thy "sum(%i.Suc(i+i), n) = n*n";
by (nat_ind_tac "n" 1);
by (simp_tac natsum_ss 1);
by (asm_simp_tac natsum_ss 1);
qed "sum_of_odds";
Old_HOL