src/HOL/Divides.thy
changeset 66806 a4e82b58d833
parent 66801 f3fda9777f9a
child 66808 1907167b6038
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -9,433 +9,9 @@
     1.4  imports Parity
     1.5  begin
     1.6  
     1.7 -subsection \<open>Quotient and remainder in integral domains with additional properties\<close>
     1.8 -
     1.9 -class semiring_div = semidom_modulo +
    1.10 -  assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    1.11 -    and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
    1.12 -begin
    1.13 -
    1.14 -lemma div_mult_self2 [simp]:
    1.15 -  assumes "b \<noteq> 0"
    1.16 -  shows "(a + b * c) div b = c + a div b"
    1.17 -  using assms div_mult_self1 [of b a c] by (simp add: mult.commute)
    1.18 -
    1.19 -lemma div_mult_self3 [simp]:
    1.20 -  assumes "b \<noteq> 0"
    1.21 -  shows "(c * b + a) div b = c + a div b"
    1.22 -  using assms by (simp add: add.commute)
    1.23 -
    1.24 -lemma div_mult_self4 [simp]:
    1.25 -  assumes "b \<noteq> 0"
    1.26 -  shows "(b * c + a) div b = c + a div b"
    1.27 -  using assms by (simp add: add.commute)
    1.28 -
    1.29 -lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b"
    1.30 -proof (cases "b = 0")
    1.31 -  case True then show ?thesis by simp
    1.32 -next
    1.33 -  case False
    1.34 -  have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b"
    1.35 -    by (simp add: div_mult_mod_eq)
    1.36 -  also from False div_mult_self1 [of b a c] have
    1.37 -    "\<dots> = (c + a div b) * b + (a + c * b) mod b"
    1.38 -      by (simp add: algebra_simps)
    1.39 -  finally have "a = a div b * b + (a + c * b) mod b"
    1.40 -    by (simp add: add.commute [of a] add.assoc distrib_right)
    1.41 -  then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
    1.42 -    by (simp add: div_mult_mod_eq)
    1.43 -  then show ?thesis by simp
    1.44 -qed
    1.45 -
    1.46 -lemma mod_mult_self2 [simp]:
    1.47 -  "(a + b * c) mod b = a mod b"
    1.48 -  by (simp add: mult.commute [of b])
    1.49 -
    1.50 -lemma mod_mult_self3 [simp]:
    1.51 -  "(c * b + a) mod b = a mod b"
    1.52 -  by (simp add: add.commute)
    1.53 -
    1.54 -lemma mod_mult_self4 [simp]:
    1.55 -  "(b * c + a) mod b = a mod b"
    1.56 -  by (simp add: add.commute)
    1.57 -
    1.58 -lemma mod_mult_self1_is_0 [simp]:
    1.59 -  "b * a mod b = 0"
    1.60 -  using mod_mult_self2 [of 0 b a] by simp
    1.61 -
    1.62 -lemma mod_mult_self2_is_0 [simp]:
    1.63 -  "a * b mod b = 0"
    1.64 -  using mod_mult_self1 [of 0 a b] by simp
    1.65 -
    1.66 -lemma div_add_self1:
    1.67 -  assumes "b \<noteq> 0"
    1.68 -  shows "(b + a) div b = a div b + 1"
    1.69 -  using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
    1.70 -
    1.71 -lemma div_add_self2:
    1.72 -  assumes "b \<noteq> 0"
    1.73 -  shows "(a + b) div b = a div b + 1"
    1.74 -  using assms div_add_self1 [of b a] by (simp add: add.commute)
    1.75 -
    1.76 -lemma mod_add_self1 [simp]:
    1.77 -  "(b + a) mod b = a mod b"
    1.78 -  using mod_mult_self1 [of a 1 b] by (simp add: add.commute)
    1.79 -
    1.80 -lemma mod_add_self2 [simp]:
    1.81 -  "(a + b) mod b = a mod b"
    1.82 -  using mod_mult_self1 [of a 1 b] by simp
    1.83 -
    1.84 -lemma mod_div_trivial [simp]:
    1.85 -  "a mod b div b = 0"
    1.86 -proof (cases "b = 0")
    1.87 -  assume "b = 0"
    1.88 -  thus ?thesis by simp
    1.89 -next
    1.90 -  assume "b \<noteq> 0"
    1.91 -  hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
    1.92 -    by (rule div_mult_self1 [symmetric])
    1.93 -  also have "\<dots> = a div b"
    1.94 -    by (simp only: mod_div_mult_eq)
    1.95 -  also have "\<dots> = a div b + 0"
    1.96 -    by simp
    1.97 -  finally show ?thesis
    1.98 -    by (rule add_left_imp_eq)
    1.99 -qed
   1.100 -
   1.101 -lemma mod_mod_trivial [simp]:
   1.102 -  "a mod b mod b = a mod b"
   1.103 -proof -
   1.104 -  have "a mod b mod b = (a mod b + a div b * b) mod b"
   1.105 -    by (simp only: mod_mult_self1)
   1.106 -  also have "\<dots> = a mod b"
   1.107 -    by (simp only: mod_div_mult_eq)
   1.108 -  finally show ?thesis .
   1.109 -qed
   1.110 -
   1.111 -lemma mod_mod_cancel:
   1.112 -  assumes "c dvd b"
   1.113 -  shows "a mod b mod c = a mod c"
   1.114 -proof -
   1.115 -  from \<open>c dvd b\<close> obtain k where "b = c * k"
   1.116 -    by (rule dvdE)
   1.117 -  have "a mod b mod c = a mod (c * k) mod c"
   1.118 -    by (simp only: \<open>b = c * k\<close>)
   1.119 -  also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
   1.120 -    by (simp only: mod_mult_self1)
   1.121 -  also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
   1.122 -    by (simp only: ac_simps)
   1.123 -  also have "\<dots> = a mod c"
   1.124 -    by (simp only: div_mult_mod_eq)
   1.125 -  finally show ?thesis .
   1.126 -qed
   1.127 -
   1.128 -lemma div_mult_mult2 [simp]:
   1.129 -  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   1.130 -  by (drule div_mult_mult1) (simp add: mult.commute)
   1.131 -
   1.132 -lemma div_mult_mult1_if [simp]:
   1.133 -  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
   1.134 -  by simp_all
   1.135 -
   1.136 -lemma mod_mult_mult1:
   1.137 -  "(c * a) mod (c * b) = c * (a mod b)"
   1.138 -proof (cases "c = 0")
   1.139 -  case True then show ?thesis by simp
   1.140 -next
   1.141 -  case False
   1.142 -  from div_mult_mod_eq
   1.143 -  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
   1.144 -  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
   1.145 -    = c * a + c * (a mod b)" by (simp add: algebra_simps)
   1.146 -  with div_mult_mod_eq show ?thesis by simp
   1.147 -qed
   1.148 -
   1.149 -lemma mod_mult_mult2:
   1.150 -  "(a * c) mod (b * c) = (a mod b) * c"
   1.151 -  using mod_mult_mult1 [of c a b] by (simp add: mult.commute)
   1.152 -
   1.153 -lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)"
   1.154 -  by (fact mod_mult_mult2 [symmetric])
   1.155 -
   1.156 -lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   1.157 -  by (fact mod_mult_mult1 [symmetric])
   1.158 -
   1.159 -lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   1.160 -  unfolding dvd_def by (auto simp add: mod_mult_mult1)
   1.161 -
   1.162 -lemma div_plus_div_distrib_dvd_left:
   1.163 -  "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c"
   1.164 -  by (cases "c = 0") (auto elim: dvdE)
   1.165 -
   1.166 -lemma div_plus_div_distrib_dvd_right:
   1.167 -  "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c"
   1.168 -  using div_plus_div_distrib_dvd_left [of c b a]
   1.169 -  by (simp add: ac_simps)
   1.170 -
   1.171 -named_theorems mod_simps
   1.172 -
   1.173 -text \<open>Addition respects modular equivalence.\<close>
   1.174 -
   1.175 -lemma mod_add_left_eq [mod_simps]:
   1.176 -  "(a mod c + b) mod c = (a + b) mod c"
   1.177 -proof -
   1.178 -  have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
   1.179 -    by (simp only: div_mult_mod_eq)
   1.180 -  also have "\<dots> = (a mod c + b + a div c * c) mod c"
   1.181 -    by (simp only: ac_simps)
   1.182 -  also have "\<dots> = (a mod c + b) mod c"
   1.183 -    by (rule mod_mult_self1)
   1.184 -  finally show ?thesis
   1.185 -    by (rule sym)
   1.186 -qed
   1.187 -
   1.188 -lemma mod_add_right_eq [mod_simps]:
   1.189 -  "(a + b mod c) mod c = (a + b) mod c"
   1.190 -  using mod_add_left_eq [of b c a] by (simp add: ac_simps)
   1.191 -
   1.192 -lemma mod_add_eq:
   1.193 -  "(a mod c + b mod c) mod c = (a + b) mod c"
   1.194 -  by (simp add: mod_add_left_eq mod_add_right_eq)
   1.195 -
   1.196 -lemma mod_sum_eq [mod_simps]:
   1.197 -  "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a"
   1.198 -proof (induct A rule: infinite_finite_induct)
   1.199 -  case (insert i A)
   1.200 -  then have "(\<Sum>i\<in>insert i A. f i mod a) mod a
   1.201 -    = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a"
   1.202 -    by simp
   1.203 -  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a"
   1.204 -    by (simp add: mod_simps)
   1.205 -  also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a"
   1.206 -    by (simp add: insert.hyps)
   1.207 -  finally show ?case
   1.208 -    by (simp add: insert.hyps mod_simps)
   1.209 -qed simp_all
   1.210 -
   1.211 -lemma mod_add_cong:
   1.212 -  assumes "a mod c = a' mod c"
   1.213 -  assumes "b mod c = b' mod c"
   1.214 -  shows "(a + b) mod c = (a' + b') mod c"
   1.215 -proof -
   1.216 -  have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
   1.217 -    unfolding assms ..
   1.218 -  then show ?thesis
   1.219 -    by (simp add: mod_add_eq)
   1.220 -qed
   1.221 -
   1.222 -text \<open>Multiplication respects modular equivalence.\<close>
   1.223 -
   1.224 -lemma mod_mult_left_eq [mod_simps]:
   1.225 -  "((a mod c) * b) mod c = (a * b) mod c"
   1.226 -proof -
   1.227 -  have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
   1.228 -    by (simp only: div_mult_mod_eq)
   1.229 -  also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
   1.230 -    by (simp only: algebra_simps)
   1.231 -  also have "\<dots> = (a mod c * b) mod c"
   1.232 -    by (rule mod_mult_self1)
   1.233 -  finally show ?thesis
   1.234 -    by (rule sym)
   1.235 -qed
   1.236 -
   1.237 -lemma mod_mult_right_eq [mod_simps]:
   1.238 -  "(a * (b mod c)) mod c = (a * b) mod c"
   1.239 -  using mod_mult_left_eq [of b c a] by (simp add: ac_simps)
   1.240 -
   1.241 -lemma mod_mult_eq:
   1.242 -  "((a mod c) * (b mod c)) mod c = (a * b) mod c"
   1.243 -  by (simp add: mod_mult_left_eq mod_mult_right_eq)
   1.244 -
   1.245 -lemma mod_prod_eq [mod_simps]:
   1.246 -  "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a"
   1.247 -proof (induct A rule: infinite_finite_induct)
   1.248 -  case (insert i A)
   1.249 -  then have "(\<Prod>i\<in>insert i A. f i mod a) mod a
   1.250 -    = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a"
   1.251 -    by simp
   1.252 -  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a"
   1.253 -    by (simp add: mod_simps)
   1.254 -  also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a"
   1.255 -    by (simp add: insert.hyps)
   1.256 -  finally show ?case
   1.257 -    by (simp add: insert.hyps mod_simps)
   1.258 -qed simp_all
   1.259 -
   1.260 -lemma mod_mult_cong:
   1.261 -  assumes "a mod c = a' mod c"
   1.262 -  assumes "b mod c = b' mod c"
   1.263 -  shows "(a * b) mod c = (a' * b') mod c"
   1.264 -proof -
   1.265 -  have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
   1.266 -    unfolding assms ..
   1.267 -  then show ?thesis
   1.268 -    by (simp add: mod_mult_eq)
   1.269 -qed
   1.270 -
   1.271 -text \<open>Exponentiation respects modular equivalence.\<close>
   1.272 -
   1.273 -lemma power_mod [mod_simps]: 
   1.274 -  "((a mod b) ^ n) mod b = (a ^ n) mod b"
   1.275 -proof (induct n)
   1.276 -  case 0
   1.277 -  then show ?case by simp
   1.278 -next
   1.279 -  case (Suc n)
   1.280 -  have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b"
   1.281 -    by (simp add: mod_mult_right_eq)
   1.282 -  with Suc show ?case
   1.283 -    by (simp add: mod_mult_left_eq mod_mult_right_eq)
   1.284 -qed
   1.285 -
   1.286 -end
   1.287 -
   1.288 -class ring_div = comm_ring_1 + semiring_div
   1.289 -begin
   1.290 -
   1.291 -subclass idom_divide ..
   1.292 -
   1.293 -lemma div_minus_minus [simp]: "(- a) div (- b) = a div b"
   1.294 -  using div_mult_mult1 [of "- 1" a b] by simp
   1.295 -
   1.296 -lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)"
   1.297 -  using mod_mult_mult1 [of "- 1" a b] by simp
   1.298 -
   1.299 -lemma div_minus_right: "a div (- b) = (- a) div b"
   1.300 -  using div_minus_minus [of "- a" b] by simp
   1.301 -
   1.302 -lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)"
   1.303 -  using mod_minus_minus [of "- a" b] by simp
   1.304 -
   1.305 -lemma div_minus1_right [simp]: "a div (- 1) = - a"
   1.306 -  using div_minus_right [of a 1] by simp
   1.307 -
   1.308 -lemma mod_minus1_right [simp]: "a mod (- 1) = 0"
   1.309 -  using mod_minus_right [of a 1] by simp
   1.310 -
   1.311 -text \<open>Negation respects modular equivalence.\<close>
   1.312 -
   1.313 -lemma mod_minus_eq [mod_simps]:
   1.314 -  "(- (a mod b)) mod b = (- a) mod b"
   1.315 -proof -
   1.316 -  have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
   1.317 -    by (simp only: div_mult_mod_eq)
   1.318 -  also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
   1.319 -    by (simp add: ac_simps)
   1.320 -  also have "\<dots> = (- (a mod b)) mod b"
   1.321 -    by (rule mod_mult_self1)
   1.322 -  finally show ?thesis
   1.323 -    by (rule sym)
   1.324 -qed
   1.325 -
   1.326 -lemma mod_minus_cong:
   1.327 -  assumes "a mod b = a' mod b"
   1.328 -  shows "(- a) mod b = (- a') mod b"
   1.329 -proof -
   1.330 -  have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
   1.331 -    unfolding assms ..
   1.332 -  then show ?thesis
   1.333 -    by (simp add: mod_minus_eq)
   1.334 -qed
   1.335 -
   1.336 -text \<open>Subtraction respects modular equivalence.\<close>
   1.337 -
   1.338 -lemma mod_diff_left_eq [mod_simps]:
   1.339 -  "(a mod c - b) mod c = (a - b) mod c"
   1.340 -  using mod_add_cong [of a c "a mod c" "- b" "- b"]
   1.341 -  by simp
   1.342 -
   1.343 -lemma mod_diff_right_eq [mod_simps]:
   1.344 -  "(a - b mod c) mod c = (a - b) mod c"
   1.345 -  using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   1.346 -  by simp
   1.347 -
   1.348 -lemma mod_diff_eq:
   1.349 -  "(a mod c - b mod c) mod c = (a - b) mod c"
   1.350 -  using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b]
   1.351 -  by simp
   1.352 -
   1.353 -lemma mod_diff_cong:
   1.354 -  assumes "a mod c = a' mod c"
   1.355 -  assumes "b mod c = b' mod c"
   1.356 -  shows "(a - b) mod c = (a' - b') mod c"
   1.357 -  using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"]
   1.358 -  by simp
   1.359 -
   1.360 -lemma minus_mod_self2 [simp]:
   1.361 -  "(a - b) mod b = a mod b"
   1.362 -  using mod_diff_right_eq [of a b b]
   1.363 -  by (simp add: mod_diff_right_eq)
   1.364 -
   1.365 -lemma minus_mod_self1 [simp]:
   1.366 -  "(b - a) mod b = - a mod b"
   1.367 -  using mod_add_self2 [of "- a" b] by simp
   1.368 -
   1.369 -end
   1.370 -
   1.371 -  
   1.372 -subsection \<open>Euclidean (semi)rings with cancel rules\<close>
   1.373 -
   1.374 -class euclidean_semiring_cancel = euclidean_semiring + semiring_div
   1.375 -
   1.376 -class euclidean_ring_cancel = euclidean_ring + ring_div
   1.377 -
   1.378 -context unique_euclidean_semiring
   1.379 -begin
   1.380 -
   1.381 -subclass euclidean_semiring_cancel
   1.382 -proof
   1.383 -  show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c
   1.384 -  proof (cases a b rule: divmod_cases)
   1.385 -    case by0
   1.386 -    with \<open>b \<noteq> 0\<close> show ?thesis
   1.387 -      by simp
   1.388 -  next
   1.389 -    case (divides q)
   1.390 -    then show ?thesis
   1.391 -      by (simp add: ac_simps)
   1.392 -  next
   1.393 -    case (remainder q r)
   1.394 -    then show ?thesis
   1.395 -      by (auto intro: div_eqI simp add: algebra_simps)
   1.396 -  qed
   1.397 -next
   1.398 -  show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c
   1.399 -  proof (cases a b rule: divmod_cases)
   1.400 -    case by0
   1.401 -    then show ?thesis
   1.402 -      by simp
   1.403 -  next
   1.404 -    case (divides q)
   1.405 -    with \<open>c \<noteq> 0\<close> show ?thesis
   1.406 -      by (simp add: mult.left_commute [of c])
   1.407 -  next
   1.408 -    case (remainder q r)
   1.409 -    from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0"
   1.410 -      by simp
   1.411 -    from remainder \<open>c \<noteq> 0\<close>
   1.412 -    have "uniqueness_constraint (r * c) (b * c)"
   1.413 -      and "euclidean_size (r * c) < euclidean_size (b * c)"
   1.414 -      by (simp_all add: uniqueness_constraint_mono_mult uniqueness_constraint_mod size_mono_mult)
   1.415 -    with remainder show ?thesis
   1.416 -      by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps)
   1.417 -        (use \<open>b * c \<noteq> 0\<close> in simp)
   1.418 -  qed
   1.419 -qed
   1.420 -
   1.421 -end
   1.422 -
   1.423 -context unique_euclidean_ring
   1.424 -begin
   1.425 -
   1.426 -subclass euclidean_ring_cancel ..
   1.427 -
   1.428 -end
   1.429 -
   1.430 -
   1.431  subsection \<open>Parity\<close>
   1.432  
   1.433 -class semiring_div_parity = semiring_div + comm_semiring_1_cancel + numeral +
   1.434 +class unique_euclidean_semiring_parity = unique_euclidean_semiring +
   1.435    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
   1.436    assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
   1.437    assumes zero_not_eq_two: "0 \<noteq> 2"
   1.438 @@ -532,7 +108,7 @@
   1.439    and less technical class hierarchy.
   1.440  \<close>
   1.441  
   1.442 -class semiring_numeral_div = semiring_div + comm_semiring_1_cancel + linordered_semidom +
   1.443 +class unique_euclidean_semiring_numeral = unique_euclidean_semiring + linordered_semidom +
   1.444    assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
   1.445      and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
   1.446      and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"
   1.447 @@ -553,7 +129,7 @@
   1.448      yields a significant speedup.\<close>
   1.449  begin
   1.450  
   1.451 -subclass semiring_div_parity
   1.452 +subclass unique_euclidean_semiring_parity
   1.453  proof
   1.454    fix a
   1.455    show "a mod 2 = 0 \<or> a mod 2 = 1"
   1.456 @@ -1050,58 +626,6 @@
   1.457  
   1.458  end
   1.459  
   1.460 -instance nat :: semiring_div
   1.461 -proof
   1.462 -  fix m n q :: nat
   1.463 -  assume "n \<noteq> 0"
   1.464 -  then show "(q + m * n) div n = m + q div n"
   1.465 -    by (induct m) (simp_all add: le_div_geq)
   1.466 -next
   1.467 -  fix m n q :: nat
   1.468 -  assume "m \<noteq> 0"
   1.469 -  show "(m * n) div (m * q) = n div q"
   1.470 -  proof (cases "q = 0")
   1.471 -    case True
   1.472 -    then show ?thesis
   1.473 -      by simp
   1.474 -  next
   1.475 -    case False
   1.476 -    show ?thesis
   1.477 -    proof (rule div_nat_unique [of _ _ _ "m * (n mod q)"])
   1.478 -      show "eucl_rel_nat (m * n) (m * q) (n div q, m * (n mod q))"
   1.479 -        by (rule eucl_rel_natI)
   1.480 -          (use \<open>m \<noteq> 0\<close> \<open>q \<noteq> 0\<close> div_mult_mod_eq [of n q] in \<open>auto simp add: algebra_simps distrib_left [symmetric]\<close>)
   1.481 -    qed          
   1.482 -  qed
   1.483 -qed
   1.484 -
   1.485 -lemma div_by_Suc_0 [simp]:
   1.486 -  "m div Suc 0 = m"
   1.487 -  using div_by_1 [of m] by simp
   1.488 -
   1.489 -lemma mod_by_Suc_0 [simp]:
   1.490 -  "m mod Suc 0 = 0"
   1.491 -  using mod_by_1 [of m] by simp
   1.492 -
   1.493 -lemma mod_greater_zero_iff_not_dvd:
   1.494 -  fixes m n :: nat
   1.495 -  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   1.496 -  by (simp add: dvd_eq_mod_eq_0)
   1.497 -
   1.498 -instantiation nat :: unique_euclidean_semiring
   1.499 -begin
   1.500 -
   1.501 -definition [simp]:
   1.502 -  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   1.503 -
   1.504 -definition [simp]:
   1.505 -  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   1.506 -
   1.507 -instance
   1.508 -  by standard (use mult_le_mono2 [of 1] in \<open>simp_all add: unit_factor_nat_def mod_greater_zero_iff_not_dvd\<close>)
   1.509 -
   1.510 -end
   1.511 -
   1.512  text \<open>Simproc for cancelling @{const divide} and @{const modulo}\<close>
   1.513  
   1.514  lemma (in semiring_modulo) cancel_div_mod_rules:
   1.515 @@ -1142,6 +666,41 @@
   1.516  simproc_setup cancel_div_mod_nat ("(m::nat) + n") =
   1.517    \<open>K Cancel_Div_Mod_Nat.proc\<close>
   1.518  
   1.519 +lemma div_by_Suc_0 [simp]:
   1.520 +  "m div Suc 0 = m"
   1.521 +  using div_by_1 [of m] by simp
   1.522 +
   1.523 +lemma mod_by_Suc_0 [simp]:
   1.524 +  "m mod Suc 0 = 0"
   1.525 +  using mod_by_1 [of m] by simp
   1.526 +
   1.527 +lemma mod_greater_zero_iff_not_dvd:
   1.528 +  fixes m n :: nat
   1.529 +  shows "m mod n > 0 \<longleftrightarrow> \<not> n dvd m"
   1.530 +  by (simp add: dvd_eq_mod_eq_0)
   1.531 +
   1.532 +instantiation nat :: unique_euclidean_semiring
   1.533 +begin
   1.534 +
   1.535 +definition [simp]:
   1.536 +  "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
   1.537 +
   1.538 +definition [simp]:
   1.539 +  "uniqueness_constraint_nat = (top :: nat \<Rightarrow> nat \<Rightarrow> bool)"
   1.540 +
   1.541 +instance proof
   1.542 +  fix n q r :: nat
   1.543 +  assume "euclidean_size r < euclidean_size n"
   1.544 +  then have "n > r"
   1.545 +    by simp_all
   1.546 +  then have "eucl_rel_nat (q * n + r) n (q, r)"
   1.547 +    by (rule eucl_rel_natI) rule
   1.548 +  then show "(q * n + r) div n = q"
   1.549 +    by (rule div_nat_unique)
   1.550 +qed (use mult_le_mono2 [of 1] in \<open>simp_all\<close>)
   1.551 +
   1.552 +end
   1.553 +  
   1.554  lemma divmod_nat_if [code]:
   1.555    "Divides.divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   1.556      let (q, r) = Divides.divmod_nat (m - n) n in (Suc q, r))"
   1.557 @@ -1262,7 +821,7 @@
   1.558  lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
   1.559  by (auto simp add: mult.commute eucl_rel_nat [THEN eucl_rel_nat_mult2_eq, THEN mod_nat_unique])
   1.560  
   1.561 -instantiation nat :: semiring_numeral_div
   1.562 +instantiation nat :: unique_euclidean_semiring_numeral
   1.563  begin
   1.564  
   1.565  definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
   1.566 @@ -1820,6 +1379,25 @@
   1.567  
   1.568  end
   1.569  
   1.570 +ML \<open>
   1.571 +structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   1.572 +(
   1.573 +  val div_name = @{const_name divide};
   1.574 +  val mod_name = @{const_name modulo};
   1.575 +  val mk_binop = HOLogic.mk_binop;
   1.576 +  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
   1.577 +  val dest_sum = Arith_Data.dest_sum;
   1.578 +
   1.579 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   1.580 +
   1.581 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   1.582 +    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   1.583 +)
   1.584 +\<close>
   1.585 +
   1.586 +simproc_setup cancel_div_mod_int ("(k::int) + l") =
   1.587 +  \<open>K Cancel_Div_Mod_Int.proc\<close>
   1.588 +
   1.589  lemma is_unit_int:
   1.590    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   1.591    by auto
   1.592 @@ -1921,50 +1499,28 @@
   1.593    using assms unfolding modulo_int_def [of k l]
   1.594    by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
   1.595  
   1.596 -instance int :: ring_div
   1.597 -proof
   1.598 -  fix k l s :: int
   1.599 -  assume "l \<noteq> 0"
   1.600 -  then have "eucl_rel_int (k + s * l) l (s + k div l, k mod l)"
   1.601 -    using eucl_rel_int [of k l]
   1.602 -    unfolding eucl_rel_int_iff by (auto simp: algebra_simps)
   1.603 -  then show "(k + s * l) div l = s + k div l"
   1.604 +instantiation int :: unique_euclidean_ring
   1.605 +begin
   1.606 +
   1.607 +definition [simp]:
   1.608 +  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   1.609 +
   1.610 +definition [simp]:
   1.611 +  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   1.612 +  
   1.613 +instance proof
   1.614 +  fix l q r:: int
   1.615 +  assume "uniqueness_constraint r l"
   1.616 +    and "euclidean_size r < euclidean_size l"
   1.617 +  then have "sgn r = sgn l" and "\<bar>r\<bar> < \<bar>l\<bar>"
   1.618 +    by simp_all
   1.619 +  then have "eucl_rel_int (q * l + r) l (q, r)"
   1.620 +    by (rule eucl_rel_int_remainderI) simp
   1.621 +  then show "(q * l + r) div l = q"
   1.622      by (rule div_int_unique)
   1.623 -next
   1.624 -  fix k l s :: int
   1.625 -  assume "s \<noteq> 0"
   1.626 -  have "\<And>q r. eucl_rel_int k l (q, r)
   1.627 -    \<Longrightarrow> eucl_rel_int (s * k) (s * l) (q, s * r)"
   1.628 -    unfolding eucl_rel_int_iff
   1.629 -    by (rule linorder_cases [of 0 l])
   1.630 -      (use \<open>s \<noteq> 0\<close> in \<open>auto simp: algebra_simps
   1.631 -      mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
   1.632 -      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
   1.633 -  then have "eucl_rel_int (s * k) (s * l) (k div l, s * (k mod l))"
   1.634 -    using eucl_rel_int [of k l] .
   1.635 -  then show "(s * k) div (s * l) = k div l"
   1.636 -    by (rule div_int_unique)
   1.637 -qed
   1.638 +qed (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>)
   1.639  
   1.640 -ML \<open>
   1.641 -structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   1.642 -(
   1.643 -  val div_name = @{const_name divide};
   1.644 -  val mod_name = @{const_name modulo};
   1.645 -  val mk_binop = HOLogic.mk_binop;
   1.646 -  val mk_sum = Arith_Data.mk_sum HOLogic.intT;
   1.647 -  val dest_sum = Arith_Data.dest_sum;
   1.648 -
   1.649 -  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
   1.650 -
   1.651 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
   1.652 -    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
   1.653 -)
   1.654 -\<close>
   1.655 -
   1.656 -simproc_setup cancel_div_mod_int ("(k::int) + l") =
   1.657 -  \<open>K Cancel_Div_Mod_Int.proc\<close>
   1.658 -
   1.659 +end
   1.660  
   1.661  text\<open>Basic laws about division and remainder\<close>
   1.662  
   1.663 @@ -2420,21 +1976,6 @@
   1.664      by simp
   1.665  qed
   1.666  
   1.667 -instantiation int :: unique_euclidean_ring
   1.668 -begin
   1.669 -
   1.670 -definition [simp]:
   1.671 -  "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
   1.672 -
   1.673 -definition [simp]:
   1.674 -  "uniqueness_constraint_int (k :: int) l \<longleftrightarrow> unit_factor k = unit_factor l"
   1.675 -  
   1.676 -instance
   1.677 -  by standard
   1.678 -    (use mult_le_mono2 [of 1] in \<open>auto simp add: abs_mult nat_mult_distrib sgn_mod zdiv_eq_0_iff sgn_1_pos sgn_mult split: abs_split\<close>)
   1.679 -
   1.680 -end
   1.681 -
   1.682    
   1.683  subsubsection \<open>Quotients of Signs\<close>
   1.684  
   1.685 @@ -2506,7 +2047,7 @@
   1.686  
   1.687  subsubsection \<open>Computation of Division and Remainder\<close>
   1.688  
   1.689 -instantiation int :: semiring_numeral_div
   1.690 +instantiation int :: unique_euclidean_semiring_numeral
   1.691  begin
   1.692  
   1.693  definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
   1.694 @@ -2687,22 +2228,6 @@
   1.695  apply (rule Divides.div_less_dividend, simp_all)
   1.696  done
   1.697  
   1.698 -lemma (in ring_div) mod_eq_dvd_iff:
   1.699 -  "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q")
   1.700 -proof
   1.701 -  assume ?P
   1.702 -  then have "(a mod c - b mod c) mod c = 0"
   1.703 -    by simp
   1.704 -  then show ?Q
   1.705 -    by (simp add: dvd_eq_mod_eq_0 mod_simps)
   1.706 -next
   1.707 -  assume ?Q
   1.708 -  then obtain d where d: "a - b = c * d" ..
   1.709 -  then have "a = c * d + b"
   1.710 -    by (simp add: algebra_simps)
   1.711 -  then show ?P by simp
   1.712 -qed
   1.713 -
   1.714  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
   1.715    shows "\<exists>q. x = y + n * q"
   1.716  proof-
   1.717 @@ -2742,23 +2267,23 @@
   1.718  \<close>
   1.719  
   1.720  simproc_setup numeral_divmod
   1.721 -  ("0 div 0 :: 'a :: semiring_numeral_div" | "0 mod 0 :: 'a :: semiring_numeral_div" |
   1.722 -   "0 div 1 :: 'a :: semiring_numeral_div" | "0 mod 1 :: 'a :: semiring_numeral_div" |
   1.723 +  ("0 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
   1.724 +   "0 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "0 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
   1.725     "0 div - 1 :: int" | "0 mod - 1 :: int" |
   1.726 -   "0 div numeral b :: 'a :: semiring_numeral_div" | "0 mod numeral b :: 'a :: semiring_numeral_div" |
   1.727 +   "0 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
   1.728     "0 div - numeral b :: int" | "0 mod - numeral b :: int" |
   1.729 -   "1 div 0 :: 'a :: semiring_numeral_div" | "1 mod 0 :: 'a :: semiring_numeral_div" |
   1.730 -   "1 div 1 :: 'a :: semiring_numeral_div" | "1 mod 1 :: 'a :: semiring_numeral_div" |
   1.731 +   "1 div 0 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
   1.732 +   "1 div 1 :: 'a :: unique_euclidean_semiring_numeral" | "1 mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
   1.733     "1 div - 1 :: int" | "1 mod - 1 :: int" |
   1.734 -   "1 div numeral b :: 'a :: semiring_numeral_div" | "1 mod numeral b :: 'a :: semiring_numeral_div" |
   1.735 +   "1 div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
   1.736     "1 div - numeral b :: int" |"1 mod - numeral b :: int" |
   1.737     "- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
   1.738     "- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
   1.739     "- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
   1.740 -   "numeral a div 0 :: 'a :: semiring_numeral_div" | "numeral a mod 0 :: 'a :: semiring_numeral_div" |
   1.741 -   "numeral a div 1 :: 'a :: semiring_numeral_div" | "numeral a mod 1 :: 'a :: semiring_numeral_div" |
   1.742 +   "numeral a div 0 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_numeral" |
   1.743 +   "numeral a div 1 :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_numeral" |
   1.744     "numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
   1.745 -   "numeral a div numeral b :: 'a :: semiring_numeral_div" | "numeral a mod numeral b :: 'a :: semiring_numeral_div" |
   1.746 +   "numeral a div numeral b :: 'a :: unique_euclidean_semiring_numeral" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_numeral" |
   1.747     "numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
   1.748     "- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
   1.749     "- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
   1.750 @@ -2818,7 +2343,7 @@
   1.751    code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   1.752  
   1.753  lemma dvd_eq_mod_eq_0_numeral:
   1.754 -  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semiring_div)"
   1.755 +  "numeral x dvd (numeral y :: 'a) \<longleftrightarrow> numeral y mod numeral x = (0 :: 'a::semidom_modulo)"
   1.756    by (fact dvd_eq_mod_eq_0)
   1.757  
   1.758  declare minus_div_mult_eq_mod [symmetric, nitpick_unfold]