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"
```