equal
deleted
inserted
replaced
33 "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
33 "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = |
34 sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
34 sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) + |
35 sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
35 sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) + |
36 sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + |
36 sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) + |
37 sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
37 sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)" |
38 by (simp add: sq_def ring_simps) |
38 by (simp add: sq_def algebra_simps) |
39 |
39 |
40 |
40 |
41 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *} |
41 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *} |
42 |
42 |
43 lemma fixes p1 :: "'a::comm_ring" shows |
43 lemma fixes p1 :: "'a::comm_ring" shows |
49 sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) + |
49 sq (p1*s2 + q1*r2 - r1*q2 + s1*p2 + t1*w2 - u1*v2 + v1*u2 - w1*t2) + |
50 sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + |
50 sq (p1*t2 - q1*u2 - r1*v2 - s1*w2 + t1*p2 + u1*q2 + v1*r2 + w1*s2) + |
51 sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + |
51 sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) + |
52 sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + |
52 sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) + |
53 sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" |
53 sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)" |
54 by (simp add: sq_def ring_simps) |
54 by (simp add: sq_def algebra_simps) |
55 |
55 |
56 end |
56 end |