--- a/src/HOL/Divides.thy Mon Jun 15 17:59:36 2009 -0700
+++ b/src/HOL/Divides.thy Mon Jun 15 21:29:04 2009 -0700
@@ -331,6 +331,12 @@
"(a * c) mod (b * c) = (a mod b) * c"
using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
+lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
+ unfolding dvd_def by (auto simp add: mod_mult_mult1)
+
+lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
+by (blast intro: dvd_mod_imp_dvd dvd_mod)
+
lemma div_power:
"y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
apply (induct n)
@@ -904,15 +910,6 @@
apply (rule dvd_refl)
done
-lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
- unfolding dvd_def
- apply (case_tac "n = 0", auto)
- apply (blast intro: mod_mult_distrib2 [symmetric])
- done
-
-lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
-by (blast intro: dvd_mod_imp_dvd dvd_mod)
-
lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
unfolding dvd_def
apply (erule exE)