src/HOL/ex/Lagrange.ML

lemmas induct_atomize = atomize_conj ...;
val local_imp_def = thm "induct_implies_def";

(*  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);
*)