| author | wenzelm |
| Mon, 08 Jun 2020 21:55:14 +0200 | |
| changeset 71926 | bee83c9d3306 |
| parent 61343 | 5b5656a63bd6 |
| permissions | -rw-r--r-- |
| 11375 | 1 |
(* Title: HOL/ex/Lagrange.thy |
| 5078 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1996 TU Muenchen |
|
4 |
*) |
|
5 |
||
| 61343 | 6 |
section \<open>A lemma for Lagrange's theorem\<close> |
| 17388 | 7 |
|
| 16417 | 8 |
theory Lagrange imports Main begin |
| 14603 | 9 |
|
| 61343 | 10 |
text \<open>This theory only contains a single theorem, which is a lemma |
| 17388 | 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. |
|
14 |
||
15 |
The enterprising reader might consider proving all of Lagrange's |
|
| 61343 | 16 |
theorem.\<close> |
| 17388 | 17 |
|
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset
|
18 |
definition sq :: "'a::times => 'a" where "sq x == x*x" |
| 5078 | 19 |
|
| 61343 | 20 |
text \<open>The following lemma essentially shows that every natural |
| 17388 | 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, |
|
| 61343 | 23 |
a priori, nothing to do with nat.\<close> |
| 14603 | 24 |
|
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset
|
25 |
lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows |
| 20807 | 26 |
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset
|
27 |
sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
|
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset
|
28 |
sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
|
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset
|
29 |
sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + |
|
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset
|
30 |
sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
|
58776
95e58e04e534
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents:
37885
diff
changeset
|
31 |
by (simp only: sq_def algebra_simps) |
| 14603 | 32 |
|
33 |
||
| 61343 | 34 |
text \<open>A challenge by John Harrison. Takes about 12s on a 1.6GHz machine.\<close> |
| 14603 | 35 |
|
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22173
diff
changeset
|
36 |
lemma fixes p1 :: "'a::comm_ring" shows |
| 20807 | 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)" |
|
|
58776
95e58e04e534
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents:
37885
diff
changeset
|
47 |
by (simp only: sq_def algebra_simps) |
| 14603 | 48 |
|
| 5078 | 49 |
end |