1(* Title: HOL/Euclidean_Division.thy 2 Author: Manuel Eberl, TU Muenchen 3 Author: Florian Haftmann, TU Muenchen 4*) 5 6section \<open>Division in euclidean (semi)rings\<close> 7 8theory Euclidean_Division 9 imports Int Lattices_Big 10begin 11 12subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close> 13 14class euclidean_semiring = semidom_modulo + 15 fixes euclidean_size :: "'a \<Rightarrow> nat" 16 assumes size_0 [simp]: "euclidean_size 0 = 0" 17 assumes mod_size_less: 18 "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b" 19 assumes size_mult_mono: 20 "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)" 21begin 22 23lemma euclidean_size_eq_0_iff [simp]: 24 "euclidean_size b = 0 \<longleftrightarrow> b = 0" 25proof 26 assume "b = 0" 27 then show "euclidean_size b = 0" 28 by simp 29next 30 assume "euclidean_size b = 0" 31 show "b = 0" 32 proof (rule ccontr) 33 assume "b \<noteq> 0" 34 with mod_size_less have "euclidean_size (b mod b) < euclidean_size b" . 35 with \<open>euclidean_size b = 0\<close> show False 36 by simp 37 qed 38qed 39 40lemma euclidean_size_greater_0_iff [simp]: 41 "euclidean_size b > 0 \<longleftrightarrow> b \<noteq> 0" 42 using euclidean_size_eq_0_iff [symmetric, of b] by safe simp 43 44lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)" 45 by (subst mult.commute) (rule size_mult_mono) 46 47lemma dvd_euclidean_size_eq_imp_dvd: 48 assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b" 49 and "b dvd a" 50 shows "a dvd b" 51proof (rule ccontr) 52 assume "\<not> a dvd b" 53 hence "b mod a \<noteq> 0" using mod_0_imp_dvd [of b a] by blast 54 then have "b mod a \<noteq> 0" by (simp add: mod_eq_0_iff_dvd) 55 from \<open>b dvd a\<close> have "b dvd b mod a" by (simp add: dvd_mod_iff) 56 then obtain c where "b mod a = b * c" unfolding dvd_def by blast 57 with \<open>b mod a \<noteq> 0\<close> have "c \<noteq> 0" by auto 58 with \<open>b mod a = b * c\<close> have "euclidean_size (b mod a) \<ge> euclidean_size b" 59 using size_mult_mono by force 60 moreover from \<open>\<not> a dvd b\<close> and \<open>a \<noteq> 0\<close> 61 have "euclidean_size (b mod a) < euclidean_size a" 62 using mod_size_less by blast 63 ultimately show False using \<open>euclidean_size a = euclidean_size b\<close> 64 by simp 65qed 66 67lemma euclidean_size_times_unit: 68 assumes "is_unit a" 69 shows "euclidean_size (a * b) = euclidean_size b" 70proof (rule antisym) 71 from assms have [simp]: "a \<noteq> 0" by auto 72 thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono') 73 from assms have "is_unit (1 div a)" by simp 74 hence "1 div a \<noteq> 0" by (intro notI) simp_all 75 hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))" 76 by (rule size_mult_mono') 77 also from assms have "(1 div a) * (a * b) = b" 78 by (simp add: algebra_simps unit_div_mult_swap) 79 finally show "euclidean_size (a * b) \<le> euclidean_size b" . 80qed 81 82lemma euclidean_size_unit: 83 "is_unit a \<Longrightarrow> euclidean_size a = euclidean_size 1" 84 using euclidean_size_times_unit [of a 1] by simp 85 86lemma unit_iff_euclidean_size: 87 "is_unit a \<longleftrightarrow> euclidean_size a = euclidean_size 1 \<and> a \<noteq> 0" 88proof safe 89 assume A: "a \<noteq> 0" and B: "euclidean_size a = euclidean_size 1" 90 show "is_unit a" 91 by (rule dvd_euclidean_size_eq_imp_dvd [OF A B]) simp_all 92qed (auto intro: euclidean_size_unit) 93 94lemma euclidean_size_times_nonunit: 95 assumes "a \<noteq> 0" "b \<noteq> 0" "\<not> is_unit a" 96 shows "euclidean_size b < euclidean_size (a * b)" 97proof (rule ccontr) 98 assume "\<not>euclidean_size b < euclidean_size (a * b)" 99 with size_mult_mono'[OF assms(1), of b] 100 have eq: "euclidean_size (a * b) = euclidean_size b" by simp 101 have "a * b dvd b" 102 by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all) 103 hence "a * b dvd 1 * b" by simp 104 with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff) 105 with assms(3) show False by contradiction 106qed 107 108lemma dvd_imp_size_le: 109 assumes "a dvd b" "b \<noteq> 0" 110 shows "euclidean_size a \<le> euclidean_size b" 111 using assms by (auto elim!: dvdE simp: size_mult_mono) 112 113lemma dvd_proper_imp_size_less: 114 assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0" 115 shows "euclidean_size a < euclidean_size b" 116proof - 117 from assms(1) obtain c where "b = a * c" by (erule dvdE) 118 hence z: "b = c * a" by (simp add: mult.commute) 119 from z assms have "\<not>is_unit c" by (auto simp: mult.commute mult_unit_dvd_iff) 120 with z assms show ?thesis 121 by (auto intro!: euclidean_size_times_nonunit) 122qed 123 124lemma unit_imp_mod_eq_0: 125 "a mod b = 0" if "is_unit b" 126 using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd) 127 128lemma coprime_mod_left_iff [simp]: 129 "coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0" 130 by (rule; rule coprimeI) 131 (use that in \<open>auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\<close>) 132 133lemma coprime_mod_right_iff [simp]: 134 "coprime a (b mod a) \<longleftrightarrow> coprime a b" if "a \<noteq> 0" 135 using that coprime_mod_left_iff [of a b] by (simp add: ac_simps) 136 137end 138 139class euclidean_ring = idom_modulo + euclidean_semiring 140begin 141 142lemma dvd_diff_commute [ac_simps]: 143 "a dvd c - b \<longleftrightarrow> a dvd b - c" 144proof - 145 have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1" 146 by (subst dvd_mult_unit_iff) simp_all 147 then show ?thesis 148 by simp 149qed 150 151end 152 153 154subsection \<open>Euclidean (semi)rings with cancel rules\<close> 155 156class euclidean_semiring_cancel = euclidean_semiring + 157 assumes div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b" 158 and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b" 159begin 160 161lemma div_mult_self2 [simp]: 162 assumes "b \<noteq> 0" 163 shows "(a + b * c) div b = c + a div b" 164 using assms div_mult_self1 [of b a c] by (simp add: mult.commute) 165 166lemma div_mult_self3 [simp]: 167 assumes "b \<noteq> 0" 168 shows "(c * b + a) div b = c + a div b" 169 using assms by (simp add: add.commute) 170 171lemma div_mult_self4 [simp]: 172 assumes "b \<noteq> 0" 173 shows "(b * c + a) div b = c + a div b" 174 using assms by (simp add: add.commute) 175 176lemma mod_mult_self1 [simp]: "(a + c * b) mod b = a mod b" 177proof (cases "b = 0") 178 case True then show ?thesis by simp 179next 180 case False 181 have "a + c * b = (a + c * b) div b * b + (a + c * b) mod b" 182 by (simp add: div_mult_mod_eq) 183 also from False div_mult_self1 [of b a c] have 184 "\<dots> = (c + a div b) * b + (a + c * b) mod b" 185 by (simp add: algebra_simps) 186 finally have "a = a div b * b + (a + c * b) mod b" 187 by (simp add: add.commute [of a] add.assoc distrib_right) 188 then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b" 189 by (simp add: div_mult_mod_eq) 190 then show ?thesis by simp 191qed 192 193lemma mod_mult_self2 [simp]: 194 "(a + b * c) mod b = a mod b" 195 by (simp add: mult.commute [of b]) 196 197lemma mod_mult_self3 [simp]: 198 "(c * b + a) mod b = a mod b" 199 by (simp add: add.commute) 200 201lemma mod_mult_self4 [simp]: 202 "(b * c + a) mod b = a mod b" 203 by (simp add: add.commute) 204 205lemma mod_mult_self1_is_0 [simp]: 206 "b * a mod b = 0" 207 using mod_mult_self2 [of 0 b a] by simp 208 209lemma mod_mult_self2_is_0 [simp]: 210 "a * b mod b = 0" 211 using mod_mult_self1 [of 0 a b] by simp 212 213lemma div_add_self1: 214 assumes "b \<noteq> 0" 215 shows "(b + a) div b = a div b + 1" 216 using assms div_mult_self1 [of b a 1] by (simp add: add.commute) 217 218lemma div_add_self2: 219 assumes "b \<noteq> 0" 220 shows "(a + b) div b = a div b + 1" 221 using assms div_add_self1 [of b a] by (simp add: add.commute) 222 223lemma mod_add_self1 [simp]: 224 "(b + a) mod b = a mod b" 225 using mod_mult_self1 [of a 1 b] by (simp add: add.commute) 226 227lemma mod_add_self2 [simp]: 228 "(a + b) mod b = a mod b" 229 using mod_mult_self1 [of a 1 b] by simp 230 231lemma mod_div_trivial [simp]: 232 "a mod b div b = 0" 233proof (cases "b = 0") 234 assume "b = 0" 235 thus ?thesis by simp 236next 237 assume "b \<noteq> 0" 238 hence "a div b + a mod b div b = (a mod b + a div b * b) div b" 239 by (rule div_mult_self1 [symmetric]) 240 also have "\<dots> = a div b" 241 by (simp only: mod_div_mult_eq) 242 also have "\<dots> = a div b + 0" 243 by simp 244 finally show ?thesis 245 by (rule add_left_imp_eq) 246qed 247 248lemma mod_mod_trivial [simp]: 249 "a mod b mod b = a mod b" 250proof - 251 have "a mod b mod b = (a mod b + a div b * b) mod b" 252 by (simp only: mod_mult_self1) 253 also have "\<dots> = a mod b" 254 by (simp only: mod_div_mult_eq) 255 finally show ?thesis . 256qed 257 258lemma mod_mod_cancel: 259 assumes "c dvd b" 260 shows "a mod b mod c = a mod c" 261proof - 262 from \<open>c dvd b\<close> obtain k where "b = c * k" 263 by (rule dvdE) 264 have "a mod b mod c = a mod (c * k) mod c" 265 by (simp only: \<open>b = c * k\<close>) 266 also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c" 267 by (simp only: mod_mult_self1) 268 also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c" 269 by (simp only: ac_simps) 270 also have "\<dots> = a mod c" 271 by (simp only: div_mult_mod_eq) 272 finally show ?thesis . 273qed 274 275lemma div_mult_mult2 [simp]: 276 "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b" 277 by (drule div_mult_mult1) (simp add: mult.commute) 278 279lemma div_mult_mult1_if [simp]: 280 "(c * a) div (c * b) = (if c = 0 then 0 else a div b)" 281 by simp_all 282 283lemma mod_mult_mult1: 284 "(c * a) mod (c * b) = c * (a mod b)" 285proof (cases "c = 0") 286 case True then show ?thesis by simp 287next 288 case False 289 from div_mult_mod_eq 290 have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" . 291 with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b) 292 = c * a + c * (a mod b)" by (simp add: algebra_simps) 293 with div_mult_mod_eq show ?thesis by simp 294qed 295 296lemma mod_mult_mult2: 297 "(a * c) mod (b * c) = (a mod b) * c" 298 using mod_mult_mult1 [of c a b] by (simp add: mult.commute) 299 300lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)" 301 by (fact mod_mult_mult2 [symmetric]) 302 303lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)" 304 by (fact mod_mult_mult1 [symmetric]) 305 306lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)" 307 unfolding dvd_def by (auto simp add: mod_mult_mult1) 308 309lemma div_plus_div_distrib_dvd_left: 310 "c dvd a \<Longrightarrow> (a + b) div c = a div c + b div c" 311 by (cases "c = 0") (auto elim: dvdE) 312 313lemma div_plus_div_distrib_dvd_right: 314 "c dvd b \<Longrightarrow> (a + b) div c = a div c + b div c" 315 using div_plus_div_distrib_dvd_left [of c b a] 316 by (simp add: ac_simps) 317 318named_theorems mod_simps 319 320text \<open>Addition respects modular equivalence.\<close> 321 322lemma mod_add_left_eq [mod_simps]: 323 "(a mod c + b) mod c = (a + b) mod c" 324proof - 325 have "(a + b) mod c = (a div c * c + a mod c + b) mod c" 326 by (simp only: div_mult_mod_eq) 327 also have "\<dots> = (a mod c + b + a div c * c) mod c" 328 by (simp only: ac_simps) 329 also have "\<dots> = (a mod c + b) mod c" 330 by (rule mod_mult_self1) 331 finally show ?thesis 332 by (rule sym) 333qed 334 335lemma mod_add_right_eq [mod_simps]: 336 "(a + b mod c) mod c = (a + b) mod c" 337 using mod_add_left_eq [of b c a] by (simp add: ac_simps) 338 339lemma mod_add_eq: 340 "(a mod c + b mod c) mod c = (a + b) mod c" 341 by (simp add: mod_add_left_eq mod_add_right_eq) 342 343lemma mod_sum_eq [mod_simps]: 344 "(\<Sum>i\<in>A. f i mod a) mod a = sum f A mod a" 345proof (induct A rule: infinite_finite_induct) 346 case (insert i A) 347 then have "(\<Sum>i\<in>insert i A. f i mod a) mod a 348 = (f i mod a + (\<Sum>i\<in>A. f i mod a)) mod a" 349 by simp 350 also have "\<dots> = (f i + (\<Sum>i\<in>A. f i mod a) mod a) mod a" 351 by (simp add: mod_simps) 352 also have "\<dots> = (f i + (\<Sum>i\<in>A. f i) mod a) mod a" 353 by (simp add: insert.hyps) 354 finally show ?case 355 by (simp add: insert.hyps mod_simps) 356qed simp_all 357 358lemma mod_add_cong: 359 assumes "a mod c = a' mod c" 360 assumes "b mod c = b' mod c" 361 shows "(a + b) mod c = (a' + b') mod c" 362proof - 363 have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c" 364 unfolding assms .. 365 then show ?thesis 366 by (simp add: mod_add_eq) 367qed 368 369text \<open>Multiplication respects modular equivalence.\<close> 370 371lemma mod_mult_left_eq [mod_simps]: 372 "((a mod c) * b) mod c = (a * b) mod c" 373proof - 374 have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c" 375 by (simp only: div_mult_mod_eq) 376 also have "\<dots> = (a mod c * b + a div c * b * c) mod c" 377 by (simp only: algebra_simps) 378 also have "\<dots> = (a mod c * b) mod c" 379 by (rule mod_mult_self1) 380 finally show ?thesis 381 by (rule sym) 382qed 383 384lemma mod_mult_right_eq [mod_simps]: 385 "(a * (b mod c)) mod c = (a * b) mod c" 386 using mod_mult_left_eq [of b c a] by (simp add: ac_simps) 387 388lemma mod_mult_eq: 389 "((a mod c) * (b mod c)) mod c = (a * b) mod c" 390 by (simp add: mod_mult_left_eq mod_mult_right_eq) 391 392lemma mod_prod_eq [mod_simps]: 393 "(\<Prod>i\<in>A. f i mod a) mod a = prod f A mod a" 394proof (induct A rule: infinite_finite_induct) 395 case (insert i A) 396 then have "(\<Prod>i\<in>insert i A. f i mod a) mod a 397 = (f i mod a * (\<Prod>i\<in>A. f i mod a)) mod a" 398 by simp 399 also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i mod a) mod a)) mod a" 400 by (simp add: mod_simps) 401 also have "\<dots> = (f i * ((\<Prod>i\<in>A. f i) mod a)) mod a" 402 by (simp add: insert.hyps) 403 finally show ?case 404 by (simp add: insert.hyps mod_simps) 405qed simp_all 406 407lemma mod_mult_cong: 408 assumes "a mod c = a' mod c" 409 assumes "b mod c = b' mod c" 410 shows "(a * b) mod c = (a' * b') mod c" 411proof - 412 have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c" 413 unfolding assms .. 414 then show ?thesis 415 by (simp add: mod_mult_eq) 416qed 417 418text \<open>Exponentiation respects modular equivalence.\<close> 419 420lemma power_mod [mod_simps]: 421 "((a mod b) ^ n) mod b = (a ^ n) mod b" 422proof (induct n) 423 case 0 424 then show ?case by simp 425next 426 case (Suc n) 427 have "(a mod b) ^ Suc n mod b = (a mod b) * ((a mod b) ^ n mod b) mod b" 428 by (simp add: mod_mult_right_eq) 429 with Suc show ?case 430 by (simp add: mod_mult_left_eq mod_mult_right_eq) 431qed 432 433end 434 435 436class euclidean_ring_cancel = euclidean_ring + euclidean_semiring_cancel 437begin 438 439subclass idom_divide .. 440 441lemma div_minus_minus [simp]: "(- a) div (- b) = a div b" 442 using div_mult_mult1 [of "- 1" a b] by simp 443 444lemma mod_minus_minus [simp]: "(- a) mod (- b) = - (a mod b)" 445 using mod_mult_mult1 [of "- 1" a b] by simp 446 447lemma div_minus_right: "a div (- b) = (- a) div b" 448 using div_minus_minus [of "- a" b] by simp 449 450lemma mod_minus_right: "a mod (- b) = - ((- a) mod b)" 451 using mod_minus_minus [of "- a" b] by simp 452 453lemma div_minus1_right [simp]: "a div (- 1) = - a" 454 using div_minus_right [of a 1] by simp 455 456lemma mod_minus1_right [simp]: "a mod (- 1) = 0" 457 using mod_minus_right [of a 1] by simp 458 459text \<open>Negation respects modular equivalence.\<close> 460 461lemma mod_minus_eq [mod_simps]: 462 "(- (a mod b)) mod b = (- a) mod b" 463proof - 464 have "(- a) mod b = (- (a div b * b + a mod b)) mod b" 465 by (simp only: div_mult_mod_eq) 466 also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b" 467 by (simp add: ac_simps) 468 also have "\<dots> = (- (a mod b)) mod b" 469 by (rule mod_mult_self1) 470 finally show ?thesis 471 by (rule sym) 472qed 473 474lemma mod_minus_cong: 475 assumes "a mod b = a' mod b" 476 shows "(- a) mod b = (- a') mod b" 477proof - 478 have "(- (a mod b)) mod b = (- (a' mod b)) mod b" 479 unfolding assms .. 480 then show ?thesis 481 by (simp add: mod_minus_eq) 482qed 483 484text \<open>Subtraction respects modular equivalence.\<close> 485 486lemma mod_diff_left_eq [mod_simps]: 487 "(a mod c - b) mod c = (a - b) mod c" 488 using mod_add_cong [of a c "a mod c" "- b" "- b"] 489 by simp 490 491lemma mod_diff_right_eq [mod_simps]: 492 "(a - b mod c) mod c = (a - b) mod c" 493 using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] 494 by simp 495 496lemma mod_diff_eq: 497 "(a mod c - b mod c) mod c = (a - b) mod c" 498 using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] 499 by simp 500 501lemma mod_diff_cong: 502 assumes "a mod c = a' mod c" 503 assumes "b mod c = b' mod c" 504 shows "(a - b) mod c = (a' - b') mod c" 505 using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] 506 by simp 507 508lemma minus_mod_self2 [simp]: 509 "(a - b) mod b = a mod b" 510 using mod_diff_right_eq [of a b b] 511 by (simp add: mod_diff_right_eq) 512 513lemma minus_mod_self1 [simp]: 514 "(b - a) mod b = - a mod b" 515 using mod_add_self2 [of "- a" b] by simp 516 517lemma mod_eq_dvd_iff: 518 "a mod c = b mod c \<longleftrightarrow> c dvd a - b" (is "?P \<longleftrightarrow> ?Q") 519proof 520 assume ?P 521 then have "(a mod c - b mod c) mod c = 0" 522 by simp 523 then show ?Q 524 by (simp add: dvd_eq_mod_eq_0 mod_simps) 525next 526 assume ?Q 527 then obtain d where d: "a - b = c * d" .. 528 then have "a = c * d + b" 529 by (simp add: algebra_simps) 530 then show ?P by simp 531qed 532 533lemma mod_eqE: 534 assumes "a mod c = b mod c" 535 obtains d where "b = a + c * d" 536proof - 537 from assms have "c dvd a - b" 538 by (simp add: mod_eq_dvd_iff) 539 then obtain d where "a - b = c * d" .. 540 then have "b = a + c * - d" 541 by (simp add: algebra_simps) 542 with that show thesis . 543qed 544 545lemma invertible_coprime: 546 "coprime a c" if "a * b mod c = 1" 547 by (rule coprimeI) (use that dvd_mod_iff [of _ c "a * b"] in auto) 548 549end 550 551 552subsection \<open>Uniquely determined division\<close> 553 554class unique_euclidean_semiring = euclidean_semiring + 555 assumes euclidean_size_mult: "euclidean_size (a * b) = euclidean_size a * euclidean_size b" 556 fixes division_segment :: "'a \<Rightarrow> 'a" 557 assumes is_unit_division_segment [simp]: "is_unit (division_segment a)" 558 and division_segment_mult: 559 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> division_segment (a * b) = division_segment a * division_segment b" 560 and division_segment_mod: 561 "b \<noteq> 0 \<Longrightarrow> \<not> b dvd a \<Longrightarrow> division_segment (a mod b) = division_segment b" 562 assumes div_bounded: 563 "b \<noteq> 0 \<Longrightarrow> division_segment r = division_segment b 564 \<Longrightarrow> euclidean_size r < euclidean_size b 565 \<Longrightarrow> (q * b + r) div b = q" 566begin 567 568lemma division_segment_not_0 [simp]: 569 "division_segment a \<noteq> 0" 570 using is_unit_division_segment [of a] is_unitE [of "division_segment a"] by blast 571 572lemma divmod_cases [case_names divides remainder by0]: 573 obtains 574 (divides) q where "b \<noteq> 0" 575 and "a div b = q" 576 and "a mod b = 0" 577 and "a = q * b" 578 | (remainder) q r where "b \<noteq> 0" 579 and "division_segment r = division_segment b" 580 and "euclidean_size r < euclidean_size b" 581 and "r \<noteq> 0" 582 and "a div b = q" 583 and "a mod b = r" 584 and "a = q * b + r" 585 | (by0) "b = 0" 586proof (cases "b = 0") 587 case True 588 then show thesis 589 by (rule by0) 590next 591 case False 592 show thesis 593 proof (cases "b dvd a") 594 case True 595 then obtain q where "a = b * q" .. 596 with \<open>b \<noteq> 0\<close> divides 597 show thesis 598 by (simp add: ac_simps) 599 next 600 case False 601 then have "a mod b \<noteq> 0" 602 by (simp add: mod_eq_0_iff_dvd) 603 moreover from \<open>b \<noteq> 0\<close> \<open>\<not> b dvd a\<close> have "division_segment (a mod b) = division_segment b" 604 by (rule division_segment_mod) 605 moreover have "euclidean_size (a mod b) < euclidean_size b" 606 using \<open>b \<noteq> 0\<close> by (rule mod_size_less) 607 moreover have "a = a div b * b + a mod b" 608 by (simp add: div_mult_mod_eq) 609 ultimately show thesis 610 using \<open>b \<noteq> 0\<close> by (blast intro!: remainder) 611 qed 612qed 613 614lemma div_eqI: 615 "a div b = q" if "b \<noteq> 0" "division_segment r = division_segment b" 616 "euclidean_size r < euclidean_size b" "q * b + r = a" 617proof - 618 from that have "(q * b + r) div b = q" 619 by (auto intro: div_bounded) 620 with that show ?thesis 621 by simp 622qed 623 624lemma mod_eqI: 625 "a mod b = r" if "b \<noteq> 0" "division_segment r = division_segment b" 626 "euclidean_size r < euclidean_size b" "q * b + r = a" 627proof - 628 from that have "a div b = q" 629 by (rule div_eqI) 630 moreover have "a div b * b + a mod b = a" 631 by (fact div_mult_mod_eq) 632 ultimately have "a div b * b + a mod b = a div b * b + r" 633 using \<open>q * b + r = a\<close> by simp 634 then show ?thesis 635 by simp 636qed 637 638subclass euclidean_semiring_cancel 639proof 640 show "(a + c * b) div b = c + a div b" if "b \<noteq> 0" for a b c 641 proof (cases a b rule: divmod_cases) 642 case by0 643 with \<open>b \<noteq> 0\<close> show ?thesis 644 by simp 645 next 646 case (divides q) 647 then show ?thesis 648 by (simp add: ac_simps) 649 next 650 case (remainder q r) 651 then show ?thesis 652 by (auto intro: div_eqI simp add: algebra_simps) 653 qed 654next 655 show"(c * a) div (c * b) = a div b" if "c \<noteq> 0" for a b c 656 proof (cases a b rule: divmod_cases) 657 case by0 658 then show ?thesis 659 by simp 660 next 661 case (divides q) 662 with \<open>c \<noteq> 0\<close> show ?thesis 663 by (simp add: mult.left_commute [of c]) 664 next 665 case (remainder q r) 666 from \<open>b \<noteq> 0\<close> \<open>c \<noteq> 0\<close> have "b * c \<noteq> 0" 667 by simp 668 from remainder \<open>c \<noteq> 0\<close> 669 have "division_segment (r * c) = division_segment (b * c)" 670 and "euclidean_size (r * c) < euclidean_size (b * c)" 671 by (simp_all add: division_segment_mult division_segment_mod euclidean_size_mult) 672 with remainder show ?thesis 673 by (auto intro!: div_eqI [of _ "c * (a mod b)"] simp add: algebra_simps) 674 (use \<open>b * c \<noteq> 0\<close> in simp) 675 qed 676qed 677 678lemma div_mult1_eq: 679 "(a * b) div c = a * (b div c) + a * (b mod c) div c" 680proof (cases "a * (b mod c)" c rule: divmod_cases) 681 case (divides q) 682 have "a * b = a * (b div c * c + b mod c)" 683 by (simp add: div_mult_mod_eq) 684 also have "\<dots> = (a * (b div c) + q) * c" 685 using divides by (simp add: algebra_simps) 686 finally have "(a * b) div c = \<dots> div c" 687 by simp 688 with divides show ?thesis 689 by simp 690next 691 case (remainder q r) 692 from remainder(1-3) show ?thesis 693 proof (rule div_eqI) 694 have "a * b = a * (b div c * c + b mod c)" 695 by (simp add: div_mult_mod_eq) 696 also have "\<dots> = a * c * (b div c) + q * c + r" 697 using remainder by (simp add: algebra_simps) 698 finally show "(a * (b div c) + a * (b mod c) div c) * c + r = a * b" 699 using remainder(5-7) by (simp add: algebra_simps) 700 qed 701next 702 case by0 703 then show ?thesis 704 by simp 705qed 706 707lemma div_add1_eq: 708 "(a + b) div c = a div c + b div c + (a mod c + b mod c) div c" 709proof (cases "a mod c + b mod c" c rule: divmod_cases) 710 case (divides q) 711 have "a + b = (a div c * c + a mod c) + (b div c * c + b mod c)" 712 using mod_mult_div_eq [of a c] mod_mult_div_eq [of b c] by (simp add: ac_simps) 713 also have "\<dots> = (a div c + b div c) * c + (a mod c + b mod c)" 714 by (simp add: algebra_simps) 715 also have "\<dots> = (a div c + b div c + q) * c" 716 using divides by (simp add: algebra_simps) 717 finally have "(a + b) div c = (a div c + b div c + q) * c div c" 718 by simp 719 with divides show ?thesis 720 by simp 721next 722 case (remainder q r) 723 from remainder(1-3) show ?thesis 724 proof (rule div_eqI) 725 have "(a div c + b div c + q) * c + r + (a mod c + b mod c) = 726 (a div c * c + a mod c) + (b div c * c + b mod c) + q * c + r" 727 by (simp add: algebra_simps) 728 also have "\<dots> = a + b + (a mod c + b mod c)" 729 by (simp add: div_mult_mod_eq remainder) (simp add: ac_simps) 730 finally show "(a div c + b div c + (a mod c + b mod c) div c) * c + r = a + b" 731 using remainder by simp 732 qed 733next 734 case by0 735 then show ?thesis 736 by simp 737qed 738 739lemma div_eq_0_iff: 740 "a div b = 0 \<longleftrightarrow> euclidean_size a < euclidean_size b \<or> b = 0" (is "_ \<longleftrightarrow> ?P") 741 if "division_segment a = division_segment b" 742proof 743 assume ?P 744 with that show "a div b = 0" 745 by (cases "b = 0") (auto intro: div_eqI) 746next 747 assume "a div b = 0" 748 then have "a mod b = a" 749 using div_mult_mod_eq [of a b] by simp 750 with mod_size_less [of b a] show ?P 751 by auto 752qed 753 754end 755 756class unique_euclidean_ring = euclidean_ring + unique_euclidean_semiring 757begin 758 759subclass euclidean_ring_cancel .. 760 761end 762 763 764subsection \<open>Euclidean division on @{typ nat}\<close> 765 766instantiation nat :: normalization_semidom 767begin 768 769definition normalize_nat :: "nat \<Rightarrow> nat" 770 where [simp]: "normalize = (id :: nat \<Rightarrow> nat)" 771 772definition unit_factor_nat :: "nat \<Rightarrow> nat" 773 where "unit_factor n = (if n = 0 then 0 else 1 :: nat)" 774 775lemma unit_factor_simps [simp]: 776 "unit_factor 0 = (0::nat)" 777 "unit_factor (Suc n) = 1" 778 by (simp_all add: unit_factor_nat_def) 779 780definition divide_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 781 where "m div n = (if n = 0 then 0 else Max {k::nat. k * n \<le> m})" 782 783instance 784 by standard (auto simp add: divide_nat_def ac_simps unit_factor_nat_def intro: Max_eqI) 785 786end 787 788lemma coprime_Suc_0_left [simp]: 789 "coprime (Suc 0) n" 790 using coprime_1_left [of n] by simp 791 792lemma coprime_Suc_0_right [simp]: 793 "coprime n (Suc 0)" 794 using coprime_1_right [of n] by simp 795 796lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1" 797 for a b :: nat 798 by (drule coprime_common_divisor [of _ _ x]) simp_all 799 800instantiation nat :: unique_euclidean_semiring 801begin 802 803definition euclidean_size_nat :: "nat \<Rightarrow> nat" 804 where [simp]: "euclidean_size_nat = id" 805 806definition division_segment_nat :: "nat \<Rightarrow> nat" 807 where [simp]: "division_segment_nat n = 1" 808 809definition modulo_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 810 where "m mod n = m - (m div n * (n::nat))" 811 812instance proof 813 fix m n :: nat 814 have ex: "\<exists>k. k * n \<le> l" for l :: nat 815 by (rule exI [of _ 0]) simp 816 have fin: "finite {k. k * n \<le> l}" if "n > 0" for l 817 proof - 818 from that have "{k. k * n \<le> l} \<subseteq> {k. k \<le> l}" 819 by (cases n) auto 820 then show ?thesis 821 by (rule finite_subset) simp 822 qed 823 have mult_div_unfold: "n * (m div n) = Max {l. l \<le> m \<and> n dvd l}" 824 proof (cases "n = 0") 825 case True 826 moreover have "{l. l = 0 \<and> l \<le> m} = {0::nat}" 827 by auto 828 ultimately show ?thesis 829 by simp 830 next 831 case False 832 with ex [of m] fin have "n * Max {k. k * n \<le> m} = Max (times n ` {k. k * n \<le> m})" 833 by (auto simp add: nat_mult_max_right intro: hom_Max_commute) 834 also have "times n ` {k. k * n \<le> m} = {l. l \<le> m \<and> n dvd l}" 835 by (auto simp add: ac_simps elim!: dvdE) 836 finally show ?thesis 837 using False by (simp add: divide_nat_def ac_simps) 838 qed 839 have less_eq: "m div n * n \<le> m" 840 by (auto simp add: mult_div_unfold ac_simps intro: Max.boundedI) 841 then show "m div n * n + m mod n = m" 842 by (simp add: modulo_nat_def) 843 assume "n \<noteq> 0" 844 show "euclidean_size (m mod n) < euclidean_size n" 845 proof - 846 have "m < Suc (m div n) * n" 847 proof (rule ccontr) 848 assume "\<not> m < Suc (m div n) * n" 849 then have "Suc (m div n) * n \<le> m" 850 by (simp add: not_less) 851 moreover from \<open>n \<noteq> 0\<close> have "Max {k. k * n \<le> m} < Suc (m div n)" 852 by (simp add: divide_nat_def) 853 with \<open>n \<noteq> 0\<close> ex fin have "\<And>k. k * n \<le> m \<Longrightarrow> k < Suc (m div n)" 854 by auto 855 ultimately have "Suc (m div n) < Suc (m div n)" 856 by blast 857 then show False 858 by simp 859 qed 860 with \<open>n \<noteq> 0\<close> show ?thesis 861 by (simp add: modulo_nat_def) 862 qed 863 show "euclidean_size m \<le> euclidean_size (m * n)" 864 using \<open>n \<noteq> 0\<close> by (cases n) simp_all 865 fix q r :: nat 866 show "(q * n + r) div n = q" if "euclidean_size r < euclidean_size n" 867 proof - 868 from that have "r < n" 869 by simp 870 have "k \<le> q" if "k * n \<le> q * n + r" for k 871 proof (rule ccontr) 872 assume "\<not> k \<le> q" 873 then have "q < k" 874 by simp 875 then obtain l where "k = Suc (q + l)" 876 by (auto simp add: less_iff_Suc_add) 877 with \<open>r < n\<close> that show False 878 by (simp add: algebra_simps) 879 qed 880 with \<open>n \<noteq> 0\<close> ex fin show ?thesis 881 by (auto simp add: divide_nat_def Max_eq_iff) 882 qed 883qed simp_all 884 885end 886 887text \<open>Tool support\<close> 888 889ML \<open> 890structure Cancel_Div_Mod_Nat = Cancel_Div_Mod 891( 892 val div_name = @{const_name divide}; 893 val mod_name = @{const_name modulo}; 894 val mk_binop = HOLogic.mk_binop; 895 val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT; 896 val mk_sum = Arith_Data.mk_sum; 897 fun dest_sum tm = 898 if HOLogic.is_zero tm then [] 899 else 900 (case try HOLogic.dest_Suc tm of 901 SOME t => HOLogic.Suc_zero :: dest_sum t 902 | NONE => 903 (case try dest_plus tm of 904 SOME (t, u) => dest_sum t @ dest_sum u 905 | NONE => [tm])); 906 907 val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules}; 908 909 val prove_eq_sums = Arith_Data.prove_conv2 all_tac 910 (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps}) 911) 912\<close> 913 914simproc_setup cancel_div_mod_nat ("(m::nat) + n") = 915 \<open>K Cancel_Div_Mod_Nat.proc\<close> 916 917lemma div_nat_eqI: 918 "m div n = q" if "n * q \<le> m" and "m < n * Suc q" for m n q :: nat 919 by (rule div_eqI [of _ "m - n * q"]) (use that in \<open>simp_all add: algebra_simps\<close>) 920 921lemma mod_nat_eqI: 922 "m mod n = r" if "r < n" and "r \<le> m" and "n dvd m - r" for m n r :: nat 923 by (rule mod_eqI [of _ _ "(m - r) div n"]) (use that in \<open>simp_all add: algebra_simps\<close>) 924 925lemma div_mult_self_is_m [simp]: 926 "m * n div n = m" if "n > 0" for m n :: nat 927 using that by simp 928 929lemma div_mult_self1_is_m [simp]: 930 "n * m div n = m" if "n > 0" for m n :: nat 931 using that by simp 932 933lemma mod_less_divisor [simp]: 934 "m mod n < n" if "n > 0" for m n :: nat 935 using mod_size_less [of n m] that by simp 936 937lemma mod_le_divisor [simp]: 938 "m mod n \<le> n" if "n > 0" for m n :: nat 939 using that by (auto simp add: le_less) 940 941lemma div_times_less_eq_dividend [simp]: 942 "m div n * n \<le> m" for m n :: nat 943 by (simp add: minus_mod_eq_div_mult [symmetric]) 944 945lemma times_div_less_eq_dividend [simp]: 946 "n * (m div n) \<le> m" for m n :: nat 947 using div_times_less_eq_dividend [of m n] 948 by (simp add: ac_simps) 949 950lemma dividend_less_div_times: 951 "m < n + (m div n) * n" if "0 < n" for m n :: nat 952proof - 953 from that have "m mod n < n" 954 by simp 955 then show ?thesis 956 by (simp add: minus_mod_eq_div_mult [symmetric]) 957qed 958 959lemma dividend_less_times_div: 960 "m < n + n * (m div n)" if "0 < n" for m n :: nat 961 using dividend_less_div_times [of n m] that 962 by (simp add: ac_simps) 963 964lemma mod_Suc_le_divisor [simp]: 965 "m mod Suc n \<le> n" 966 using mod_less_divisor [of "Suc n" m] by arith 967 968lemma mod_less_eq_dividend [simp]: 969 "m mod n \<le> m" for m n :: nat 970proof (rule add_leD2) 971 from div_mult_mod_eq have "m div n * n + m mod n = m" . 972 then show "m div n * n + m mod n \<le> m" by auto 973qed 974 975lemma 976 div_less [simp]: "m div n = 0" 977 and mod_less [simp]: "m mod n = m" 978 if "m < n" for m n :: nat 979 using that by (auto intro: div_eqI mod_eqI) 980 981lemma le_div_geq: 982 "m div n = Suc ((m - n) div n)" if "0 < n" and "n \<le> m" for m n :: nat 983proof - 984 from \<open>n \<le> m\<close> obtain q where "m = n + q" 985 by (auto simp add: le_iff_add) 986 with \<open>0 < n\<close> show ?thesis 987 by (simp add: div_add_self1) 988qed 989 990lemma le_mod_geq: 991 "m mod n = (m - n) mod n" if "n \<le> m" for m n :: nat 992proof - 993 from \<open>n \<le> m\<close> obtain q where "m = n + q" 994 by (auto simp add: le_iff_add) 995 then show ?thesis 996 by simp 997qed 998 999lemma div_if: 1000 "m div n = (if m < n \<or> n = 0 then 0 else Suc ((m - n) div n))" 1001 by (simp add: le_div_geq) 1002 1003lemma mod_if: 1004 "m mod n = (if m < n then m else (m - n) mod n)" for m n :: nat 1005 by (simp add: le_mod_geq) 1006 1007lemma div_eq_0_iff: 1008 "m div n = 0 \<longleftrightarrow> m < n \<or> n = 0" for m n :: nat 1009 by (simp add: div_eq_0_iff) 1010 1011lemma div_greater_zero_iff: 1012 "m div n > 0 \<longleftrightarrow> n \<le> m \<and> n > 0" for m n :: nat 1013 using div_eq_0_iff [of m n] by auto 1014 1015lemma mod_greater_zero_iff_not_dvd: 1016 "m mod n > 0 \<longleftrightarrow> \<not> n dvd m" for m n :: nat 1017 by (simp add: dvd_eq_mod_eq_0) 1018 1019lemma div_by_Suc_0 [simp]: 1020 "m div Suc 0 = m" 1021 using div_by_1 [of m] by simp 1022 1023lemma mod_by_Suc_0 [simp]: 1024 "m mod Suc 0 = 0" 1025 using mod_by_1 [of m] by simp 1026 1027lemma div2_Suc_Suc [simp]: 1028 "Suc (Suc m) div 2 = Suc (m div 2)" 1029 by (simp add: numeral_2_eq_2 le_div_geq) 1030 1031lemma Suc_n_div_2_gt_zero [simp]: 1032 "0 < Suc n div 2" if "n > 0" for n :: nat 1033 using that by (cases n) simp_all 1034 1035lemma div_2_gt_zero [simp]: 1036 "0 < n div 2" if "Suc 0 < n" for n :: nat 1037 using that Suc_n_div_2_gt_zero [of "n - 1"] by simp 1038 1039lemma mod2_Suc_Suc [simp]: 1040 "Suc (Suc m) mod 2 = m mod 2" 1041 by (simp add: numeral_2_eq_2 le_mod_geq) 1042 1043lemma add_self_div_2 [simp]: 1044 "(m + m) div 2 = m" for m :: nat 1045 by (simp add: mult_2 [symmetric]) 1046 1047lemma add_self_mod_2 [simp]: 1048 "(m + m) mod 2 = 0" for m :: nat 1049 by (simp add: mult_2 [symmetric]) 1050 1051lemma mod2_gr_0 [simp]: 1052 "0 < m mod 2 \<longleftrightarrow> m mod 2 = 1" for m :: nat 1053proof - 1054 have "m mod 2 < 2" 1055 by (rule mod_less_divisor) simp 1056 then have "m mod 2 = 0 \<or> m mod 2 = 1" 1057 by arith 1058 then show ?thesis 1059 by auto 1060qed 1061 1062lemma mod_Suc_eq [mod_simps]: 1063 "Suc (m mod n) mod n = Suc m mod n" 1064proof - 1065 have "(m mod n + 1) mod n = (m + 1) mod n" 1066 by (simp only: mod_simps) 1067 then show ?thesis 1068 by simp 1069qed 1070 1071lemma mod_Suc_Suc_eq [mod_simps]: 1072 "Suc (Suc (m mod n)) mod n = Suc (Suc m) mod n" 1073proof - 1074 have "(m mod n + 2) mod n = (m + 2) mod n" 1075 by (simp only: mod_simps) 1076 then show ?thesis 1077 by simp 1078qed 1079 1080lemma 1081 Suc_mod_mult_self1 [simp]: "Suc (m + k * n) mod n = Suc m mod n" 1082 and Suc_mod_mult_self2 [simp]: "Suc (m + n * k) mod n = Suc m mod n" 1083 and Suc_mod_mult_self3 [simp]: "Suc (k * n + m) mod n = Suc m mod n" 1084 and Suc_mod_mult_self4 [simp]: "Suc (n * k + m) mod n = Suc m mod n" 1085 by (subst mod_Suc_eq [symmetric], simp add: mod_simps)+ 1086 1087lemma Suc_0_mod_eq [simp]: 1088 "Suc 0 mod n = of_bool (n \<noteq> Suc 0)" 1089 by (cases n) simp_all 1090 1091context 1092 fixes m n q :: nat 1093begin 1094 1095private lemma eucl_rel_mult2: 1096 "m mod n + n * (m div n mod q) < n * q" 1097 if "n > 0" and "q > 0" 1098proof - 1099 from \<open>n > 0\<close> have "m mod n < n" 1100 by (rule mod_less_divisor) 1101 from \<open>q > 0\<close> have "m div n mod q < q" 1102 by (rule mod_less_divisor) 1103 then obtain s where "q = Suc (m div n mod q + s)" 1104 by (blast dest: less_imp_Suc_add) 1105 moreover have "m mod n + n * (m div n mod q) < n * Suc (m div n mod q + s)" 1106 using \<open>m mod n < n\<close> by (simp add: add_mult_distrib2) 1107 ultimately show ?thesis 1108 by simp 1109qed 1110 1111lemma div_mult2_eq: 1112 "m div (n * q) = (m div n) div q" 1113proof (cases "n = 0 \<or> q = 0") 1114 case True 1115 then show ?thesis 1116 by auto 1117next 1118 case False 1119 with eucl_rel_mult2 show ?thesis 1120 by (auto intro: div_eqI [of _ "n * (m div n mod q) + m mod n"] 1121 simp add: algebra_simps add_mult_distrib2 [symmetric]) 1122qed 1123 1124lemma mod_mult2_eq: 1125 "m mod (n * q) = n * (m div n mod q) + m mod n" 1126proof (cases "n = 0 \<or> q = 0") 1127 case True 1128 then show ?thesis 1129 by auto 1130next 1131 case False 1132 with eucl_rel_mult2 show ?thesis 1133 by (auto intro: mod_eqI [of _ _ "(m div n) div q"] 1134 simp add: algebra_simps add_mult_distrib2 [symmetric]) 1135qed 1136 1137end 1138 1139lemma div_le_mono: 1140 "m div k \<le> n div k" if "m \<le> n" for m n k :: nat 1141proof - 1142 from that obtain q where "n = m + q" 1143 by (auto simp add: le_iff_add) 1144 then show ?thesis 1145 by (simp add: div_add1_eq [of m q k]) 1146qed 1147 1148text \<open>Antimonotonicity of @{const divide} in second argument\<close> 1149 1150lemma div_le_mono2: 1151 "k div n \<le> k div m" if "0 < m" and "m \<le> n" for m n k :: nat 1152using that proof (induct k arbitrary: m rule: less_induct) 1153 case (less k) 1154 show ?case 1155 proof (cases "n \<le> k") 1156 case False 1157 then show ?thesis 1158 by simp 1159 next 1160 case True 1161 have "(k - n) div n \<le> (k - m) div n" 1162 using less.prems 1163 by (blast intro: div_le_mono diff_le_mono2) 1164 also have "\<dots> \<le> (k - m) div m" 1165 using \<open>n \<le> k\<close> less.prems less.hyps [of "k - m" m] 1166 by simp 1167 finally show ?thesis 1168 using \<open>n \<le> k\<close> less.prems 1169 by (simp add: le_div_geq) 1170 qed 1171qed 1172 1173lemma div_le_dividend [simp]: 1174 "m div n \<le> m" for m n :: nat 1175 using div_le_mono2 [of 1 n m] by (cases "n = 0") simp_all 1176 1177lemma div_less_dividend [simp]: 1178 "m div n < m" if "1 < n" and "0 < m" for m n :: nat 1179using that proof (induct m rule: less_induct) 1180 case (less m) 1181 show ?case 1182 proof (cases "n < m") 1183 case False 1184 with less show ?thesis 1185 by (cases "n = m") simp_all 1186 next 1187 case True 1188 then show ?thesis 1189 using less.hyps [of "m - n"] less.prems 1190 by (simp add: le_div_geq) 1191 qed 1192qed 1193 1194lemma div_eq_dividend_iff: 1195 "m div n = m \<longleftrightarrow> n = 1" if "m > 0" for m n :: nat 1196proof 1197 assume "n = 1" 1198 then show "m div n = m" 1199 by simp 1200next 1201 assume P: "m div n = m" 1202 show "n = 1" 1203 proof (rule ccontr) 1204 have "n \<noteq> 0" 1205 by (rule ccontr) (use that P in auto) 1206 moreover assume "n \<noteq> 1" 1207 ultimately have "n > 1" 1208 by simp 1209 with that have "m div n < m" 1210 by simp 1211 with P show False 1212 by simp 1213 qed 1214qed 1215 1216lemma less_mult_imp_div_less: 1217 "m div n < i" if "m < i * n" for m n i :: nat 1218proof - 1219 from that have "i * n > 0" 1220 by (cases "i * n = 0") simp_all 1221 then have "i > 0" and "n > 0" 1222 by simp_all 1223 have "m div n * n \<le> m" 1224 by simp 1225 then have "m div n * n < i * n" 1226 using that by (rule le_less_trans) 1227 with \<open>n > 0\<close> show ?thesis 1228 by simp 1229qed 1230 1231text \<open>A fact for the mutilated chess board\<close> 1232 1233lemma mod_Suc: 1234 "Suc m mod n = (if Suc (m mod n) = n then 0 else Suc (m mod n))" (is "_ = ?rhs") 1235proof (cases "n = 0") 1236 case True 1237 then show ?thesis 1238 by simp 1239next 1240 case False 1241 have "Suc m mod n = Suc (m mod n) mod n" 1242 by (simp add: mod_simps) 1243 also have "\<dots> = ?rhs" 1244 using False by (auto intro!: mod_nat_eqI intro: neq_le_trans simp add: Suc_le_eq) 1245 finally show ?thesis . 1246qed 1247 1248lemma Suc_times_mod_eq: 1249 "Suc (m * n) mod m = 1" if "Suc 0 < m" 1250 using that by (simp add: mod_Suc) 1251 1252lemma Suc_times_numeral_mod_eq [simp]: 1253 "Suc (numeral k * n) mod numeral k = 1" if "numeral k \<noteq> (1::nat)" 1254 by (rule Suc_times_mod_eq) (use that in simp) 1255 1256lemma Suc_div_le_mono [simp]: 1257 "m div n \<le> Suc m div n" 1258 by (simp add: div_le_mono) 1259 1260text \<open>These lemmas collapse some needless occurrences of Suc: 1261 at least three Sucs, since two and fewer are rewritten back to Suc again! 1262 We already have some rules to simplify operands smaller than 3.\<close> 1263 1264lemma div_Suc_eq_div_add3 [simp]: 1265 "m div Suc (Suc (Suc n)) = m div (3 + n)" 1266 by (simp add: Suc3_eq_add_3) 1267 1268lemma mod_Suc_eq_mod_add3 [simp]: 1269 "m mod Suc (Suc (Suc n)) = m mod (3 + n)" 1270 by (simp add: Suc3_eq_add_3) 1271 1272lemma Suc_div_eq_add3_div: 1273 "Suc (Suc (Suc m)) div n = (3 + m) div n" 1274 by (simp add: Suc3_eq_add_3) 1275 1276lemma Suc_mod_eq_add3_mod: 1277 "Suc (Suc (Suc m)) mod n = (3 + m) mod n" 1278 by (simp add: Suc3_eq_add_3) 1279 1280lemmas Suc_div_eq_add3_div_numeral [simp] = 1281 Suc_div_eq_add3_div [of _ "numeral v"] for v 1282 1283lemmas Suc_mod_eq_add3_mod_numeral [simp] = 1284 Suc_mod_eq_add3_mod [of _ "numeral v"] for v 1285 1286lemma (in field_char_0) of_nat_div: 1287 "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)" 1288proof - 1289 have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)" 1290 unfolding of_nat_add by (cases "n = 0") simp_all 1291 then show ?thesis 1292 by simp 1293qed 1294 1295text \<open>An ``induction'' law for modulus arithmetic.\<close> 1296 1297lemma mod_induct [consumes 3, case_names step]: 1298 "P m" if "P n" and "n < p" and "m < p" 1299 and step: "\<And>n. n < p \<Longrightarrow> P n \<Longrightarrow> P (Suc n mod p)" 1300using \<open>m < p\<close> proof (induct m) 1301 case 0 1302 show ?case 1303 proof (rule ccontr) 1304 assume "\<not> P 0" 1305 from \<open>n < p\<close> have "0 < p" 1306 by simp 1307 from \<open>n < p\<close> obtain m where "0 < m" and "p = n + m" 1308 by (blast dest: less_imp_add_positive) 1309 with \<open>P n\<close> have "P (p - m)" 1310 by simp 1311 moreover have "\<not> P (p - m)" 1312 using \<open>0 < m\<close> proof (induct m) 1313 case 0 1314 then show ?case 1315 by simp 1316 next 1317 case (Suc m) 1318 show ?case 1319 proof 1320 assume P: "P (p - Suc m)" 1321 with \<open>\<not> P 0\<close> have "Suc m < p" 1322 by (auto intro: ccontr) 1323 then have "Suc (p - Suc m) = p - m" 1324 by arith 1325 moreover from \<open>0 < p\<close> have "p - Suc m < p" 1326 by arith 1327 with P step have "P ((Suc (p - Suc m)) mod p)" 1328 by blast 1329 ultimately show False 1330 using \<open>\<not> P 0\<close> Suc.hyps by (cases "m = 0") simp_all 1331 qed 1332 qed 1333 ultimately show False 1334 by blast 1335 qed 1336next 1337 case (Suc m) 1338 then have "m < p" and mod: "Suc m mod p = Suc m" 1339 by simp_all 1340 from \<open>m < p\<close> have "P m" 1341 by (rule Suc.hyps) 1342 with \<open>m < p\<close> have "P (Suc m mod p)" 1343 by (rule step) 1344 with mod show ?case 1345 by simp 1346qed 1347 1348lemma split_div: 1349 "P (m div n) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (n \<noteq> 0 \<longrightarrow> 1350 (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P i))" 1351 (is "?P = ?Q") for m n :: nat 1352proof (cases "n = 0") 1353 case True 1354 then show ?thesis 1355 by simp 1356next 1357 case False 1358 show ?thesis 1359 proof 1360 assume ?P 1361 with False show ?Q 1362 by auto 1363 next 1364 assume ?Q 1365 with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P i" 1366 by simp 1367 with False show ?P 1368 by (auto intro: * [of "m mod n"]) 1369 qed 1370qed 1371 1372lemma split_div': 1373 "P (m div n) \<longleftrightarrow> n = 0 \<and> P 0 \<or> (\<exists>q. (n * q \<le> m \<and> m < n * Suc q) \<and> P q)" 1374proof (cases "n = 0") 1375 case True 1376 then show ?thesis 1377 by simp 1378next 1379 case False 1380 then have "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> m div n = q" for q 1381 by (auto intro: div_nat_eqI dividend_less_times_div) 1382 then show ?thesis 1383 by auto 1384qed 1385 1386lemma split_mod: 1387 "P (m mod n) \<longleftrightarrow> (n = 0 \<longrightarrow> P m) \<and> (n \<noteq> 0 \<longrightarrow> 1388 (\<forall>i j. j < n \<longrightarrow> m = n * i + j \<longrightarrow> P j))" 1389 (is "?P \<longleftrightarrow> ?Q") for m n :: nat 1390proof (cases "n = 0") 1391 case True 1392 then show ?thesis 1393 by simp 1394next 1395 case False 1396 show ?thesis 1397 proof 1398 assume ?P 1399 with False show ?Q 1400 by auto 1401 next 1402 assume ?Q 1403 with False have *: "\<And>i j. j < n \<Longrightarrow> m = n * i + j \<Longrightarrow> P j" 1404 by simp 1405 with False show ?P 1406 by (auto intro: * [of _ "m div n"]) 1407 qed 1408qed 1409 1410 1411subsection \<open>Euclidean division on @{typ int}\<close> 1412 1413instantiation int :: normalization_semidom 1414begin 1415 1416definition normalize_int :: "int \<Rightarrow> int" 1417 where [simp]: "normalize = (abs :: int \<Rightarrow> int)" 1418 1419definition unit_factor_int :: "int \<Rightarrow> int" 1420 where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)" 1421 1422definition divide_int :: "int \<Rightarrow> int \<Rightarrow> int" 1423 where "k div l = (if l = 0 then 0 1424 else if sgn k = sgn l 1425 then int (nat \<bar>k\<bar> div nat \<bar>l\<bar>) 1426 else - int (nat \<bar>k\<bar> div nat \<bar>l\<bar> + of_bool (\<not> l dvd k)))" 1427 1428lemma divide_int_unfold: 1429 "(sgn k * int m) div (sgn l * int n) = 1430 (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then 0 1431 else if sgn k = sgn l 1432 then int (m div n) 1433 else - int (m div n + of_bool (\<not> n dvd m)))" 1434 by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult 1435 nat_mult_distrib) 1436 1437instance proof 1438 fix k :: int show "k div 0 = 0" 1439 by (simp add: divide_int_def) 1440next 1441 fix k l :: int 1442 assume "l \<noteq> 0" 1443 obtain n m and s t where k: "k = sgn s * int n" and l: "l = sgn t * int m" 1444 by (blast intro: int_sgnE elim: that) 1445 then have "k * l = sgn (s * t) * int (n * m)" 1446 by (simp add: ac_simps sgn_mult) 1447 with k l \<open>l \<noteq> 0\<close> show "k * l div l = k" 1448 by (simp only: divide_int_unfold) 1449 (auto simp add: algebra_simps sgn_mult sgn_1_pos sgn_0_0) 1450qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff') 1451 1452end 1453 1454lemma coprime_int_iff [simp]: 1455 "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q") 1456proof 1457 assume ?P 1458 show ?Q 1459 proof (rule coprimeI) 1460 fix q 1461 assume "q dvd m" "q dvd n" 1462 then have "int q dvd int m" "int q dvd int n" 1463 by simp_all 1464 with \<open>?P\<close> have "is_unit (int q)" 1465 by (rule coprime_common_divisor) 1466 then show "is_unit q" 1467 by simp 1468 qed 1469next 1470 assume ?Q 1471 show ?P 1472 proof (rule coprimeI) 1473 fix k 1474 assume "k dvd int m" "k dvd int n" 1475 then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n" 1476 by simp_all 1477 with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)" 1478 by (rule coprime_common_divisor) 1479 then show "is_unit k" 1480 by simp 1481 qed 1482qed 1483 1484lemma coprime_abs_left_iff [simp]: 1485 "coprime \<bar>k\<bar> l \<longleftrightarrow> coprime k l" for k l :: int 1486 using coprime_normalize_left_iff [of k l] by simp 1487 1488lemma coprime_abs_right_iff [simp]: 1489 "coprime k \<bar>l\<bar> \<longleftrightarrow> coprime k l" for k l :: int 1490 using coprime_abs_left_iff [of l k] by (simp add: ac_simps) 1491 1492lemma coprime_nat_abs_left_iff [simp]: 1493 "coprime (nat \<bar>k\<bar>) n \<longleftrightarrow> coprime k (int n)" 1494proof - 1495 define m where "m = nat \<bar>k\<bar>" 1496 then have "\<bar>k\<bar> = int m" 1497 by simp 1498 moreover have "coprime k (int n) \<longleftrightarrow> coprime \<bar>k\<bar> (int n)" 1499 by simp 1500 ultimately show ?thesis 1501 by simp 1502qed 1503 1504lemma coprime_nat_abs_right_iff [simp]: 1505 "coprime n (nat \<bar>k\<bar>) \<longleftrightarrow> coprime (int n) k" 1506 using coprime_nat_abs_left_iff [of k n] by (simp add: ac_simps) 1507 1508lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1" 1509 for a b :: int 1510 by (drule coprime_common_divisor [of _ _ x]) simp_all 1511 1512instantiation int :: idom_modulo 1513begin 1514 1515definition modulo_int :: "int \<Rightarrow> int \<Rightarrow> int" 1516 where "k mod l = (if l = 0 then k 1517 else if sgn k = sgn l 1518 then sgn l * int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>) 1519 else sgn l * (\<bar>l\<bar> * of_bool (\<not> l dvd k) - int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)))" 1520 1521lemma modulo_int_unfold: 1522 "(sgn k * int m) mod (sgn l * int n) = 1523 (if sgn l = 0 \<or> sgn k = 0 \<or> n = 0 then sgn k * int m 1524 else if sgn k = sgn l 1525 then sgn l * int (m mod n) 1526 else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))" 1527 by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult 1528 nat_mult_distrib) 1529 1530instance proof 1531 fix k l :: int 1532 obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 1533 by (blast intro: int_sgnE elim: that) 1534 then show "k div l * l + k mod l = k" 1535 by (auto simp add: divide_int_unfold modulo_int_unfold algebra_simps dest!: sgn_not_eq_imp) 1536 (simp_all add: of_nat_mult [symmetric] of_nat_add [symmetric] 1537 distrib_left [symmetric] minus_mult_right 1538 del: of_nat_mult minus_mult_right [symmetric]) 1539qed 1540 1541end 1542 1543instantiation int :: unique_euclidean_ring 1544begin 1545 1546definition euclidean_size_int :: "int \<Rightarrow> nat" 1547 where [simp]: "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)" 1548 1549definition division_segment_int :: "int \<Rightarrow> int" 1550 where "division_segment_int k = (if k \<ge> 0 then 1 else - 1)" 1551 1552lemma division_segment_eq_sgn: 1553 "division_segment k = sgn k" if "k \<noteq> 0" for k :: int 1554 using that by (simp add: division_segment_int_def) 1555 1556lemma abs_division_segment [simp]: 1557 "\<bar>division_segment k\<bar> = 1" for k :: int 1558 by (simp add: division_segment_int_def) 1559 1560lemma abs_mod_less: 1561 "\<bar>k mod l\<bar> < \<bar>l\<bar>" if "l \<noteq> 0" for k l :: int 1562proof - 1563 obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 1564 by (blast intro: int_sgnE elim: that) 1565 with that show ?thesis 1566 by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg 1567 abs_mult mod_greater_zero_iff_not_dvd) 1568qed 1569 1570lemma sgn_mod: 1571 "sgn (k mod l) = sgn l" if "l \<noteq> 0" "\<not> l dvd k" for k l :: int 1572proof - 1573 obtain n m and s t where "k = sgn s * int n" and "l = sgn t * int m" 1574 by (blast intro: int_sgnE elim: that) 1575 with that show ?thesis 1576 by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg 1577 sgn_mult mod_eq_0_iff_dvd) 1578qed 1579 1580instance proof 1581 fix k l :: int 1582 show "division_segment (k mod l) = division_segment l" if 1583 "l \<noteq> 0" and "\<not> l dvd k" 1584 using that by (simp add: division_segment_eq_sgn dvd_eq_mod_eq_0 sgn_mod) 1585next 1586 fix l q r :: int 1587 obtain n m and s t 1588 where l: "l = sgn s * int n" and q: "q = sgn t * int m" 1589 by (blast intro: int_sgnE elim: that) 1590 assume \<open>l \<noteq> 0\<close> 1591 with l have "s \<noteq> 0" and "n > 0" 1592 by (simp_all add: sgn_0_0) 1593 assume "division_segment r = division_segment l" 1594 moreover have "r = sgn r * \<bar>r\<bar>" 1595 by (simp add: sgn_mult_abs) 1596 moreover define u where "u = nat \<bar>r\<bar>" 1597 ultimately have "r = sgn l * int u" 1598 using division_segment_eq_sgn \<open>l \<noteq> 0\<close> by (cases "r = 0") simp_all 1599 with l \<open>n > 0\<close> have r: "r = sgn s * int u" 1600 by (simp add: sgn_mult) 1601 assume "euclidean_size r < euclidean_size l" 1602 with l r \<open>s \<noteq> 0\<close> have "u < n" 1603 by (simp add: abs_mult) 1604 show "(q * l + r) div l = q" 1605 proof (cases "q = 0 \<or> r = 0") 1606 case True 1607 then show ?thesis 1608 proof 1609 assume "q = 0" 1610 then show ?thesis 1611 using l r \<open>u < n\<close> by (simp add: divide_int_unfold) 1612 next 1613 assume "r = 0" 1614 from \<open>r = 0\<close> have *: "q * l + r = sgn (t * s) * int (n * m)" 1615 using q l by (simp add: ac_simps sgn_mult) 1616 from \<open>s \<noteq> 0\<close> \<open>n > 0\<close> show ?thesis 1617 by (simp only: *, simp only: q l divide_int_unfold) 1618 (auto simp add: sgn_mult sgn_0_0 sgn_1_pos) 1619 qed 1620 next 1621 case False 1622 with q r have "t \<noteq> 0" and "m > 0" and "s \<noteq> 0" and "u > 0" 1623 by (simp_all add: sgn_0_0) 1624 moreover from \<open>0 < m\<close> \<open>u < n\<close> have "u \<le> m * n" 1625 using mult_le_less_imp_less [of 1 m u n] by simp 1626 ultimately have *: "q * l + r = sgn (s * t) 1627 * int (if t < 0 then m * n - u else m * n + u)" 1628 using l q r 1629 by (simp add: sgn_mult algebra_simps of_nat_diff) 1630 have "(m * n - u) div n = m - 1" if "u > 0" 1631 using \<open>0 < m\<close> \<open>u < n\<close> that 1632 by (auto intro: div_nat_eqI simp add: algebra_simps) 1633 moreover have "n dvd m * n - u \<longleftrightarrow> n dvd u" 1634 using \<open>u \<le> m * n\<close> dvd_diffD1 [of n "m * n" u] 1635 by auto 1636 ultimately show ?thesis 1637 using \<open>s \<noteq> 0\<close> \<open>m > 0\<close> \<open>u > 0\<close> \<open>u < n\<close> \<open>u \<le> m * n\<close> 1638 by (simp only: *, simp only: l q divide_int_unfold) 1639 (auto simp add: sgn_mult sgn_0_0 sgn_1_pos algebra_simps dest: dvd_imp_le) 1640 qed 1641qed (use mult_le_mono2 [of 1] in \<open>auto simp add: division_segment_int_def not_le zero_less_mult_iff mult_less_0_iff abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib\<close>) 1642 1643end 1644 1645lemma pos_mod_bound [simp]: 1646 "k mod l < l" if "l > 0" for k l :: int 1647proof - 1648 obtain m and s where "k = sgn s * int m" 1649 by (blast intro: int_sgnE elim: that) 1650 moreover from that obtain n where "l = sgn 1 * int n" 1651 by (cases l) auto 1652 ultimately show ?thesis 1653 using that by (simp only: modulo_int_unfold) 1654 (simp add: mod_greater_zero_iff_not_dvd) 1655qed 1656 1657lemma pos_mod_sign [simp]: 1658 "0 \<le> k mod l" if "l > 0" for k l :: int 1659proof - 1660 obtain m and s where "k = sgn s * int m" 1661 by (blast intro: int_sgnE elim: that) 1662 moreover from that obtain n where "l = sgn 1 * int n" 1663 by (cases l) auto 1664 ultimately show ?thesis 1665 using that by (simp only: modulo_int_unfold) simp 1666qed 1667 1668 1669subsection \<open>Code generation\<close> 1670 1671code_identifier 1672 code_module Euclidean_Division \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 1673 1674end 1675