src/HOL/Groebner_Basis.thy
changeset 30240 5b25fee0362c
parent 29667 53103fc8ffa3
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4  next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
     1.5  next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
     1.6  next show "pwr x 0 = r1" using pwr_0 .
     1.7 -next show "pwr x 1 = x" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
     1.8 +next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
     1.9  next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
    1.10  next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
    1.11  next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
    1.12 @@ -436,8 +436,8 @@
    1.13  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    1.14  declare dvd_def[algebra]
    1.15  declare dvd_eq_mod_eq_0[symmetric, algebra]
    1.16 -declare nat_mod_div_trivial[algebra]
    1.17 -declare nat_mod_mod_trivial[algebra]
    1.18 +declare mod_div_trivial[algebra]
    1.19 +declare mod_mod_trivial[algebra]
    1.20  declare conjunct1[OF DIVISION_BY_ZERO, algebra]
    1.21  declare conjunct2[OF DIVISION_BY_ZERO, algebra]
    1.22  declare zmod_zdiv_equality[symmetric,algebra]
    1.23 @@ -448,16 +448,16 @@
    1.24  declare zmod_zminus2[algebra]
    1.25  declare zdiv_zero[algebra]
    1.26  declare zmod_zero[algebra]
    1.27 -declare zmod_1[algebra]
    1.28 -declare zdiv_1[algebra]
    1.29 +declare mod_by_1[algebra]
    1.30 +declare div_by_1[algebra]
    1.31  declare zmod_minus1_right[algebra]
    1.32  declare zdiv_minus1_right[algebra]
    1.33  declare mod_div_trivial[algebra]
    1.34  declare mod_mod_trivial[algebra]
    1.35 -declare zmod_zmult_self1[algebra]
    1.36 -declare zmod_zmult_self2[algebra]
    1.37 +declare mod_mult_self2_is_0[algebra]
    1.38 +declare mod_mult_self1_is_0[algebra]
    1.39  declare zmod_eq_0_iff[algebra]
    1.40 -declare zdvd_0_left[algebra]
    1.41 +declare dvd_0_left_iff[algebra]
    1.42  declare zdvd1_eq[algebra]
    1.43  declare zmod_eq_dvd_iff[algebra]
    1.44  declare nat_mod_eq_iff[algebra]