src/HOL/ex/Lagrange.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 37885 c43805c80eb6 child 58776 95e58e04e534 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
1 (*  Title:      HOL/ex/Lagrange.thy
2     Author:     Tobias Nipkow
3     Copyright   1996 TU Muenchen
4 *)
6 header {* A lemma for Lagrange's theorem *}
8 theory Lagrange imports Main begin
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.
15 The enterprising reader might consider proving all of Lagrange's
16 theorem.  *}
18 definition sq :: "'a::times => 'a" where "sq x == x*x"
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. *}
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 field_simps)
34 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
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 field_simps)
49 end