src/HOL/Divides.thy
changeset 47268 262d96552e50
parent 47255 30a1692557b0
child 48561 12aa0cb2b447
     1.1 --- a/src/HOL/Divides.thy	Sun Apr 01 23:21:54 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Apr 02 09:18:16 2012 +0200
     1.3 @@ -2126,11 +2126,15 @@
     1.4  
     1.5  subsubsection {* The Divides Relation *}
     1.6  
     1.7 -lemmas zdvd_iff_zmod_eq_0_numeral [simp] =
     1.8 -  dvd_eq_mod_eq_0 [of "numeral x::int" "numeral y::int"]
     1.9 -  dvd_eq_mod_eq_0 [of "numeral x::int" "neg_numeral y::int"]
    1.10 -  dvd_eq_mod_eq_0 [of "neg_numeral x::int" "numeral y::int"]
    1.11 -  dvd_eq_mod_eq_0 [of "neg_numeral x::int" "neg_numeral y::int"] for x y
    1.12 +lemma dvd_neg_numeral_left [simp]:
    1.13 +  fixes y :: "'a::comm_ring_1"
    1.14 +  shows "(neg_numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
    1.15 +  unfolding neg_numeral_def minus_dvd_iff ..
    1.16 +
    1.17 +lemma dvd_neg_numeral_right [simp]:
    1.18 +  fixes x :: "'a::comm_ring_1"
    1.19 +  shows "x dvd (neg_numeral k) \<longleftrightarrow> x dvd (numeral k)"
    1.20 +  unfolding neg_numeral_def dvd_minus_iff ..
    1.21  
    1.22  lemmas dvd_eq_mod_eq_0_numeral [simp] =
    1.23    dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y