src/HOL/ex/Lagrange.thy
changeset 25475 d5a382ccb5cc
parent 23477 f4b83f03cac9
child 26480 544cef16045b
equal deleted inserted replaced
25474:c41b433b0f65 25475:d5a382ccb5cc
    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 ring_simps)
    39 
    39 
    40 
    40 
    41 text {* A challenge by John Harrison. Takes about 17s 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
    44   "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    44   "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) * 
    45    (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    45    (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2) 
    46     = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) + 
    46     = sq (p1*p2 - q1*q2 - r1*r2 - s1*s2 - t1*t2 - u1*u2 - v1*v2 - w1*w2) +