1 (* Title: HOL/ex/Lagrange.thy
4 Copyright 1996 TU Muenchen
7 This theory only contains a single theorem, which is a lemma in Lagrange's
8 proof that every natural number is the sum of 4 squares. Its sole purpose is
9 to demonstrate ordered rewriting for commutative rings.
11 The enterprising reader might consider proving all of Lagrange's theorem.
14 theory Lagrange = Main:
16 constdefs sq :: "'a::times => 'a"
19 (* The following lemma essentially shows that every natural number is the sum
20 of four squares, provided all prime numbers are. However, this is an
21 abstract theorem about commutative rings. It has, a priori, nothing to do
24 (*once a slow step, but now (2001) just three seconds!*)
26 "!!x1::'a::comm_ring_1.
27 (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
28 sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) +
29 sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) +
30 sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) +
31 sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)"
32 by(simp add: sq_def ring_eq_simps)
35 (* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine.
37 lemma "!!p1::'a::comm_ring_1.
38 (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
39 (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
40 = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
41 sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
42 sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
43 sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
44 sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
45 sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
46 sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
47 sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
48 by(simp add: sq_def ring_eq_simps)