src/HOL/Groebner_Basis.thy
changeset 23477 f4b83f03cac9
parent 23458 b2267a9e9e28
child 23573 d85a277f90fd
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Jun 22 22:41:17 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Jun 23 19:33:22 2007 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4  
     1.5  interpretation class_semiring: gb_semiring
     1.6      ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
     1.7 -  by unfold_locales (auto simp add: ring_eq_simps power_Suc)
     1.8 +  by unfold_locales (auto simp add: ring_simps power_Suc)
     1.9  
    1.10  lemmas nat_arith =
    1.11    add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
    1.12 @@ -341,13 +341,13 @@
    1.13  
    1.14  interpretation class_ringb: ringb
    1.15    ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
    1.16 -proof(unfold_locales, simp add: ring_eq_simps power_Suc, auto)
    1.17 +proof(unfold_locales, simp add: ring_simps power_Suc, auto)
    1.18    fix w x y z ::"'a::{idom,recpower,number_ring}"
    1.19    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.20    hence ynz': "y - z \<noteq> 0" by simp
    1.21    from p have "w * y + x* z - w*z - x*y = 0" by simp
    1.22 -  hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_eq_simps)
    1.23 -  hence "(y - z) * (w - x) = 0" by (simp add: ring_eq_simps)
    1.24 +  hence "w* (y - z) - x * (y - z) = 0" by (simp add: ring_simps)
    1.25 +  hence "(y - z) * (w - x) = 0" by (simp add: ring_simps)
    1.26    with  no_zero_divirors_neq0 [OF ynz']
    1.27    have "w - x = 0" by blast
    1.28    thus "w = x"  by simp
    1.29 @@ -368,20 +368,20 @@
    1.30  
    1.31  interpretation natgb: semiringb
    1.32    ["op +" "op *" "op ^" "0::nat" "1"]
    1.33 -proof (unfold_locales, simp add: ring_eq_simps power_Suc)
    1.34 +proof (unfold_locales, simp add: ring_simps power_Suc)
    1.35    fix w x y z ::"nat"
    1.36    { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.37      hence "y < z \<or> y > z" by arith
    1.38      moreover {
    1.39        assume lt:"y <z" hence "\<exists>k. z = y + k \<and> k > 0" by (rule_tac x="z - y" in exI, auto)
    1.40        then obtain k where kp: "k>0" and yz:"z = y + k" by blast
    1.41 -      from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_eq_simps)
    1.42 +      from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz ring_simps)
    1.43        hence "x*k = w*k" by simp
    1.44        hence "w = x" using kp by (simp add: mult_cancel2) }
    1.45      moreover {
    1.46        assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
    1.47        then obtain k where kp: "k>0" and yz:"y = z + k" by blast
    1.48 -      from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_eq_simps)
    1.49 +      from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz ring_simps)
    1.50        hence "w*k = x*k" by simp
    1.51        hence "w = x" using kp by (simp add: mult_cancel2)}
    1.52      ultimately have "w=x" by blast }