1(* Title: HOL/Rings.thy 2 Author: Gertrud Bauer 3 Author: Steven Obua 4 Author: Tobias Nipkow 5 Author: Lawrence C Paulson 6 Author: Markus Wenzel 7 Author: Jeremy Avigad 8*) 9 10section \<open>Rings\<close> 11 12theory Rings 13 imports Groups Set Fun 14begin 15 16subsection \<open>Semirings and rings\<close> 17 18class semiring = ab_semigroup_add + semigroup_mult + 19 assumes distrib_right [algebra_simps, algebra_split_simps]: "(a + b) * c = a * c + b * c" 20 assumes distrib_left [algebra_simps, algebra_split_simps]: "a * (b + c) = a * b + a * c" 21begin 22 23text \<open>For the \<open>combine_numerals\<close> simproc\<close> 24lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c" 25 by (simp add: distrib_right ac_simps) 26 27end 28 29class mult_zero = times + zero + 30 assumes mult_zero_left [simp]: "0 * a = 0" 31 assumes mult_zero_right [simp]: "a * 0 = 0" 32begin 33 34lemma mult_not_zero: "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0" 35 by auto 36 37end 38 39class semiring_0 = semiring + comm_monoid_add + mult_zero 40 41class semiring_0_cancel = semiring + cancel_comm_monoid_add 42begin 43 44subclass semiring_0 45proof 46 fix a :: 'a 47 have "0 * a + 0 * a = 0 * a + 0" 48 by (simp add: distrib_right [symmetric]) 49 then show "0 * a = 0" 50 by (simp only: add_left_cancel) 51 have "a * 0 + a * 0 = a * 0 + 0" 52 by (simp add: distrib_left [symmetric]) 53 then show "a * 0 = 0" 54 by (simp only: add_left_cancel) 55qed 56 57end 58 59class comm_semiring = ab_semigroup_add + ab_semigroup_mult + 60 assumes distrib: "(a + b) * c = a * c + b * c" 61begin 62 63subclass semiring 64proof 65 fix a b c :: 'a 66 show "(a + b) * c = a * c + b * c" 67 by (simp add: distrib) 68 have "a * (b + c) = (b + c) * a" 69 by (simp add: ac_simps) 70 also have "\<dots> = b * a + c * a" 71 by (simp only: distrib) 72 also have "\<dots> = a * b + a * c" 73 by (simp add: ac_simps) 74 finally show "a * (b + c) = a * b + a * c" 75 by blast 76qed 77 78end 79 80class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero 81begin 82 83subclass semiring_0 .. 84 85end 86 87class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add 88begin 89 90subclass semiring_0_cancel .. 91 92subclass comm_semiring_0 .. 93 94end 95 96class zero_neq_one = zero + one + 97 assumes zero_neq_one [simp]: "0 \<noteq> 1" 98begin 99 100lemma one_neq_zero [simp]: "1 \<noteq> 0" 101 by (rule not_sym) (rule zero_neq_one) 102 103definition of_bool :: "bool \<Rightarrow> 'a" 104 where "of_bool p = (if p then 1 else 0)" 105 106lemma of_bool_eq [simp, code]: 107 "of_bool False = 0" 108 "of_bool True = 1" 109 by (simp_all add: of_bool_def) 110 111lemma of_bool_eq_iff: "of_bool p = of_bool q \<longleftrightarrow> p = q" 112 by (simp add: of_bool_def) 113 114lemma split_of_bool [split]: "P (of_bool p) \<longleftrightarrow> (p \<longrightarrow> P 1) \<and> (\<not> p \<longrightarrow> P 0)" 115 by (cases p) simp_all 116 117lemma split_of_bool_asm: "P (of_bool p) \<longleftrightarrow> \<not> (p \<and> \<not> P 1 \<or> \<not> p \<and> \<not> P 0)" 118 by (cases p) simp_all 119 120end 121 122class semiring_1 = zero_neq_one + semiring_0 + monoid_mult 123begin 124 125lemma of_bool_conj: 126 "of_bool (P \<and> Q) = of_bool P * of_bool Q" 127 by auto 128 129end 130 131lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = (*) 0" 132 by auto 133 134lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1" 135 by auto 136 137subsection \<open>Abstract divisibility\<close> 138 139class dvd = times 140begin 141 142definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50) 143 where "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)" 144 145lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a" 146 unfolding dvd_def .. 147 148lemma dvdE [elim]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P" 149 unfolding dvd_def by blast 150 151end 152 153context comm_monoid_mult 154begin 155 156subclass dvd . 157 158lemma dvd_refl [simp]: "a dvd a" 159proof 160 show "a = a * 1" by simp 161qed 162 163lemma dvd_trans [trans]: 164 assumes "a dvd b" and "b dvd c" 165 shows "a dvd c" 166proof - 167 from assms obtain v where "b = a * v" 168 by auto 169 moreover from assms obtain w where "c = b * w" 170 by auto 171 ultimately have "c = a * (v * w)" 172 by (simp add: mult.assoc) 173 then show ?thesis .. 174qed 175 176lemma subset_divisors_dvd: "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b" 177 by (auto simp add: subset_iff intro: dvd_trans) 178 179lemma strict_subset_divisors_dvd: "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a" 180 by (auto simp add: subset_iff intro: dvd_trans) 181 182lemma one_dvd [simp]: "1 dvd a" 183 by (auto intro: dvdI) 184 185lemma dvd_mult [simp]: "a dvd (b * c)" if "a dvd c" 186 using that by rule (auto intro: mult.left_commute dvdI) 187 188lemma dvd_mult2 [simp]: "a dvd (b * c)" if "a dvd b" 189 using that dvd_mult [of a b c] by (simp add: ac_simps) 190 191lemma dvd_triv_right [simp]: "a dvd b * a" 192 by (rule dvd_mult) (rule dvd_refl) 193 194lemma dvd_triv_left [simp]: "a dvd a * b" 195 by (rule dvd_mult2) (rule dvd_refl) 196 197lemma mult_dvd_mono: 198 assumes "a dvd b" 199 and "c dvd d" 200 shows "a * c dvd b * d" 201proof - 202 from \<open>a dvd b\<close> obtain b' where "b = a * b'" .. 203 moreover from \<open>c dvd d\<close> obtain d' where "d = c * d'" .. 204 ultimately have "b * d = (a * c) * (b' * d')" 205 by (simp add: ac_simps) 206 then show ?thesis .. 207qed 208 209lemma dvd_mult_left: "a * b dvd c \<Longrightarrow> a dvd c" 210 by (simp add: dvd_def mult.assoc) blast 211 212lemma dvd_mult_right: "a * b dvd c \<Longrightarrow> b dvd c" 213 using dvd_mult_left [of b a c] by (simp add: ac_simps) 214 215end 216 217class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult 218begin 219 220subclass semiring_1 .. 221 222lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0" 223 by auto 224 225lemma dvd_0_right [iff]: "a dvd 0" 226proof 227 show "0 = a * 0" by simp 228qed 229 230lemma dvd_0_left: "0 dvd a \<Longrightarrow> a = 0" 231 by simp 232 233lemma dvd_add [simp]: 234 assumes "a dvd b" and "a dvd c" 235 shows "a dvd (b + c)" 236proof - 237 from \<open>a dvd b\<close> obtain b' where "b = a * b'" .. 238 moreover from \<open>a dvd c\<close> obtain c' where "c = a * c'" .. 239 ultimately have "b + c = a * (b' + c')" 240 by (simp add: distrib_left) 241 then show ?thesis .. 242qed 243 244end 245 246class semiring_1_cancel = semiring + cancel_comm_monoid_add 247 + zero_neq_one + monoid_mult 248begin 249 250subclass semiring_0_cancel .. 251 252subclass semiring_1 .. 253 254end 255 256class comm_semiring_1_cancel = 257 comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult + 258 assumes right_diff_distrib' [algebra_simps, algebra_split_simps]: 259 "a * (b - c) = a * b - a * c" 260begin 261 262subclass semiring_1_cancel .. 263subclass comm_semiring_0_cancel .. 264subclass comm_semiring_1 .. 265 266lemma left_diff_distrib' [algebra_simps, algebra_split_simps]: 267 "(b - c) * a = b * a - c * a" 268 by (simp add: algebra_simps) 269 270lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b" 271proof - 272 have "a dvd a * c + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q") 273 proof 274 assume ?Q 275 then show ?P by simp 276 next 277 assume ?P 278 then obtain d where "a * c + b = a * d" .. 279 then have "a * c + b - a * c = a * d - a * c" by simp 280 then have "b = a * d - a * c" by simp 281 then have "b = a * (d - c)" by (simp add: algebra_simps) 282 then show ?Q .. 283 qed 284 then show "a dvd c * a + b \<longleftrightarrow> a dvd b" by (simp add: ac_simps) 285qed 286 287lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \<longleftrightarrow> a dvd b" 288 using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps) 289 290lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \<longleftrightarrow> a dvd b" 291 using dvd_add_times_triv_left_iff [of a 1 b] by simp 292 293lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \<longleftrightarrow> a dvd b" 294 using dvd_add_times_triv_right_iff [of a b 1] by simp 295 296lemma dvd_add_right_iff: 297 assumes "a dvd b" 298 shows "a dvd b + c \<longleftrightarrow> a dvd c" (is "?P \<longleftrightarrow> ?Q") 299proof 300 assume ?P 301 then obtain d where "b + c = a * d" .. 302 moreover from \<open>a dvd b\<close> obtain e where "b = a * e" .. 303 ultimately have "a * e + c = a * d" by simp 304 then have "a * e + c - a * e = a * d - a * e" by simp 305 then have "c = a * d - a * e" by simp 306 then have "c = a * (d - e)" by (simp add: algebra_simps) 307 then show ?Q .. 308next 309 assume ?Q 310 with assms show ?P by simp 311qed 312 313lemma dvd_add_left_iff: "a dvd c \<Longrightarrow> a dvd b + c \<longleftrightarrow> a dvd b" 314 using dvd_add_right_iff [of a c b] by (simp add: ac_simps) 315 316end 317 318class ring = semiring + ab_group_add 319begin 320 321subclass semiring_0_cancel .. 322 323text \<open>Distribution rules\<close> 324 325lemma minus_mult_left: "- (a * b) = - a * b" 326 by (rule minus_unique) (simp add: distrib_right [symmetric]) 327 328lemma minus_mult_right: "- (a * b) = a * - b" 329 by (rule minus_unique) (simp add: distrib_left [symmetric]) 330 331text \<open>Extract signs from products\<close> 332lemmas mult_minus_left [simp] = minus_mult_left [symmetric] 333lemmas mult_minus_right [simp] = minus_mult_right [symmetric] 334 335lemma minus_mult_minus [simp]: "- a * - b = a * b" 336 by simp 337 338lemma minus_mult_commute: "- a * b = a * - b" 339 by simp 340 341lemma right_diff_distrib [algebra_simps, algebra_split_simps]: 342 "a * (b - c) = a * b - a * c" 343 using distrib_left [of a b "-c "] by simp 344 345lemma left_diff_distrib [algebra_simps, algebra_split_simps]: 346 "(a - b) * c = a * c - b * c" 347 using distrib_right [of a "- b" c] by simp 348 349lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib 350 351lemma eq_add_iff1: "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d" 352 by (simp add: algebra_simps) 353 354lemma eq_add_iff2: "a * e + c = b * e + d \<longleftrightarrow> c = (b - a) * e + d" 355 by (simp add: algebra_simps) 356 357end 358 359lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib 360 361class comm_ring = comm_semiring + ab_group_add 362begin 363 364subclass ring .. 365subclass comm_semiring_0_cancel .. 366 367lemma square_diff_square_factored: "x * x - y * y = (x + y) * (x - y)" 368 by (simp add: algebra_simps) 369 370end 371 372class ring_1 = ring + zero_neq_one + monoid_mult 373begin 374 375subclass semiring_1_cancel .. 376 377lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)" 378 by (simp add: algebra_simps) 379 380end 381 382class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult 383begin 384 385subclass ring_1 .. 386subclass comm_semiring_1_cancel 387 by standard (simp add: algebra_simps) 388 389lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y" 390proof 391 assume "x dvd - y" 392 then have "x dvd - 1 * - y" by (rule dvd_mult) 393 then show "x dvd y" by simp 394next 395 assume "x dvd y" 396 then have "x dvd - 1 * y" by (rule dvd_mult) 397 then show "x dvd - y" by simp 398qed 399 400lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y" 401proof 402 assume "- x dvd y" 403 then obtain k where "y = - x * k" .. 404 then have "y = x * - k" by simp 405 then show "x dvd y" .. 406next 407 assume "x dvd y" 408 then obtain k where "y = x * k" .. 409 then have "y = - x * - k" by simp 410 then show "- x dvd y" .. 411qed 412 413lemma dvd_diff [simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)" 414 using dvd_add [of x y "- z"] by simp 415 416end 417 418 419subsection \<open>Towards integral domains\<close> 420 421class semiring_no_zero_divisors = semiring_0 + 422 assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0" 423begin 424 425lemma divisors_zero: 426 assumes "a * b = 0" 427 shows "a = 0 \<or> b = 0" 428proof (rule classical) 429 assume "\<not> ?thesis" 430 then have "a \<noteq> 0" and "b \<noteq> 0" by auto 431 with no_zero_divisors have "a * b \<noteq> 0" by blast 432 with assms show ?thesis by simp 433qed 434 435lemma mult_eq_0_iff [simp]: "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 436proof (cases "a = 0 \<or> b = 0") 437 case False 438 then have "a \<noteq> 0" and "b \<noteq> 0" by auto 439 then show ?thesis using no_zero_divisors by simp 440next 441 case True 442 then show ?thesis by auto 443qed 444 445end 446 447class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors 448 449class semiring_no_zero_divisors_cancel = semiring_no_zero_divisors + 450 assumes mult_cancel_right [simp]: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" 451 and mult_cancel_left [simp]: "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" 452begin 453 454lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> c * a = c * b \<longleftrightarrow> a = b" 455 by simp 456 457lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> a * c = b * c \<longleftrightarrow> a = b" 458 by simp 459 460end 461 462class ring_no_zero_divisors = ring + semiring_no_zero_divisors 463begin 464 465subclass semiring_no_zero_divisors_cancel 466proof 467 fix a b c 468 have "a * c = b * c \<longleftrightarrow> (a - b) * c = 0" 469 by (simp add: algebra_simps) 470 also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b" 471 by auto 472 finally show "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" . 473 have "c * a = c * b \<longleftrightarrow> c * (a - b) = 0" 474 by (simp add: algebra_simps) 475 also have "\<dots> \<longleftrightarrow> c = 0 \<or> a = b" 476 by auto 477 finally show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" . 478qed 479 480end 481 482class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors 483begin 484 485subclass semiring_1_no_zero_divisors .. 486 487lemma square_eq_1_iff: "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1" 488proof - 489 have "(x - 1) * (x + 1) = x * x - 1" 490 by (simp add: algebra_simps) 491 then have "x * x = 1 \<longleftrightarrow> (x - 1) * (x + 1) = 0" 492 by simp 493 then show ?thesis 494 by (simp add: eq_neg_iff_add_eq_0) 495qed 496 497lemma mult_cancel_right1 [simp]: "c = b * c \<longleftrightarrow> c = 0 \<or> b = 1" 498 using mult_cancel_right [of 1 c b] by auto 499 500lemma mult_cancel_right2 [simp]: "a * c = c \<longleftrightarrow> c = 0 \<or> a = 1" 501 using mult_cancel_right [of a c 1] by simp 502 503lemma mult_cancel_left1 [simp]: "c = c * b \<longleftrightarrow> c = 0 \<or> b = 1" 504 using mult_cancel_left [of c 1 b] by force 505 506lemma mult_cancel_left2 [simp]: "c * a = c \<longleftrightarrow> c = 0 \<or> a = 1" 507 using mult_cancel_left [of c a 1] by simp 508 509end 510 511class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors 512begin 513 514subclass semiring_1_no_zero_divisors .. 515 516end 517 518class idom = comm_ring_1 + semiring_no_zero_divisors 519begin 520 521subclass semidom .. 522 523subclass ring_1_no_zero_divisors .. 524 525lemma dvd_mult_cancel_right [simp]: 526 "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b" 527proof - 528 have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)" 529 by (auto simp add: ac_simps) 530 also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b" 531 by auto 532 finally show ?thesis . 533qed 534 535lemma dvd_mult_cancel_left [simp]: 536 "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b" 537 using dvd_mult_cancel_right [of a c b] by (simp add: ac_simps) 538 539lemma square_eq_iff: "a * a = b * b \<longleftrightarrow> a = b \<or> a = - b" 540proof 541 assume "a * a = b * b" 542 then have "(a - b) * (a + b) = 0" 543 by (simp add: algebra_simps) 544 then show "a = b \<or> a = - b" 545 by (simp add: eq_neg_iff_add_eq_0) 546next 547 assume "a = b \<or> a = - b" 548 then show "a * a = b * b" by auto 549qed 550 551end 552 553class idom_abs_sgn = idom + abs + sgn + 554 assumes sgn_mult_abs: "sgn a * \<bar>a\<bar> = a" 555 and sgn_sgn [simp]: "sgn (sgn a) = sgn a" 556 and abs_abs [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" 557 and abs_0 [simp]: "\<bar>0\<bar> = 0" 558 and sgn_0 [simp]: "sgn 0 = 0" 559 and sgn_1 [simp]: "sgn 1 = 1" 560 and sgn_minus_1: "sgn (- 1) = - 1" 561 and sgn_mult: "sgn (a * b) = sgn a * sgn b" 562begin 563 564lemma sgn_eq_0_iff: 565 "sgn a = 0 \<longleftrightarrow> a = 0" 566proof - 567 { assume "sgn a = 0" 568 then have "sgn a * \<bar>a\<bar> = 0" 569 by simp 570 then have "a = 0" 571 by (simp add: sgn_mult_abs) 572 } then show ?thesis 573 by auto 574qed 575 576lemma abs_eq_0_iff: 577 "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" 578proof - 579 { assume "\<bar>a\<bar> = 0" 580 then have "sgn a * \<bar>a\<bar> = 0" 581 by simp 582 then have "a = 0" 583 by (simp add: sgn_mult_abs) 584 } then show ?thesis 585 by auto 586qed 587 588lemma abs_mult_sgn: 589 "\<bar>a\<bar> * sgn a = a" 590 using sgn_mult_abs [of a] by (simp add: ac_simps) 591 592lemma abs_1 [simp]: 593 "\<bar>1\<bar> = 1" 594 using sgn_mult_abs [of 1] by simp 595 596lemma sgn_abs [simp]: 597 "\<bar>sgn a\<bar> = of_bool (a \<noteq> 0)" 598 using sgn_mult_abs [of "sgn a"] mult_cancel_left [of "sgn a" "\<bar>sgn a\<bar>" 1] 599 by (auto simp add: sgn_eq_0_iff) 600 601lemma abs_sgn [simp]: 602 "sgn \<bar>a\<bar> = of_bool (a \<noteq> 0)" 603 using sgn_mult_abs [of "\<bar>a\<bar>"] mult_cancel_right [of "sgn \<bar>a\<bar>" "\<bar>a\<bar>" 1] 604 by (auto simp add: abs_eq_0_iff) 605 606lemma abs_mult: 607 "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 608proof (cases "a = 0 \<or> b = 0") 609 case True 610 then show ?thesis 611 by auto 612next 613 case False 614 then have *: "sgn (a * b) \<noteq> 0" 615 by (simp add: sgn_eq_0_iff) 616 from abs_mult_sgn [of "a * b"] abs_mult_sgn [of a] abs_mult_sgn [of b] 617 have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * sgn a * \<bar>b\<bar> * sgn b" 618 by (simp add: ac_simps) 619 then have "\<bar>a * b\<bar> * sgn (a * b) = \<bar>a\<bar> * \<bar>b\<bar> * sgn (a * b)" 620 by (simp add: sgn_mult ac_simps) 621 with * show ?thesis 622 by simp 623qed 624 625lemma sgn_minus [simp]: 626 "sgn (- a) = - sgn a" 627proof - 628 from sgn_minus_1 have "sgn (- 1 * a) = - 1 * sgn a" 629 by (simp only: sgn_mult) 630 then show ?thesis 631 by simp 632qed 633 634lemma abs_minus [simp]: 635 "\<bar>- a\<bar> = \<bar>a\<bar>" 636proof - 637 have [simp]: "\<bar>- 1\<bar> = 1" 638 using sgn_mult_abs [of "- 1"] by simp 639 then have "\<bar>- 1 * a\<bar> = 1 * \<bar>a\<bar>" 640 by (simp only: abs_mult) 641 then show ?thesis 642 by simp 643qed 644 645end 646 647 648subsection \<open>(Partial) Division\<close> 649 650class divide = 651 fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70) 652 653setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close> 654 655context semiring 656begin 657 658lemma [field_simps, field_split_simps]: 659 shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c" 660 and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c" 661 by (rule distrib_left distrib_right)+ 662 663end 664 665context ring 666begin 667 668lemma [field_simps, field_split_simps]: 669 shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c" 670 and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c" 671 by (rule left_diff_distrib right_diff_distrib)+ 672 673end 674 675setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a::divide \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close> 676 677text \<open>Algebraic classes with division\<close> 678 679class semidom_divide = semidom + divide + 680 assumes nonzero_mult_div_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a" 681 assumes div_by_0 [simp]: "a div 0 = 0" 682begin 683 684lemma nonzero_mult_div_cancel_left [simp]: "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b" 685 using nonzero_mult_div_cancel_right [of a b] by (simp add: ac_simps) 686 687subclass semiring_no_zero_divisors_cancel 688proof 689 show *: "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b" for a b c 690 proof (cases "c = 0") 691 case True 692 then show ?thesis by simp 693 next 694 case False 695 have "a = b" if "a * c = b * c" 696 proof - 697 from that have "a * c div c = b * c div c" 698 by simp 699 with False show ?thesis 700 by simp 701 qed 702 then show ?thesis by auto 703 qed 704 show "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" for a b c 705 using * [of a c b] by (simp add: ac_simps) 706qed 707 708lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1" 709 using nonzero_mult_div_cancel_left [of a 1] by simp 710 711lemma div_0 [simp]: "0 div a = 0" 712proof (cases "a = 0") 713 case True 714 then show ?thesis by simp 715next 716 case False 717 then have "a * 0 div a = 0" 718 by (rule nonzero_mult_div_cancel_left) 719 then show ?thesis by simp 720qed 721 722lemma div_by_1 [simp]: "a div 1 = a" 723 using nonzero_mult_div_cancel_left [of 1 a] by simp 724 725lemma dvd_div_eq_0_iff: 726 assumes "b dvd a" 727 shows "a div b = 0 \<longleftrightarrow> a = 0" 728 using assms by (elim dvdE, cases "b = 0") simp_all 729 730lemma dvd_div_eq_cancel: 731 "a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b" 732 by (elim dvdE, cases "c = 0") simp_all 733 734lemma dvd_div_eq_iff: 735 "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b" 736 by (elim dvdE, cases "c = 0") simp_all 737 738lemma inj_on_mult: 739 "inj_on ((*) a) A" if "a \<noteq> 0" 740proof (rule inj_onI) 741 fix b c 742 assume "a * b = a * c" 743 then have "a * b div a = a * c div a" 744 by (simp only:) 745 with that show "b = c" 746 by simp 747qed 748 749end 750 751class idom_divide = idom + semidom_divide 752begin 753 754lemma dvd_neg_div: 755 assumes "b dvd a" 756 shows "- a div b = - (a div b)" 757proof (cases "b = 0") 758 case True 759 then show ?thesis by simp 760next 761 case False 762 from assms obtain c where "a = b * c" .. 763 then have "- a div b = (b * - c) div b" 764 by simp 765 from False also have "\<dots> = - c" 766 by (rule nonzero_mult_div_cancel_left) 767 with False \<open>a = b * c\<close> show ?thesis 768 by simp 769qed 770 771lemma dvd_div_neg: 772 assumes "b dvd a" 773 shows "a div - b = - (a div b)" 774proof (cases "b = 0") 775 case True 776 then show ?thesis by simp 777next 778 case False 779 then have "- b \<noteq> 0" 780 by simp 781 from assms obtain c where "a = b * c" .. 782 then have "a div - b = (- b * - c) div - b" 783 by simp 784 from \<open>- b \<noteq> 0\<close> also have "\<dots> = - c" 785 by (rule nonzero_mult_div_cancel_left) 786 with False \<open>a = b * c\<close> show ?thesis 787 by simp 788qed 789 790end 791 792class algebraic_semidom = semidom_divide 793begin 794 795text \<open> 796 Class \<^class>\<open>algebraic_semidom\<close> enriches a integral domain 797 by notions from algebra, like units in a ring. 798 It is a separate class to avoid spoiling fields with notions 799 which are degenerated there. 800\<close> 801 802lemma dvd_times_left_cancel_iff [simp]: 803 assumes "a \<noteq> 0" 804 shows "a * b dvd a * c \<longleftrightarrow> b dvd c" 805 (is "?lhs \<longleftrightarrow> ?rhs") 806proof 807 assume ?lhs 808 then obtain d where "a * c = a * b * d" .. 809 with assms have "c = b * d" by (simp add: ac_simps) 810 then show ?rhs .. 811next 812 assume ?rhs 813 then obtain d where "c = b * d" .. 814 then have "a * c = a * b * d" by (simp add: ac_simps) 815 then show ?lhs .. 816qed 817 818lemma dvd_times_right_cancel_iff [simp]: 819 assumes "a \<noteq> 0" 820 shows "b * a dvd c * a \<longleftrightarrow> b dvd c" 821 using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps) 822 823lemma div_dvd_iff_mult: 824 assumes "b \<noteq> 0" and "b dvd a" 825 shows "a div b dvd c \<longleftrightarrow> a dvd c * b" 826proof - 827 from \<open>b dvd a\<close> obtain d where "a = b * d" .. 828 with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps) 829qed 830 831lemma dvd_div_iff_mult: 832 assumes "c \<noteq> 0" and "c dvd b" 833 shows "a dvd b div c \<longleftrightarrow> a * c dvd b" 834proof - 835 from \<open>c dvd b\<close> obtain d where "b = c * d" .. 836 with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a]) 837qed 838 839lemma div_dvd_div [simp]: 840 assumes "a dvd b" and "a dvd c" 841 shows "b div a dvd c div a \<longleftrightarrow> b dvd c" 842proof (cases "a = 0") 843 case True 844 with assms show ?thesis by simp 845next 846 case False 847 moreover from assms obtain k l where "b = a * k" and "c = a * l" 848 by blast 849 ultimately show ?thesis by simp 850qed 851 852lemma div_add [simp]: 853 assumes "c dvd a" and "c dvd b" 854 shows "(a + b) div c = a div c + b div c" 855proof (cases "c = 0") 856 case True 857 then show ?thesis by simp 858next 859 case False 860 moreover from assms obtain k l where "a = c * k" and "b = c * l" 861 by blast 862 moreover have "c * k + c * l = c * (k + l)" 863 by (simp add: algebra_simps) 864 ultimately show ?thesis 865 by simp 866qed 867 868lemma div_mult_div_if_dvd: 869 assumes "b dvd a" and "d dvd c" 870 shows "(a div b) * (c div d) = (a * c) div (b * d)" 871proof (cases "b = 0 \<or> c = 0") 872 case True 873 with assms show ?thesis by auto 874next 875 case False 876 moreover from assms obtain k l where "a = b * k" and "c = d * l" 877 by blast 878 moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)" 879 by (simp add: ac_simps) 880 ultimately show ?thesis by simp 881qed 882 883lemma dvd_div_eq_mult: 884 assumes "a \<noteq> 0" and "a dvd b" 885 shows "b div a = c \<longleftrightarrow> b = c * a" 886 (is "?lhs \<longleftrightarrow> ?rhs") 887proof 888 assume ?rhs 889 then show ?lhs by (simp add: assms) 890next 891 assume ?lhs 892 then have "b div a * a = c * a" by simp 893 moreover from assms have "b div a * a = b" 894 by (auto simp add: ac_simps) 895 ultimately show ?rhs by simp 896qed 897 898lemma dvd_div_mult_self [simp]: "a dvd b \<Longrightarrow> b div a * a = b" 899 by (cases "a = 0") (auto simp add: ac_simps) 900 901lemma dvd_mult_div_cancel [simp]: "a dvd b \<Longrightarrow> a * (b div a) = b" 902 using dvd_div_mult_self [of a b] by (simp add: ac_simps) 903 904lemma div_mult_swap: 905 assumes "c dvd b" 906 shows "a * (b div c) = (a * b) div c" 907proof (cases "c = 0") 908 case True 909 then show ?thesis by simp 910next 911 case False 912 from assms obtain d where "b = c * d" .. 913 moreover from False have "a * divide (d * c) c = ((a * d) * c) div c" 914 by simp 915 ultimately show ?thesis by (simp add: ac_simps) 916qed 917 918lemma dvd_div_mult: "c dvd b \<Longrightarrow> b div c * a = (b * a) div c" 919 using div_mult_swap [of c b a] by (simp add: ac_simps) 920 921lemma dvd_div_mult2_eq: 922 assumes "b * c dvd a" 923 shows "a div (b * c) = a div b div c" 924proof - 925 from assms obtain k where "a = b * c * k" .. 926 then show ?thesis 927 by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps) 928qed 929 930lemma dvd_div_div_eq_mult: 931 assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d" 932 shows "b div a = d div c \<longleftrightarrow> b * c = a * d" 933 (is "?lhs \<longleftrightarrow> ?rhs") 934proof - 935 from assms have "a * c \<noteq> 0" by simp 936 then have "?lhs \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)" 937 by simp 938 also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a" 939 by (simp add: ac_simps) 940 also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a" 941 using assms by (simp add: div_mult_swap) 942 also have "\<dots> \<longleftrightarrow> ?rhs" 943 using assms by (simp add: ac_simps) 944 finally show ?thesis . 945qed 946 947lemma dvd_mult_imp_div: 948 assumes "a * c dvd b" 949 shows "a dvd b div c" 950proof (cases "c = 0") 951 case True then show ?thesis by simp 952next 953 case False 954 from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" .. 955 with False show ?thesis 956 by (simp add: mult.commute [of a] mult.assoc) 957qed 958 959lemma div_div_eq_right: 960 assumes "c dvd b" "b dvd a" 961 shows "a div (b div c) = a div b * c" 962proof (cases "c = 0 \<or> b = 0") 963 case True 964 then show ?thesis 965 by auto 966next 967 case False 968 from assms obtain r s where "b = c * r" and "a = c * r * s" 969 by blast 970 moreover with False have "r \<noteq> 0" 971 by auto 972 ultimately show ?thesis using False 973 by simp (simp add: mult.commute [of _ r] mult.assoc mult.commute [of c]) 974qed 975 976lemma div_div_div_same: 977 assumes "d dvd b" "b dvd a" 978 shows "(a div d) div (b div d) = a div b" 979proof (cases "b = 0 \<or> d = 0") 980 case True 981 with assms show ?thesis 982 by auto 983next 984 case False 985 from assms obtain r s 986 where "a = d * r * s" and "b = d * r" 987 by blast 988 with False show ?thesis 989 by simp (simp add: ac_simps) 990qed 991 992 993text \<open>Units: invertible elements in a ring\<close> 994 995abbreviation is_unit :: "'a \<Rightarrow> bool" 996 where "is_unit a \<equiv> a dvd 1" 997 998lemma not_is_unit_0 [simp]: "\<not> is_unit 0" 999 by simp 1000 1001lemma unit_imp_dvd [dest]: "is_unit b \<Longrightarrow> b dvd a" 1002 by (rule dvd_trans [of _ 1]) simp_all 1003 1004lemma unit_dvdE: 1005 assumes "is_unit a" 1006 obtains c where "a \<noteq> 0" and "b = a * c" 1007proof - 1008 from assms have "a dvd b" by auto 1009 then obtain c where "b = a * c" .. 1010 moreover from assms have "a \<noteq> 0" by auto 1011 ultimately show thesis using that by blast 1012qed 1013 1014lemma dvd_unit_imp_unit: "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a" 1015 by (rule dvd_trans) 1016 1017lemma unit_div_1_unit [simp, intro]: 1018 assumes "is_unit a" 1019 shows "is_unit (1 div a)" 1020proof - 1021 from assms have "1 = 1 div a * a" by simp 1022 then show "is_unit (1 div a)" by (rule dvdI) 1023qed 1024 1025lemma is_unitE [elim?]: 1026 assumes "is_unit a" 1027 obtains b where "a \<noteq> 0" and "b \<noteq> 0" 1028 and "is_unit b" and "1 div a = b" and "1 div b = a" 1029 and "a * b = 1" and "c div a = c * b" 1030proof (rule that) 1031 define b where "b = 1 div a" 1032 then show "1 div a = b" by simp 1033 from assms b_def show "is_unit b" by simp 1034 with assms show "a \<noteq> 0" and "b \<noteq> 0" by auto 1035 from assms b_def show "a * b = 1" by simp 1036 then have "1 = a * b" .. 1037 with b_def \<open>b \<noteq> 0\<close> show "1 div b = a" by simp 1038 from assms have "a dvd c" .. 1039 then obtain d where "c = a * d" .. 1040 with \<open>a \<noteq> 0\<close> \<open>a * b = 1\<close> show "c div a = c * b" 1041 by (simp add: mult.assoc mult.left_commute [of a]) 1042qed 1043 1044lemma unit_prod [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)" 1045 by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 1046 1047lemma is_unit_mult_iff: "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" 1048 by (auto dest: dvd_mult_left dvd_mult_right) 1049 1050lemma unit_div [intro]: "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)" 1051 by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod) 1052 1053lemma mult_unit_dvd_iff: 1054 assumes "is_unit b" 1055 shows "a * b dvd c \<longleftrightarrow> a dvd c" 1056proof 1057 assume "a * b dvd c" 1058 with assms show "a dvd c" 1059 by (simp add: dvd_mult_left) 1060next 1061 assume "a dvd c" 1062 then obtain k where "c = a * k" .. 1063 with assms have "c = (a * b) * (1 div b * k)" 1064 by (simp add: mult_ac) 1065 then show "a * b dvd c" by (rule dvdI) 1066qed 1067 1068lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c" 1069 using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps) 1070 1071lemma dvd_mult_unit_iff: 1072 assumes "is_unit b" 1073 shows "a dvd c * b \<longleftrightarrow> a dvd c" 1074proof 1075 assume "a dvd c * b" 1076 with assms have "c * b dvd c * (b * (1 div b))" 1077 by (subst mult_assoc [symmetric]) simp 1078 also from assms have "b * (1 div b) = 1" 1079 by (rule is_unitE) simp 1080 finally have "c * b dvd c" by simp 1081 with \<open>a dvd c * b\<close> show "a dvd c" by (rule dvd_trans) 1082next 1083 assume "a dvd c" 1084 then show "a dvd c * b" by simp 1085qed 1086 1087lemma dvd_mult_unit_iff': "is_unit b \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd c" 1088 using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps) 1089 1090lemma div_unit_dvd_iff: "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c" 1091 by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff) 1092 1093lemma dvd_div_unit_iff: "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c" 1094 by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff) 1095 1096lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff' 1097 dvd_mult_unit_iff dvd_mult_unit_iff' 1098 div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *) 1099 1100lemma unit_mult_div_div [simp]: "is_unit a \<Longrightarrow> b * (1 div a) = b div a" 1101 by (erule is_unitE [of _ b]) simp 1102 1103lemma unit_div_mult_self [simp]: "is_unit a \<Longrightarrow> b div a * a = b" 1104 by (rule dvd_div_mult_self) auto 1105 1106lemma unit_div_1_div_1 [simp]: "is_unit a \<Longrightarrow> 1 div (1 div a) = a" 1107 by (erule is_unitE) simp 1108 1109lemma unit_div_mult_swap: "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c" 1110 by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c]) 1111 1112lemma unit_div_commute: "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b" 1113 using unit_div_mult_swap [of b c a] by (simp add: ac_simps) 1114 1115lemma unit_eq_div1: "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b" 1116 by (auto elim: is_unitE) 1117 1118lemma unit_eq_div2: "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c" 1119 using unit_eq_div1 [of b c a] by auto 1120 1121lemma unit_mult_left_cancel: "is_unit a \<Longrightarrow> a * b = a * c \<longleftrightarrow> b = c" 1122 using mult_cancel_left [of a b c] by auto 1123 1124lemma unit_mult_right_cancel: "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c" 1125 using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps) 1126 1127lemma unit_div_cancel: 1128 assumes "is_unit a" 1129 shows "b div a = c div a \<longleftrightarrow> b = c" 1130proof - 1131 from assms have "is_unit (1 div a)" by simp 1132 then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c" 1133 by (rule unit_mult_right_cancel) 1134 with assms show ?thesis by simp 1135qed 1136 1137lemma is_unit_div_mult2_eq: 1138 assumes "is_unit b" and "is_unit c" 1139 shows "a div (b * c) = a div b div c" 1140proof - 1141 from assms have "is_unit (b * c)" 1142 by (simp add: unit_prod) 1143 then have "b * c dvd a" 1144 by (rule unit_imp_dvd) 1145 then show ?thesis 1146 by (rule dvd_div_mult2_eq) 1147qed 1148 1149lemma is_unit_div_mult_cancel_left: 1150 assumes "a \<noteq> 0" and "is_unit b" 1151 shows "a div (a * b) = 1 div b" 1152proof - 1153 from assms have "a div (a * b) = a div a div b" 1154 by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq) 1155 with assms show ?thesis by simp 1156qed 1157 1158lemma is_unit_div_mult_cancel_right: 1159 assumes "a \<noteq> 0" and "is_unit b" 1160 shows "a div (b * a) = 1 div b" 1161 using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps) 1162 1163lemma unit_div_eq_0_iff: 1164 assumes "is_unit b" 1165 shows "a div b = 0 \<longleftrightarrow> a = 0" 1166 by (rule dvd_div_eq_0_iff) (insert assms, auto) 1167 1168lemma div_mult_unit2: 1169 "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c" 1170 by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff) 1171 1172 1173text \<open>Coprimality\<close> 1174 1175definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 1176 where "coprime a b \<longleftrightarrow> (\<forall>c. c dvd a \<longrightarrow> c dvd b \<longrightarrow> is_unit c)" 1177 1178lemma coprimeI: 1179 assumes "\<And>c. c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> is_unit c" 1180 shows "coprime a b" 1181 using assms by (auto simp: coprime_def) 1182 1183lemma not_coprimeI: 1184 assumes "c dvd a" and "c dvd b" and "\<not> is_unit c" 1185 shows "\<not> coprime a b" 1186 using assms by (auto simp: coprime_def) 1187 1188lemma coprime_common_divisor: 1189 "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b" 1190 using that by (auto simp: coprime_def) 1191 1192lemma not_coprimeE: 1193 assumes "\<not> coprime a b" 1194 obtains c where "c dvd a" and "c dvd b" and "\<not> is_unit c" 1195 using assms by (auto simp: coprime_def) 1196 1197lemma coprime_imp_coprime: 1198 "coprime a b" if "coprime c d" 1199 and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd c" 1200 and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd d" 1201proof (rule coprimeI) 1202 fix e 1203 assume "e dvd a" and "e dvd b" 1204 with that have "e dvd c" and "e dvd d" 1205 by (auto intro: dvd_trans) 1206 with \<open>coprime c d\<close> show "is_unit e" 1207 by (rule coprime_common_divisor) 1208qed 1209 1210lemma coprime_divisors: 1211 "coprime a b" if "a dvd c" "b dvd d" and "coprime c d" 1212using \<open>coprime c d\<close> proof (rule coprime_imp_coprime) 1213 fix e 1214 assume "e dvd a" then show "e dvd c" 1215 using \<open>a dvd c\<close> by (rule dvd_trans) 1216 assume "e dvd b" then show "e dvd d" 1217 using \<open>b dvd d\<close> by (rule dvd_trans) 1218qed 1219 1220lemma coprime_self [simp]: 1221 "coprime a a \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q") 1222proof 1223 assume ?P 1224 then show ?Q 1225 by (rule coprime_common_divisor) simp_all 1226next 1227 assume ?Q 1228 show ?P 1229 by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>) 1230qed 1231 1232lemma coprime_commute [ac_simps]: 1233 "coprime b a \<longleftrightarrow> coprime a b" 1234 unfolding coprime_def by auto 1235 1236lemma is_unit_left_imp_coprime: 1237 "coprime a b" if "is_unit a" 1238proof (rule coprimeI) 1239 fix c 1240 assume "c dvd a" 1241 with that show "is_unit c" 1242 by (auto intro: dvd_unit_imp_unit) 1243qed 1244 1245lemma is_unit_right_imp_coprime: 1246 "coprime a b" if "is_unit b" 1247 using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps) 1248 1249lemma coprime_1_left [simp]: 1250 "coprime 1 a" 1251 by (rule coprimeI) 1252 1253lemma coprime_1_right [simp]: 1254 "coprime a 1" 1255 by (rule coprimeI) 1256 1257lemma coprime_0_left_iff [simp]: 1258 "coprime 0 a \<longleftrightarrow> is_unit a" 1259 by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a]) 1260 1261lemma coprime_0_right_iff [simp]: 1262 "coprime a 0 \<longleftrightarrow> is_unit a" 1263 using coprime_0_left_iff [of a] by (simp add: ac_simps) 1264 1265lemma coprime_mult_self_left_iff [simp]: 1266 "coprime (c * a) (c * b) \<longleftrightarrow> is_unit c \<and> coprime a b" 1267 by (auto intro: coprime_common_divisor) 1268 (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+ 1269 1270lemma coprime_mult_self_right_iff [simp]: 1271 "coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b" 1272 using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps) 1273 1274lemma coprime_absorb_left: 1275 assumes "x dvd y" 1276 shows "coprime x y \<longleftrightarrow> is_unit x" 1277 using assms coprime_common_divisor is_unit_left_imp_coprime by auto 1278 1279lemma coprime_absorb_right: 1280 assumes "y dvd x" 1281 shows "coprime x y \<longleftrightarrow> is_unit y" 1282 using assms coprime_common_divisor is_unit_right_imp_coprime by auto 1283 1284end 1285 1286class unit_factor = 1287 fixes unit_factor :: "'a \<Rightarrow> 'a" 1288 1289class semidom_divide_unit_factor = semidom_divide + unit_factor + 1290 assumes unit_factor_0 [simp]: "unit_factor 0 = 0" 1291 and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a" 1292 and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1" 1293 and unit_factor_mult_unit_left: "a dvd 1 \<Longrightarrow> unit_factor (a * b) = a * unit_factor b" 1294 \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close> 1295begin 1296 1297lemma unit_factor_mult_unit_right: "a dvd 1 \<Longrightarrow> unit_factor (b * a) = unit_factor b * a" 1298 using unit_factor_mult_unit_left[of a b] by (simp add: mult_ac) 1299 1300lemmas [simp] = unit_factor_mult_unit_left unit_factor_mult_unit_right 1301 1302end 1303 1304class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor + 1305 fixes normalize :: "'a \<Rightarrow> 'a" 1306 assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a" 1307 and normalize_0 [simp]: "normalize 0 = 0" 1308begin 1309 1310text \<open> 1311 Class \<^class>\<open>normalization_semidom\<close> cultivates the idea that each integral 1312 domain can be split into equivalence classes whose representants are 1313 associated, i.e. divide each other. \<^const>\<open>normalize\<close> specifies a canonical 1314 representant for each equivalence class. The rationale behind this is that 1315 it is easier to reason about equality than equivalences, hence we prefer to 1316 think about equality of normalized values rather than associated elements. 1317\<close> 1318 1319declare unit_factor_is_unit [iff] 1320 1321lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b" 1322 by (rule unit_imp_dvd) simp 1323 1324lemma unit_factor_self [simp]: "unit_factor a dvd a" 1325 by (cases "a = 0") simp_all 1326 1327lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a" 1328 using unit_factor_mult_normalize [of a] by (simp add: ac_simps) 1329 1330lemma normalize_eq_0_iff [simp]: "normalize a = 0 \<longleftrightarrow> a = 0" 1331 (is "?lhs \<longleftrightarrow> ?rhs") 1332proof 1333 assume ?lhs 1334 moreover have "unit_factor a * normalize a = a" by simp 1335 ultimately show ?rhs by simp 1336next 1337 assume ?rhs 1338 then show ?lhs by simp 1339qed 1340 1341lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \<longleftrightarrow> a = 0" 1342 (is "?lhs \<longleftrightarrow> ?rhs") 1343proof 1344 assume ?lhs 1345 moreover have "unit_factor a * normalize a = a" by simp 1346 ultimately show ?rhs by simp 1347next 1348 assume ?rhs 1349 then show ?lhs by simp 1350qed 1351 1352lemma div_unit_factor [simp]: "a div unit_factor a = normalize a" 1353proof (cases "a = 0") 1354 case True 1355 then show ?thesis by simp 1356next 1357 case False 1358 then have "unit_factor a \<noteq> 0" 1359 by simp 1360 with nonzero_mult_div_cancel_left 1361 have "unit_factor a * normalize a div unit_factor a = normalize a" 1362 by blast 1363 then show ?thesis by simp 1364qed 1365 1366lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a" 1367proof (cases "a = 0") 1368 case True 1369 then show ?thesis by simp 1370next 1371 case False 1372 have "normalize a div a = normalize a div (unit_factor a * normalize a)" 1373 by simp 1374 also have "\<dots> = 1 div unit_factor a" 1375 using False by (subst is_unit_div_mult_cancel_right) simp_all 1376 finally show ?thesis . 1377qed 1378 1379lemma is_unit_normalize: 1380 assumes "is_unit a" 1381 shows "normalize a = 1" 1382proof - 1383 from assms have "unit_factor a = a" 1384 by (rule is_unit_unit_factor) 1385 moreover from assms have "a \<noteq> 0" 1386 by auto 1387 moreover have "normalize a = a div unit_factor a" 1388 by simp 1389 ultimately show ?thesis 1390 by simp 1391qed 1392 1393lemma unit_factor_1 [simp]: "unit_factor 1 = 1" 1394 by (rule is_unit_unit_factor) simp 1395 1396lemma normalize_1 [simp]: "normalize 1 = 1" 1397 by (rule is_unit_normalize) simp 1398 1399lemma normalize_1_iff: "normalize a = 1 \<longleftrightarrow> is_unit a" 1400 (is "?lhs \<longleftrightarrow> ?rhs") 1401proof 1402 assume ?rhs 1403 then show ?lhs by (rule is_unit_normalize) 1404next 1405 assume ?lhs 1406 then have "unit_factor a * normalize a = unit_factor a * 1" 1407 by simp 1408 then have "unit_factor a = a" 1409 by simp 1410 moreover 1411 from \<open>?lhs\<close> have "a \<noteq> 0" by auto 1412 then have "is_unit (unit_factor a)" by simp 1413 ultimately show ?rhs by simp 1414qed 1415 1416lemma div_normalize [simp]: "a div normalize a = unit_factor a" 1417proof (cases "a = 0") 1418 case True 1419 then show ?thesis by simp 1420next 1421 case False 1422 then have "normalize a \<noteq> 0" by simp 1423 with nonzero_mult_div_cancel_right 1424 have "unit_factor a * normalize a div normalize a = unit_factor a" by blast 1425 then show ?thesis by simp 1426qed 1427 1428lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b" 1429 by (cases "b = 0") simp_all 1430 1431lemma inv_unit_factor_eq_0_iff [simp]: 1432 "1 div unit_factor a = 0 \<longleftrightarrow> a = 0" 1433 (is "?lhs \<longleftrightarrow> ?rhs") 1434proof 1435 assume ?lhs 1436 then have "a * (1 div unit_factor a) = a * 0" 1437 by simp 1438 then show ?rhs 1439 by simp 1440next 1441 assume ?rhs 1442 then show ?lhs by simp 1443qed 1444 1445lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a" 1446 by (cases "a = 0") (auto intro: is_unit_unit_factor) 1447 1448lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1" 1449 by (rule is_unit_normalize) simp 1450 1451lemma normalize_mult_unit_left [simp]: 1452 assumes "a dvd 1" 1453 shows "normalize (a * b) = normalize b" 1454proof (cases "b = 0") 1455 case False 1456 have "a * unit_factor b * normalize (a * b) = unit_factor (a * b) * normalize (a * b)" 1457 using assms by (subst unit_factor_mult_unit_left) auto 1458 also have "\<dots> = a * b" by simp 1459 also have "b = unit_factor b * normalize b" by simp 1460 hence "a * b = a * unit_factor b * normalize b" 1461 by (simp only: mult_ac) 1462 finally show ?thesis 1463 using assms False by auto 1464qed auto 1465 1466lemma normalize_mult_unit_right [simp]: 1467 assumes "b dvd 1" 1468 shows "normalize (a * b) = normalize a" 1469 using assms by (subst mult.commute) auto 1470 1471lemma normalize_idem [simp]: "normalize (normalize a) = normalize a" 1472proof (cases "a = 0") 1473 case False 1474 have "normalize a = normalize (unit_factor a * normalize a)" 1475 by simp 1476 also from False have "\<dots> = normalize (normalize a)" 1477 by (subst normalize_mult_unit_left) auto 1478 finally show ?thesis .. 1479qed auto 1480 1481lemma unit_factor_normalize [simp]: 1482 assumes "a \<noteq> 0" 1483 shows "unit_factor (normalize a) = 1" 1484proof - 1485 from assms have *: "normalize a \<noteq> 0" 1486 by simp 1487 have "unit_factor (normalize a) * normalize (normalize a) = normalize a" 1488 by (simp only: unit_factor_mult_normalize) 1489 then have "unit_factor (normalize a) * normalize a = normalize a" 1490 by simp 1491 with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" 1492 by simp 1493 with * show ?thesis 1494 by simp 1495qed 1496 1497lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b" 1498proof - 1499 have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b" 1500 using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b] 1501 by (cases "a = 0") simp_all 1502 then show ?thesis by simp 1503qed 1504 1505lemma dvd_normalize_iff [simp]: "a dvd normalize b \<longleftrightarrow> a dvd b" 1506proof - 1507 have "a dvd normalize b \<longleftrightarrow> a dvd normalize b * unit_factor b" 1508 using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"] 1509 by (cases "b = 0") simp_all 1510 then show ?thesis by simp 1511qed 1512 1513lemma normalize_idem_imp_unit_factor_eq: 1514 assumes "normalize a = a" 1515 shows "unit_factor a = of_bool (a \<noteq> 0)" 1516proof (cases "a = 0") 1517 case True 1518 then show ?thesis 1519 by simp 1520next 1521 case False 1522 then show ?thesis 1523 using assms unit_factor_normalize [of a] by simp 1524qed 1525 1526lemma normalize_idem_imp_is_unit_iff: 1527 assumes "normalize a = a" 1528 shows "is_unit a \<longleftrightarrow> a = 1" 1529 using assms by (cases "a = 0") (auto dest: is_unit_normalize) 1530 1531lemma coprime_normalize_left_iff [simp]: 1532 "coprime (normalize a) b \<longleftrightarrow> coprime a b" 1533 by (rule; rule coprimeI) (auto intro: coprime_common_divisor) 1534 1535lemma coprime_normalize_right_iff [simp]: 1536 "coprime a (normalize b) \<longleftrightarrow> coprime a b" 1537 using coprime_normalize_left_iff [of b a] by (simp add: ac_simps) 1538 1539text \<open> 1540 We avoid an explicit definition of associated elements but prefer explicit 1541 normalisation instead. In theory we could define an abbreviation like \<^prop>\<open>associated a b \<longleftrightarrow> normalize a = normalize b\<close> but this is counterproductive 1542 without suggestive infix syntax, which we do not want to sacrifice for this 1543 purpose here. 1544\<close> 1545 1546lemma associatedI: 1547 assumes "a dvd b" and "b dvd a" 1548 shows "normalize a = normalize b" 1549proof (cases "a = 0 \<or> b = 0") 1550 case True 1551 with assms show ?thesis by auto 1552next 1553 case False 1554 from \<open>a dvd b\<close> obtain c where b: "b = a * c" .. 1555 moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" .. 1556 ultimately have "b * 1 = b * (c * d)" 1557 by (simp add: ac_simps) 1558 with False have "1 = c * d" 1559 unfolding mult_cancel_left by simp 1560 then have "is_unit c" and "is_unit d" 1561 by auto 1562 with a b show ?thesis 1563 by (simp add: is_unit_normalize) 1564qed 1565 1566lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b" 1567 using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric] 1568 by simp 1569 1570lemma associatedD2: "normalize a = normalize b \<Longrightarrow> b dvd a" 1571 using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric] 1572 by simp 1573 1574lemma associated_unit: "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b" 1575 using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2) 1576 1577lemma associated_iff_dvd: "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" 1578 (is "?lhs \<longleftrightarrow> ?rhs") 1579proof 1580 assume ?rhs 1581 then show ?lhs by (auto intro!: associatedI) 1582next 1583 assume ?lhs 1584 then have "unit_factor a * normalize a = unit_factor a * normalize b" 1585 by simp 1586 then have *: "normalize b * unit_factor a = a" 1587 by (simp add: ac_simps) 1588 show ?rhs 1589 proof (cases "a = 0 \<or> b = 0") 1590 case True 1591 with \<open>?lhs\<close> show ?thesis by auto 1592 next 1593 case False 1594 then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b" 1595 by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff) 1596 with * show ?thesis by simp 1597 qed 1598qed 1599 1600lemma associated_eqI: 1601 assumes "a dvd b" and "b dvd a" 1602 assumes "normalize a = a" and "normalize b = b" 1603 shows "a = b" 1604proof - 1605 from assms have "normalize a = normalize b" 1606 unfolding associated_iff_dvd by simp 1607 with \<open>normalize a = a\<close> have "a = normalize b" 1608 by simp 1609 with \<open>normalize b = b\<close> show "a = b" 1610 by simp 1611qed 1612 1613lemma normalize_unit_factor_eqI: 1614 assumes "normalize a = normalize b" 1615 and "unit_factor a = unit_factor b" 1616 shows "a = b" 1617proof - 1618 from assms have "unit_factor a * normalize a = unit_factor b * normalize b" 1619 by simp 1620 then show ?thesis 1621 by simp 1622qed 1623 1624lemma normalize_mult_normalize_left [simp]: "normalize (normalize a * b) = normalize (a * b)" 1625 by (rule associated_eqI) (auto intro!: mult_dvd_mono) 1626 1627lemma normalize_mult_normalize_right [simp]: "normalize (a * normalize b) = normalize (a * b)" 1628 by (rule associated_eqI) (auto intro!: mult_dvd_mono) 1629 1630end 1631 1632 1633class normalization_semidom_multiplicative = normalization_semidom + 1634 assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b" 1635begin 1636 1637lemma normalize_mult: "normalize (a * b) = normalize a * normalize b" 1638proof (cases "a = 0 \<or> b = 0") 1639 case True 1640 then show ?thesis by auto 1641next 1642 case False 1643 have "unit_factor (a * b) * normalize (a * b) = a * b" 1644 by (rule unit_factor_mult_normalize) 1645 then have "normalize (a * b) = a * b div unit_factor (a * b)" 1646 by simp 1647 also have "\<dots> = a * b div unit_factor (b * a)" 1648 by (simp add: ac_simps) 1649 also have "\<dots> = a * b div unit_factor b div unit_factor a" 1650 using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) 1651 also have "\<dots> = a * (b div unit_factor b) div unit_factor a" 1652 using False by (subst unit_div_mult_swap) simp_all 1653 also have "\<dots> = normalize a * normalize b" 1654 using False 1655 by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) 1656 finally show ?thesis . 1657qed 1658 1659lemma dvd_unit_factor_div: 1660 assumes "b dvd a" 1661 shows "unit_factor (a div b) = unit_factor a div unit_factor b" 1662proof - 1663 from assms have "a = a div b * b" 1664 by simp 1665 then have "unit_factor a = unit_factor (a div b * b)" 1666 by simp 1667 then show ?thesis 1668 by (cases "b = 0") (simp_all add: unit_factor_mult) 1669qed 1670 1671lemma dvd_normalize_div: 1672 assumes "b dvd a" 1673 shows "normalize (a div b) = normalize a div normalize b" 1674proof - 1675 from assms have "a = a div b * b" 1676 by simp 1677 then have "normalize a = normalize (a div b * b)" 1678 by simp 1679 then show ?thesis 1680 by (cases "b = 0") (simp_all add: normalize_mult) 1681qed 1682 1683end 1684 1685 1686 1687 1688text \<open>Syntactic division remainder operator\<close> 1689 1690class modulo = dvd + divide + 1691 fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70) 1692 1693text \<open>Arbitrary quotient and remainder partitions\<close> 1694 1695class semiring_modulo = comm_semiring_1_cancel + divide + modulo + 1696 assumes div_mult_mod_eq: "a div b * b + a mod b = a" 1697begin 1698 1699lemma mod_div_decomp: 1700 fixes a b 1701 obtains q r where "q = a div b" and "r = a mod b" 1702 and "a = q * b + r" 1703proof - 1704 from div_mult_mod_eq have "a = a div b * b + a mod b" by simp 1705 moreover have "a div b = a div b" .. 1706 moreover have "a mod b = a mod b" .. 1707 note that ultimately show thesis by blast 1708qed 1709 1710lemma mult_div_mod_eq: "b * (a div b) + a mod b = a" 1711 using div_mult_mod_eq [of a b] by (simp add: ac_simps) 1712 1713lemma mod_div_mult_eq: "a mod b + a div b * b = a" 1714 using div_mult_mod_eq [of a b] by (simp add: ac_simps) 1715 1716lemma mod_mult_div_eq: "a mod b + b * (a div b) = a" 1717 using div_mult_mod_eq [of a b] by (simp add: ac_simps) 1718 1719lemma minus_div_mult_eq_mod: "a - a div b * b = a mod b" 1720 by (rule add_implies_diff [symmetric]) (fact mod_div_mult_eq) 1721 1722lemma minus_mult_div_eq_mod: "a - b * (a div b) = a mod b" 1723 by (rule add_implies_diff [symmetric]) (fact mod_mult_div_eq) 1724 1725lemma minus_mod_eq_div_mult: "a - a mod b = a div b * b" 1726 by (rule add_implies_diff [symmetric]) (fact div_mult_mod_eq) 1727 1728lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)" 1729 by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq) 1730 1731lemma mod_0_imp_dvd [dest!]: 1732 "b dvd a" if "a mod b = 0" 1733proof - 1734 have "b dvd (a div b) * b" by simp 1735 also have "(a div b) * b = a" 1736 using div_mult_mod_eq [of a b] by (simp add: that) 1737 finally show ?thesis . 1738qed 1739 1740lemma [nitpick_unfold]: 1741 "a mod b = a - a div b * b" 1742 by (fact minus_div_mult_eq_mod [symmetric]) 1743 1744end 1745 1746 1747subsection \<open>Quotient and remainder in integral domains\<close> 1748 1749class semidom_modulo = algebraic_semidom + semiring_modulo 1750begin 1751 1752lemma mod_0 [simp]: "0 mod a = 0" 1753 using div_mult_mod_eq [of 0 a] by simp 1754 1755lemma mod_by_0 [simp]: "a mod 0 = a" 1756 using div_mult_mod_eq [of a 0] by simp 1757 1758lemma mod_by_1 [simp]: 1759 "a mod 1 = 0" 1760proof - 1761 from div_mult_mod_eq [of a one] div_by_1 have "a + a mod 1 = a" by simp 1762 then have "a + a mod 1 = a + 0" by simp 1763 then show ?thesis by (rule add_left_imp_eq) 1764qed 1765 1766lemma mod_self [simp]: 1767 "a mod a = 0" 1768 using div_mult_mod_eq [of a a] by simp 1769 1770lemma dvd_imp_mod_0 [simp]: 1771 "b mod a = 0" if "a dvd b" 1772 using that minus_div_mult_eq_mod [of b a] by simp 1773 1774lemma mod_eq_0_iff_dvd: 1775 "a mod b = 0 \<longleftrightarrow> b dvd a" 1776 by (auto intro: mod_0_imp_dvd) 1777 1778lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]: 1779 "a dvd b \<longleftrightarrow> b mod a = 0" 1780 by (simp add: mod_eq_0_iff_dvd) 1781 1782lemma dvd_mod_iff: 1783 assumes "c dvd b" 1784 shows "c dvd a mod b \<longleftrightarrow> c dvd a" 1785proof - 1786 from assms have "(c dvd a mod b) \<longleftrightarrow> (c dvd ((a div b) * b + a mod b))" 1787 by (simp add: dvd_add_right_iff) 1788 also have "(a div b) * b + a mod b = a" 1789 using div_mult_mod_eq [of a b] by simp 1790 finally show ?thesis . 1791qed 1792 1793lemma dvd_mod_imp_dvd: 1794 assumes "c dvd a mod b" and "c dvd b" 1795 shows "c dvd a" 1796 using assms dvd_mod_iff [of c b a] by simp 1797 1798lemma dvd_minus_mod [simp]: 1799 "b dvd a - a mod b" 1800 by (simp add: minus_mod_eq_div_mult) 1801 1802lemma cancel_div_mod_rules: 1803 "((a div b) * b + a mod b) + c = a + c" 1804 "(b * (a div b) + a mod b) + c = a + c" 1805 by (simp_all add: div_mult_mod_eq mult_div_mod_eq) 1806 1807end 1808 1809class idom_modulo = idom + semidom_modulo 1810begin 1811 1812subclass idom_divide .. 1813 1814lemma div_diff [simp]: 1815 "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> (a - b) div c = a div c - b div c" 1816 using div_add [of _ _ "- b"] by (simp add: dvd_neg_div) 1817 1818end 1819 1820 1821subsection \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close> 1822 1823named_theorems arith "arith facts -- only ground formulas" 1824ML_file \<open>Tools/arith_data.ML\<close> 1825 1826ML_file \<open>~~/src/Provers/Arith/cancel_div_mod.ML\<close> 1827 1828ML \<open> 1829structure Cancel_Div_Mod_Ring = Cancel_Div_Mod 1830( 1831 val div_name = \<^const_name>\<open>divide\<close>; 1832 val mod_name = \<^const_name>\<open>modulo\<close>; 1833 val mk_binop = HOLogic.mk_binop; 1834 val mk_sum = Arith_Data.mk_sum; 1835 val dest_sum = Arith_Data.dest_sum; 1836 1837 val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules}; 1838 1839 val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 1840 @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps}) 1841) 1842\<close> 1843 1844simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") = 1845 \<open>K Cancel_Div_Mod_Ring.proc\<close> 1846 1847 1848subsection \<open>Ordered semirings and rings\<close> 1849 1850text \<open> 1851 The theory of partially ordered rings is taken from the books: 1852 \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979 1853 \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963 1854 1855 Most of the used notions can also be looked up in 1856 \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al. 1857 \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer 1858\<close> 1859 1860class ordered_semiring = semiring + ordered_comm_monoid_add + 1861 assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 1862 assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c" 1863begin 1864 1865lemma mult_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d" 1866 apply (erule (1) mult_right_mono [THEN order_trans]) 1867 apply (erule (1) mult_left_mono) 1868 done 1869 1870lemma mult_mono': "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d" 1871 by (rule mult_mono) (fast intro: order_trans)+ 1872 1873end 1874 1875class ordered_semiring_0 = semiring_0 + ordered_semiring 1876begin 1877 1878lemma mult_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b" 1879 using mult_left_mono [of 0 b a] by simp 1880 1881lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0" 1882 using mult_left_mono [of b 0 a] by simp 1883 1884lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0" 1885 using mult_right_mono [of a 0 b] by simp 1886 1887text \<open>Legacy -- use @{thm [source] mult_nonpos_nonneg}.\<close> 1888lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0" 1889 by (drule mult_right_mono [of b 0]) auto 1890 1891lemma split_mult_neg_le: "(0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b) \<Longrightarrow> a * b \<le> 0" 1892 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) 1893 1894end 1895 1896class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add 1897begin 1898 1899subclass semiring_0_cancel .. 1900 1901subclass ordered_semiring_0 .. 1902 1903end 1904 1905class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add 1906begin 1907 1908subclass ordered_cancel_semiring .. 1909 1910subclass ordered_cancel_comm_monoid_add .. 1911 1912subclass ordered_ab_semigroup_monoid_add_imp_le .. 1913 1914lemma mult_left_less_imp_less: "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 1915 by (force simp add: mult_left_mono not_le [symmetric]) 1916 1917lemma mult_right_less_imp_less: "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b" 1918 by (force simp add: mult_right_mono not_le [symmetric]) 1919 1920end 1921 1922class zero_less_one = order + zero + one + 1923 assumes zero_less_one [simp]: "0 < 1" 1924 1925class linordered_semiring_1 = linordered_semiring + semiring_1 + zero_less_one 1926begin 1927 1928lemma convex_bound_le: 1929 assumes "x \<le> a" "y \<le> a" "0 \<le> u" "0 \<le> v" "u + v = 1" 1930 shows "u * x + v * y \<le> a" 1931proof- 1932 from assms have "u * x + v * y \<le> u * a + v * a" 1933 by (simp add: add_mono mult_left_mono) 1934 with assms show ?thesis 1935 unfolding distrib_right[symmetric] by simp 1936qed 1937 1938end 1939 1940class linordered_semiring_strict = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + 1941 assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 1942 assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c" 1943begin 1944 1945subclass semiring_0_cancel .. 1946 1947subclass linordered_semiring 1948proof 1949 fix a b c :: 'a 1950 assume *: "a \<le> b" "0 \<le> c" 1951 then show "c * a \<le> c * b" 1952 unfolding le_less 1953 using mult_strict_left_mono by (cases "c = 0") auto 1954 from * show "a * c \<le> b * c" 1955 unfolding le_less 1956 using mult_strict_right_mono by (cases "c = 0") auto 1957qed 1958 1959lemma mult_left_le_imp_le: "c * a \<le> c * b \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 1960 by (auto simp add: mult_strict_left_mono _not_less [symmetric]) 1961 1962lemma mult_right_le_imp_le: "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b" 1963 by (auto simp add: mult_strict_right_mono not_less [symmetric]) 1964 1965lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b" 1966 using mult_strict_left_mono [of 0 b a] by simp 1967 1968lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0" 1969 using mult_strict_left_mono [of b 0 a] by simp 1970 1971lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0" 1972 using mult_strict_right_mono [of a 0 b] by simp 1973 1974text \<open>Legacy -- use @{thm [source] mult_neg_pos}.\<close> 1975lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0" 1976 by (drule mult_strict_right_mono [of b 0]) auto 1977 1978lemma zero_less_mult_pos: "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b" 1979 apply (cases "b \<le> 0") 1980 apply (auto simp add: le_less not_less) 1981 apply (drule_tac mult_pos_neg [of a b]) 1982 apply (auto dest: less_not_sym) 1983 done 1984 1985lemma zero_less_mult_pos2: "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b" 1986 apply (cases "b \<le> 0") 1987 apply (auto simp add: le_less not_less) 1988 apply (drule_tac mult_pos_neg2 [of a b]) 1989 apply (auto dest: less_not_sym) 1990 done 1991 1992text \<open>Strict monotonicity in both arguments\<close> 1993lemma mult_strict_mono: 1994 assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c" 1995 shows "a * c < b * d" 1996 using assms 1997 apply (cases "c = 0") 1998 apply simp 1999 apply (erule mult_strict_right_mono [THEN less_trans]) 2000 apply (auto simp add: le_less) 2001 apply (erule (1) mult_strict_left_mono) 2002 done 2003 2004text \<open>This weaker variant has more natural premises\<close> 2005lemma mult_strict_mono': 2006 assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c" 2007 shows "a * c < b * d" 2008 by (rule mult_strict_mono) (insert assms, auto) 2009 2010lemma mult_less_le_imp_less: 2011 assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c" 2012 shows "a * c < b * d" 2013 using assms 2014 apply (subgoal_tac "a * c < b * c") 2015 apply (erule less_le_trans) 2016 apply (erule mult_left_mono) 2017 apply simp 2018 apply (erule (1) mult_strict_right_mono) 2019 done 2020 2021lemma mult_le_less_imp_less: 2022 assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c" 2023 shows "a * c < b * d" 2024 using assms 2025 apply (subgoal_tac "a * c \<le> b * c") 2026 apply (erule le_less_trans) 2027 apply (erule mult_strict_left_mono) 2028 apply simp 2029 apply (erule (1) mult_right_mono) 2030 done 2031 2032end 2033 2034class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1 + zero_less_one 2035begin 2036 2037subclass linordered_semiring_1 .. 2038 2039lemma convex_bound_lt: 2040 assumes "x < a" "y < a" "0 \<le> u" "0 \<le> v" "u + v = 1" 2041 shows "u * x + v * y < a" 2042proof - 2043 from assms have "u * x + v * y < u * a + v * a" 2044 by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono) 2045 with assms show ?thesis 2046 unfolding distrib_right[symmetric] by simp 2047qed 2048 2049end 2050 2051class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 2052 assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b" 2053begin 2054 2055subclass ordered_semiring 2056proof 2057 fix a b c :: 'a 2058 assume "a \<le> b" "0 \<le> c" 2059 then show "c * a \<le> c * b" by (rule comm_mult_left_mono) 2060 then show "a * c \<le> b * c" by (simp only: mult.commute) 2061qed 2062 2063end 2064 2065class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add 2066begin 2067 2068subclass comm_semiring_0_cancel .. 2069subclass ordered_comm_semiring .. 2070subclass ordered_cancel_semiring .. 2071 2072end 2073 2074class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add + 2075 assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 2076begin 2077 2078subclass linordered_semiring_strict 2079proof 2080 fix a b c :: 'a 2081 assume "a < b" "0 < c" 2082 then show "c * a < c * b" 2083 by (rule comm_mult_strict_left_mono) 2084 then show "a * c < b * c" 2085 by (simp only: mult.commute) 2086qed 2087 2088subclass ordered_cancel_comm_semiring 2089proof 2090 fix a b c :: 'a 2091 assume "a \<le> b" "0 \<le> c" 2092 then show "c * a \<le> c * b" 2093 unfolding le_less 2094 using mult_strict_left_mono by (cases "c = 0") auto 2095qed 2096 2097end 2098 2099class ordered_ring = ring + ordered_cancel_semiring 2100begin 2101 2102subclass ordered_ab_group_add .. 2103 2104lemma less_add_iff1: "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d" 2105 by (simp add: algebra_simps) 2106 2107lemma less_add_iff2: "a * e + c < b * e + d \<longleftrightarrow> c < (b - a) * e + d" 2108 by (simp add: algebra_simps) 2109 2110lemma le_add_iff1: "a * e + c \<le> b * e + d \<longleftrightarrow> (a - b) * e + c \<le> d" 2111 by (simp add: algebra_simps) 2112 2113lemma le_add_iff2: "a * e + c \<le> b * e + d \<longleftrightarrow> c \<le> (b - a) * e + d" 2114 by (simp add: algebra_simps) 2115 2116lemma mult_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b" 2117 apply (drule mult_left_mono [of _ _ "- c"]) 2118 apply simp_all 2119 done 2120 2121lemma mult_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c" 2122 apply (drule mult_right_mono [of _ _ "- c"]) 2123 apply simp_all 2124 done 2125 2126lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b" 2127 using mult_right_mono_neg [of a 0 b] by simp 2128 2129lemma split_mult_pos_le: "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b" 2130 by (auto simp add: mult_nonpos_nonpos) 2131 2132end 2133 2134class abs_if = minus + uminus + ord + zero + abs + 2135 assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)" 2136 2137class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if 2138begin 2139 2140subclass ordered_ring .. 2141 2142subclass ordered_ab_group_add_abs 2143proof 2144 fix a b 2145 show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 2146 by (auto simp add: abs_if not_le not_less algebra_simps 2147 simp del: add.commute dest: add_neg_neg add_nonneg_nonneg) 2148qed (auto simp: abs_if) 2149 2150lemma zero_le_square [simp]: "0 \<le> a * a" 2151 using linear [of 0 a] by (auto simp add: mult_nonpos_nonpos) 2152 2153lemma not_square_less_zero [simp]: "\<not> (a * a < 0)" 2154 by (simp add: not_less) 2155 2156proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y" 2157 by (auto simp add: abs_if split: if_split_asm) 2158 2159lemma abs_eq_iff': 2160 "\<bar>a\<bar> = b \<longleftrightarrow> b \<ge> 0 \<and> (a = b \<or> a = - b)" 2161 by (cases "a \<ge> 0") auto 2162 2163lemma eq_abs_iff': 2164 "a = \<bar>b\<bar> \<longleftrightarrow> a \<ge> 0 \<and> (b = a \<or> b = - a)" 2165 using abs_eq_iff' [of b a] by auto 2166 2167lemma sum_squares_ge_zero: "0 \<le> x * x + y * y" 2168 by (intro add_nonneg_nonneg zero_le_square) 2169 2170lemma not_sum_squares_lt_zero: "\<not> x * x + y * y < 0" 2171 by (simp add: not_less sum_squares_ge_zero) 2172 2173end 2174 2175class linordered_ring_strict = ring + linordered_semiring_strict 2176 + ordered_ab_group_add + abs_if 2177begin 2178 2179subclass linordered_ring .. 2180 2181lemma mult_strict_left_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b" 2182 using mult_strict_left_mono [of b a "- c"] by simp 2183 2184lemma mult_strict_right_mono_neg: "b < a \<Longrightarrow> c < 0 \<Longrightarrow> a * c < b * c" 2185 using mult_strict_right_mono [of b a "- c"] by simp 2186 2187lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b" 2188 using mult_strict_right_mono_neg [of a 0 b] by simp 2189 2190subclass ring_no_zero_divisors 2191proof 2192 fix a b 2193 assume "a \<noteq> 0" 2194 then have a: "a < 0 \<or> 0 < a" by (simp add: neq_iff) 2195 assume "b \<noteq> 0" 2196 then have b: "b < 0 \<or> 0 < b" by (simp add: neq_iff) 2197 have "a * b < 0 \<or> 0 < a * b" 2198 proof (cases "a < 0") 2199 case True 2200 show ?thesis 2201 proof (cases "b < 0") 2202 case True 2203 with \<open>a < 0\<close> show ?thesis by (auto dest: mult_neg_neg) 2204 next 2205 case False 2206 with b have "0 < b" by auto 2207 with \<open>a < 0\<close> show ?thesis by (auto dest: mult_strict_right_mono) 2208 qed 2209 next 2210 case False 2211 with a have "0 < a" by auto 2212 show ?thesis 2213 proof (cases "b < 0") 2214 case True 2215 with \<open>0 < a\<close> show ?thesis 2216 by (auto dest: mult_strict_right_mono_neg) 2217 next 2218 case False 2219 with b have "0 < b" by auto 2220 with \<open>0 < a\<close> show ?thesis by auto 2221 qed 2222 qed 2223 then show "a * b \<noteq> 0" 2224 by (simp add: neq_iff) 2225qed 2226 2227lemma zero_less_mult_iff [algebra_split_simps, field_split_simps]: 2228 "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 2229 by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) 2230 (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2) 2231 2232lemma zero_le_mult_iff [algebra_split_simps, field_split_simps]: 2233 "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 2234 by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) 2235 2236lemma mult_less_0_iff [algebra_split_simps, field_split_simps]: 2237 "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 2238 using zero_less_mult_iff [of "- a" b] by auto 2239 2240lemma mult_le_0_iff [algebra_split_simps, field_split_simps]: 2241 "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b" 2242 using zero_le_mult_iff [of "- a" b] by auto 2243 2244text \<open> 2245 Cancellation laws for \<^term>\<open>c * a < c * b\<close> and \<^term>\<open>a * c < b * c\<close>, 2246 also with the relations \<open>\<le>\<close> and equality. 2247\<close> 2248 2249text \<open> 2250 These ``disjunction'' versions produce two cases when the comparison is 2251 an assumption, but effectively four when the comparison is a goal. 2252\<close> 2253 2254lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a" 2255 apply (cases "c = 0") 2256 apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg) 2257 apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a]) 2258 apply (erule_tac [!] notE) 2259 apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg) 2260 done 2261 2262lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a" 2263 apply (cases "c = 0") 2264 apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg) 2265 apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a]) 2266 apply (erule_tac [!] notE) 2267 apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg) 2268 done 2269 2270text \<open> 2271 The ``conjunction of implication'' lemmas produce two cases when the 2272 comparison is a goal, but give four when the comparison is an assumption. 2273\<close> 2274 2275lemma mult_less_cancel_right: "a * c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)" 2276 using mult_less_cancel_right_disj [of a c b] by auto 2277 2278lemma mult_less_cancel_left: "c * a < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < b) \<and> (c \<le> 0 \<longrightarrow> b < a)" 2279 using mult_less_cancel_left_disj [of c a b] by auto 2280 2281lemma mult_le_cancel_right: "a * c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 2282 by (simp add: not_less [symmetric] mult_less_cancel_right_disj) 2283 2284lemma mult_le_cancel_left: "c * a \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 2285 by (simp add: not_less [symmetric] mult_less_cancel_left_disj) 2286 2287lemma mult_le_cancel_left_pos: "0 < c \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> a \<le> b" 2288 by (auto simp: mult_le_cancel_left) 2289 2290lemma mult_le_cancel_left_neg: "c < 0 \<Longrightarrow> c * a \<le> c * b \<longleftrightarrow> b \<le> a" 2291 by (auto simp: mult_le_cancel_left) 2292 2293lemma mult_less_cancel_left_pos: "0 < c \<Longrightarrow> c * a < c * b \<longleftrightarrow> a < b" 2294 by (auto simp: mult_less_cancel_left) 2295 2296lemma mult_less_cancel_left_neg: "c < 0 \<Longrightarrow> c * a < c * b \<longleftrightarrow> b < a" 2297 by (auto simp: mult_less_cancel_left) 2298 2299end 2300 2301lemmas mult_sign_intros = 2302 mult_nonneg_nonneg mult_nonneg_nonpos 2303 mult_nonpos_nonneg mult_nonpos_nonpos 2304 mult_pos_pos mult_pos_neg 2305 mult_neg_pos mult_neg_neg 2306 2307class ordered_comm_ring = comm_ring + ordered_comm_semiring 2308begin 2309 2310subclass ordered_ring .. 2311subclass ordered_cancel_comm_semiring .. 2312 2313end 2314 2315class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one + 2316 assumes add_mono1: "a < b \<Longrightarrow> a + 1 < b + 1" 2317begin 2318 2319subclass zero_neq_one 2320 by standard (insert zero_less_one, blast) 2321 2322subclass comm_semiring_1 2323 by standard (rule mult_1_left) 2324 2325lemma zero_le_one [simp]: "0 \<le> 1" 2326 by (rule zero_less_one [THEN less_imp_le]) 2327 2328lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0" 2329 by (simp add: not_le) 2330 2331lemma not_one_less_zero [simp]: "\<not> 1 < 0" 2332 by (simp add: not_less) 2333 2334lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a" 2335 using mult_left_mono[of c 1 a] by simp 2336 2337lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1" 2338 using mult_mono[of a 1 b 1] by simp 2339 2340lemma zero_less_two: "0 < 1 + 1" 2341 using add_pos_pos[OF zero_less_one zero_less_one] . 2342 2343end 2344 2345class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one + 2346 assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a" 2347begin 2348 2349subclass linordered_nonzero_semiring 2350proof 2351 show "a + 1 < b + 1" if "a < b" for a b 2352 proof (rule ccontr, simp add: not_less) 2353 assume "b \<le> a" 2354 with that show False 2355 by (simp add: ) 2356 qed 2357qed 2358 2359text \<open>Addition is the inverse of subtraction.\<close> 2360 2361lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a" 2362 by (frule le_add_diff_inverse2) (simp add: add.commute) 2363 2364lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a" 2365 by simp 2366 2367lemma add_le_imp_le_diff: "i + k \<le> n \<Longrightarrow> i \<le> n - k" 2368 apply (subst add_le_cancel_right [where c=k, symmetric]) 2369 apply (frule le_add_diff_inverse2) 2370 apply (simp only: add.assoc [symmetric]) 2371 using add_implies_diff 2372 apply fastforce 2373 done 2374 2375lemma add_le_add_imp_diff_le: 2376 assumes 1: "i + k \<le> n" 2377 and 2: "n \<le> j + k" 2378 shows "i + k \<le> n \<Longrightarrow> n \<le> j + k \<Longrightarrow> n - k \<le> j" 2379proof - 2380 have "n - (i + k) + (i + k) = n" 2381 using 1 by simp 2382 moreover have "n - k = n - k - i + i" 2383 using 1 by (simp add: add_le_imp_le_diff) 2384 ultimately show ?thesis 2385 using 2 2386 apply (simp add: add.assoc [symmetric]) 2387 apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right']) 2388 apply (simp add: add.commute diff_diff_add) 2389 done 2390qed 2391 2392lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n" 2393 using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one]) 2394 2395end 2396 2397class linordered_idom = comm_ring_1 + linordered_comm_semiring_strict + 2398 ordered_ab_group_add + abs_if + sgn + 2399 assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" 2400begin 2401 2402subclass linordered_ring_strict .. 2403 2404subclass linordered_semiring_1_strict 2405proof 2406 have "0 \<le> 1 * 1" 2407 by (fact zero_le_square) 2408 then show "0 < 1" 2409 by (simp add: le_less) 2410qed 2411 2412subclass ordered_comm_ring .. 2413subclass idom .. 2414 2415subclass linordered_semidom 2416 by standard simp 2417 2418subclass idom_abs_sgn 2419 by standard 2420 (auto simp add: sgn_if abs_if zero_less_mult_iff) 2421 2422lemma linorder_neqE_linordered_idom: 2423 assumes "x \<noteq> y" 2424 obtains "x < y" | "y < x" 2425 using assms by (rule neqE) 2426 2427text \<open>These cancellation simp rules also produce two cases when the comparison is a goal.\<close> 2428 2429lemma mult_le_cancel_right1: "c \<le> b * c \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)" 2430 using mult_le_cancel_right [of 1 c b] by simp 2431 2432lemma mult_le_cancel_right2: "a * c \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)" 2433 using mult_le_cancel_right [of a c 1] by simp 2434 2435lemma mult_le_cancel_left1: "c \<le> c * b \<longleftrightarrow> (0 < c \<longrightarrow> 1 \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> 1)" 2436 using mult_le_cancel_left [of c 1 b] by simp 2437 2438lemma mult_le_cancel_left2: "c * a \<le> c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> 1) \<and> (c < 0 \<longrightarrow> 1 \<le> a)" 2439 using mult_le_cancel_left [of c a 1] by simp 2440 2441lemma mult_less_cancel_right1: "c < b * c \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)" 2442 using mult_less_cancel_right [of 1 c b] by simp 2443 2444lemma mult_less_cancel_right2: "a * c < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)" 2445 using mult_less_cancel_right [of a c 1] by simp 2446 2447lemma mult_less_cancel_left1: "c < c * b \<longleftrightarrow> (0 \<le> c \<longrightarrow> 1 < b) \<and> (c \<le> 0 \<longrightarrow> b < 1)" 2448 using mult_less_cancel_left [of c 1 b] by simp 2449 2450lemma mult_less_cancel_left2: "c * a < c \<longleftrightarrow> (0 \<le> c \<longrightarrow> a < 1) \<and> (c \<le> 0 \<longrightarrow> 1 < a)" 2451 using mult_less_cancel_left [of c a 1] by simp 2452 2453lemma sgn_0_0: "sgn a = 0 \<longleftrightarrow> a = 0" 2454 by (fact sgn_eq_0_iff) 2455 2456lemma sgn_1_pos: "sgn a = 1 \<longleftrightarrow> a > 0" 2457 unfolding sgn_if by simp 2458 2459lemma sgn_1_neg: "sgn a = - 1 \<longleftrightarrow> a < 0" 2460 unfolding sgn_if by auto 2461 2462lemma sgn_pos [simp]: "0 < a \<Longrightarrow> sgn a = 1" 2463 by (simp only: sgn_1_pos) 2464 2465lemma sgn_neg [simp]: "a < 0 \<Longrightarrow> sgn a = - 1" 2466 by (simp only: sgn_1_neg) 2467 2468lemma abs_sgn: "\<bar>k\<bar> = k * sgn k" 2469 unfolding sgn_if abs_if by auto 2470 2471lemma sgn_greater [simp]: "0 < sgn a \<longleftrightarrow> 0 < a" 2472 unfolding sgn_if by auto 2473 2474lemma sgn_less [simp]: "sgn a < 0 \<longleftrightarrow> a < 0" 2475 unfolding sgn_if by auto 2476 2477lemma abs_sgn_eq_1 [simp]: 2478 "a \<noteq> 0 \<Longrightarrow> \<bar>sgn a\<bar> = 1" 2479 by simp 2480 2481lemma abs_sgn_eq: "\<bar>sgn a\<bar> = (if a = 0 then 0 else 1)" 2482 by (simp add: sgn_if) 2483 2484lemma sgn_mult_self_eq [simp]: 2485 "sgn a * sgn a = of_bool (a \<noteq> 0)" 2486 by (cases "a > 0") simp_all 2487 2488lemma abs_mult_self_eq [simp]: 2489 "\<bar>a\<bar> * \<bar>a\<bar> = a * a" 2490 by (cases "a > 0") simp_all 2491 2492lemma same_sgn_sgn_add: 2493 "sgn (a + b) = sgn a" if "sgn b = sgn a" 2494proof (cases a 0 rule: linorder_cases) 2495 case equal 2496 with that show ?thesis 2497 by simp 2498next 2499 case less 2500 with that have "b < 0" 2501 by (simp add: sgn_1_neg) 2502 with \<open>a < 0\<close> have "a + b < 0" 2503 by (rule add_neg_neg) 2504 with \<open>a < 0\<close> show ?thesis 2505 by simp 2506next 2507 case greater 2508 with that have "b > 0" 2509 by (simp add: sgn_1_pos) 2510 with \<open>a > 0\<close> have "a + b > 0" 2511 by (rule add_pos_pos) 2512 with \<open>a > 0\<close> show ?thesis 2513 by simp 2514qed 2515 2516lemma same_sgn_abs_add: 2517 "\<bar>a + b\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" if "sgn b = sgn a" 2518proof - 2519 have "a + b = sgn a * \<bar>a\<bar> + sgn b * \<bar>b\<bar>" 2520 by (simp add: sgn_mult_abs) 2521 also have "\<dots> = sgn a * (\<bar>a\<bar> + \<bar>b\<bar>)" 2522 using that by (simp add: algebra_simps) 2523 finally show ?thesis 2524 by (auto simp add: abs_mult) 2525qed 2526 2527lemma sgn_not_eq_imp: 2528 "sgn a = - sgn b" if "sgn b \<noteq> sgn a" and "sgn a \<noteq> 0" and "sgn b \<noteq> 0" 2529 using that by (cases "a < 0") (auto simp add: sgn_0_0 sgn_1_pos sgn_1_neg) 2530 2531lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k" 2532 by (simp add: abs_if) 2533 2534lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k" 2535 by (simp add: abs_if) 2536 2537lemma dvd_if_abs_eq: "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k" 2538 by (subst abs_dvd_iff [symmetric]) simp 2539 2540text \<open> 2541 The following lemmas can be proven in more general structures, but 2542 are dangerous as simp rules in absence of @{thm neg_equal_zero}, 2543 @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. 2544\<close> 2545 2546lemma equation_minus_iff_1 [simp, no_atp]: "1 = - a \<longleftrightarrow> a = - 1" 2547 by (fact equation_minus_iff) 2548 2549lemma minus_equation_iff_1 [simp, no_atp]: "- a = 1 \<longleftrightarrow> a = - 1" 2550 by (subst minus_equation_iff, auto) 2551 2552lemma le_minus_iff_1 [simp, no_atp]: "1 \<le> - b \<longleftrightarrow> b \<le> - 1" 2553 by (fact le_minus_iff) 2554 2555lemma minus_le_iff_1 [simp, no_atp]: "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a" 2556 by (fact minus_le_iff) 2557 2558lemma less_minus_iff_1 [simp, no_atp]: "1 < - b \<longleftrightarrow> b < - 1" 2559 by (fact less_minus_iff) 2560 2561lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \<longleftrightarrow> - 1 < a" 2562 by (fact minus_less_iff) 2563 2564lemma add_less_zeroD: 2565 shows "x+y < 0 \<Longrightarrow> x<0 \<or> y<0" 2566 by (auto simp: not_less intro: le_less_trans [of _ "x+y"]) 2567 2568end 2569 2570text \<open>Reasoning about inequalities with division\<close> 2571 2572context linordered_semidom 2573begin 2574 2575lemma less_add_one: "a < a + 1" 2576proof - 2577 have "a + 0 < a + 1" 2578 by (blast intro: zero_less_one add_strict_left_mono) 2579 then show ?thesis by simp 2580qed 2581 2582end 2583 2584context linordered_idom 2585begin 2586 2587lemma mult_right_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x" 2588 by (rule mult_left_le) 2589 2590lemma mult_left_le_one_le: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x" 2591 by (auto simp add: mult_le_cancel_right2) 2592 2593end 2594 2595text \<open>Absolute Value\<close> 2596 2597context linordered_idom 2598begin 2599 2600lemma mult_sgn_abs: "sgn x * \<bar>x\<bar> = x" 2601 by (fact sgn_mult_abs) 2602 2603lemma abs_one: "\<bar>1\<bar> = 1" 2604 by (fact abs_1) 2605 2606end 2607 2608class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs + 2609 assumes abs_eq_mult: 2610 "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 2611 2612context linordered_idom 2613begin 2614 2615subclass ordered_ring_abs 2616 by standard (auto simp: abs_if not_less mult_less_0_iff) 2617 2618lemma abs_mult_self: "\<bar>a\<bar> * \<bar>a\<bar> = a * a" 2619 by (fact abs_mult_self_eq) 2620 2621lemma abs_mult_less: 2622 assumes ac: "\<bar>a\<bar> < c" 2623 and bd: "\<bar>b\<bar> < d" 2624 shows "\<bar>a\<bar> * \<bar>b\<bar> < c * d" 2625proof - 2626 from ac have "0 < c" 2627 by (blast intro: le_less_trans abs_ge_zero) 2628 with bd show ?thesis by (simp add: ac mult_strict_mono) 2629qed 2630 2631lemma abs_less_iff: "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 2632 by (simp add: less_le abs_le_iff) (auto simp add: abs_if) 2633 2634lemma abs_mult_pos: "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>" 2635 by (simp add: abs_mult) 2636 2637lemma abs_diff_less_iff: "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r" 2638 by (auto simp add: diff_less_eq ac_simps abs_less_iff) 2639 2640lemma abs_diff_le_iff: "\<bar>x - a\<bar> \<le> r \<longleftrightarrow> a - r \<le> x \<and> x \<le> a + r" 2641 by (auto simp add: diff_le_eq ac_simps abs_le_iff) 2642 2643lemma abs_add_one_gt_zero: "0 < 1 + \<bar>x\<bar>" 2644 by (auto simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans) 2645 2646end 2647 2648 2649subsection \<open>Dioids\<close> 2650 2651text \<open> 2652 Dioids are the alternative extensions of semirings, a semiring can 2653 either be a ring or a dioid but never both. 2654\<close> 2655 2656class dioid = semiring_1 + canonically_ordered_monoid_add 2657begin 2658 2659subclass ordered_semiring 2660 by standard (auto simp: le_iff_add distrib_left distrib_right) 2661 2662end 2663 2664 2665hide_fact (open) comm_mult_left_mono comm_mult_strict_left_mono distrib 2666 2667code_identifier 2668 code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 2669 2670end 2671