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.71 +    by (simp add: dvd_add_right_iff)
    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.109 -qed (simp add: div_by_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.138  lemma div_add_self1:
   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.282    apply (auto simp add: add_mult_distrib)
   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.288      by (simp add: divmod_nat_rel_def)
   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.397 +qed (simp_all add: unit_factor_nat_def)
   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.513  by (simp add: le_mod_geq)
   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.554 +    by (auto simp add: le_iff_add)
   1.555 +  then show ?thesis
   1.556 +    by (simp add: div_add1_eq [of m q k])
   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.571  by (simp add: div_le_mono)
   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.626 -  apply (simp_all del: of_nat_add of_nat_mult add: mod_greater_zero_iff_not_dvd not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
   1.627 -  apply (cases l rule: int_cases3)
   1.628 -  apply (simp_all del: of_nat_add of_nat_mult add: not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
   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.645 +        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   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.653 +        simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
   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.779 -    (Arith_Data.simp_all_tac @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   1.780 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   1.781 +    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   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