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