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.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.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.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.53 -
1.54 -lemma mod_mult_self4 [simp]:
1.55 -  "(b * c + a) mod b = a mod b"
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.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.72 -  assumes "b \<noteq> 0"
1.73 -  shows "(a + b) div b = a div b + 1"
1.75 -
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.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.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.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.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.193 -  "(a mod c + b mod c) mod c = (a + b) mod c"
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.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.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.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.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]
```