src/HOL/ex/Groebner_Examples.thy
changeset 47108 2a1953f0d20d
parent 42463 f270e3e18be5
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/ex/Groebner_Examples.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/ex/Groebner_Examples.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4      (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_conv @{context})))) *})
     1.5    by (rule refl)
     1.6  
     1.7 -lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})"
     1.8 +lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{comm_ring_1})"
     1.9    apply (simp only: power_Suc power_0)
    1.10    apply (simp only: semiring_norm)
    1.11    oops
    1.12 @@ -58,7 +58,7 @@
    1.13    by algebra
    1.14  
    1.15  lemma
    1.16 -  fixes x::"'a::{idom,number_ring}"
    1.17 +  fixes x::"'a::{idom}"
    1.18    shows "x^2*y = x^2 & x*y^2 = y^2 \<longleftrightarrow>  x=1 & y=1 | x=0 & y=0"
    1.19    by algebra
    1.20  
    1.21 @@ -69,7 +69,7 @@
    1.22    "sq x == x*x"
    1.23  
    1.24  lemma
    1.25 -  fixes x1 :: "'a::{idom,number_ring}"
    1.26 +  fixes x1 :: "'a::{idom}"
    1.27    shows
    1.28    "(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
    1.29      sq (x1*y1 - x2*y2 - x3*y3 - x4*y4)  +
    1.30 @@ -79,7 +79,7 @@
    1.31    by (algebra add: sq_def)
    1.32  
    1.33  lemma
    1.34 -  fixes p1 :: "'a::{idom,number_ring}"
    1.35 +  fixes p1 :: "'a::{idom}"
    1.36    shows
    1.37    "(sq p1 + sq q1 + sq r1 + sq s1 + sq t1 + sq u1 + sq v1 + sq w1) *
    1.38     (sq p2 + sq q2 + sq r2 + sq s2 + sq t2 + sq u2 + sq v2 + sq w2)