src/HOL/Divides.thy
changeset 17084 fb0a80aef0be
parent 16796 140f1e0ea846
child 17085 5b57f995a179
     1.1 --- a/src/HOL/Divides.thy	Tue Aug 16 13:54:24 2005 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Aug 16 15:36:28 2005 +0200
     1.3 @@ -562,8 +562,11 @@
     1.4  apply (erule dvd_mult)
     1.5  done
     1.6  
     1.7 -(* k dvd (m*k) *)
     1.8 -declare dvd_refl [THEN dvd_mult, iff] dvd_refl [THEN dvd_mult2, iff]
     1.9 +lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
    1.10 +by (rule dvd_refl [THEN dvd_mult])
    1.11 +
    1.12 +lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
    1.13 +by (rule dvd_refl [THEN dvd_mult2])
    1.14  
    1.15  lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
    1.16  apply (rule iffI)
    1.17 @@ -648,7 +651,9 @@
    1.18  
    1.19  lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
    1.20  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
    1.21 -declare mod_eq_0_iff [THEN iffD1, dest!]
    1.22 +
    1.23 +lemmas mod_eq_0D = mod_eq_0_iff [THEN iffD1]
    1.24 +declare mod_eq_0D [dest!]
    1.25  
    1.26  (*Loses information, namely we also have r<d provided d is nonzero*)
    1.27  lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"