src/HOL/ex/Lagrange.thy
changeset 30601 febd9234abdd
parent 29667 53103fc8ffa3
child 36350 bc7982c54e37
equal deleted inserted replaced
30600:de241396389c 30601:febd9234abdd
     1 (*  Title:      HOL/ex/Lagrange.thy
     1 (*  Title:      HOL/ex/Lagrange.thy
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow
     2     Author:     Tobias Nipkow
     4     Copyright   1996 TU Muenchen
     3     Copyright   1996 TU Muenchen
     5 *)
     4 *)
     6 
     5 
     7 header {* A lemma for Lagrange's theorem *}
     6 header {* A lemma for Lagrange's theorem *}
    33   "(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) =
    34    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    33    sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    35    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    34    sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
    36    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    35    sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
    37    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    36    sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
    38 by (simp add: sq_def algebra_simps)
    37 by (simp only: sq_def ring_simps)
    39 
    38 
    40 
    39 
    41 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
    40 text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
    42 
    41 
    43 lemma fixes p1 :: "'a::comm_ring" shows
    42 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) +
    48       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) +
    49       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) +
    50       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) +
    51       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)"
    52       sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    54 by (simp add: sq_def algebra_simps)
    53 by (simp only: sq_def ring_simps)
    55 
    54 
    56 end
    55 end