1 (* Title: HOL/ex/Lagrange.thy |
1 (* Title: HOL/ex/Lagrange.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1996 TU Muenchen |
4 Copyright 1996 TU Muenchen |
5 |
|
6 |
|
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. |
|
10 |
|
11 The enterprising reader might consider proving all of Lagrange's theorem. |
|
12 *) |
5 *) |
13 |
6 |
|
7 header {* A lemma for Lagrange's theorem *} |
|
8 |
14 theory Lagrange imports Main begin |
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. *} |
15 |
18 |
16 constdefs sq :: "'a::times => 'a" |
19 constdefs sq :: "'a::times => 'a" |
17 "sq x == x*x" |
20 "sq x == x*x" |
18 |
21 |
19 (* The following lemma essentially shows that every natural number is the sum |
22 text {* The following lemma essentially shows that every natural |
20 of four squares, provided all prime numbers are. However, this is an |
23 number is the sum of four squares, provided all prime numbers are. |
21 abstract theorem about commutative rings. It has, a priori, nothing to do |
24 However, this is an abstract theorem about commutative rings. It has, |
22 with nat.*) |
25 a priori, nothing to do with nat. *} |
23 |
26 |
24 ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]" |
27 ML"Delsimprocs[ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]" |
25 |
28 |
26 (*once a slow step, but now (2001) just three seconds!*) |
29 -- {* once a slow step, but now (2001) just three seconds! *} |
27 lemma Lagrange_lemma: |
30 lemma Lagrange_lemma: |
28 "!!x1::'a::comm_ring. |
31 "!!x1::'a::comm_ring. |
29 (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
32 (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
30 sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
33 sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
31 sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
34 sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
34 by(simp add: sq_def ring_eq_simps) |
37 by(simp add: sq_def ring_eq_simps) |
35 |
38 |
36 |
39 |
37 text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*} |
40 text{*A challenge by John Harrison. Takes about 74s on a 2.5GHz Apple G5.*} |
38 |
41 |
39 (* |
|
40 lemma "!!p1::'a::comm_ring. |
42 lemma "!!p1::'a::comm_ring. |
41 (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * |
43 (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * |
42 (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) |
44 (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) |
43 = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + |
45 = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + |
44 sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) + |
46 sq (p1*q2 + q1*p2 + r1*s2 - s1*r2 + t1*u2 - u1*t2 - v1*w2 + w1*v2) + |
46 sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) + |
48 sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) + |
47 sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + |
49 sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + |
48 sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + |
50 sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + |
49 sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + |
51 sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + |
50 sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" |
52 sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" |
|
53 oops |
|
54 (* |
51 by(simp add: sq_def ring_eq_simps) |
55 by(simp add: sq_def ring_eq_simps) |
52 *) |
56 *) |
53 |
57 |
54 end |
58 end |