# HG changeset patch
# User haftmann
# Date 1201039641 -3600
# Node ID a52309ac4a4da39046e6444bb178f7b53969ebf2
# Parent  0929d6d08dd3547cd6a5822f2711c59af0df9a8d
added class semiring_div

diff -r 0929d6d08dd3 -r a52309ac4a4d NEWS
--- a/NEWS	Tue Jan 22 23:06:58 2008 +0100
+++ b/NEWS	Tue Jan 22 23:07:21 2008 +0100
@@ -25,6 +25,9 @@
 
 *** HOL ***
 
+* New class semiring_div provides basic abstract properties of semirings
+with division and modulo operations.  Subsumes former class dvd_mod.
+
 * Merged theories IntDef, Numeral and IntArith into unified theory Int.
 INCOMPATIBILITY.
 
diff -r 0929d6d08dd3 -r a52309ac4a4d src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Jan 22 23:06:58 2008 +0100
+++ b/src/HOL/Divides.thy	Tue Jan 22 23:07:21 2008 +0100
@@ -11,97 +11,237 @@
 uses "~~/src/Provers/Arith/cancel_div_mod.ML"
 begin
 
+subsection {* Syntactic division operations *}
+
 class div = times +
   fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
+begin
 
-instantiation nat :: Divides.div
+definition
+  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
+where
+  [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
+
+end
+
+subsection {* Abstract divisibility in commutative semirings. *}
+
+class semiring_div = comm_semiring_1_cancel + div + 
+  assumes mod_div_equality: "a div b * b + a mod b = a"
+    and div_by_0: "a div 0 = 0"
+    and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+begin
+
+lemma div_by_1: "a div 1 = a"
+  using mult_div [of one a] zero_neq_one by simp
+
+lemma mod_by_1: "a mod 1 = 0"
+proof -
+  from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
+  then have "a + a mod 1 = a + 0" by simp
+  then show ?thesis by (rule add_left_imp_eq)
+qed
+
+lemma mod_by_0: "a mod 0 = a"
+  using mod_div_equality [of a zero] by simp
+
+lemma mult_mod: "a * b mod b = 0"
+proof (cases "b = 0")
+  case True then show ?thesis by (simp add: mod_by_0)
+next
+  case False with mult_div have abb: "a * b div b = a" .
+  from mod_div_equality have "a * b div b * b + a * b mod b = a * b" .
+  with abb have "a * b + a * b mod b = a * b + 0" by simp
+  then show ?thesis by (rule add_left_imp_eq)
+qed
+
+lemma mod_self: "a mod a = 0"
+  using mult_mod [of one] by simp
+
+lemma div_self: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
+  using mult_div [of _ one] by simp
+
+lemma div_0: "0 div a = 0"
+proof (cases "a = 0")
+  case True then show ?thesis by (simp add: div_by_0)
+next
+  case False with mult_div have "0 * a div a = 0" .
+  then show ?thesis by simp
+qed
+
+lemma mod_0: "0 mod a = 0"
+  using mod_div_equality [of zero a] div_0 by simp 
+
+lemma dvd_def_mod [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
+proof
+  assume "b mod a = 0"
+  with mod_div_equality [of b a] have "b div a * a = b" by simp
+  then have "b = a * (b div a)" unfolding mult_commute ..
+  then have "\<exists>c. b = a * c" ..
+  then show "a dvd b" unfolding dvd_def .
+next
+  assume "a dvd b"
+  then have "\<exists>c. b = a * c" unfolding dvd_def .
+  then obtain c where "b = a * c" ..
+  then have "b mod a = a * c mod a" by simp
+  then have "b mod a = c * a mod a" by (simp add: mult_commute)
+  then show "b mod a = 0" by (simp add: mult_mod)
+qed
+
+lemma dvd_refl: "a dvd a"
+  unfolding dvd_def_mod mod_self ..
+
+lemma dvd_trans:
+  assumes "a dvd b" and "b dvd c"
+  shows "a dvd c"
+proof -
+  from assms obtain v where "b = a * v" unfolding dvd_def by auto
+  moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
+  ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
+  then show ?thesis unfolding dvd_def ..
+qed
+
+lemma one_dvd: "1 dvd a"
+  unfolding dvd_def by simp
+
+lemma dvd_0: "a dvd 0"
+unfolding dvd_def proof
+  show "0 = a * 0" by simp
+qed
+
+end
+
+
+subsection {* Division on the natural numbers *}
+
+instantiation nat :: semiring_div
 begin
 
 definition
   div_def: "m div n == wfrec (pred_nat^+)
                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
 
+lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
+               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
+by (simp add: div_def)
+
 definition
   mod_def: "m mod n == wfrec (pred_nat^+)
                           (%f j. if j<n | n=0 then j else f (j-n)) m"
 
-instance ..
-
-end
-
-definition (in div)
-  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
-where
-  [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
-
-class dvd_mod = div + zero + -- {* for code generation *}
-  assumes dvd_def_mod [code func]: "x dvd y \<longleftrightarrow> y mod x = 0"
-
-definition
-  quorem :: "(nat*nat) * (nat*nat) => bool" where
-  (*This definition helps prove the harder properties of div and mod.
-    It is copied from IntDiv.thy; should it be overloaded?*)
-  "quorem = (%((a,b), (q,r)).
-                    a = b*q + r &
-                    (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
-
-
-
-subsection{*Initial Lemmas*}
-
-lemmas wf_less_trans =
-       def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
-                  standard]
-
 lemma mod_eq: "(%m. m mod n) =
               wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
 by (simp add: mod_def)
 
-lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
-               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
-by (simp add: div_def)
+lemmas wf_less_trans = def_wfrec [THEN trans,
+  OF eq_reflection wf_pred_nat [THEN wf_trancl], standard]
+
+lemma div_less [simp]: "m < n \<Longrightarrow> m div n = (0\<Colon>nat)"
+  by (rule div_eq [THEN wf_less_trans]) simp
+
+lemma le_div_geq: "0 < n \<Longrightarrow> n \<le> m \<Longrightarrow> m div n = Suc ((m - n) div n)"
+  by (rule div_eq [THEN wf_less_trans]) (simp add: cut_apply less_eq)
 
+lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a\<Colon>nat)"
+  by (rule mod_eq [THEN wf_less_trans]) simp
+
+lemma mod_less [simp]: "m < n \<Longrightarrow> m mod n = (m\<Colon>nat)"
+  by (rule mod_eq [THEN wf_less_trans]) simp
+
+lemma le_mod_geq: "(n\<Colon>nat) \<le> m \<Longrightarrow> m mod n = (m - n) mod n"
+  by (cases "n = 0", simp, rule mod_eq [THEN wf_less_trans])
+    (simp add: cut_apply less_eq)
 
-(** Aribtrary definitions for division by zero.  Useful to simplify
-    certain equations **)
+lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"
+  by (simp add: le_mod_geq)
 
-lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
-  by (rule div_eq [THEN wf_less_trans], simp)
-
-lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
-  by (rule mod_eq [THEN wf_less_trans], simp)
+instance proof
+  fix n m :: nat
+  show "(m div n) * n + m mod n = m"
+    apply (cases "n = 0", simp)
+    apply (induct m rule: nat_less_induct [rule_format])
+    apply (subst mod_if)
+    apply (simp add: add_assoc add_diff_inverse le_div_geq)
+    done
+next
+  fix n :: nat
+  show "n div 0 = 0"
+    by (rule div_eq [THEN wf_less_trans], simp)
+next
+  fix n m :: nat
+  assume "n \<noteq> 0"
+  then show "m * n div n = m"
+    by (induct m) (simp_all add: le_div_geq)
+qed
+  
+end
 
 
-subsection{*Remainder*}
+subsubsection{*Simproc for Cancelling Div and Mod*}
+
+lemmas mod_div_equality = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
+
+lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
+  unfolding mult_commute [of n]
+  by (rule mod_div_equality)
+
+lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
+  by (simp add: mod_div_equality)
+
+lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
+  by (simp add: mod_div_equality2)
+
+ML {*
+structure CancelDivModData =
+struct
+
+val div_name = @{const_name Divides.div};
+val mod_name = @{const_name Divides.mod};
+val mk_binop = HOLogic.mk_binop;
+val mk_sum = NatArithUtils.mk_sum;
+val dest_sum = NatArithUtils.dest_sum;
+
+(*logic*)
 
-lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
-  by (rule mod_eq [THEN wf_less_trans]) simp
+val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
+
+val trans = trans
+
+val prove_eq_sums =
+  let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
+  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
+
+end;
+
+structure CancelDivMod = CancelDivModFun(CancelDivModData);
+
+val cancel_div_mod_proc = NatArithUtils.prep_simproc
+      ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
+
+Addsimprocs[cancel_div_mod_proc];
+*}
+
+
+subsubsection {* Remainder *}
+
+lemmas DIVISION_BY_ZERO_MOD [simp] = mod_by_0 [of "a\<Colon>nat", standard]
+
+lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
+  by (induct m) (simp_all add: le_div_geq)
 
 lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
-  apply (cases "n=0")
-   apply simp
-  apply (rule mod_eq [THEN wf_less_trans])
-  apply (simp add: cut_apply less_eq)
-  done
-
-(*Avoids the ugly ~m<n above*)
-lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
-  by (simp add: mod_geq linorder_not_less)
-
-lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
-  by (simp add: mod_geq)
+  by (simp add: le_mod_geq linorder_not_less)
 
 lemma mod_1 [simp]: "m mod Suc 0 = 0"
   by (induct m) (simp_all add: mod_geq)
 
-lemma mod_self [simp]: "n mod n = (0::nat)"
-  by (cases "n = 0") (simp_all add: mod_geq)
+lemmas mod_self [simp] = semiring_div_class.mod_self [of "n\<Colon>nat", standard]
 
 lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
   apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
    apply (simp add: add_commute)
-  apply (subst mod_geq [symmetric], simp_all)
+  apply (subst le_mod_geq [symmetric], simp_all)
   done
 
 lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
@@ -136,76 +276,17 @@
   by (simp add: mult_commute mod_mult_self_is_0)
 
 
-subsection{*Quotient*}
+subsubsection{*Quotient*}
 
-lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
-  by (rule div_eq [THEN wf_less_trans], simp)
+lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\<Colon>nat", standard]
 
 lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
-  apply (rule div_eq [THEN wf_less_trans])
-  apply (simp add: cut_apply less_eq)
-  done
-
-(*Avoids the ugly ~m<n above*)
-lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
-  by (simp add: div_geq linorder_not_less)
+  by (simp add: le_div_geq linorder_not_less)
 
 lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
   by (simp add: div_geq)
 
 
-(*Main Result about quotient and remainder.*)
-lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
-  apply (cases "n = 0", simp)
-  apply (induct m rule: nat_less_induct)
-  apply (subst mod_if)
-  apply (simp_all add: add_assoc div_geq add_diff_inverse)
-  done
-
-lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
-  apply (cut_tac m = m and n = n in mod_div_equality)
-  apply (simp add: mult_commute)
-  done
-
-subsection{*Simproc for Cancelling Div and Mod*}
-
-lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
-  by (simp add: mod_div_equality)
-
-lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
-  by (simp add: mod_div_equality2)
-
-ML
-{*
-structure CancelDivModData =
-struct
-
-val div_name = @{const_name Divides.div};
-val mod_name = @{const_name Divides.mod};
-val mk_binop = HOLogic.mk_binop;
-val mk_sum = NatArithUtils.mk_sum;
-val dest_sum = NatArithUtils.dest_sum;
-
-(*logic*)
-
-val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
-
-val trans = trans
-
-val prove_eq_sums =
-  let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
-  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
-
-end;
-
-structure CancelDivMod = CancelDivModFun(CancelDivModData);
-
-val cancel_div_mod_proc = NatArithUtils.prep_simproc
-      ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
-
-Addsimprocs[cancel_div_mod_proc];
-*}
-
 
 (* a simple rearrangement of mod_div_equality: *)
 lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
@@ -224,16 +305,21 @@
   apply simp
   done
 
-lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
-  by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
-
 lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   by (simp add: mult_commute div_mult_self_is_m)
 
 (*mod_mult_distrib2 above is the counterpart for remainder*)
 
 
-subsection{*Proving facts about Quotient and Remainder*}
+subsubsection {* Proving advancedfacts about Quotient and Remainder *}
+
+definition
+  quorem :: "(nat*nat) * (nat*nat) => bool" where
+  (*This definition helps prove the harder properties of div and mod.
+    It is copied from IntDiv.thy; should it be overloaded?*)
+  "quorem = (%((a,b), (q,r)).
+                    a = b*q + r &
+                    (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
 
 lemma unique_quotient_lemma:
      "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]
@@ -270,11 +356,9 @@
 
 (** A dividend of zero **)
 
-lemma div_0 [simp]: "0 div m = (0::nat)"
-  by (cases "m = 0") simp_all
+lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\<Colon>nat", standard]
 
-lemma mod_0 [simp]: "0 mod m = (0::nat)"
-  by (cases "m = 0") simp_all
+lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\<Colon>nat", standard]
 
 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
 
@@ -285,6 +369,7 @@
 
 lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
 apply (cases "c = 0", simp)
+thm DIVISION_BY_ZERO_DIV
 apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
 done
 
@@ -326,7 +411,7 @@
 done
 
 
-subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
+subsubsection {* Proving @{prop "a div (b*c) = (a div b) div c"} *}
 
 (** first, a lemma to bound the remainder **)
 
@@ -354,7 +439,7 @@
   done
 
 
-subsection{*Cancellation of Common Factors in Division*}
+subsubsection{*Cancellation of Common Factors in Division*}
 
 lemma div_mult_mult_lemma:
     "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
@@ -371,13 +456,12 @@
   done
 
 
-subsection{*Further Facts about Quotient and Remainder*}
+subsubsection{*Further Facts about Quotient and Remainder*}
 
 lemma div_1 [simp]: "m div Suc 0 = m"
   by (induct m) (simp_all add: div_geq)
 
-lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
-  by (simp add: div_geq)
+lemmas div_self [simp] = semiring_div_class.div_self [of "n\<Colon>nat", standard]
 
 lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
   apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
@@ -474,7 +558,7 @@
   by (cases "n = 0") auto
 
 
-subsection{*The Divides Relation*}
+subsubsection{*The Divides Relation*}
 
 lemma dvdI [intro?]: "n = m * k ==> m dvd n"
   unfolding dvd_def by blast
@@ -499,11 +583,8 @@
 lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
   by (simp add: dvd_def)
 
-lemma dvd_refl [simp]: "m dvd (m::nat)"
-  unfolding dvd_def by (blast intro: mult_1_right [symmetric])
-
-lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
-  unfolding dvd_def by (blast intro: mult_assoc)
+lemmas dvd_refl [simp] = semiring_div_class.dvd_refl [of "m\<Colon>nat", standard]
+lemmas dvd_trans [trans] = semiring_div_class.dvd_trans [of "m\<Colon>nat" n p, standard]
 
 lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   unfolding dvd_def
@@ -511,7 +592,7 @@
 
 text {* @{term "op dvd"} is a partial order *}
 
-interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> m \<noteq> n"]
+interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
   by unfold_locales (auto intro: dvd_trans dvd_anti_sym)
 
 lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
@@ -611,13 +692,7 @@
    apply (erule_tac [2] Suc_leI, simp)
   done
 
-lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
-  apply (unfold dvd_def)
-  apply (case_tac "k=0", simp, safe)
-   apply (simp add: mult_commute)
-  apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
-  apply (subst mult_commute, simp)
-  done
+lemmas dvd_eq_mod_eq_0 = dvd_def_mod [of "k\<Colon>nat" n, standard]
 
 lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
   apply (subgoal_tac "m mod n = 0")
@@ -776,7 +851,7 @@
 qed
 
 
-subsection {*An ``induction'' law for modulus arithmetic.*}
+subsubsection {*An ``induction'' law for modulus arithmetic.*}
 
 lemma mod_induct_0:
   assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
@@ -889,7 +964,7 @@
 qed
 
 
-subsection {* Code generation for div, mod and dvd on nat *}
+subsubsection {* Code generation for div, mod and dvd on nat *}
 
 definition [code func del]:
   "divmod (m\<Colon>nat) n = (m div n, m mod n)"
@@ -911,9 +986,6 @@
 lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
   unfolding divmod_def by simp
 
-instance nat :: dvd_mod
-  by default (simp add: dvd_eq_mod_eq_0)
-
 code_modulename SML
   Divides Nat
 
diff -r 0929d6d08dd3 -r a52309ac4a4d src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Tue Jan 22 23:06:58 2008 +0100
+++ b/src/HOL/IntDiv.thy	Tue Jan 22 23:07:21 2008 +0100
@@ -712,6 +712,7 @@
 apply (erule subst, simp_all)
 done
 
+
 subsection{*More Algebraic Laws for div and mod*}
 
 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
@@ -746,6 +747,9 @@
 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
 by (simp add: zdiv_zmult1_eq)
 
+instance int :: semiring_div
+  by intro_classes auto
+
 lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
 by (subst mult_commute, erule zdiv_zmult_self1)
 
@@ -1053,7 +1057,6 @@
        simp) 
 done
 
-
 (*Not clear why this must be proved separately; probably number_of causes
   simplification problems*)
 lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
@@ -1152,9 +1155,6 @@
 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
   by (simp add: dvd_def zmod_eq_0_iff)
 
-instance int :: dvd_mod
-  by default (simp add: zdvd_iff_zmod_eq_0)
-
 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
   zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]