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
```