21 abstract theorem about commutative rings. It has, a priori, nothing to do |
21 abstract theorem about commutative rings. It has, a priori, nothing to do |
22 with nat.*) |
22 with nat.*) |
23 |
23 |
24 (*once a slow step, but now (2001) just three seconds!*) |
24 (*once a slow step, but now (2001) just three seconds!*) |
25 lemma Lagrange_lemma: |
25 lemma Lagrange_lemma: |
26 "!!x1::'a::ring. |
26 "!!x1::'a::comm_ring_1. |
27 (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
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) + |
28 sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
29 sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
29 sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
30 sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) + |
30 sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) + |
31 sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
31 sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
32 by(simp add: sq_def ring_eq_simps) |
32 by(simp add: sq_def ring_eq_simps) |
33 |
33 |
34 |
34 |
35 (* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine. |
35 (* A challenge by John Harrison. Takes about 4 mins on a 3GHz machine. |
36 |
36 |
37 lemma "!!p1::'a::ring. |
37 lemma "!!p1::'a::comm_ring_1. |
38 (sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * |
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) |
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) + |
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) + |
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) + |
42 sq (p1*r2 - q1*s2 + r1*p2 + s1*q2 + t1*v2 + u1*w2 - v1*t2 - w1*u2) + |