1(* Title: HOL/Fields.thy 2 Author: Gertrud Bauer 3 Author: Steven Obua 4 Author: Tobias Nipkow 5 Author: Lawrence C Paulson 6 Author: Markus Wenzel 7 Author: Jeremy Avigad 8*) 9 10section \<open>Fields\<close> 11 12theory Fields 13imports Nat 14begin 15 16subsection \<open>Division rings\<close> 17 18text \<open> 19 A division ring is like a field, but without the commutativity requirement. 20\<close> 21 22class inverse = divide + 23 fixes inverse :: "'a \<Rightarrow> 'a" 24begin 25 26abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70) 27where 28 "inverse_divide \<equiv> divide" 29 30end 31 32text \<open>Setup for linear arithmetic prover\<close> 33 34ML_file "~~/src/Provers/Arith/fast_lin_arith.ML" 35ML_file "Tools/lin_arith.ML" 36setup \<open>Lin_Arith.global_setup\<close> 37declaration \<open>K Lin_Arith.setup\<close> 38 39simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") = 40 \<open>K Lin_Arith.simproc\<close> 41(* Because of this simproc, the arithmetic solver is really only 42useful to detect inconsistencies among the premises for subgoals which are 43*not* themselves (in)equalities, because the latter activate 44fast_nat_arith_simproc anyway. However, it seems cheaper to activate the 45solver all the time rather than add the additional check. *) 46 47lemmas [arith_split] = nat_diff_split split_min split_max 48 49context linordered_nonzero_semiring 50begin 51lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)" 52 by (auto simp: max_def) 53 54lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)" 55 by (auto simp: min_def) 56end 57 58text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close> 59 60named_theorems divide_simps "rewrite rules to eliminate divisions" 61 62class division_ring = ring_1 + inverse + 63 assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 64 assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1" 65 assumes divide_inverse: "a / b = a * inverse b" 66 assumes inverse_zero [simp]: "inverse 0 = 0" 67begin 68 69subclass ring_1_no_zero_divisors 70proof 71 fix a b :: 'a 72 assume a: "a \<noteq> 0" and b: "b \<noteq> 0" 73 show "a * b \<noteq> 0" 74 proof 75 assume ab: "a * b = 0" 76 hence "0 = inverse a * (a * b) * inverse b" by simp 77 also have "\<dots> = (inverse a * a) * (b * inverse b)" 78 by (simp only: mult.assoc) 79 also have "\<dots> = 1" using a b by simp 80 finally show False by simp 81 qed 82qed 83 84lemma nonzero_imp_inverse_nonzero: 85 "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0" 86proof 87 assume ianz: "inverse a = 0" 88 assume "a \<noteq> 0" 89 hence "1 = a * inverse a" by simp 90 also have "... = 0" by (simp add: ianz) 91 finally have "1 = 0" . 92 thus False by (simp add: eq_commute) 93qed 94 95lemma inverse_zero_imp_zero: 96 "inverse a = 0 \<Longrightarrow> a = 0" 97apply (rule classical) 98apply (drule nonzero_imp_inverse_nonzero) 99apply auto 100done 101 102lemma inverse_unique: 103 assumes ab: "a * b = 1" 104 shows "inverse a = b" 105proof - 106 have "a \<noteq> 0" using ab by (cases "a = 0") simp_all 107 moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 108 ultimately show ?thesis by (simp add: mult.assoc [symmetric]) 109qed 110 111lemma nonzero_inverse_minus_eq: 112 "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a" 113by (rule inverse_unique) simp 114 115lemma nonzero_inverse_inverse_eq: 116 "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a" 117by (rule inverse_unique) simp 118 119lemma nonzero_inverse_eq_imp_eq: 120 assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0" 121 shows "a = b" 122proof - 123 from \<open>inverse a = inverse b\<close> 124 have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) 125 with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> show "a = b" 126 by (simp add: nonzero_inverse_inverse_eq) 127qed 128 129lemma inverse_1 [simp]: "inverse 1 = 1" 130by (rule inverse_unique) simp 131 132lemma nonzero_inverse_mult_distrib: 133 assumes "a \<noteq> 0" and "b \<noteq> 0" 134 shows "inverse (a * b) = inverse b * inverse a" 135proof - 136 have "a * (b * inverse b) * inverse a = 1" using assms by simp 137 hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult.assoc) 138 thus ?thesis by (rule inverse_unique) 139qed 140 141lemma division_ring_inverse_add: 142 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b" 143by (simp add: algebra_simps) 144 145lemma division_ring_inverse_diff: 146 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b" 147by (simp add: algebra_simps) 148 149lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b" 150proof 151 assume neq: "b \<noteq> 0" 152 { 153 hence "a = (a / b) * b" by (simp add: divide_inverse mult.assoc) 154 also assume "a / b = 1" 155 finally show "a = b" by simp 156 next 157 assume "a = b" 158 with neq show "a / b = 1" by (simp add: divide_inverse) 159 } 160qed 161 162lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a" 163by (simp add: divide_inverse) 164 165lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1" 166by (simp add: divide_inverse) 167 168lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a" 169by (simp add: divide_inverse) 170 171lemma add_divide_distrib: "(a+b) / c = a/c + b/c" 172by (simp add: divide_inverse algebra_simps) 173 174lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c" 175 by (simp add: divide_inverse mult.assoc) 176 177lemma minus_divide_left: "- (a / b) = (-a) / b" 178 by (simp add: divide_inverse) 179 180lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)" 181 by (simp add: divide_inverse nonzero_inverse_minus_eq) 182 183lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b" 184 by (simp add: divide_inverse nonzero_inverse_minus_eq) 185 186lemma divide_minus_left [simp]: "(-a) / b = - (a / b)" 187 by (simp add: divide_inverse) 188 189lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" 190 using add_divide_distrib [of a "- b" c] by simp 191 192lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b" 193proof - 194 assume [simp]: "c \<noteq> 0" 195 have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp 196 also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult.assoc) 197 finally show ?thesis . 198qed 199 200lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c" 201proof - 202 assume [simp]: "c \<noteq> 0" 203 have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp 204 also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult.assoc) 205 finally show ?thesis . 206qed 207 208lemma nonzero_neg_divide_eq_eq [field_simps]: "b \<noteq> 0 \<Longrightarrow> - (a / b) = c \<longleftrightarrow> - a = c * b" 209 using nonzero_divide_eq_eq[of b "-a" c] by simp 210 211lemma nonzero_neg_divide_eq_eq2 [field_simps]: "b \<noteq> 0 \<Longrightarrow> c = - (a / b) \<longleftrightarrow> c * b = - a" 212 using nonzero_neg_divide_eq_eq[of b a c] by auto 213 214lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a" 215 by (simp add: divide_inverse mult.assoc) 216 217lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c" 218 by (drule sym) (simp add: divide_inverse mult.assoc) 219 220lemma add_divide_eq_iff [field_simps]: 221 "z \<noteq> 0 \<Longrightarrow> x + y / z = (x * z + y) / z" 222 by (simp add: add_divide_distrib nonzero_eq_divide_eq) 223 224lemma divide_add_eq_iff [field_simps]: 225 "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + y * z) / z" 226 by (simp add: add_divide_distrib nonzero_eq_divide_eq) 227 228lemma diff_divide_eq_iff [field_simps]: 229 "z \<noteq> 0 \<Longrightarrow> x - y / z = (x * z - y) / z" 230 by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq) 231 232lemma minus_divide_add_eq_iff [field_simps]: 233 "z \<noteq> 0 \<Longrightarrow> - (x / z) + y = (- x + y * z) / z" 234 by (simp add: add_divide_distrib diff_divide_eq_iff) 235 236lemma divide_diff_eq_iff [field_simps]: 237 "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z" 238 by (simp add: field_simps) 239 240lemma minus_divide_diff_eq_iff [field_simps]: 241 "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z" 242 by (simp add: divide_diff_eq_iff[symmetric]) 243 244lemma division_ring_divide_zero [simp]: 245 "a / 0 = 0" 246 by (simp add: divide_inverse) 247 248lemma divide_self_if [simp]: 249 "a / a = (if a = 0 then 0 else 1)" 250 by simp 251 252lemma inverse_nonzero_iff_nonzero [simp]: 253 "inverse a = 0 \<longleftrightarrow> a = 0" 254 by rule (fact inverse_zero_imp_zero, simp) 255 256lemma inverse_minus_eq [simp]: 257 "inverse (- a) = - inverse a" 258proof cases 259 assume "a=0" thus ?thesis by simp 260next 261 assume "a\<noteq>0" 262 thus ?thesis by (simp add: nonzero_inverse_minus_eq) 263qed 264 265lemma inverse_inverse_eq [simp]: 266 "inverse (inverse a) = a" 267proof cases 268 assume "a=0" thus ?thesis by simp 269next 270 assume "a\<noteq>0" 271 thus ?thesis by (simp add: nonzero_inverse_inverse_eq) 272qed 273 274lemma inverse_eq_imp_eq: 275 "inverse a = inverse b \<Longrightarrow> a = b" 276 by (drule arg_cong [where f="inverse"], simp) 277 278lemma inverse_eq_iff_eq [simp]: 279 "inverse a = inverse b \<longleftrightarrow> a = b" 280 by (force dest!: inverse_eq_imp_eq) 281 282lemma add_divide_eq_if_simps [divide_simps]: 283 "a + b / z = (if z = 0 then a else (a * z + b) / z)" 284 "a / z + b = (if z = 0 then b else (a + b * z) / z)" 285 "- (a / z) + b = (if z = 0 then b else (-a + b * z) / z)" 286 "a - b / z = (if z = 0 then a else (a * z - b) / z)" 287 "a / z - b = (if z = 0 then -b else (a - b * z) / z)" 288 "- (a / z) - b = (if z = 0 then -b else (- a - b * z) / z)" 289 by (simp_all add: add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff 290 minus_divide_diff_eq_iff) 291 292lemma [divide_simps]: 293 shows divide_eq_eq: "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)" 294 and eq_divide_eq: "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)" 295 and minus_divide_eq_eq: "- (b / c) = a \<longleftrightarrow> (if c \<noteq> 0 then - b = a * c else a = 0)" 296 and eq_minus_divide_eq: "a = - (b / c) \<longleftrightarrow> (if c \<noteq> 0 then a * c = - b else a = 0)" 297 by (auto simp add: field_simps) 298 299end 300 301subsection \<open>Fields\<close> 302 303class field = comm_ring_1 + inverse + 304 assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 305 assumes field_divide_inverse: "a / b = a * inverse b" 306 assumes field_inverse_zero: "inverse 0 = 0" 307begin 308 309subclass division_ring 310proof 311 fix a :: 'a 312 assume "a \<noteq> 0" 313 thus "inverse a * a = 1" by (rule field_inverse) 314 thus "a * inverse a = 1" by (simp only: mult.commute) 315next 316 fix a b :: 'a 317 show "a / b = a * inverse b" by (rule field_divide_inverse) 318next 319 show "inverse 0 = 0" 320 by (fact field_inverse_zero) 321qed 322 323subclass idom_divide 324proof 325 fix b a 326 assume "b \<noteq> 0" 327 then show "a * b / b = a" 328 by (simp add: divide_inverse ac_simps) 329next 330 fix a 331 show "a / 0 = 0" 332 by (simp add: divide_inverse) 333qed 334 335text\<open>There is no slick version using division by zero.\<close> 336lemma inverse_add: 337 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b" 338 by (simp add: division_ring_inverse_add ac_simps) 339 340lemma nonzero_mult_divide_mult_cancel_left [simp]: 341 assumes [simp]: "c \<noteq> 0" 342 shows "(c * a) / (c * b) = a / b" 343proof (cases "b = 0") 344 case True then show ?thesis by simp 345next 346 case False 347 then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" 348 by (simp add: divide_inverse nonzero_inverse_mult_distrib) 349 also have "... = a * inverse b * (inverse c * c)" 350 by (simp only: ac_simps) 351 also have "... = a * inverse b" by simp 352 finally show ?thesis by (simp add: divide_inverse) 353qed 354 355lemma nonzero_mult_divide_mult_cancel_right [simp]: 356 "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b" 357 using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps) 358 359lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c" 360 by (simp add: divide_inverse ac_simps) 361 362lemma divide_inverse_commute: "a / b = inverse b * a" 363 by (simp add: divide_inverse mult.commute) 364 365lemma add_frac_eq: 366 assumes "y \<noteq> 0" and "z \<noteq> 0" 367 shows "x / y + w / z = (x * z + w * y) / (y * z)" 368proof - 369 have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)" 370 using assms by simp 371 also have "\<dots> = (x * z + y * w) / (y * z)" 372 by (simp only: add_divide_distrib) 373 finally show ?thesis 374 by (simp only: mult.commute) 375qed 376 377text\<open>Special Cancellation Simprules for Division\<close> 378 379lemma nonzero_divide_mult_cancel_right [simp]: 380 "b \<noteq> 0 \<Longrightarrow> b / (a * b) = 1 / a" 381 using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp 382 383lemma nonzero_divide_mult_cancel_left [simp]: 384 "a \<noteq> 0 \<Longrightarrow> a / (a * b) = 1 / b" 385 using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp 386 387lemma nonzero_mult_divide_mult_cancel_left2 [simp]: 388 "c \<noteq> 0 \<Longrightarrow> (c * a) / (b * c) = a / b" 389 using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps) 390 391lemma nonzero_mult_divide_mult_cancel_right2 [simp]: 392 "c \<noteq> 0 \<Longrightarrow> (a * c) / (c * b) = a / b" 393 using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps) 394 395lemma diff_frac_eq: 396 "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)" 397 by (simp add: field_simps) 398 399lemma frac_eq_eq: 400 "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)" 401 by (simp add: field_simps) 402 403lemma divide_minus1 [simp]: "x / - 1 = - x" 404 using nonzero_minus_divide_right [of "1" x] by simp 405 406text\<open>This version builds in division by zero while also re-orienting 407 the right-hand side.\<close> 408lemma inverse_mult_distrib [simp]: 409 "inverse (a * b) = inverse a * inverse b" 410proof cases 411 assume "a \<noteq> 0 \<and> b \<noteq> 0" 412 thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps) 413next 414 assume "\<not> (a \<noteq> 0 \<and> b \<noteq> 0)" 415 thus ?thesis by force 416qed 417 418lemma inverse_divide [simp]: 419 "inverse (a / b) = b / a" 420 by (simp add: divide_inverse mult.commute) 421 422 423text \<open>Calculations with fractions\<close> 424 425text\<open>There is a whole bunch of simp-rules just for class \<open>field\<close> but none for class \<open>field\<close> and \<open>nonzero_divides\<close> 426because the latter are covered by a simproc.\<close> 427 428lemmas mult_divide_mult_cancel_left = nonzero_mult_divide_mult_cancel_left 429 430lemmas mult_divide_mult_cancel_right = nonzero_mult_divide_mult_cancel_right 431 432lemma divide_divide_eq_right [simp]: 433 "a / (b / c) = (a * c) / b" 434 by (simp add: divide_inverse ac_simps) 435 436lemma divide_divide_eq_left [simp]: 437 "(a / b) / c = a / (b * c)" 438 by (simp add: divide_inverse mult.assoc) 439 440lemma divide_divide_times_eq: 441 "(x / y) / (z / w) = (x * w) / (y * z)" 442 by simp 443 444text \<open>Special Cancellation Simprules for Division\<close> 445 446lemma mult_divide_mult_cancel_left_if [simp]: 447 shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)" 448 by simp 449 450 451text \<open>Division and Unary Minus\<close> 452 453lemma minus_divide_right: 454 "- (a / b) = a / - b" 455 by (simp add: divide_inverse) 456 457lemma divide_minus_right [simp]: 458 "a / - b = - (a / b)" 459 by (simp add: divide_inverse) 460 461lemma minus_divide_divide: 462 "(- a) / (- b) = a / b" 463 by (cases "b=0") (simp_all add: nonzero_minus_divide_divide) 464 465lemma inverse_eq_1_iff [simp]: 466 "inverse x = 1 \<longleftrightarrow> x = 1" 467 by (insert inverse_eq_iff_eq [of x 1], simp) 468 469lemma divide_eq_0_iff [simp]: 470 "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 471 by (simp add: divide_inverse) 472 473lemma divide_cancel_right [simp]: 474 "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b" 475 by (cases "c=0") (simp_all add: divide_inverse) 476 477lemma divide_cancel_left [simp]: 478 "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b" 479 by (cases "c=0") (simp_all add: divide_inverse) 480 481lemma divide_eq_1_iff [simp]: 482 "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b" 483 by (cases "b=0") (simp_all add: right_inverse_eq) 484 485lemma one_eq_divide_iff [simp]: 486 "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b" 487 by (simp add: eq_commute [of 1]) 488 489lemma divide_eq_minus_1_iff: 490 "(a / b = - 1) \<longleftrightarrow> b \<noteq> 0 \<and> a = - b" 491using divide_eq_1_iff by fastforce 492 493lemma times_divide_times_eq: 494 "(x / y) * (z / w) = (x * z) / (y * w)" 495 by simp 496 497lemma add_frac_num: 498 "y \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y" 499 by (simp add: add_divide_distrib) 500 501lemma add_num_frac: 502 "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y" 503 by (simp add: add_divide_distrib add.commute) 504 505lemma dvd_field_iff: 506 "a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)" 507proof (cases "a = 0") 508 case False 509 then have "b = a * (b / a)" 510 by (simp add: field_simps) 511 then have "a dvd b" .. 512 with False show ?thesis 513 by simp 514qed simp 515 516end 517 518class field_char_0 = field + ring_char_0 519 520 521subsection \<open>Ordered fields\<close> 522 523class field_abs_sgn = field + idom_abs_sgn 524begin 525 526lemma sgn_inverse [simp]: 527 "sgn (inverse a) = inverse (sgn a)" 528proof (cases "a = 0") 529 case True then show ?thesis by simp 530next 531 case False 532 then have "a * inverse a = 1" 533 by simp 534 then have "sgn (a * inverse a) = sgn 1" 535 by simp 536 then have "sgn a * sgn (inverse a) = 1" 537 by (simp add: sgn_mult) 538 then have "inverse (sgn a) * (sgn a * sgn (inverse a)) = inverse (sgn a) * 1" 539 by simp 540 then have "(inverse (sgn a) * sgn a) * sgn (inverse a) = inverse (sgn a)" 541 by (simp add: ac_simps) 542 with False show ?thesis 543 by (simp add: sgn_eq_0_iff) 544qed 545 546lemma abs_inverse [simp]: 547 "\<bar>inverse a\<bar> = inverse \<bar>a\<bar>" 548proof - 549 from sgn_mult_abs [of "inverse a"] sgn_mult_abs [of a] 550 have "inverse (sgn a) * \<bar>inverse a\<bar> = inverse (sgn a * \<bar>a\<bar>)" 551 by simp 552 then show ?thesis by (auto simp add: sgn_eq_0_iff) 553qed 554 555lemma sgn_divide [simp]: 556 "sgn (a / b) = sgn a / sgn b" 557 unfolding divide_inverse sgn_mult by simp 558 559lemma abs_divide [simp]: 560 "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>" 561 unfolding divide_inverse abs_mult by simp 562 563end 564 565class linordered_field = field + linordered_idom 566begin 567 568lemma positive_imp_inverse_positive: 569 assumes a_gt_0: "0 < a" 570 shows "0 < inverse a" 571proof - 572 have "0 < a * inverse a" 573 by (simp add: a_gt_0 [THEN less_imp_not_eq2]) 574 thus "0 < inverse a" 575 by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff) 576qed 577 578lemma negative_imp_inverse_negative: 579 "a < 0 \<Longrightarrow> inverse a < 0" 580 by (insert positive_imp_inverse_positive [of "-a"], 581 simp add: nonzero_inverse_minus_eq less_imp_not_eq) 582 583lemma inverse_le_imp_le: 584 assumes invle: "inverse a \<le> inverse b" and apos: "0 < a" 585 shows "b \<le> a" 586proof (rule classical) 587 assume "\<not> b \<le> a" 588 hence "a < b" by (simp add: linorder_not_le) 589 hence bpos: "0 < b" by (blast intro: apos less_trans) 590 hence "a * inverse a \<le> a * inverse b" 591 by (simp add: apos invle less_imp_le mult_left_mono) 592 hence "(a * inverse a) * b \<le> (a * inverse b) * b" 593 by (simp add: bpos less_imp_le mult_right_mono) 594 thus "b \<le> a" by (simp add: mult.assoc apos bpos less_imp_not_eq2) 595qed 596 597lemma inverse_positive_imp_positive: 598 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0" 599 shows "0 < a" 600proof - 601 have "0 < inverse (inverse a)" 602 using inv_gt_0 by (rule positive_imp_inverse_positive) 603 thus "0 < a" 604 using nz by (simp add: nonzero_inverse_inverse_eq) 605qed 606 607lemma inverse_negative_imp_negative: 608 assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0" 609 shows "a < 0" 610proof - 611 have "inverse (inverse a) < 0" 612 using inv_less_0 by (rule negative_imp_inverse_negative) 613 thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq) 614qed 615 616lemma linordered_field_no_lb: 617 "\<forall>x. \<exists>y. y < x" 618proof 619 fix x::'a 620 have m1: "- (1::'a) < 0" by simp 621 from add_strict_right_mono[OF m1, where c=x] 622 have "(- 1) + x < x" by simp 623 thus "\<exists>y. y < x" by blast 624qed 625 626lemma linordered_field_no_ub: 627 "\<forall> x. \<exists>y. y > x" 628proof 629 fix x::'a 630 have m1: " (1::'a) > 0" by simp 631 from add_strict_right_mono[OF m1, where c=x] 632 have "1 + x > x" by simp 633 thus "\<exists>y. y > x" by blast 634qed 635 636lemma less_imp_inverse_less: 637 assumes less: "a < b" and apos: "0 < a" 638 shows "inverse b < inverse a" 639proof (rule ccontr) 640 assume "\<not> inverse b < inverse a" 641 hence "inverse a \<le> inverse b" by simp 642 hence "\<not> (a < b)" 643 by (simp add: not_less inverse_le_imp_le [OF _ apos]) 644 thus False by (rule notE [OF _ less]) 645qed 646 647lemma inverse_less_imp_less: 648 "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a" 649apply (simp add: less_le [of "inverse a"] less_le [of "b"]) 650apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 651done 652 653text\<open>Both premises are essential. Consider -1 and 1.\<close> 654lemma inverse_less_iff_less [simp]: 655 "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a" 656 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 657 658lemma le_imp_inverse_le: 659 "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a" 660 by (force simp add: le_less less_imp_inverse_less) 661 662lemma inverse_le_iff_le [simp]: 663 "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a" 664 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 665 666 667text\<open>These results refer to both operands being negative. The opposite-sign 668case is trivial, since inverse preserves signs.\<close> 669lemma inverse_le_imp_le_neg: 670 "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a" 671apply (rule classical) 672apply (subgoal_tac "a < 0") 673 prefer 2 apply force 674apply (insert inverse_le_imp_le [of "-b" "-a"]) 675apply (simp add: nonzero_inverse_minus_eq) 676done 677 678lemma less_imp_inverse_less_neg: 679 "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a" 680apply (subgoal_tac "a < 0") 681 prefer 2 apply (blast intro: less_trans) 682apply (insert less_imp_inverse_less [of "-b" "-a"]) 683apply (simp add: nonzero_inverse_minus_eq) 684done 685 686lemma inverse_less_imp_less_neg: 687 "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a" 688apply (rule classical) 689apply (subgoal_tac "a < 0") 690 prefer 2 691 apply force 692apply (insert inverse_less_imp_less [of "-b" "-a"]) 693apply (simp add: nonzero_inverse_minus_eq) 694done 695 696lemma inverse_less_iff_less_neg [simp]: 697 "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a" 698apply (insert inverse_less_iff_less [of "-b" "-a"]) 699apply (simp del: inverse_less_iff_less 700 add: nonzero_inverse_minus_eq) 701done 702 703lemma le_imp_inverse_le_neg: 704 "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a" 705 by (force simp add: le_less less_imp_inverse_less_neg) 706 707lemma inverse_le_iff_le_neg [simp]: 708 "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a" 709 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 710 711lemma one_less_inverse: 712 "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a" 713 using less_imp_inverse_less [of a 1, unfolded inverse_1] . 714 715lemma one_le_inverse: 716 "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a" 717 using le_imp_inverse_le [of a 1, unfolded inverse_1] . 718 719lemma pos_le_divide_eq [field_simps]: 720 assumes "0 < c" 721 shows "a \<le> b / c \<longleftrightarrow> a * c \<le> b" 722proof - 723 from assms have "a \<le> b / c \<longleftrightarrow> a * c \<le> (b / c) * c" 724 using mult_le_cancel_right [of a c "b * inverse c"] by (auto simp add: field_simps) 725 also have "... \<longleftrightarrow> a * c \<le> b" 726 by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 727 finally show ?thesis . 728qed 729 730lemma pos_less_divide_eq [field_simps]: 731 assumes "0 < c" 732 shows "a < b / c \<longleftrightarrow> a * c < b" 733proof - 734 from assms have "a < b / c \<longleftrightarrow> a * c < (b / c) * c" 735 using mult_less_cancel_right [of a c "b / c"] by auto 736 also have "... = (a*c < b)" 737 by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 738 finally show ?thesis . 739qed 740 741lemma neg_less_divide_eq [field_simps]: 742 assumes "c < 0" 743 shows "a < b / c \<longleftrightarrow> b < a * c" 744proof - 745 from assms have "a < b / c \<longleftrightarrow> (b / c) * c < a * c" 746 using mult_less_cancel_right [of "b / c" c a] by auto 747 also have "... \<longleftrightarrow> b < a * c" 748 by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 749 finally show ?thesis . 750qed 751 752lemma neg_le_divide_eq [field_simps]: 753 assumes "c < 0" 754 shows "a \<le> b / c \<longleftrightarrow> b \<le> a * c" 755proof - 756 from assms have "a \<le> b / c \<longleftrightarrow> (b / c) * c \<le> a * c" 757 using mult_le_cancel_right [of "b * inverse c" c a] by (auto simp add: field_simps) 758 also have "... \<longleftrightarrow> b \<le> a * c" 759 by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 760 finally show ?thesis . 761qed 762 763lemma pos_divide_le_eq [field_simps]: 764 assumes "0 < c" 765 shows "b / c \<le> a \<longleftrightarrow> b \<le> a * c" 766proof - 767 from assms have "b / c \<le> a \<longleftrightarrow> (b / c) * c \<le> a * c" 768 using mult_le_cancel_right [of "b / c" c a] by auto 769 also have "... \<longleftrightarrow> b \<le> a * c" 770 by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 771 finally show ?thesis . 772qed 773 774lemma pos_divide_less_eq [field_simps]: 775 assumes "0 < c" 776 shows "b / c < a \<longleftrightarrow> b < a * c" 777proof - 778 from assms have "b / c < a \<longleftrightarrow> (b / c) * c < a * c" 779 using mult_less_cancel_right [of "b / c" c a] by auto 780 also have "... \<longleftrightarrow> b < a * c" 781 by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 782 finally show ?thesis . 783qed 784 785lemma neg_divide_le_eq [field_simps]: 786 assumes "c < 0" 787 shows "b / c \<le> a \<longleftrightarrow> a * c \<le> b" 788proof - 789 from assms have "b / c \<le> a \<longleftrightarrow> a * c \<le> (b / c) * c" 790 using mult_le_cancel_right [of a c "b / c"] by auto 791 also have "... \<longleftrightarrow> a * c \<le> b" 792 by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 793 finally show ?thesis . 794qed 795 796lemma neg_divide_less_eq [field_simps]: 797 assumes "c < 0" 798 shows "b / c < a \<longleftrightarrow> a * c < b" 799proof - 800 from assms have "b / c < a \<longleftrightarrow> a * c < b / c * c" 801 using mult_less_cancel_right [of a c "b / c"] by auto 802 also have "... \<longleftrightarrow> a * c < b" 803 by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 804 finally show ?thesis . 805qed 806 807text\<open>The following \<open>field_simps\<close> rules are necessary, as minus is always moved atop of 808division but we want to get rid of division.\<close> 809 810lemma pos_le_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> a * c \<le> - b" 811 unfolding minus_divide_left by (rule pos_le_divide_eq) 812 813lemma neg_le_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> - b \<le> a * c" 814 unfolding minus_divide_left by (rule neg_le_divide_eq) 815 816lemma pos_less_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < - (b / c) \<longleftrightarrow> a * c < - b" 817 unfolding minus_divide_left by (rule pos_less_divide_eq) 818 819lemma neg_less_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < - (b / c) \<longleftrightarrow> - b < a * c" 820 unfolding minus_divide_left by (rule neg_less_divide_eq) 821 822lemma pos_minus_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) < a \<longleftrightarrow> - b < a * c" 823 unfolding minus_divide_left by (rule pos_divide_less_eq) 824 825lemma neg_minus_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) < a \<longleftrightarrow> a * c < - b" 826 unfolding minus_divide_left by (rule neg_divide_less_eq) 827 828lemma pos_minus_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> - b \<le> a * c" 829 unfolding minus_divide_left by (rule pos_divide_le_eq) 830 831lemma neg_minus_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> a * c \<le> - b" 832 unfolding minus_divide_left by (rule neg_divide_le_eq) 833 834lemma frac_less_eq: 835 "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z - w * y) / (y * z) < 0" 836 by (subst less_iff_diff_less_0) (simp add: diff_frac_eq ) 837 838lemma frac_le_eq: 839 "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0" 840 by (subst le_iff_diff_le_0) (simp add: diff_frac_eq ) 841 842text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs 843of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case 844explosions.\<close> 845 846(* Only works once linear arithmetic is installed: 847text{*An example:*} 848lemma fixes a b c d e f :: "'a::linordered_field" 849shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow> 850 ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < 851 ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u" 852apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0") 853 prefer 2 apply(simp add:sign_simps) 854apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0") 855 prefer 2 apply(simp add:sign_simps) 856apply(simp add:field_simps) 857done 858*) 859 860lemma divide_pos_pos[simp]: 861 "0 < x ==> 0 < y ==> 0 < x / y" 862by(simp add:field_simps) 863 864lemma divide_nonneg_pos: 865 "0 <= x ==> 0 < y ==> 0 <= x / y" 866by(simp add:field_simps) 867 868lemma divide_neg_pos: 869 "x < 0 ==> 0 < y ==> x / y < 0" 870by(simp add:field_simps) 871 872lemma divide_nonpos_pos: 873 "x <= 0 ==> 0 < y ==> x / y <= 0" 874by(simp add:field_simps) 875 876lemma divide_pos_neg: 877 "0 < x ==> y < 0 ==> x / y < 0" 878by(simp add:field_simps) 879 880lemma divide_nonneg_neg: 881 "0 <= x ==> y < 0 ==> x / y <= 0" 882by(simp add:field_simps) 883 884lemma divide_neg_neg: 885 "x < 0 ==> y < 0 ==> 0 < x / y" 886by(simp add:field_simps) 887 888lemma divide_nonpos_neg: 889 "x <= 0 ==> y < 0 ==> 0 <= x / y" 890by(simp add:field_simps) 891 892lemma divide_strict_right_mono: 893 "[|a < b; 0 < c|] ==> a / c < b / c" 894by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono 895 positive_imp_inverse_positive) 896 897 898lemma divide_strict_right_mono_neg: 899 "[|b < a; c < 0|] ==> a / c < b / c" 900apply (drule divide_strict_right_mono [of _ _ "-c"], simp) 901apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric]) 902done 903 904text\<open>The last premise ensures that @{term a} and @{term b} 905 have the same sign\<close> 906lemma divide_strict_left_mono: 907 "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b" 908 by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono) 909 910lemma divide_left_mono: 911 "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b" 912 by (auto simp: field_simps zero_less_mult_iff mult_right_mono) 913 914lemma divide_strict_left_mono_neg: 915 "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b" 916 by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg) 917 918lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==> 919 x / y <= z" 920by (subst pos_divide_le_eq, assumption+) 921 922lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==> 923 z <= x / y" 924by(simp add:field_simps) 925 926lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==> 927 x / y < z" 928by(simp add:field_simps) 929 930lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==> 931 z < x / y" 932by(simp add:field_simps) 933 934lemma frac_le: "0 <= x ==> 935 x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" 936 apply (rule mult_imp_div_pos_le) 937 apply simp 938 apply (subst times_divide_eq_left) 939 apply (rule mult_imp_le_div_pos, assumption) 940 apply (rule mult_mono) 941 apply simp_all 942done 943 944lemma frac_less: "0 <= x ==> 945 x < y ==> 0 < w ==> w <= z ==> x / z < y / w" 946 apply (rule mult_imp_div_pos_less) 947 apply simp 948 apply (subst times_divide_eq_left) 949 apply (rule mult_imp_less_div_pos, assumption) 950 apply (erule mult_less_le_imp_less) 951 apply simp_all 952done 953 954lemma frac_less2: "0 < x ==> 955 x <= y ==> 0 < w ==> w < z ==> x / z < y / w" 956 apply (rule mult_imp_div_pos_less) 957 apply simp_all 958 apply (rule mult_imp_less_div_pos, assumption) 959 apply (erule mult_le_less_imp_less) 960 apply simp_all 961done 962 963lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)" 964by (simp add: field_simps zero_less_two) 965 966lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b" 967by (simp add: field_simps zero_less_two) 968 969subclass unbounded_dense_linorder 970proof 971 fix x y :: 'a 972 from less_add_one show "\<exists>y. x < y" .. 973 from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono) 974 then have "x - 1 < x + 1 - 1" by simp 975 then have "x - 1 < x" by (simp add: algebra_simps) 976 then show "\<exists>y. y < x" .. 977 show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum) 978qed 979 980subclass field_abs_sgn .. 981 982lemma inverse_sgn [simp]: 983 "inverse (sgn a) = sgn a" 984 by (cases a 0 rule: linorder_cases) simp_all 985 986lemma divide_sgn [simp]: 987 "a / sgn b = a * sgn b" 988 by (cases b 0 rule: linorder_cases) simp_all 989 990lemma nonzero_abs_inverse: 991 "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>" 992 by (rule abs_inverse) 993 994lemma nonzero_abs_divide: 995 "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>" 996 by (rule abs_divide) 997 998lemma field_le_epsilon: 999 assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e" 1000 shows "x \<le> y" 1001proof (rule dense_le) 1002 fix t assume "t < x" 1003 hence "0 < x - t" by (simp add: less_diff_eq) 1004 from e [OF this] have "x + 0 \<le> x + (y - t)" by (simp add: algebra_simps) 1005 then have "0 \<le> y - t" by (simp only: add_le_cancel_left) 1006 then show "t \<le> y" by (simp add: algebra_simps) 1007qed 1008 1009lemma inverse_positive_iff_positive [simp]: 1010 "(0 < inverse a) = (0 < a)" 1011apply (cases "a = 0", simp) 1012apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) 1013done 1014 1015lemma inverse_negative_iff_negative [simp]: 1016 "(inverse a < 0) = (a < 0)" 1017apply (cases "a = 0", simp) 1018apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative) 1019done 1020 1021lemma inverse_nonnegative_iff_nonnegative [simp]: 1022 "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a" 1023 by (simp add: not_less [symmetric]) 1024 1025lemma inverse_nonpositive_iff_nonpositive [simp]: 1026 "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0" 1027 by (simp add: not_less [symmetric]) 1028 1029lemma one_less_inverse_iff: "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1" 1030 using less_trans[of 1 x 0 for x] 1031 by (cases x 0 rule: linorder_cases) (auto simp add: field_simps) 1032 1033lemma one_le_inverse_iff: "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1" 1034proof (cases "x = 1") 1035 case True then show ?thesis by simp 1036next 1037 case False then have "inverse x \<noteq> 1" by simp 1038 then have "1 \<noteq> inverse x" by blast 1039 then have "1 \<le> inverse x \<longleftrightarrow> 1 < inverse x" by (simp add: le_less) 1040 with False show ?thesis by (auto simp add: one_less_inverse_iff) 1041qed 1042 1043lemma inverse_less_1_iff: "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x" 1044 by (simp add: not_le [symmetric] one_le_inverse_iff) 1045 1046lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x" 1047 by (simp add: not_less [symmetric] one_less_inverse_iff) 1048 1049lemma [divide_simps]: 1050 shows le_divide_eq: "a \<le> b / c \<longleftrightarrow> (if 0 < c then a * c \<le> b else if c < 0 then b \<le> a * c else a \<le> 0)" 1051 and divide_le_eq: "b / c \<le> a \<longleftrightarrow> (if 0 < c then b \<le> a * c else if c < 0 then a * c \<le> b else 0 \<le> a)" 1052 and less_divide_eq: "a < b / c \<longleftrightarrow> (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)" 1053 and divide_less_eq: "b / c < a \<longleftrightarrow> (if 0 < c then b < a * c else if c < 0 then a * c < b else 0 < a)" 1054 and le_minus_divide_eq: "a \<le> - (b / c) \<longleftrightarrow> (if 0 < c then a * c \<le> - b else if c < 0 then - b \<le> a * c else a \<le> 0)" 1055 and minus_divide_le_eq: "- (b / c) \<le> a \<longleftrightarrow> (if 0 < c then - b \<le> a * c else if c < 0 then a * c \<le> - b else 0 \<le> a)" 1056 and less_minus_divide_eq: "a < - (b / c) \<longleftrightarrow> (if 0 < c then a * c < - b else if c < 0 then - b < a * c else a < 0)" 1057 and minus_divide_less_eq: "- (b / c) < a \<longleftrightarrow> (if 0 < c then - b < a * c else if c < 0 then a * c < - b else 0 < a)" 1058 by (auto simp: field_simps not_less dest: antisym) 1059 1060text \<open>Division and Signs\<close> 1061 1062lemma 1063 shows zero_less_divide_iff: "0 < a / b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 1064 and divide_less_0_iff: "a / b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 1065 and zero_le_divide_iff: "0 \<le> a / b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 1066 and divide_le_0_iff: "a / b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b" 1067 by (auto simp add: divide_simps) 1068 1069text \<open>Division and the Number One\<close> 1070 1071text\<open>Simplify expressions equated with 1\<close> 1072 1073lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a \<longleftrightarrow> a = 0" 1074 by (cases "a = 0") (auto simp: field_simps) 1075 1076lemma one_divide_eq_0_iff [simp]: "1 / a = 0 \<longleftrightarrow> a = 0" 1077 using zero_eq_1_divide_iff[of a] by simp 1078 1079text\<open>Simplify expressions such as \<open>0 < 1/x\<close> to \<open>0 < x\<close>\<close> 1080 1081lemma zero_le_divide_1_iff [simp]: 1082 "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a" 1083 by (simp add: zero_le_divide_iff) 1084 1085lemma zero_less_divide_1_iff [simp]: 1086 "0 < 1 / a \<longleftrightarrow> 0 < a" 1087 by (simp add: zero_less_divide_iff) 1088 1089lemma divide_le_0_1_iff [simp]: 1090 "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0" 1091 by (simp add: divide_le_0_iff) 1092 1093lemma divide_less_0_1_iff [simp]: 1094 "1 / a < 0 \<longleftrightarrow> a < 0" 1095 by (simp add: divide_less_0_iff) 1096 1097lemma divide_right_mono: 1098 "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c" 1099by (force simp add: divide_strict_right_mono le_less) 1100 1101lemma divide_right_mono_neg: "a <= b 1102 ==> c <= 0 ==> b / c <= a / c" 1103apply (drule divide_right_mono [of _ _ "- c"]) 1104apply auto 1105done 1106 1107lemma divide_left_mono_neg: "a <= b 1108 ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" 1109 apply (drule divide_left_mono [of _ _ "- c"]) 1110 apply (auto simp add: mult.commute) 1111done 1112 1113lemma inverse_le_iff: "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)" 1114 by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) 1115 (auto simp add: field_simps zero_less_mult_iff mult_le_0_iff) 1116 1117lemma inverse_less_iff: "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)" 1118 by (subst less_le) (auto simp: inverse_le_iff) 1119 1120lemma divide_le_cancel: "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 1121 by (simp add: divide_inverse mult_le_cancel_right) 1122 1123lemma divide_less_cancel: "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0" 1124 by (auto simp add: divide_inverse mult_less_cancel_right) 1125 1126text\<open>Simplify quotients that are compared with the value 1.\<close> 1127 1128lemma le_divide_eq_1: 1129 "(1 \<le> b / a) = ((0 < a \<and> a \<le> b) \<or> (a < 0 \<and> b \<le> a))" 1130by (auto simp add: le_divide_eq) 1131 1132lemma divide_le_eq_1: 1133 "(b / a \<le> 1) = ((0 < a \<and> b \<le> a) \<or> (a < 0 \<and> a \<le> b) \<or> a=0)" 1134by (auto simp add: divide_le_eq) 1135 1136lemma less_divide_eq_1: 1137 "(1 < b / a) = ((0 < a \<and> a < b) \<or> (a < 0 \<and> b < a))" 1138by (auto simp add: less_divide_eq) 1139 1140lemma divide_less_eq_1: 1141 "(b / a < 1) = ((0 < a \<and> b < a) \<or> (a < 0 \<and> a < b) \<or> a=0)" 1142by (auto simp add: divide_less_eq) 1143 1144lemma divide_nonneg_nonneg [simp]: 1145 "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y" 1146 by (auto simp add: divide_simps) 1147 1148lemma divide_nonpos_nonpos: 1149 "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> 0 \<le> x / y" 1150 by (auto simp add: divide_simps) 1151 1152lemma divide_nonneg_nonpos: 1153 "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> x / y \<le> 0" 1154 by (auto simp add: divide_simps) 1155 1156lemma divide_nonpos_nonneg: 1157 "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x / y \<le> 0" 1158 by (auto simp add: divide_simps) 1159 1160text \<open>Conditional Simplification Rules: No Case Splits\<close> 1161 1162lemma le_divide_eq_1_pos [simp]: 1163 "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)" 1164by (auto simp add: le_divide_eq) 1165 1166lemma le_divide_eq_1_neg [simp]: 1167 "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)" 1168by (auto simp add: le_divide_eq) 1169 1170lemma divide_le_eq_1_pos [simp]: 1171 "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)" 1172by (auto simp add: divide_le_eq) 1173 1174lemma divide_le_eq_1_neg [simp]: 1175 "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)" 1176by (auto simp add: divide_le_eq) 1177 1178lemma less_divide_eq_1_pos [simp]: 1179 "0 < a \<Longrightarrow> (1 < b/a) = (a < b)" 1180by (auto simp add: less_divide_eq) 1181 1182lemma less_divide_eq_1_neg [simp]: 1183 "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)" 1184by (auto simp add: less_divide_eq) 1185 1186lemma divide_less_eq_1_pos [simp]: 1187 "0 < a \<Longrightarrow> (b/a < 1) = (b < a)" 1188by (auto simp add: divide_less_eq) 1189 1190lemma divide_less_eq_1_neg [simp]: 1191 "a < 0 \<Longrightarrow> b/a < 1 \<longleftrightarrow> a < b" 1192by (auto simp add: divide_less_eq) 1193 1194lemma eq_divide_eq_1 [simp]: 1195 "(1 = b/a) = ((a \<noteq> 0 \<and> a = b))" 1196by (auto simp add: eq_divide_eq) 1197 1198lemma divide_eq_eq_1 [simp]: 1199 "(b/a = 1) = ((a \<noteq> 0 \<and> a = b))" 1200by (auto simp add: divide_eq_eq) 1201 1202lemma abs_div_pos: "0 < y ==> 1203 \<bar>x\<bar> / y = \<bar>x / y\<bar>" 1204 apply (subst abs_divide) 1205 apply (simp add: order_less_imp_le) 1206done 1207 1208lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / \<bar>b\<bar>) = (0 \<le> a \<or> b = 0)" 1209by (auto simp: zero_le_divide_iff) 1210 1211lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 \<or> b = 0)" 1212by (auto simp: divide_le_0_iff) 1213 1214lemma field_le_mult_one_interval: 1215 assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y" 1216 shows "x \<le> y" 1217proof (cases "0 < x") 1218 assume "0 < x" 1219 thus ?thesis 1220 using dense_le_bounded[of 0 1 "y/x"] * 1221 unfolding le_divide_eq if_P[OF \<open>0 < x\<close>] by simp 1222next 1223 assume "\<not>0 < x" hence "x \<le> 0" by simp 1224 obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1::'a"] by auto 1225 hence "x \<le> s * x" using mult_le_cancel_right[of 1 x s] \<open>x \<le> 0\<close> by auto 1226 also note *[OF s] 1227 finally show ?thesis . 1228qed 1229 1230text\<open>For creating values between @{term u} and @{term v}.\<close> 1231lemma scaling_mono: 1232 assumes "u \<le> v" "0 \<le> r" "r \<le> s" 1233 shows "u + r * (v - u) / s \<le> v" 1234proof - 1235 have "r/s \<le> 1" using assms 1236 using divide_le_eq_1 by fastforce 1237 then have "(r/s) * (v - u) \<le> 1 * (v - u)" 1238 apply (rule mult_right_mono) 1239 using assms by simp 1240 then show ?thesis 1241 by (simp add: field_simps) 1242qed 1243 1244end 1245 1246text \<open>Min/max Simplification Rules\<close> 1247 1248lemma min_mult_distrib_left: 1249 fixes x::"'a::linordered_idom" 1250 shows "p * min x y = (if 0 \<le> p then min (p*x) (p*y) else max (p*x) (p*y))" 1251by (auto simp add: min_def max_def mult_le_cancel_left) 1252 1253lemma min_mult_distrib_right: 1254 fixes x::"'a::linordered_idom" 1255 shows "min x y * p = (if 0 \<le> p then min (x*p) (y*p) else max (x*p) (y*p))" 1256by (auto simp add: min_def max_def mult_le_cancel_right) 1257 1258lemma min_divide_distrib_right: 1259 fixes x::"'a::linordered_field" 1260 shows "min x y / p = (if 0 \<le> p then min (x/p) (y/p) else max (x/p) (y/p))" 1261by (simp add: min_mult_distrib_right divide_inverse) 1262 1263lemma max_mult_distrib_left: 1264 fixes x::"'a::linordered_idom" 1265 shows "p * max x y = (if 0 \<le> p then max (p*x) (p*y) else min (p*x) (p*y))" 1266by (auto simp add: min_def max_def mult_le_cancel_left) 1267 1268lemma max_mult_distrib_right: 1269 fixes x::"'a::linordered_idom" 1270 shows "max x y * p = (if 0 \<le> p then max (x*p) (y*p) else min (x*p) (y*p))" 1271by (auto simp add: min_def max_def mult_le_cancel_right) 1272 1273lemma max_divide_distrib_right: 1274 fixes x::"'a::linordered_field" 1275 shows "max x y / p = (if 0 \<le> p then max (x/p) (y/p) else min (x/p) (y/p))" 1276by (simp add: max_mult_distrib_right divide_inverse) 1277 1278hide_fact (open) field_inverse field_divide_inverse field_inverse_zero 1279 1280code_identifier 1281 code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 1282 1283end 1284