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