src/HOL/Divides.thy
changeset 25942 a52309ac4a4d
parent 25571 c9e39eafc7a0
child 25947 1f2f4d941e9e
     1.1 --- a/src/HOL/Divides.thy	Tue Jan 22 23:06:58 2008 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Jan 22 23:07:21 2008 +0100
     1.3 @@ -11,97 +11,237 @@
     1.4  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
     1.5  begin
     1.6  
     1.7 +subsection {* Syntactic division operations *}
     1.8 +
     1.9  class div = times +
    1.10    fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
    1.11    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
    1.12 +begin
    1.13  
    1.14 -instantiation nat :: Divides.div
    1.15 +definition
    1.16 +  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
    1.17 +where
    1.18 +  [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
    1.19 +
    1.20 +end
    1.21 +
    1.22 +subsection {* Abstract divisibility in commutative semirings. *}
    1.23 +
    1.24 +class semiring_div = comm_semiring_1_cancel + div + 
    1.25 +  assumes mod_div_equality: "a div b * b + a mod b = a"
    1.26 +    and div_by_0: "a div 0 = 0"
    1.27 +    and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.28 +begin
    1.29 +
    1.30 +lemma div_by_1: "a div 1 = a"
    1.31 +  using mult_div [of one a] zero_neq_one by simp
    1.32 +
    1.33 +lemma mod_by_1: "a mod 1 = 0"
    1.34 +proof -
    1.35 +  from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
    1.36 +  then have "a + a mod 1 = a + 0" by simp
    1.37 +  then show ?thesis by (rule add_left_imp_eq)
    1.38 +qed
    1.39 +
    1.40 +lemma mod_by_0: "a mod 0 = a"
    1.41 +  using mod_div_equality [of a zero] by simp
    1.42 +
    1.43 +lemma mult_mod: "a * b mod b = 0"
    1.44 +proof (cases "b = 0")
    1.45 +  case True then show ?thesis by (simp add: mod_by_0)
    1.46 +next
    1.47 +  case False with mult_div have abb: "a * b div b = a" .
    1.48 +  from mod_div_equality have "a * b div b * b + a * b mod b = a * b" .
    1.49 +  with abb have "a * b + a * b mod b = a * b + 0" by simp
    1.50 +  then show ?thesis by (rule add_left_imp_eq)
    1.51 +qed
    1.52 +
    1.53 +lemma mod_self: "a mod a = 0"
    1.54 +  using mult_mod [of one] by simp
    1.55 +
    1.56 +lemma div_self: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
    1.57 +  using mult_div [of _ one] by simp
    1.58 +
    1.59 +lemma div_0: "0 div a = 0"
    1.60 +proof (cases "a = 0")
    1.61 +  case True then show ?thesis by (simp add: div_by_0)
    1.62 +next
    1.63 +  case False with mult_div have "0 * a div a = 0" .
    1.64 +  then show ?thesis by simp
    1.65 +qed
    1.66 +
    1.67 +lemma mod_0: "0 mod a = 0"
    1.68 +  using mod_div_equality [of zero a] div_0 by simp 
    1.69 +
    1.70 +lemma dvd_def_mod [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
    1.71 +proof
    1.72 +  assume "b mod a = 0"
    1.73 +  with mod_div_equality [of b a] have "b div a * a = b" by simp
    1.74 +  then have "b = a * (b div a)" unfolding mult_commute ..
    1.75 +  then have "\<exists>c. b = a * c" ..
    1.76 +  then show "a dvd b" unfolding dvd_def .
    1.77 +next
    1.78 +  assume "a dvd b"
    1.79 +  then have "\<exists>c. b = a * c" unfolding dvd_def .
    1.80 +  then obtain c where "b = a * c" ..
    1.81 +  then have "b mod a = a * c mod a" by simp
    1.82 +  then have "b mod a = c * a mod a" by (simp add: mult_commute)
    1.83 +  then show "b mod a = 0" by (simp add: mult_mod)
    1.84 +qed
    1.85 +
    1.86 +lemma dvd_refl: "a dvd a"
    1.87 +  unfolding dvd_def_mod mod_self ..
    1.88 +
    1.89 +lemma dvd_trans:
    1.90 +  assumes "a dvd b" and "b dvd c"
    1.91 +  shows "a dvd c"
    1.92 +proof -
    1.93 +  from assms obtain v where "b = a * v" unfolding dvd_def by auto
    1.94 +  moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
    1.95 +  ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
    1.96 +  then show ?thesis unfolding dvd_def ..
    1.97 +qed
    1.98 +
    1.99 +lemma one_dvd: "1 dvd a"
   1.100 +  unfolding dvd_def by simp
   1.101 +
   1.102 +lemma dvd_0: "a dvd 0"
   1.103 +unfolding dvd_def proof
   1.104 +  show "0 = a * 0" by simp
   1.105 +qed
   1.106 +
   1.107 +end
   1.108 +
   1.109 +
   1.110 +subsection {* Division on the natural numbers *}
   1.111 +
   1.112 +instantiation nat :: semiring_div
   1.113  begin
   1.114  
   1.115  definition
   1.116    div_def: "m div n == wfrec (pred_nat^+)
   1.117                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
   1.118  
   1.119 +lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
   1.120 +               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
   1.121 +by (simp add: div_def)
   1.122 +
   1.123  definition
   1.124    mod_def: "m mod n == wfrec (pred_nat^+)
   1.125                            (%f j. if j<n | n=0 then j else f (j-n)) m"
   1.126  
   1.127 -instance ..
   1.128 -
   1.129 -end
   1.130 -
   1.131 -definition (in div)
   1.132 -  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
   1.133 -where
   1.134 -  [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
   1.135 -
   1.136 -class dvd_mod = div + zero + -- {* for code generation *}
   1.137 -  assumes dvd_def_mod [code func]: "x dvd y \<longleftrightarrow> y mod x = 0"
   1.138 -
   1.139 -definition
   1.140 -  quorem :: "(nat*nat) * (nat*nat) => bool" where
   1.141 -  (*This definition helps prove the harder properties of div and mod.
   1.142 -    It is copied from IntDiv.thy; should it be overloaded?*)
   1.143 -  "quorem = (%((a,b), (q,r)).
   1.144 -                    a = b*q + r &
   1.145 -                    (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
   1.146 -
   1.147 -
   1.148 -
   1.149 -subsection{*Initial Lemmas*}
   1.150 -
   1.151 -lemmas wf_less_trans =
   1.152 -       def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
   1.153 -                  standard]
   1.154 -
   1.155  lemma mod_eq: "(%m. m mod n) =
   1.156                wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
   1.157  by (simp add: mod_def)
   1.158  
   1.159 -lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
   1.160 -               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
   1.161 -by (simp add: div_def)
   1.162 +lemmas wf_less_trans = def_wfrec [THEN trans,
   1.163 +  OF eq_reflection wf_pred_nat [THEN wf_trancl], standard]
   1.164 +
   1.165 +lemma div_less [simp]: "m < n \<Longrightarrow> m div n = (0\<Colon>nat)"
   1.166 +  by (rule div_eq [THEN wf_less_trans]) simp
   1.167 +
   1.168 +lemma le_div_geq: "0 < n \<Longrightarrow> n \<le> m \<Longrightarrow> m div n = Suc ((m - n) div n)"
   1.169 +  by (rule div_eq [THEN wf_less_trans]) (simp add: cut_apply less_eq)
   1.170  
   1.171 +lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a\<Colon>nat)"
   1.172 +  by (rule mod_eq [THEN wf_less_trans]) simp
   1.173 +
   1.174 +lemma mod_less [simp]: "m < n \<Longrightarrow> m mod n = (m\<Colon>nat)"
   1.175 +  by (rule mod_eq [THEN wf_less_trans]) simp
   1.176 +
   1.177 +lemma le_mod_geq: "(n\<Colon>nat) \<le> m \<Longrightarrow> m mod n = (m - n) mod n"
   1.178 +  by (cases "n = 0", simp, rule mod_eq [THEN wf_less_trans])
   1.179 +    (simp add: cut_apply less_eq)
   1.180  
   1.181 -(** Aribtrary definitions for division by zero.  Useful to simplify
   1.182 -    certain equations **)
   1.183 +lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"
   1.184 +  by (simp add: le_mod_geq)
   1.185  
   1.186 -lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
   1.187 -  by (rule div_eq [THEN wf_less_trans], simp)
   1.188 -
   1.189 -lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
   1.190 -  by (rule mod_eq [THEN wf_less_trans], simp)
   1.191 +instance proof
   1.192 +  fix n m :: nat
   1.193 +  show "(m div n) * n + m mod n = m"
   1.194 +    apply (cases "n = 0", simp)
   1.195 +    apply (induct m rule: nat_less_induct [rule_format])
   1.196 +    apply (subst mod_if)
   1.197 +    apply (simp add: add_assoc add_diff_inverse le_div_geq)
   1.198 +    done
   1.199 +next
   1.200 +  fix n :: nat
   1.201 +  show "n div 0 = 0"
   1.202 +    by (rule div_eq [THEN wf_less_trans], simp)
   1.203 +next
   1.204 +  fix n m :: nat
   1.205 +  assume "n \<noteq> 0"
   1.206 +  then show "m * n div n = m"
   1.207 +    by (induct m) (simp_all add: le_div_geq)
   1.208 +qed
   1.209 +  
   1.210 +end
   1.211  
   1.212  
   1.213 -subsection{*Remainder*}
   1.214 +subsubsection{*Simproc for Cancelling Div and Mod*}
   1.215 +
   1.216 +lemmas mod_div_equality = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
   1.217 +
   1.218 +lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
   1.219 +  unfolding mult_commute [of n]
   1.220 +  by (rule mod_div_equality)
   1.221 +
   1.222 +lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
   1.223 +  by (simp add: mod_div_equality)
   1.224 +
   1.225 +lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
   1.226 +  by (simp add: mod_div_equality2)
   1.227 +
   1.228 +ML {*
   1.229 +structure CancelDivModData =
   1.230 +struct
   1.231 +
   1.232 +val div_name = @{const_name Divides.div};
   1.233 +val mod_name = @{const_name Divides.mod};
   1.234 +val mk_binop = HOLogic.mk_binop;
   1.235 +val mk_sum = NatArithUtils.mk_sum;
   1.236 +val dest_sum = NatArithUtils.dest_sum;
   1.237 +
   1.238 +(*logic*)
   1.239  
   1.240 -lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
   1.241 -  by (rule mod_eq [THEN wf_less_trans]) simp
   1.242 +val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
   1.243 +
   1.244 +val trans = trans
   1.245 +
   1.246 +val prove_eq_sums =
   1.247 +  let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
   1.248 +  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
   1.249 +
   1.250 +end;
   1.251 +
   1.252 +structure CancelDivMod = CancelDivModFun(CancelDivModData);
   1.253 +
   1.254 +val cancel_div_mod_proc = NatArithUtils.prep_simproc
   1.255 +      ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
   1.256 +
   1.257 +Addsimprocs[cancel_div_mod_proc];
   1.258 +*}
   1.259 +
   1.260 +
   1.261 +subsubsection {* Remainder *}
   1.262 +
   1.263 +lemmas DIVISION_BY_ZERO_MOD [simp] = mod_by_0 [of "a\<Colon>nat", standard]
   1.264 +
   1.265 +lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   1.266 +  by (induct m) (simp_all add: le_div_geq)
   1.267  
   1.268  lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
   1.269 -  apply (cases "n=0")
   1.270 -   apply simp
   1.271 -  apply (rule mod_eq [THEN wf_less_trans])
   1.272 -  apply (simp add: cut_apply less_eq)
   1.273 -  done
   1.274 -
   1.275 -(*Avoids the ugly ~m<n above*)
   1.276 -lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
   1.277 -  by (simp add: mod_geq linorder_not_less)
   1.278 -
   1.279 -lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
   1.280 -  by (simp add: mod_geq)
   1.281 +  by (simp add: le_mod_geq linorder_not_less)
   1.282  
   1.283  lemma mod_1 [simp]: "m mod Suc 0 = 0"
   1.284    by (induct m) (simp_all add: mod_geq)
   1.285  
   1.286 -lemma mod_self [simp]: "n mod n = (0::nat)"
   1.287 -  by (cases "n = 0") (simp_all add: mod_geq)
   1.288 +lemmas mod_self [simp] = semiring_div_class.mod_self [of "n\<Colon>nat", standard]
   1.289  
   1.290  lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
   1.291    apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
   1.292     apply (simp add: add_commute)
   1.293 -  apply (subst mod_geq [symmetric], simp_all)
   1.294 +  apply (subst le_mod_geq [symmetric], simp_all)
   1.295    done
   1.296  
   1.297  lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
   1.298 @@ -136,76 +276,17 @@
   1.299    by (simp add: mult_commute mod_mult_self_is_0)
   1.300  
   1.301  
   1.302 -subsection{*Quotient*}
   1.303 +subsubsection{*Quotient*}
   1.304  
   1.305 -lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
   1.306 -  by (rule div_eq [THEN wf_less_trans], simp)
   1.307 +lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\<Colon>nat", standard]
   1.308  
   1.309  lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
   1.310 -  apply (rule div_eq [THEN wf_less_trans])
   1.311 -  apply (simp add: cut_apply less_eq)
   1.312 -  done
   1.313 -
   1.314 -(*Avoids the ugly ~m<n above*)
   1.315 -lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
   1.316 -  by (simp add: div_geq linorder_not_less)
   1.317 +  by (simp add: le_div_geq linorder_not_less)
   1.318  
   1.319  lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
   1.320    by (simp add: div_geq)
   1.321  
   1.322  
   1.323 -(*Main Result about quotient and remainder.*)
   1.324 -lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
   1.325 -  apply (cases "n = 0", simp)
   1.326 -  apply (induct m rule: nat_less_induct)
   1.327 -  apply (subst mod_if)
   1.328 -  apply (simp_all add: add_assoc div_geq add_diff_inverse)
   1.329 -  done
   1.330 -
   1.331 -lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
   1.332 -  apply (cut_tac m = m and n = n in mod_div_equality)
   1.333 -  apply (simp add: mult_commute)
   1.334 -  done
   1.335 -
   1.336 -subsection{*Simproc for Cancelling Div and Mod*}
   1.337 -
   1.338 -lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
   1.339 -  by (simp add: mod_div_equality)
   1.340 -
   1.341 -lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
   1.342 -  by (simp add: mod_div_equality2)
   1.343 -
   1.344 -ML
   1.345 -{*
   1.346 -structure CancelDivModData =
   1.347 -struct
   1.348 -
   1.349 -val div_name = @{const_name Divides.div};
   1.350 -val mod_name = @{const_name Divides.mod};
   1.351 -val mk_binop = HOLogic.mk_binop;
   1.352 -val mk_sum = NatArithUtils.mk_sum;
   1.353 -val dest_sum = NatArithUtils.dest_sum;
   1.354 -
   1.355 -(*logic*)
   1.356 -
   1.357 -val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
   1.358 -
   1.359 -val trans = trans
   1.360 -
   1.361 -val prove_eq_sums =
   1.362 -  let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
   1.363 -  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
   1.364 -
   1.365 -end;
   1.366 -
   1.367 -structure CancelDivMod = CancelDivModFun(CancelDivModData);
   1.368 -
   1.369 -val cancel_div_mod_proc = NatArithUtils.prep_simproc
   1.370 -      ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
   1.371 -
   1.372 -Addsimprocs[cancel_div_mod_proc];
   1.373 -*}
   1.374 -
   1.375  
   1.376  (* a simple rearrangement of mod_div_equality: *)
   1.377  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
   1.378 @@ -224,16 +305,21 @@
   1.379    apply simp
   1.380    done
   1.381  
   1.382 -lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   1.383 -  by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
   1.384 -
   1.385  lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   1.386    by (simp add: mult_commute div_mult_self_is_m)
   1.387  
   1.388  (*mod_mult_distrib2 above is the counterpart for remainder*)
   1.389  
   1.390  
   1.391 -subsection{*Proving facts about Quotient and Remainder*}
   1.392 +subsubsection {* Proving advancedfacts about Quotient and Remainder *}
   1.393 +
   1.394 +definition
   1.395 +  quorem :: "(nat*nat) * (nat*nat) => bool" where
   1.396 +  (*This definition helps prove the harder properties of div and mod.
   1.397 +    It is copied from IntDiv.thy; should it be overloaded?*)
   1.398 +  "quorem = (%((a,b), (q,r)).
   1.399 +                    a = b*q + r &
   1.400 +                    (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
   1.401  
   1.402  lemma unique_quotient_lemma:
   1.403       "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]
   1.404 @@ -270,11 +356,9 @@
   1.405  
   1.406  (** A dividend of zero **)
   1.407  
   1.408 -lemma div_0 [simp]: "0 div m = (0::nat)"
   1.409 -  by (cases "m = 0") simp_all
   1.410 +lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\<Colon>nat", standard]
   1.411  
   1.412 -lemma mod_0 [simp]: "0 mod m = (0::nat)"
   1.413 -  by (cases "m = 0") simp_all
   1.414 +lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\<Colon>nat", standard]
   1.415  
   1.416  (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   1.417  
   1.418 @@ -285,6 +369,7 @@
   1.419  
   1.420  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
   1.421  apply (cases "c = 0", simp)
   1.422 +thm DIVISION_BY_ZERO_DIV
   1.423  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
   1.424  done
   1.425  
   1.426 @@ -326,7 +411,7 @@
   1.427  done
   1.428  
   1.429  
   1.430 -subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
   1.431 +subsubsection {* Proving @{prop "a div (b*c) = (a div b) div c"} *}
   1.432  
   1.433  (** first, a lemma to bound the remainder **)
   1.434  
   1.435 @@ -354,7 +439,7 @@
   1.436    done
   1.437  
   1.438  
   1.439 -subsection{*Cancellation of Common Factors in Division*}
   1.440 +subsubsection{*Cancellation of Common Factors in Division*}
   1.441  
   1.442  lemma div_mult_mult_lemma:
   1.443      "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
   1.444 @@ -371,13 +456,12 @@
   1.445    done
   1.446  
   1.447  
   1.448 -subsection{*Further Facts about Quotient and Remainder*}
   1.449 +subsubsection{*Further Facts about Quotient and Remainder*}
   1.450  
   1.451  lemma div_1 [simp]: "m div Suc 0 = m"
   1.452    by (induct m) (simp_all add: div_geq)
   1.453  
   1.454 -lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
   1.455 -  by (simp add: div_geq)
   1.456 +lemmas div_self [simp] = semiring_div_class.div_self [of "n\<Colon>nat", standard]
   1.457  
   1.458  lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
   1.459    apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
   1.460 @@ -474,7 +558,7 @@
   1.461    by (cases "n = 0") auto
   1.462  
   1.463  
   1.464 -subsection{*The Divides Relation*}
   1.465 +subsubsection{*The Divides Relation*}
   1.466  
   1.467  lemma dvdI [intro?]: "n = m * k ==> m dvd n"
   1.468    unfolding dvd_def by blast
   1.469 @@ -499,11 +583,8 @@
   1.470  lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
   1.471    by (simp add: dvd_def)
   1.472  
   1.473 -lemma dvd_refl [simp]: "m dvd (m::nat)"
   1.474 -  unfolding dvd_def by (blast intro: mult_1_right [symmetric])
   1.475 -
   1.476 -lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
   1.477 -  unfolding dvd_def by (blast intro: mult_assoc)
   1.478 +lemmas dvd_refl [simp] = semiring_div_class.dvd_refl [of "m\<Colon>nat", standard]
   1.479 +lemmas dvd_trans [trans] = semiring_div_class.dvd_trans [of "m\<Colon>nat" n p, standard]
   1.480  
   1.481  lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   1.482    unfolding dvd_def
   1.483 @@ -511,7 +592,7 @@
   1.484  
   1.485  text {* @{term "op dvd"} is a partial order *}
   1.486  
   1.487 -interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> m \<noteq> n"]
   1.488 +interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
   1.489    by unfold_locales (auto intro: dvd_trans dvd_anti_sym)
   1.490  
   1.491  lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
   1.492 @@ -611,13 +692,7 @@
   1.493     apply (erule_tac [2] Suc_leI, simp)
   1.494    done
   1.495  
   1.496 -lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
   1.497 -  apply (unfold dvd_def)
   1.498 -  apply (case_tac "k=0", simp, safe)
   1.499 -   apply (simp add: mult_commute)
   1.500 -  apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
   1.501 -  apply (subst mult_commute, simp)
   1.502 -  done
   1.503 +lemmas dvd_eq_mod_eq_0 = dvd_def_mod [of "k\<Colon>nat" n, standard]
   1.504  
   1.505  lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
   1.506    apply (subgoal_tac "m mod n = 0")
   1.507 @@ -776,7 +851,7 @@
   1.508  qed
   1.509  
   1.510  
   1.511 -subsection {*An ``induction'' law for modulus arithmetic.*}
   1.512 +subsubsection {*An ``induction'' law for modulus arithmetic.*}
   1.513  
   1.514  lemma mod_induct_0:
   1.515    assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
   1.516 @@ -889,7 +964,7 @@
   1.517  qed
   1.518  
   1.519  
   1.520 -subsection {* Code generation for div, mod and dvd on nat *}
   1.521 +subsubsection {* Code generation for div, mod and dvd on nat *}
   1.522  
   1.523  definition [code func del]:
   1.524    "divmod (m\<Colon>nat) n = (m div n, m mod n)"
   1.525 @@ -911,9 +986,6 @@
   1.526  lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
   1.527    unfolding divmod_def by simp
   1.528  
   1.529 -instance nat :: dvd_mod
   1.530 -  by default (simp add: dvd_eq_mod_eq_0)
   1.531 -
   1.532  code_modulename SML
   1.533    Divides Nat
   1.534