src/HOL/ex/Lagrange.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5078 7b5ea59c0275
child 11375 a6730c90e753
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  Title:      HOL/Integ/Lagrange.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1996 TU Muenchen


The following lemma essentially shows that all composite natural numbers are
sums of fours squares, provided all prime numbers are. However, this is an
abstract thm about commutative rings and 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)";
(*Takes up to three minutes...*)
by (cring_tac 1);
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)";

*)