src/HOL/Divides.thy
 changeset 64592 7759f1766189 parent 64250 0cde0b4d4cb5 child 64593 50c715579715
```     1.1 --- a/src/HOL/Divides.thy	Sat Dec 17 15:22:13 2016 +0100
1.2 +++ b/src/HOL/Divides.thy	Sat Dec 17 15:22:14 2016 +0100
1.3 @@ -3,37 +3,95 @@
1.4      Copyright   1999  University of Cambridge
1.5  *)
1.6
1.7 -section \<open>The division operators div and mod\<close>
1.8 +section \<open>Quotient and remainder\<close>
1.9
1.10  theory Divides
1.11  imports Parity
1.12  begin
1.13
1.14 -subsection \<open>Abstract division in commutative semirings.\<close>
1.15 -
1.16 -class semiring_div = semidom + semiring_modulo +
1.17 -  assumes div_by_0: "a div 0 = 0"
1.18 -    and div_0: "0 div a = 0"
1.19 -    and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
1.20 +subsection \<open>Quotient and remainder in integral domains\<close>
1.21 +
1.22 +class semidom_modulo = algebraic_semidom + semiring_modulo
1.23 +begin
1.24 +
1.25 +lemma mod_0 [simp]: "0 mod a = 0"
1.26 +  using div_mult_mod_eq [of 0 a] by simp
1.27 +
1.28 +lemma mod_by_0 [simp]: "a mod 0 = a"
1.29 +  using div_mult_mod_eq [of a 0] by simp
1.30 +
1.31 +lemma mod_by_1 [simp]:
1.32 +  "a mod 1 = 0"
1.33 +proof -
1.34 +  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
1.35 +  then have "a + a mod 1 = a + 0" by simp
1.36 +  then show ?thesis by (rule add_left_imp_eq)
1.37 +qed
1.38 +
1.39 +lemma mod_self [simp]:
1.40 +  "a mod a = 0"
1.41 +  using div_mult_mod_eq [of a a] by simp
1.42 +
1.43 +lemma dvd_imp_mod_0 [simp]:
1.44 +  assumes "a dvd b"
1.45 +  shows "b mod a = 0"
1.46 +  using assms minus_div_mult_eq_mod [of b a] by simp
1.47 +
1.48 +lemma mod_0_imp_dvd:
1.49 +  assumes "a mod b = 0"
1.50 +  shows   "b dvd a"
1.51 +proof -
1.52 +  have "b dvd ((a div b) * b)" by simp
1.53 +  also have "(a div b) * b = a"
1.54 +    using div_mult_mod_eq [of a b] by (simp add: assms)
1.55 +  finally show ?thesis .
1.56 +qed
1.57 +
1.58 +lemma mod_eq_0_iff_dvd:
1.59 +  "a mod b = 0 \<longleftrightarrow> b dvd a"
1.60 +  by (auto intro: mod_0_imp_dvd)
1.61 +
1.62 +lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
1.63 +  "a dvd b \<longleftrightarrow> b mod a = 0"
1.64 +  by (simp add: mod_eq_0_iff_dvd)
1.65 +
1.66 +lemma dvd_mod_iff:
1.67 +  assumes "c dvd b"
1.68 +  shows "c dvd a mod b \<longleftrightarrow> c dvd a"
1.69 +proof -
1.70 +  from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))"
1.72 +  also have "(a div b) * b + a mod b = a"
1.73 +    using div_mult_mod_eq [of a b] by simp
1.74 +  finally show ?thesis .
1.75 +qed
1.76 +
1.77 +lemma dvd_mod_imp_dvd:
1.78 +  assumes "c dvd a mod b" and "c dvd b"
1.79 +  shows "c dvd a"
1.80 +  using assms dvd_mod_iff [of c b a] by simp
1.81 +
1.82 +end
1.83 +
1.84 +class idom_modulo = idom + semidom_modulo
1.85 +begin
1.86 +
1.87 +subclass idom_divide ..
1.88 +
1.89 +lemma div_diff [simp]:
1.90 +  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c"
1.91 +  using div_add [of _  _ "- b"] by (simp add: dvd_neg_div)
1.92 +
1.93 +end
1.94 +
1.95 +
1.96 +subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
1.97 +
1.98 +class semiring_div = semidom_modulo +
1.99 +  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
1.100      and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
1.101  begin
1.102
1.103 -subclass algebraic_semidom
1.104 -proof
1.105 -  fix b a
1.106 -  assume "b \<noteq> 0"
1.107 -  then show "a * b div b = a"
1.108 -    using div_mult_self1 [of b 0 a] by (simp add: ac_simps div_0)
1.110 -
1.111 -text \<open>@{const divide} and @{const modulo}\<close>
1.112 -
1.113 -lemma mod_by_0 [simp]: "a mod 0 = a"
1.114 -  using div_mult_mod_eq [of a zero] by simp
1.115 -
1.116 -lemma mod_0 [simp]: "0 mod a = 0"
1.117 -  using div_mult_mod_eq [of zero a] div_0 by simp
1.118 -
1.119  lemma div_mult_self2 [simp]:
1.120    assumes "b \<noteq> 0"
1.121    shows "(a + b * c) div b = c + a div b"
1.122 @@ -86,18 +144,6 @@
1.123    "a * b mod b = 0"
1.124    using mod_mult_self1 [of 0 a b] by simp
1.125
1.126 -lemma mod_by_1 [simp]:
1.127 -  "a mod 1 = 0"
1.128 -proof -
1.129 -  from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp
1.130 -  then have "a + a mod 1 = a + 0" by simp
1.131 -  then show ?thesis by (rule add_left_imp_eq)
1.132 -qed
1.133 -
1.134 -lemma mod_self [simp]:
1.135 -  "a mod a = 0"
1.136 -  using mod_mult_self2_is_0 [of 1] by simp
1.137 -
1.139    assumes "b \<noteq> 0"
1.140    shows "(b + a) div b = a div b + 1"
1.141 @@ -116,31 +162,6 @@
1.142    "(a + b) mod b = a mod b"
1.143    using mod_mult_self1 [of a 1 b] by simp
1.144
1.145 -lemma dvd_imp_mod_0 [simp]:
1.146 -  assumes "a dvd b"
1.147 -  shows "b mod a = 0"
1.148 -proof -
1.149 -  from assms obtain c where "b = a * c" ..
1.150 -  then have "b mod a = a * c mod a" by simp
1.151 -  then show "b mod a = 0" by simp
1.152 -qed
1.153 -
1.154 -lemma mod_eq_0_iff_dvd:
1.155 -  "a mod b = 0 \<longleftrightarrow> b dvd a"
1.156 -proof
1.157 -  assume "b dvd a"
1.158 -  then show "a mod b = 0" by simp
1.159 -next
1.160 -  assume "a mod b = 0"
1.161 -  with div_mult_mod_eq [of a b] have "a div b * b = a" by simp
1.162 -  then have "a = b * (a div b)" by (simp add: ac_simps)
1.163 -  then show "b dvd a" ..
1.164 -qed
1.165 -
1.166 -lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
1.167 -  "a dvd b \<longleftrightarrow> b mod a = 0"
1.168 -  by (simp add: mod_eq_0_iff_dvd)
1.169 -
1.170  lemma mod_div_trivial [simp]:
1.171    "a mod b div b = 0"
1.172  proof (cases "b = 0")
1.173 @@ -168,15 +189,6 @@
1.174    finally show ?thesis .
1.175  qed
1.176
1.177 -lemma dvd_mod_imp_dvd:
1.178 -  assumes "k dvd m mod n" and "k dvd n"
1.179 -  shows "k dvd m"
1.180 -proof -
1.181 -  from assms have "k dvd (m div n) * n + m mod n"
1.182 -    by (simp only: dvd_add dvd_mult)
1.183 -  then show ?thesis by (simp add: div_mult_mod_eq)
1.184 -qed
1.185 -
1.186  text \<open>Addition respects modular equivalence.\<close>
1.187
1.188  lemma mod_add_left_eq: \<comment> \<open>FIXME reorient\<close>
1.189 @@ -319,31 +331,6 @@
1.190  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
1.191    unfolding dvd_def by (auto simp add: mod_mult_mult1)
1.192
1.193 -lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
1.194 -by (blast intro: dvd_mod_imp_dvd dvd_mod)
1.195 -
1.196 -lemma div_div_eq_right:
1.197 -  assumes "c dvd b" "b dvd a"
1.198 -  shows   "a div (b div c) = a div b * c"
1.199 -proof -
1.200 -  from assms have "a div b * c = (a * c) div b"
1.201 -    by (subst dvd_div_mult) simp_all
1.202 -  also from assms have "\<dots> = (a * c) div ((b div c) * c)" by simp
1.203 -  also have "a * c div (b div c * c) = a div (b div c)"
1.204 -    by (cases "c = 0") simp_all
1.205 -  finally show ?thesis ..
1.206 -qed
1.207 -
1.208 -lemma div_div_div_same:
1.209 -  assumes "d dvd a" "d dvd b" "b dvd a"
1.210 -  shows   "(a div d) div (b div d) = a div b"
1.211 -  using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
1.212 -
1.213 -lemma cancel_div_mod_rules:
1.214 -  "((a div b) * b + a mod b) + c = a + c"
1.215 -  "(b * (a div b) + a mod b) + c = a + c"
1.216 -  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
1.217 -
1.218  end
1.219
1.220  class ring_div = comm_ring_1 + semiring_div
1.221 @@ -394,28 +381,6 @@
1.222    shows "(a - b) mod c = (a' - b') mod c"
1.223    using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
1.224
1.225 -lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
1.226 -apply (case_tac "y = 0") apply simp
1.227 -apply (auto simp add: dvd_def)
1.228 -apply (subgoal_tac "-(y * k) = y * - k")
1.229 - apply (simp only:)
1.230 - apply (erule nonzero_mult_div_cancel_left)
1.231 -apply simp
1.232 -done
1.233 -
1.234 -lemma dvd_div_neg: "y dvd x \<Longrightarrow> x div -y = - (x div y)"
1.235 -apply (case_tac "y = 0") apply simp
1.236 -apply (auto simp add: dvd_def)
1.237 -apply (subgoal_tac "y * k = -y * -k")
1.238 - apply (erule ssubst, rule nonzero_mult_div_cancel_left)
1.239 - apply simp
1.240 -apply simp
1.241 -done
1.242 -
1.243 -lemma div_diff [simp]:
1.244 -  "z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x - y) div z = x div z - y div z"
1.245 -  using div_add [of _ _ "- y"] by (simp add: dvd_neg_div)
1.246 -
1.247  lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
1.248    using div_mult_mult1 [of "- 1" a b]
1.249    unfolding neg_equal_0_iff_equal by simp
1.250 @@ -446,7 +411,7 @@
1.251  end
1.252
1.253
1.254 -subsubsection \<open>Parity and division\<close>
1.255 +subsection \<open>Parity\<close>
1.256
1.257  class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
1.258    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
1.259 @@ -532,7 +497,7 @@
1.260  end
1.261
1.262
1.263 -subsection \<open>Generic numeral division with a pragmatic type class\<close>
1.264 +subsection \<open>Numeral division with a pragmatic type class\<close>
1.265
1.266  text \<open>
1.267    The following type class contains everything necessary to formulate
1.268 @@ -826,8 +791,10 @@
1.269        from m n have "Suc m = q' * n + Suc r'" by simp
1.270        with True show ?thesis by blast
1.271      next
1.272 -      case False then have "n \<le> Suc r'" by auto
1.273 -      moreover from n have "Suc r' \<le> n" by auto
1.274 +      case False then have "n \<le> Suc r'"
1.275 +        by (simp add: not_less)
1.276 +      moreover from n have "Suc r' \<le> n"
1.277 +        by (simp add: Suc_le_eq)
1.278        ultimately have "n = Suc r'" by auto
1.279        with m have "Suc m = Suc q' * n + 0" by simp
1.280        with \<open>n \<noteq> 0\<close> show ?thesis by blast
1.281 @@ -855,7 +822,7 @@
1.283    done
1.284    from \<open>n \<noteq> 0\<close> assms have *: "fst qr = fst qr'"
1.285 -    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
1.286 +    by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym split: if_splits)
1.287    with assms have "snd qr = snd qr'"
1.289    with * show ?thesis by (cases qr, cases qr') simp
1.290 @@ -884,10 +851,10 @@
1.291    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
1.292
1.293  qualified lemma divmod_nat_zero: "divmod_nat m 0 = (0, m)"
1.294 -  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
1.295 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
1.296
1.297  qualified lemma divmod_nat_zero_left: "divmod_nat 0 n = (0, 0)"
1.298 -  by (simp add: Divides.divmod_nat_unique divmod_nat_rel_def)
1.299 +  by (simp add: divmod_nat_unique divmod_nat_rel_def)
1.300
1.301  qualified lemma divmod_nat_base: "m < n \<Longrightarrow> divmod_nat m n = (0, m)"
1.302    by (simp add: divmod_nat_unique divmod_nat_rel_def)
1.303 @@ -899,19 +866,31 @@
1.304    have "divmod_nat_rel (m - n) n (divmod_nat (m - n) n)"
1.305      by (fact divmod_nat_rel_divmod_nat)
1.306    then show "divmod_nat_rel m n (apfst Suc (divmod_nat (m - n) n))"
1.307 -    unfolding divmod_nat_rel_def using assms by auto
1.308 +    unfolding divmod_nat_rel_def using assms
1.309 +      by (auto split: if_splits simp add: algebra_simps)
1.310  qed
1.311
1.312  end
1.313 -
1.314 -instantiation nat :: semiring_div
1.315 +
1.316 +instantiation nat :: "{semidom_modulo, normalization_semidom}"
1.317  begin
1.318
1.319 -definition divide_nat where
1.320 -  div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
1.321 -
1.322 -definition modulo_nat where
1.323 -  mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
1.324 +definition normalize_nat :: "nat \<Rightarrow> nat"
1.325 +  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
1.326 +
1.327 +definition unit_factor_nat :: "nat \<Rightarrow> nat"
1.328 +  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
1.329 +
1.330 +lemma unit_factor_simps [simp]:
1.331 +  "unit_factor 0 = (0::nat)"
1.332 +  "unit_factor (Suc n) = 1"
1.333 +  by (simp_all add: unit_factor_nat_def)
1.334 +
1.335 +definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.336 +  where div_nat_def: "m div n = fst (Divides.divmod_nat m n)"
1.337 +
1.338 +definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.339 +  where mod_nat_def: "m mod n = snd (Divides.divmod_nat m n)"
1.340
1.341  lemma fst_divmod_nat [simp]:
1.342    "fst (Divides.divmod_nat m n) = m div n"
1.343 @@ -928,15 +907,18 @@
1.344  lemma div_nat_unique:
1.345    assumes "divmod_nat_rel m n (q, r)"
1.346    shows "m div n = q"
1.347 -  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
1.348 +  using assms
1.349 +  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
1.350
1.351  lemma mod_nat_unique:
1.352    assumes "divmod_nat_rel m n (q, r)"
1.353    shows "m mod n = r"
1.354 -  using assms by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
1.355 +  using assms
1.356 +  by (auto dest!: Divides.divmod_nat_unique simp add: prod_eq_iff)
1.357
1.358  lemma divmod_nat_rel: "divmod_nat_rel m n (m div n, m mod n)"
1.359 -  using Divides.divmod_nat_rel_divmod_nat by (simp add: divmod_nat_div_mod)
1.360 +  using Divides.divmod_nat_rel_divmod_nat
1.361 +  by (simp add: divmod_nat_div_mod)
1.362
1.363  text \<open>The ''recursion'' equations for @{const divide} and @{const modulo}\<close>
1.364
1.365 @@ -964,11 +946,40 @@
1.366    shows "m mod n = (m - n) mod n"
1.367    using assms Divides.divmod_nat_step by (cases "n = 0") (simp_all add: prod_eq_iff)
1.368
1.369 +lemma mod_less_divisor [simp]:
1.370 +  fixes m n :: nat
1.371 +  assumes "n > 0"
1.372 +  shows "m mod n < n"
1.373 +  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def
1.374 +  by (auto split: if_splits)
1.375 +
1.376 +lemma mod_le_divisor [simp]:
1.377 +  fixes m n :: nat
1.378 +  assumes "n > 0"
1.379 +  shows "m mod n \<le> n"
1.380 +proof (rule less_imp_le)
1.381 +  from assms show "m mod n < n"
1.382 +    by simp
1.383 +qed
1.384 +
1.385  instance proof
1.386    fix m n :: nat
1.387    show "m div n * n + m mod n = m"
1.388      using divmod_nat_rel [of m n] by (simp add: divmod_nat_rel_def)
1.389  next
1.390 +  fix n :: nat show "n div 0 = 0"
1.391 +    by (simp add: div_nat_def Divides.divmod_nat_zero)
1.392 +next
1.393 +  fix m n :: nat
1.394 +  assume "n \<noteq> 0"
1.395 +  then show "m * n div n = m"
1.396 +    by (auto simp add: divmod_nat_rel_def intro: div_nat_unique [of _ _ _ 0])
1.398 +
1.399 +end
1.400 +
1.401 +instance nat :: semiring_div
1.402 +proof
1.403    fix m n q :: nat
1.404    assume "n \<noteq> 0"
1.405    then show "(q + m * n) div n = m + q div n"
1.406 @@ -976,48 +987,33 @@
1.407  next
1.408    fix m n q :: nat
1.409    assume "m \<noteq> 0"
1.410 -  hence "\<And>a b. divmod_nat_rel n q (a, b) \<Longrightarrow> divmod_nat_rel (m * n) (m * q) (a, m * b)"
1.411 -    unfolding divmod_nat_rel_def
1.412 -    by (auto split: if_split_asm, simp_all add: algebra_simps)
1.413 -  moreover from divmod_nat_rel have "divmod_nat_rel n q (n div q, n mod q)" .
1.414 -  ultimately have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))" .
1.415 -  thus "(m * n) div (m * q) = n div q" by (rule div_nat_unique)
1.416 -next
1.417 -  fix n :: nat show "n div 0 = 0"
1.418 -    by (simp add: div_nat_def Divides.divmod_nat_zero)
1.419 -next
1.420 -  fix n :: nat show "0 div n = 0"
1.421 -    by (simp add: div_nat_def Divides.divmod_nat_zero_left)
1.422 +  then have "divmod_nat_rel (m * n) (m * q) (n div q, m * (n mod q))"
1.423 +    using div_mult_mod_eq [of n q]
1.424 +    by (auto simp add: divmod_nat_rel_def algebra_simps distrib_left [symmetric] simp del: distrib_left)
1.425 +  then show "(m * n) div (m * q) = n div q"
1.426 +    by (rule div_nat_unique)
1.427  qed
1.428
1.429 -end
1.430 -
1.431 -instantiation nat :: normalization_semidom
1.432 -begin
1.433 -
1.434 -definition normalize_nat
1.435 -  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
1.436 -
1.437 -definition unit_factor_nat
1.438 -  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
1.439 -
1.440 -lemma unit_factor_simps [simp]:
1.441 -  "unit_factor 0 = (0::nat)"
1.442 -  "unit_factor (Suc n) = 1"
1.443 -  by (simp_all add: unit_factor_nat_def)
1.444 -
1.445 -instance
1.446 -  by standard (simp_all add: unit_factor_nat_def)
1.447 -
1.448 -end
1.449 -
1.450 -lemma divmod_nat_if [code]:
1.451 -  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
1.452 -    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
1.453 -  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
1.454 +lemma div_by_Suc_0 [simp]:
1.455 +  "m div Suc 0 = m"
1.456 +  using div_by_1 [of m] by simp
1.457 +
1.458 +lemma mod_by_Suc_0 [simp]:
1.459 +  "m mod Suc 0 = 0"
1.460 +  using mod_by_1 [of m] by simp
1.461 +
1.462 +lemma mod_greater_zero_iff_not_dvd:
1.463 +  fixes m n :: nat
1.464 +  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
1.465 +  by (simp add: dvd_eq_mod_eq_0)
1.466
1.467  text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
1.468
1.469 +lemma (in semiring_modulo) cancel_div_mod_rules:
1.470 +  "((a div b) * b + a mod b) + c = a + c"
1.471 +  "(b * (a div b) + a mod b) + c = a + c"
1.472 +  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
1.473 +
1.474  ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
1.475
1.476  ML \<open>
1.477 @@ -1048,7 +1044,13 @@
1.478  )
1.479  \<close>
1.480
1.481 -simproc_setup cancel_div_mod_nat ("(m::nat) + n") = \<open>K Cancel_Div_Mod_Nat.proc\<close>
1.482 +simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
1.483 +  \<open>K Cancel_Div_Mod_Nat.proc\<close>
1.484 +
1.485 +lemma divmod_nat_if [code]:
1.486 +  "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
1.487 +    let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
1.488 +  by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
1.489
1.490
1.491  subsubsection \<open>Quotient\<close>
1.492 @@ -1077,16 +1079,11 @@
1.493  qed
1.494
1.495  lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
1.496 -  by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less)
1.497 +  by auto (metis div_positive less_numeral_extra(3) not_less)
1.498 +
1.499
1.500  subsubsection \<open>Remainder\<close>
1.501
1.502 -lemma mod_less_divisor [simp]:
1.503 -  fixes m n :: nat
1.504 -  assumes "n > 0"
1.505 -  shows "m mod n < (n::nat)"
1.506 -  using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
1.507 -
1.508  lemma mod_Suc_le_divisor [simp]:
1.509    "m mod Suc n \<le> n"
1.510    using mod_less_divisor [of "Suc n" m] by arith
1.511 @@ -1105,13 +1102,6 @@
1.512  lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
1.514
1.515 -lemma mod_by_Suc_0 [simp]: "m mod Suc 0 = 0"
1.516 -by (induct m) (simp_all add: mod_geq)
1.517 -
1.518 -lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
1.519 -  apply (drule mod_less_divisor [where m = m])
1.520 -  apply simp
1.521 -  done
1.522
1.523  subsubsection \<open>Quotient and Remainder\<close>
1.524
1.525 @@ -1180,25 +1170,16 @@
1.526
1.527  subsubsection \<open>Further Facts about Quotient and Remainder\<close>
1.528
1.529 -lemma div_by_Suc_0 [simp]:
1.530 -  "m div Suc 0 = m"
1.531 -  using div_by_1 [of m] by simp
1.532 -
1.533 -(* Monotonicity of div in first argument *)
1.534 -lemma div_le_mono [rule_format (no_asm)]:
1.535 -    "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
1.536 -apply (case_tac "k=0", simp)
1.537 -apply (induct "n" rule: nat_less_induct, clarify)
1.538 -apply (case_tac "n<k")
1.539 -(* 1  case n<k *)
1.540 -apply simp
1.541 -(* 2  case n >= k *)
1.542 -apply (case_tac "m<k")
1.543 -(* 2.1  case m<k *)
1.544 -apply simp
1.545 -(* 2.2  case m>=k *)
1.546 -apply (simp add: div_geq diff_le_mono)
1.547 -done
1.548 +lemma div_le_mono:
1.549 +  fixes m n k :: nat
1.550 +  assumes "m \<le> n"
1.551 +  shows "m div k \<le> n div k"
1.552 +proof -
1.553 +  from assms obtain q where "n = m + q"
1.555 +  then show ?thesis
1.557 +qed
1.558
1.559  (* Antimonotonicity of div in second argument *)
1.560  lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
1.561 @@ -1519,11 +1500,6 @@
1.562
1.563  declare Suc_times_mod_eq [of "numeral w", simp] for w
1.564
1.565 -lemma mod_greater_zero_iff_not_dvd:
1.566 -  fixes m n :: nat
1.567 -  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
1.568 -  by (simp add: dvd_eq_mod_eq_0)
1.569 -
1.570  lemma Suc_div_le_mono [simp]: "n div k \<le> (Suc n) div k"
1.572
1.573 @@ -1643,6 +1619,9 @@
1.574
1.575  subsection \<open>Division on @{typ int}\<close>
1.576
1.577 +context
1.578 +begin
1.579 +
1.580  definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" \<comment> \<open>definition of quotient and remainder\<close>
1.581    where "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
1.582      (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
1.583 @@ -1678,10 +1657,18 @@
1.584  apply (blast intro: unique_quotient)
1.585  done
1.586
1.587 -instantiation int :: modulo
1.588 +end
1.589 +
1.590 +instantiation int :: "{idom_modulo, normalization_semidom}"
1.591  begin
1.592
1.593 -definition divide_int
1.594 +definition normalize_int :: "int \<Rightarrow> int"
1.595 +  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
1.596 +
1.597 +definition unit_factor_int :: "int \<Rightarrow> int"
1.598 +  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
1.599 +
1.600 +definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int"
1.601    where "k div l = (if l = 0 \<or> k = 0 then 0
1.602      else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
1.603        then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
1.604 @@ -1689,32 +1676,35 @@
1.605          if l dvd k then - int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)
1.606          else - int (Suc (nat \<bar>k\<bar> div nat \<bar>l\<bar>)))"
1.607
1.608 -definition modulo_int
1.609 +definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int"
1.610    where "k mod l = (if l = 0 then k else if l dvd k then 0
1.611      else if k > 0 \<and> l > 0 \<or> k < 0 \<and> l < 0
1.612        then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)
1.613        else sgn l * (\<bar>l\<bar> - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))"
1.614
1.615 -instance ..
1.616 -
1.617 -end
1.618 -
1.619  lemma divmod_int_rel:
1.620    "divmod_int_rel k l (k div l, k mod l)"
1.621 -  unfolding divmod_int_rel_def divide_int_def modulo_int_def
1.622 -  apply (cases k rule: int_cases3)
1.623 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
1.624 -  apply (cases l rule: int_cases3)
1.625 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
1.627 -  apply (cases l rule: int_cases3)
1.629 -  done
1.630 -
1.631 -instantiation int :: ring_div
1.632 -begin
1.633 -
1.634 -subsubsection \<open>Uniqueness and Monotonicity of Quotients and Remainders\<close>
1.635 +proof (cases k rule: int_cases3)
1.636 +  case zero
1.637 +  then show ?thesis
1.638 +    by (simp add: divmod_int_rel_def divide_int_def modulo_int_def)
1.639 +next
1.640 +  case (pos n)
1.641 +  then show ?thesis
1.642 +    using div_mult_mod_eq [of n]
1.643 +    by (cases l rule: int_cases3)
1.644 +      (auto simp del: of_nat_mult of_nat_add
1.646 +        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
1.647 +next
1.648 +  case (neg n)
1.649 +  then show ?thesis
1.650 +    using div_mult_mod_eq [of n]
1.651 +    by (cases l rule: int_cases3)
1.652 +      (auto simp del: of_nat_mult of_nat_add
1.654 +        divmod_int_rel_def divide_int_def modulo_int_def int_dvd_iff)
1.655 +qed
1.656
1.657  lemma divmod_int_unique:
1.658    assumes "divmod_int_rel k l (q, r)"
1.659 @@ -1722,42 +1712,21 @@
1.660    using assms divmod_int_rel [of k l]
1.661    using unique_quotient [of k l] unique_remainder [of k l]
1.662    by auto
1.663 -
1.664 -instance
1.665 -proof
1.666 -  fix a b :: int
1.667 -  show "a div b * b + a mod b = a"
1.668 -    using divmod_int_rel [of a b]
1.669 -    unfolding divmod_int_rel_def by (simp add: mult.commute)
1.670 -next
1.671 -  fix a b c :: int
1.672 -  assume "b \<noteq> 0"
1.673 -  hence "divmod_int_rel (a + c * b) b (c + a div b, a mod b)"
1.674 -    using divmod_int_rel [of a b]
1.675 -    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
1.676 -  thus "(a + c * b) div b = c + a div b"
1.677 -    by (rule div_int_unique)
1.678 +
1.679 +instance proof
1.680 +  fix k l :: int
1.681 +  show "k div l * l + k mod l = k"
1.682 +    using divmod_int_rel [of k l]
1.683 +    unfolding divmod_int_rel_def by (simp add: ac_simps)
1.684  next
1.685 -  fix a b c :: int
1.686 -  assume c: "c \<noteq> 0"
1.687 -  have "\<And>q r. divmod_int_rel a b (q, r)
1.688 -    \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
1.689 -    unfolding divmod_int_rel_def
1.690 -    by (rule linorder_cases [of 0 b])
1.691 -      (use c in \<open>auto simp: algebra_simps
1.692 -      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
1.693 -      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
1.694 -  hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
1.695 -    using divmod_int_rel [of a b] .
1.696 -  thus "(c * a) div (c * b) = a div b"
1.697 -    by (rule div_int_unique)
1.698 -next
1.699 -  fix a :: int show "a div 0 = 0"
1.700 +  fix k :: int show "k div 0 = 0"
1.701      by (rule div_int_unique, simp add: divmod_int_rel_def)
1.702  next
1.703 -  fix a :: int show "0 div a = 0"
1.704 -    by (rule div_int_unique, auto simp add: divmod_int_rel_def)
1.705 -qed
1.706 +  fix k l :: int
1.707 +  assume "l \<noteq> 0"
1.708 +  then show "k * l div l = k"
1.709 +    by (auto simp add: divmod_int_rel_def ac_simps intro: div_int_unique [of _ _ _ 0])
1.710 +qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
1.711
1.712  end
1.713
1.714 @@ -1765,36 +1734,30 @@
1.715    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
1.716    by auto
1.717
1.718 -instantiation int :: normalization_semidom
1.719 -begin
1.720 -
1.721 -definition normalize_int
1.722 -  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
1.723 -
1.724 -definition unit_factor_int
1.725 -  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
1.726 -
1.727 -instance
1.728 +instance int :: ring_div
1.729  proof
1.730 -  fix k :: int
1.731 -  assume "k \<noteq> 0"
1.732 -  then have "\<bar>sgn k\<bar> = 1"
1.733 -    by (cases "0::int" k rule: linorder_cases) simp_all
1.734 -  then show "is_unit (unit_factor k)"
1.735 -    by simp
1.736 -qed (simp_all add: sgn_mult mult_sgn_abs)
1.737 -
1.738 -end
1.739 -
1.740 -text\<open>Basic laws about division and remainder\<close>
1.741 -
1.742 -lemma zdiv_int: "int (a div b) = int a div int b"
1.743 -  by (simp add: divide_int_def)
1.744 -
1.745 -lemma zmod_int: "int (a mod b) = int a mod int b"
1.746 -  by (simp add: modulo_int_def int_dvd_iff)
1.747 -
1.748 -text \<open>Tool setup\<close>
1.749 +  fix k l s :: int
1.750 +  assume "l \<noteq> 0"
1.751 +  then have "divmod_int_rel (k + s * l) l (s + k div l, k mod l)"
1.752 +    using divmod_int_rel [of k l]
1.753 +    unfolding divmod_int_rel_def by (auto simp: algebra_simps)
1.754 +  then show "(k + s * l) div l = s + k div l"
1.755 +    by (rule div_int_unique)
1.756 +next
1.757 +  fix k l s :: int
1.758 +  assume "s \<noteq> 0"
1.759 +  have "\<And>q r. divmod_int_rel k l (q, r)
1.760 +    \<Longrightarrow> divmod_int_rel (s * k) (s * l) (q, s * r)"
1.761 +    unfolding divmod_int_rel_def
1.762 +    by (rule linorder_cases [of 0 l])
1.763 +      (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
1.764 +      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
1.765 +      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
1.766 +  then have "divmod_int_rel (s * k) (s * l) (k div l, s * (k mod l))"
1.767 +    using divmod_int_rel [of k l] .
1.768 +  then show "(s * k) div (s * l) = k div l"
1.769 +    by (rule div_int_unique)
1.770 +qed
1.771
1.772  ML \<open>
1.773  structure Cancel_Div_Mod_Int = Cancel_Div_Mod
1.774 @@ -1807,12 +1770,22 @@
1.775
1.776    val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
1.777
1.778 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
1.780 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
1.782  )
1.783  \<close>
1.784
1.785 -simproc_setup cancel_div_mod_int ("(k::int) + l") = \<open>K Cancel_Div_Mod_Int.proc\<close>
1.786 +simproc_setup cancel_div_mod_int ("(k::int) + l") =
1.787 +  \<open>K Cancel_Div_Mod_Int.proc\<close>
1.788 +
1.789 +
1.790 +text\<open>Basic laws about division and remainder\<close>
1.791 +
1.792 +lemma zdiv_int: "int (a div b) = int a div int b"
1.793 +  by (simp add: divide_int_def)
1.794 +
1.795 +lemma zmod_int: "int (a mod b) = int a mod int b"
1.796 +  by (simp add: modulo_int_def int_dvd_iff)
1.797
1.798  lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
1.799    using divmod_int_rel [of a b]
1.800 @@ -1887,10 +1860,15 @@
1.801  apply (blast intro: divmod_int_rel [THEN zminus1_lemma, THEN mod_int_unique])
1.802  done
1.803
1.804 -lemma zmod_zminus1_not_zero:
1.805 +lemma zmod_zminus1_not_zero: -- \<open>FIXME generalize\<close>
1.806    fixes k l :: int
1.807    shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
1.808 -  unfolding zmod_zminus1_eq_if by auto
1.809 +  by (simp add: mod_eq_0_iff_dvd)
1.810 +
1.811 +lemma zmod_zminus2_not_zero: -- \<open>FIXME generalize\<close>
1.812 +  fixes k l :: int
1.813 +  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
1.814 +  by (simp add: mod_eq_0_iff_dvd)
1.815
1.816  lemma zdiv_zminus2_eq_if:
1.817       "b \<noteq> (0::int)
1.818 @@ -1902,11 +1880,6 @@
1.819       "a mod (-b::int) = (if a mod b = 0 then 0 else  (a mod b) - b)"
1.820  by (simp add: zmod_zminus1_eq_if mod_minus_right)
1.821
1.822 -lemma zmod_zminus2_not_zero:
1.823 -  fixes k l :: int
1.824 -  shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
1.825 -  unfolding zmod_zminus2_eq_if by auto
1.826 -
1.827
1.828  subsubsection \<open>Monotonicity in the First Argument (Dividend)\<close>
1.829
1.830 @@ -2666,6 +2639,4 @@
1.831
1.832  declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]
1.833
1.834 -hide_fact (open) div_0 div_by_0
1.835 -
1.836  end
```