11375
|
1 |
(* Title: HOL/ex/Lagrange.thy
|
5078
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1996 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
17388
|
7 |
header {* A lemma for Lagrange's theorem *}
|
|
8 |
|
16417
|
9 |
theory Lagrange imports Main begin
|
14603
|
10 |
|
17388
|
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 |
|
19736
|
19 |
definition
|
|
20 |
sq :: "'a::times => 'a"
|
|
21 |
"sq x == x*x"
|
5078
|
22 |
|
17388
|
23 |
text {* The following lemma essentially shows that every natural
|
|
24 |
number is the sum of four squares, provided all prime numbers are.
|
|
25 |
However, this is an abstract theorem about commutative rings. It has,
|
|
26 |
a priori, nothing to do with nat. *}
|
14603
|
27 |
|
20807
|
28 |
ML_setup {*
|
|
29 |
Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
|
|
30 |
*}
|
16568
|
31 |
|
14603
|
32 |
lemma Lagrange_lemma:
|
20807
|
33 |
fixes x1 :: "'a::comm_ring"
|
|
34 |
shows
|
|
35 |
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
|
|
36 |
sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) +
|
|
37 |
sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) +
|
|
38 |
sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) +
|
|
39 |
sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
|
|
40 |
by (simp add: sq_def ring_eq_simps)
|
14603
|
41 |
|
|
42 |
|
20807
|
43 |
text {*
|
|
44 |
A challenge by John Harrison. Takes about 22s on a 1.6GHz machine.
|
|
45 |
*}
|
14603
|
46 |
|
20807
|
47 |
lemma
|
|
48 |
fixes p1 :: "'a::comm_ring"
|
|
49 |
shows
|
|
50 |
"(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
|
|
51 |
(sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)
|
|
52 |
= sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +
|
|
53 |
sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) +
|
|
54 |
sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) +
|
|
55 |
sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) +
|
|
56 |
sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) +
|
|
57 |
sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
|
|
58 |
sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
|
|
59 |
sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
|
|
60 |
by (simp add: sq_def ring_eq_simps)
|
14603
|
61 |
|
5078
|
62 |
end
|