added class semiring_div
authorhaftmann
Tue Jan 22 23:07:21 2008 +0100 (2008-01-22)
changeset 25942a52309ac4a4d
parent 25941 0929d6d08dd3
child 25943 d431d65346a1
added class semiring_div
NEWS
src/HOL/Divides.thy
src/HOL/IntDiv.thy
     1.1 --- a/NEWS	Tue Jan 22 23:06:58 2008 +0100
     1.2 +++ b/NEWS	Tue Jan 22 23:07:21 2008 +0100
     1.3 @@ -25,6 +25,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New class semiring_div provides basic abstract properties of semirings
     1.8 +with division and modulo operations.  Subsumes former class dvd_mod.
     1.9 +
    1.10  * Merged theories IntDef, Numeral and IntArith into unified theory Int.
    1.11  INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/HOL/Divides.thy	Tue Jan 22 23:06:58 2008 +0100
     2.2 +++ b/src/HOL/Divides.thy	Tue Jan 22 23:07:21 2008 +0100
     2.3 @@ -11,97 +11,237 @@
     2.4  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
     2.5  begin
     2.6  
     2.7 +subsection {* Syntactic division operations *}
     2.8 +
     2.9  class div = times +
    2.10    fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
    2.11    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
    2.12 +begin
    2.13  
    2.14 -instantiation nat :: Divides.div
    2.15 +definition
    2.16 +  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
    2.17 +where
    2.18 +  [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
    2.19 +
    2.20 +end
    2.21 +
    2.22 +subsection {* Abstract divisibility in commutative semirings. *}
    2.23 +
    2.24 +class semiring_div = comm_semiring_1_cancel + div + 
    2.25 +  assumes mod_div_equality: "a div b * b + a mod b = a"
    2.26 +    and div_by_0: "a div 0 = 0"
    2.27 +    and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    2.28 +begin
    2.29 +
    2.30 +lemma div_by_1: "a div 1 = a"
    2.31 +  using mult_div [of one a] zero_neq_one by simp
    2.32 +
    2.33 +lemma mod_by_1: "a mod 1 = 0"
    2.34 +proof -
    2.35 +  from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
    2.36 +  then have "a + a mod 1 = a + 0" by simp
    2.37 +  then show ?thesis by (rule add_left_imp_eq)
    2.38 +qed
    2.39 +
    2.40 +lemma mod_by_0: "a mod 0 = a"
    2.41 +  using mod_div_equality [of a zero] by simp
    2.42 +
    2.43 +lemma mult_mod: "a * b mod b = 0"
    2.44 +proof (cases "b = 0")
    2.45 +  case True then show ?thesis by (simp add: mod_by_0)
    2.46 +next
    2.47 +  case False with mult_div have abb: "a * b div b = a" .
    2.48 +  from mod_div_equality have "a * b div b * b + a * b mod b = a * b" .
    2.49 +  with abb have "a * b + a * b mod b = a * b + 0" by simp
    2.50 +  then show ?thesis by (rule add_left_imp_eq)
    2.51 +qed
    2.52 +
    2.53 +lemma mod_self: "a mod a = 0"
    2.54 +  using mult_mod [of one] by simp
    2.55 +
    2.56 +lemma div_self: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
    2.57 +  using mult_div [of _ one] by simp
    2.58 +
    2.59 +lemma div_0: "0 div a = 0"
    2.60 +proof (cases "a = 0")
    2.61 +  case True then show ?thesis by (simp add: div_by_0)
    2.62 +next
    2.63 +  case False with mult_div have "0 * a div a = 0" .
    2.64 +  then show ?thesis by simp
    2.65 +qed
    2.66 +
    2.67 +lemma mod_0: "0 mod a = 0"
    2.68 +  using mod_div_equality [of zero a] div_0 by simp 
    2.69 +
    2.70 +lemma dvd_def_mod [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
    2.71 +proof
    2.72 +  assume "b mod a = 0"
    2.73 +  with mod_div_equality [of b a] have "b div a * a = b" by simp
    2.74 +  then have "b = a * (b div a)" unfolding mult_commute ..
    2.75 +  then have "\<exists>c. b = a * c" ..
    2.76 +  then show "a dvd b" unfolding dvd_def .
    2.77 +next
    2.78 +  assume "a dvd b"
    2.79 +  then have "\<exists>c. b = a * c" unfolding dvd_def .
    2.80 +  then obtain c where "b = a * c" ..
    2.81 +  then have "b mod a = a * c mod a" by simp
    2.82 +  then have "b mod a = c * a mod a" by (simp add: mult_commute)
    2.83 +  then show "b mod a = 0" by (simp add: mult_mod)
    2.84 +qed
    2.85 +
    2.86 +lemma dvd_refl: "a dvd a"
    2.87 +  unfolding dvd_def_mod mod_self ..
    2.88 +
    2.89 +lemma dvd_trans:
    2.90 +  assumes "a dvd b" and "b dvd c"
    2.91 +  shows "a dvd c"
    2.92 +proof -
    2.93 +  from assms obtain v where "b = a * v" unfolding dvd_def by auto
    2.94 +  moreover from assms obtain w where "c = b * w" unfolding dvd_def by auto
    2.95 +  ultimately have "c = a * (v * w)" by (simp add: mult_assoc)
    2.96 +  then show ?thesis unfolding dvd_def ..
    2.97 +qed
    2.98 +
    2.99 +lemma one_dvd: "1 dvd a"
   2.100 +  unfolding dvd_def by simp
   2.101 +
   2.102 +lemma dvd_0: "a dvd 0"
   2.103 +unfolding dvd_def proof
   2.104 +  show "0 = a * 0" by simp
   2.105 +qed
   2.106 +
   2.107 +end
   2.108 +
   2.109 +
   2.110 +subsection {* Division on the natural numbers *}
   2.111 +
   2.112 +instantiation nat :: semiring_div
   2.113  begin
   2.114  
   2.115  definition
   2.116    div_def: "m div n == wfrec (pred_nat^+)
   2.117                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
   2.118  
   2.119 +lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
   2.120 +               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
   2.121 +by (simp add: div_def)
   2.122 +
   2.123  definition
   2.124    mod_def: "m mod n == wfrec (pred_nat^+)
   2.125                            (%f j. if j<n | n=0 then j else f (j-n)) m"
   2.126  
   2.127 -instance ..
   2.128 -
   2.129 -end
   2.130 -
   2.131 -definition (in div)
   2.132 -  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
   2.133 -where
   2.134 -  [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
   2.135 -
   2.136 -class dvd_mod = div + zero + -- {* for code generation *}
   2.137 -  assumes dvd_def_mod [code func]: "x dvd y \<longleftrightarrow> y mod x = 0"
   2.138 -
   2.139 -definition
   2.140 -  quorem :: "(nat*nat) * (nat*nat) => bool" where
   2.141 -  (*This definition helps prove the harder properties of div and mod.
   2.142 -    It is copied from IntDiv.thy; should it be overloaded?*)
   2.143 -  "quorem = (%((a,b), (q,r)).
   2.144 -                    a = b*q + r &
   2.145 -                    (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
   2.146 -
   2.147 -
   2.148 -
   2.149 -subsection{*Initial Lemmas*}
   2.150 -
   2.151 -lemmas wf_less_trans =
   2.152 -       def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
   2.153 -                  standard]
   2.154 -
   2.155  lemma mod_eq: "(%m. m mod n) =
   2.156                wfrec (pred_nat^+) (%f j. if j<n | n=0 then j else f (j-n))"
   2.157  by (simp add: mod_def)
   2.158  
   2.159 -lemma div_eq: "(%m. m div n) = wfrec (pred_nat^+)
   2.160 -               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
   2.161 -by (simp add: div_def)
   2.162 +lemmas wf_less_trans = def_wfrec [THEN trans,
   2.163 +  OF eq_reflection wf_pred_nat [THEN wf_trancl], standard]
   2.164 +
   2.165 +lemma div_less [simp]: "m < n \<Longrightarrow> m div n = (0\<Colon>nat)"
   2.166 +  by (rule div_eq [THEN wf_less_trans]) simp
   2.167 +
   2.168 +lemma le_div_geq: "0 < n \<Longrightarrow> n \<le> m \<Longrightarrow> m div n = Suc ((m - n) div n)"
   2.169 +  by (rule div_eq [THEN wf_less_trans]) (simp add: cut_apply less_eq)
   2.170  
   2.171 +lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a\<Colon>nat)"
   2.172 +  by (rule mod_eq [THEN wf_less_trans]) simp
   2.173 +
   2.174 +lemma mod_less [simp]: "m < n \<Longrightarrow> m mod n = (m\<Colon>nat)"
   2.175 +  by (rule mod_eq [THEN wf_less_trans]) simp
   2.176 +
   2.177 +lemma le_mod_geq: "(n\<Colon>nat) \<le> m \<Longrightarrow> m mod n = (m - n) mod n"
   2.178 +  by (cases "n = 0", simp, rule mod_eq [THEN wf_less_trans])
   2.179 +    (simp add: cut_apply less_eq)
   2.180  
   2.181 -(** Aribtrary definitions for division by zero.  Useful to simplify
   2.182 -    certain equations **)
   2.183 +lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"
   2.184 +  by (simp add: le_mod_geq)
   2.185  
   2.186 -lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
   2.187 -  by (rule div_eq [THEN wf_less_trans], simp)
   2.188 -
   2.189 -lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
   2.190 -  by (rule mod_eq [THEN wf_less_trans], simp)
   2.191 +instance proof
   2.192 +  fix n m :: nat
   2.193 +  show "(m div n) * n + m mod n = m"
   2.194 +    apply (cases "n = 0", simp)
   2.195 +    apply (induct m rule: nat_less_induct [rule_format])
   2.196 +    apply (subst mod_if)
   2.197 +    apply (simp add: add_assoc add_diff_inverse le_div_geq)
   2.198 +    done
   2.199 +next
   2.200 +  fix n :: nat
   2.201 +  show "n div 0 = 0"
   2.202 +    by (rule div_eq [THEN wf_less_trans], simp)
   2.203 +next
   2.204 +  fix n m :: nat
   2.205 +  assume "n \<noteq> 0"
   2.206 +  then show "m * n div n = m"
   2.207 +    by (induct m) (simp_all add: le_div_geq)
   2.208 +qed
   2.209 +  
   2.210 +end
   2.211  
   2.212  
   2.213 -subsection{*Remainder*}
   2.214 +subsubsection{*Simproc for Cancelling Div and Mod*}
   2.215 +
   2.216 +lemmas mod_div_equality = semiring_div_class.times_div_mod_plus_zero_one.mod_div_equality [of "m\<Colon>nat" n, standard]
   2.217 +
   2.218 +lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
   2.219 +  unfolding mult_commute [of n]
   2.220 +  by (rule mod_div_equality)
   2.221 +
   2.222 +lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
   2.223 +  by (simp add: mod_div_equality)
   2.224 +
   2.225 +lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
   2.226 +  by (simp add: mod_div_equality2)
   2.227 +
   2.228 +ML {*
   2.229 +structure CancelDivModData =
   2.230 +struct
   2.231 +
   2.232 +val div_name = @{const_name Divides.div};
   2.233 +val mod_name = @{const_name Divides.mod};
   2.234 +val mk_binop = HOLogic.mk_binop;
   2.235 +val mk_sum = NatArithUtils.mk_sum;
   2.236 +val dest_sum = NatArithUtils.dest_sum;
   2.237 +
   2.238 +(*logic*)
   2.239  
   2.240 -lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
   2.241 -  by (rule mod_eq [THEN wf_less_trans]) simp
   2.242 +val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
   2.243 +
   2.244 +val trans = trans
   2.245 +
   2.246 +val prove_eq_sums =
   2.247 +  let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
   2.248 +  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
   2.249 +
   2.250 +end;
   2.251 +
   2.252 +structure CancelDivMod = CancelDivModFun(CancelDivModData);
   2.253 +
   2.254 +val cancel_div_mod_proc = NatArithUtils.prep_simproc
   2.255 +      ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
   2.256 +
   2.257 +Addsimprocs[cancel_div_mod_proc];
   2.258 +*}
   2.259 +
   2.260 +
   2.261 +subsubsection {* Remainder *}
   2.262 +
   2.263 +lemmas DIVISION_BY_ZERO_MOD [simp] = mod_by_0 [of "a\<Colon>nat", standard]
   2.264 +
   2.265 +lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   2.266 +  by (induct m) (simp_all add: le_div_geq)
   2.267  
   2.268  lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
   2.269 -  apply (cases "n=0")
   2.270 -   apply simp
   2.271 -  apply (rule mod_eq [THEN wf_less_trans])
   2.272 -  apply (simp add: cut_apply less_eq)
   2.273 -  done
   2.274 -
   2.275 -(*Avoids the ugly ~m<n above*)
   2.276 -lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
   2.277 -  by (simp add: mod_geq linorder_not_less)
   2.278 -
   2.279 -lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
   2.280 -  by (simp add: mod_geq)
   2.281 +  by (simp add: le_mod_geq linorder_not_less)
   2.282  
   2.283  lemma mod_1 [simp]: "m mod Suc 0 = 0"
   2.284    by (induct m) (simp_all add: mod_geq)
   2.285  
   2.286 -lemma mod_self [simp]: "n mod n = (0::nat)"
   2.287 -  by (cases "n = 0") (simp_all add: mod_geq)
   2.288 +lemmas mod_self [simp] = semiring_div_class.mod_self [of "n\<Colon>nat", standard]
   2.289  
   2.290  lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
   2.291    apply (subgoal_tac "(n + m) mod n = (n+m-n) mod n")
   2.292     apply (simp add: add_commute)
   2.293 -  apply (subst mod_geq [symmetric], simp_all)
   2.294 +  apply (subst le_mod_geq [symmetric], simp_all)
   2.295    done
   2.296  
   2.297  lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
   2.298 @@ -136,76 +276,17 @@
   2.299    by (simp add: mult_commute mod_mult_self_is_0)
   2.300  
   2.301  
   2.302 -subsection{*Quotient*}
   2.303 +subsubsection{*Quotient*}
   2.304  
   2.305 -lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
   2.306 -  by (rule div_eq [THEN wf_less_trans], simp)
   2.307 +lemmas DIVISION_BY_ZERO_DIV [simp] = div_by_0 [of "a\<Colon>nat", standard]
   2.308  
   2.309  lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
   2.310 -  apply (rule div_eq [THEN wf_less_trans])
   2.311 -  apply (simp add: cut_apply less_eq)
   2.312 -  done
   2.313 -
   2.314 -(*Avoids the ugly ~m<n above*)
   2.315 -lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
   2.316 -  by (simp add: div_geq linorder_not_less)
   2.317 +  by (simp add: le_div_geq linorder_not_less)
   2.318  
   2.319  lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
   2.320    by (simp add: div_geq)
   2.321  
   2.322  
   2.323 -(*Main Result about quotient and remainder.*)
   2.324 -lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
   2.325 -  apply (cases "n = 0", simp)
   2.326 -  apply (induct m rule: nat_less_induct)
   2.327 -  apply (subst mod_if)
   2.328 -  apply (simp_all add: add_assoc div_geq add_diff_inverse)
   2.329 -  done
   2.330 -
   2.331 -lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
   2.332 -  apply (cut_tac m = m and n = n in mod_div_equality)
   2.333 -  apply (simp add: mult_commute)
   2.334 -  done
   2.335 -
   2.336 -subsection{*Simproc for Cancelling Div and Mod*}
   2.337 -
   2.338 -lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
   2.339 -  by (simp add: mod_div_equality)
   2.340 -
   2.341 -lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
   2.342 -  by (simp add: mod_div_equality2)
   2.343 -
   2.344 -ML
   2.345 -{*
   2.346 -structure CancelDivModData =
   2.347 -struct
   2.348 -
   2.349 -val div_name = @{const_name Divides.div};
   2.350 -val mod_name = @{const_name Divides.mod};
   2.351 -val mk_binop = HOLogic.mk_binop;
   2.352 -val mk_sum = NatArithUtils.mk_sum;
   2.353 -val dest_sum = NatArithUtils.dest_sum;
   2.354 -
   2.355 -(*logic*)
   2.356 -
   2.357 -val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]
   2.358 -
   2.359 -val trans = trans
   2.360 -
   2.361 -val prove_eq_sums =
   2.362 -  let val simps = @{thm add_0} :: @{thm add_0_right} :: @{thms add_ac}
   2.363 -  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
   2.364 -
   2.365 -end;
   2.366 -
   2.367 -structure CancelDivMod = CancelDivModFun(CancelDivModData);
   2.368 -
   2.369 -val cancel_div_mod_proc = NatArithUtils.prep_simproc
   2.370 -      ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
   2.371 -
   2.372 -Addsimprocs[cancel_div_mod_proc];
   2.373 -*}
   2.374 -
   2.375  
   2.376  (* a simple rearrangement of mod_div_equality: *)
   2.377  lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
   2.378 @@ -224,16 +305,21 @@
   2.379    apply simp
   2.380    done
   2.381  
   2.382 -lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   2.383 -  by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
   2.384 -
   2.385  lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   2.386    by (simp add: mult_commute div_mult_self_is_m)
   2.387  
   2.388  (*mod_mult_distrib2 above is the counterpart for remainder*)
   2.389  
   2.390  
   2.391 -subsection{*Proving facts about Quotient and Remainder*}
   2.392 +subsubsection {* Proving advancedfacts about Quotient and Remainder *}
   2.393 +
   2.394 +definition
   2.395 +  quorem :: "(nat*nat) * (nat*nat) => bool" where
   2.396 +  (*This definition helps prove the harder properties of div and mod.
   2.397 +    It is copied from IntDiv.thy; should it be overloaded?*)
   2.398 +  "quorem = (%((a,b), (q,r)).
   2.399 +                    a = b*q + r &
   2.400 +                    (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
   2.401  
   2.402  lemma unique_quotient_lemma:
   2.403       "[| b*q' + r'  \<le> b*q + r;  x < b;  r < b |]
   2.404 @@ -270,11 +356,9 @@
   2.405  
   2.406  (** A dividend of zero **)
   2.407  
   2.408 -lemma div_0 [simp]: "0 div m = (0::nat)"
   2.409 -  by (cases "m = 0") simp_all
   2.410 +lemmas div_0 [simp] = semiring_div_class.div_0 [of "n\<Colon>nat", standard]
   2.411  
   2.412 -lemma mod_0 [simp]: "0 mod m = (0::nat)"
   2.413 -  by (cases "m = 0") simp_all
   2.414 +lemmas mod_0 [simp] = semiring_div_class.mod_0 [of "n\<Colon>nat", standard]
   2.415  
   2.416  (** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   2.417  
   2.418 @@ -285,6 +369,7 @@
   2.419  
   2.420  lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
   2.421  apply (cases "c = 0", simp)
   2.422 +thm DIVISION_BY_ZERO_DIV
   2.423  apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
   2.424  done
   2.425  
   2.426 @@ -326,7 +411,7 @@
   2.427  done
   2.428  
   2.429  
   2.430 -subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
   2.431 +subsubsection {* Proving @{prop "a div (b*c) = (a div b) div c"} *}
   2.432  
   2.433  (** first, a lemma to bound the remainder **)
   2.434  
   2.435 @@ -354,7 +439,7 @@
   2.436    done
   2.437  
   2.438  
   2.439 -subsection{*Cancellation of Common Factors in Division*}
   2.440 +subsubsection{*Cancellation of Common Factors in Division*}
   2.441  
   2.442  lemma div_mult_mult_lemma:
   2.443      "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
   2.444 @@ -371,13 +456,12 @@
   2.445    done
   2.446  
   2.447  
   2.448 -subsection{*Further Facts about Quotient and Remainder*}
   2.449 +subsubsection{*Further Facts about Quotient and Remainder*}
   2.450  
   2.451  lemma div_1 [simp]: "m div Suc 0 = m"
   2.452    by (induct m) (simp_all add: div_geq)
   2.453  
   2.454 -lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
   2.455 -  by (simp add: div_geq)
   2.456 +lemmas div_self [simp] = semiring_div_class.div_self [of "n\<Colon>nat", standard]
   2.457  
   2.458  lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
   2.459    apply (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n) ")
   2.460 @@ -474,7 +558,7 @@
   2.461    by (cases "n = 0") auto
   2.462  
   2.463  
   2.464 -subsection{*The Divides Relation*}
   2.465 +subsubsection{*The Divides Relation*}
   2.466  
   2.467  lemma dvdI [intro?]: "n = m * k ==> m dvd n"
   2.468    unfolding dvd_def by blast
   2.469 @@ -499,11 +583,8 @@
   2.470  lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
   2.471    by (simp add: dvd_def)
   2.472  
   2.473 -lemma dvd_refl [simp]: "m dvd (m::nat)"
   2.474 -  unfolding dvd_def by (blast intro: mult_1_right [symmetric])
   2.475 -
   2.476 -lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
   2.477 -  unfolding dvd_def by (blast intro: mult_assoc)
   2.478 +lemmas dvd_refl [simp] = semiring_div_class.dvd_refl [of "m\<Colon>nat", standard]
   2.479 +lemmas dvd_trans [trans] = semiring_div_class.dvd_trans [of "m\<Colon>nat" n p, standard]
   2.480  
   2.481  lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   2.482    unfolding dvd_def
   2.483 @@ -511,7 +592,7 @@
   2.484  
   2.485  text {* @{term "op dvd"} is a partial order *}
   2.486  
   2.487 -interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> m \<noteq> n"]
   2.488 +interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
   2.489    by unfold_locales (auto intro: dvd_trans dvd_anti_sym)
   2.490  
   2.491  lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
   2.492 @@ -611,13 +692,7 @@
   2.493     apply (erule_tac [2] Suc_leI, simp)
   2.494    done
   2.495  
   2.496 -lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
   2.497 -  apply (unfold dvd_def)
   2.498 -  apply (case_tac "k=0", simp, safe)
   2.499 -   apply (simp add: mult_commute)
   2.500 -  apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
   2.501 -  apply (subst mult_commute, simp)
   2.502 -  done
   2.503 +lemmas dvd_eq_mod_eq_0 = dvd_def_mod [of "k\<Colon>nat" n, standard]
   2.504  
   2.505  lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
   2.506    apply (subgoal_tac "m mod n = 0")
   2.507 @@ -776,7 +851,7 @@
   2.508  qed
   2.509  
   2.510  
   2.511 -subsection {*An ``induction'' law for modulus arithmetic.*}
   2.512 +subsubsection {*An ``induction'' law for modulus arithmetic.*}
   2.513  
   2.514  lemma mod_induct_0:
   2.515    assumes step: "\<forall>i<p. P i \<longrightarrow> P ((Suc i) mod p)"
   2.516 @@ -889,7 +964,7 @@
   2.517  qed
   2.518  
   2.519  
   2.520 -subsection {* Code generation for div, mod and dvd on nat *}
   2.521 +subsubsection {* Code generation for div, mod and dvd on nat *}
   2.522  
   2.523  definition [code func del]:
   2.524    "divmod (m\<Colon>nat) n = (m div n, m mod n)"
   2.525 @@ -911,9 +986,6 @@
   2.526  lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
   2.527    unfolding divmod_def by simp
   2.528  
   2.529 -instance nat :: dvd_mod
   2.530 -  by default (simp add: dvd_eq_mod_eq_0)
   2.531 -
   2.532  code_modulename SML
   2.533    Divides Nat
   2.534  
     3.1 --- a/src/HOL/IntDiv.thy	Tue Jan 22 23:06:58 2008 +0100
     3.2 +++ b/src/HOL/IntDiv.thy	Tue Jan 22 23:07:21 2008 +0100
     3.3 @@ -712,6 +712,7 @@
     3.4  apply (erule subst, simp_all)
     3.5  done
     3.6  
     3.7 +
     3.8  subsection{*More Algebraic Laws for div and mod*}
     3.9  
    3.10  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
    3.11 @@ -746,6 +747,9 @@
    3.12  lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
    3.13  by (simp add: zdiv_zmult1_eq)
    3.14  
    3.15 +instance int :: semiring_div
    3.16 +  by intro_classes auto
    3.17 +
    3.18  lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
    3.19  by (subst mult_commute, erule zdiv_zmult_self1)
    3.20  
    3.21 @@ -1053,7 +1057,6 @@
    3.22         simp) 
    3.23  done
    3.24  
    3.25 -
    3.26  (*Not clear why this must be proved separately; probably number_of causes
    3.27    simplification problems*)
    3.28  lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
    3.29 @@ -1152,9 +1155,6 @@
    3.30  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
    3.31    by (simp add: dvd_def zmod_eq_0_iff)
    3.32  
    3.33 -instance int :: dvd_mod
    3.34 -  by default (simp add: zdvd_iff_zmod_eq_0)
    3.35 -
    3.36  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    3.37    zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
    3.38