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