Re: Inference rules in the Veda system

Lawrence C Paulson (Larry.Paulson@cl.cam.ac.uk)
Thu, 14 Mar 1996 14:48:14 +0100

Tobias Nipkow proved the sums of squares example in Isabelle some years ago.
Here it is, expressed as 6*(1^2 + ... + n^2) = n*(n+1)*(2n+1):

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 1);
by (nat_ind_tac "n" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "sum_of_squares";

Four commands generate the proof: an initial rewriting, then induction and
further rewriting of the base case and inductive step. The worst thing about
this version is Isabelle/HOL's unary syntax for natural numbers.

The Isabelle distribution contains similarly simple proofs for sums of cubes,
sums of odd integers, etc.

-- 
							Larry Paulson