src/HOL/ex/Lagrange.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17388 495c799df31d
child 19736 d8d0f8f51d69
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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 constdefs sq :: "'a::times => 'a"
    20          "sq x == x*x"
    21 
    22 text {* The following lemma essentially shows that every natural
    23 number is the sum of four squares, provided all prime numbers are.
    24 However, this is an abstract theorem about commutative rings.  It has,
    25 a priori, nothing to do with nat. *}
    26 
    27 ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]"
    28 
    29 -- {* once a slow step, but now (2001) just three seconds! *}
    30 lemma Lagrange_lemma:
    31  "!!x1::'a::comm_ring.
    32   (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    33   sq(x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    34   sq(x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    35   sq(x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    36   sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    37 by(simp add: sq_def ring_eq_simps)
    38 
    39 
    40 text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*}
    41 
    42 lemma "!!p1::'a::comm_ring.
    43  (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    44  (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    45   = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
    46     sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
    47     sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
    48     sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
    49     sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
    50     sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    51     sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    52     sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    53 oops
    54 (*
    55 by(simp add: sq_def ring_eq_simps)
    56 *)
    57 
    58 end