(* Title: HOL/Integ/Lagrange.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1996 TU Muenchen
The following lemma essentially shows that every natural number is the sum of
four squares, provided all prime numbers are. However, this is an abstract
theorem about commutative rings. It has, a priori, nothing to do with nat.*)
Goalw [Lagrange.sq_def]
"!!x1::'a::cring. \
\ (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
\ sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + \
\ sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + \
\ sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) + \
\ sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
by (cring_tac 1); (*once a slow step, but now (2001) just three seconds!*)
qed "Lagrange_lemma";
(* A challenge by John Harrison.
Takes forever because of the naive bottom-up strategy of the rewriter.
Goalw [Lagrange.sq_def] "!!p1::'a::cring.\
\ (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * \
\ (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) \
\ = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + \
\ sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +\
\ sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +\
\ sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +\
\ sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +\
\ sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +\
\ sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +\
\ sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)";
by (cring_tac 1);
*)