src/HOL/ex/Lagrange.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29667 53103fc8ffa3
child 30601 febd9234abdd
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/Lagrange.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996 TU Muenchen
     5 *)
     6 
     7 header {* A lemma for Lagrange's theorem *}
     8 
     9 theory Lagrange imports Main begin
    10 
    11 text {* This theory only contains a single theorem, which is a lemma
    12 in Lagrange's proof that every natural number is the sum of 4 squares.
    13 Its sole purpose is to demonstrate ordered rewriting for commutative
    14 rings.
    15 
    16 The enterprising reader might consider proving all of Lagrange's
    17 theorem.  *}
    18 
    19 definition sq :: "'a::times => 'a" where "sq x == x*x"
    20 
    21 text {* The following lemma essentially shows that every natural
    22 number is the sum of four squares, provided all prime numbers are.
    23 However, this is an abstract theorem about commutative rings.  It has,
    24 a priori, nothing to do with nat. *}
    25 
    26 (* These two simprocs are even less efficient than ordered rewriting
    27    and kill the second example: *)
    28 ML {*
    29   Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
    30 *}
    31 
    32 lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows
    33   "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    34    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    35    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    36    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    37    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    38 by (simp add: sq_def algebra_simps)
    39 
    40 
    41 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
    42 
    43 lemma fixes p1 :: "'a::comm_ring" shows
    44   "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    45    (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    46     = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
    47       sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
    48       sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
    49       sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
    50       sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
    51       sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    52       sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    53       sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    54 by (simp add: sq_def algebra_simps)
    55 
    56 end