# HG changeset patch
# User huffman
# Date 1245126544 25200
# Node ID 57f7ef0dba8eb5e8f636e2160b054514ca590dcf
# Parent  1e252b8b2334014df45840734fee63b1aa19e78e
generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div

diff -r 1e252b8b2334 -r 57f7ef0dba8e src/HOL/Divides.thy
--- 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)
diff -r 1e252b8b2334 -r 57f7ef0dba8e src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Mon Jun 15 17:59:36 2009 -0700
+++ b/src/HOL/IntDiv.thy	Mon Jun 15 21:29:04 2009 -0700
@@ -1059,13 +1059,10 @@
 done
 
 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
-  by (auto elim!: dvdE simp add: mod_mult_mult1)
+  by (rule dvd_mod) (* TODO: remove *)
 
 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
-  apply (subgoal_tac "k dvd n * (m div n) + m mod n")
-   apply (simp add: zmod_zdiv_equality [symmetric])
-  apply (simp only: dvd_add dvd_mult2)
-  done
+  by (rule dvd_mod_imp_dvd) (* TODO: remove *)
 
 lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   apply (auto elim!: dvdE)