src/HOL/Integ/Lagrange.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2281 e00c13a29eda
child 3239 6e2ceb50e17b
permissions -rw-r--r--
added AxClasses test;
nipkow@2281
     1
(*  Title:      HOL/Integ/Lagrange.ML
nipkow@2281
     2
    ID:         $Id$
nipkow@2281
     3
    Author:     Tobias Nipkow
nipkow@2281
     4
    Copyright   1996 TU Muenchen
nipkow@2281
     5
nipkow@2281
     6
nipkow@2281
     7
The following lemma essentially shows that all composite natural numbers are
nipkow@2281
     8
sums of fours squares, provided all prime numbers are. However, this is an
nipkow@2281
     9
abstract thm about commutative rings and has a priori nothing to do with nat.
nipkow@2281
    10
*)
nipkow@2281
    11
nipkow@2281
    12
goalw Lagrange.thy [Lagrange.sq_def] "!!x1::'a::cring. \
nipkow@2281
    13
\  (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \
nipkow@2281
    14
\  sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  + \
nipkow@2281
    15
\  sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  + \
nipkow@2281
    16
\  sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  + \
nipkow@2281
    17
\  sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)";
nipkow@2281
    18
by(cring_simp 1);
nipkow@2281
    19
qed "Lagrange_lemma";