src/HOL/ex/Lagrange.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58776 95e58e04e534
child 61343 5b5656a63bd6
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      HOL/ex/Lagrange.thy
     2     Author:     Tobias Nipkow
     3     Copyright   1996 TU Muenchen
     4 *)
     5 
     6 section {* A lemma for Lagrange's theorem *}
     7 
     8 theory Lagrange imports Main begin
     9 
    10 text {* This theory only contains a single theorem, which is a lemma
    11 in Lagrange's proof that every natural number is the sum of 4 squares.
    12 Its sole purpose is to demonstrate ordered rewriting for commutative
    13 rings.
    14 
    15 The enterprising reader might consider proving all of Lagrange's
    16 theorem.  *}
    17 
    18 definition sq :: "'a::times => 'a" where "sq x == x*x"
    19 
    20 text {* The following lemma essentially shows that every natural
    21 number is the sum of four squares, provided all prime numbers are.
    22 However, this is an abstract theorem about commutative rings.  It has,
    23 a priori, nothing to do with nat. *}
    24 
    25 lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows
    26   "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    27    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    28    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    29    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    30    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    31 by (simp only: sq_def algebra_simps)
    32 
    33 
    34 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
    35 
    36 lemma fixes p1 :: "'a::comm_ring" shows
    37   "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    38    (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    39     = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
    40       sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
    41       sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
    42       sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
    43       sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
    44       sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    45       sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    46       sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    47 by (simp only: sq_def algebra_simps)
    48 
    49 end