src/HOL/ex/Lagrange.thy

tuned eq_ix;

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


This theory only contains a single theorem, which is a lemma in Lagrange's
proof that every natural number is the sum of 4 squares.  Its sole purpose is
to demonstrate ordered rewriting for commutative rings.

The enterprising reader might consider proving all of Lagrange's theorem.
*)

theory Lagrange imports Main begin

constdefs sq :: "'a::times => 'a"
         "sq x == x*x"

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

ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"

(*once a slow step, but now (2001) just three seconds!*)
lemma Lagrange_lemma:
 "!!x1::'a::comm_ring.
  (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(simp add: sq_def ring_eq_simps)


(* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine.

lemma "!!p1::'a::comm_ring.
 (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(simp add: sq_def ring_eq_simps)
*)

end