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