Tuned proofs : now use 'algebra ad: ...'
authorchaieb
Tue Jun 12 10:40:44 2007 +0200 (2007-06-12)
changeset 233383f1a453cb538
parent 23337 e7f96b296453
child 23339 babddcf161ca
Tuned proofs : now use 'algebra ad: ...'
src/HOL/ex/Groebner_Examples.thy
     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Tue Jun 12 10:15:58 2007 +0200
     1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Tue Jun 12 10:40:44 2007 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4      sq (x1*y2 + x2*y1 + x3*y4 - x4*y3)  +
     1.5      sq (x1*y3 - x2*y4 + x3*y1 + x4*y2)  +
     1.6      sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
     1.7 -  unfolding sq_def by algebra
     1.8 +  by (algebra add: sq_def)
     1.9  
    1.10  lemma
    1.11    fixes p1 :: "'a::{idom,recpower,number_ring}"
    1.12 @@ -79,7 +79,7 @@
    1.13        sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
    1.14        sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
    1.15        sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
    1.16 -  unfolding sq_def by algebra
    1.17 +  by (algebra add: sq_def)
    1.18  
    1.19  
    1.20  subsection {* Colinearity is invariant by rotation *}
    1.21 @@ -94,7 +94,7 @@
    1.22    assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<twosuperior> + s\<twosuperior> = 1"
    1.23    shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
    1.24      (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
    1.25 -  using assms unfolding collinear_def split_def fst_conv snd_conv
    1.26 -  by algebra
    1.27 +  using assms 
    1.28 +  by (algebra add: collinear_def split_def fst_conv snd_conv)
    1.29  
    1.30  end