library theories for debugging and parallel computing using code generation towards Isabelle/ML
1 (* Title: HOL/Fields.thy
5 Author: Lawrence C Paulson
16 subsection {* Division rings *}
19 A division ring is like a field, but without the commutativity requirement.
23 fixes inverse :: "'a \<Rightarrow> 'a"
24 and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
26 class division_ring = ring_1 + inverse +
27 assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
28 assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
29 assumes divide_inverse: "a / b = a * inverse b"
32 subclass ring_1_no_zero_divisors
35 assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
36 show "a * b \<noteq> 0"
38 assume ab: "a * b = 0"
39 hence "0 = inverse a * (a * b) * inverse b" by simp
40 also have "\<dots> = (inverse a * a) * (b * inverse b)"
41 by (simp only: mult_assoc)
42 also have "\<dots> = 1" using a b by simp
43 finally show False by simp
47 lemma nonzero_imp_inverse_nonzero:
48 "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
50 assume ianz: "inverse a = 0"
52 hence "1 = a * inverse a" by simp
53 also have "... = 0" by (simp add: ianz)
54 finally have "1 = 0" .
55 thus False by (simp add: eq_commute)
58 lemma inverse_zero_imp_zero:
59 "inverse a = 0 \<Longrightarrow> a = 0"
60 apply (rule classical)
61 apply (drule nonzero_imp_inverse_nonzero)
66 assumes ab: "a * b = 1"
69 have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
70 moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
71 ultimately show ?thesis by (simp add: mult_assoc [symmetric])
74 lemma nonzero_inverse_minus_eq:
75 "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
76 by (rule inverse_unique) simp
78 lemma nonzero_inverse_inverse_eq:
79 "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
80 by (rule inverse_unique) simp
82 lemma nonzero_inverse_eq_imp_eq:
83 assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
86 from `inverse a = inverse b`
87 have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
88 with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
89 by (simp add: nonzero_inverse_inverse_eq)
92 lemma inverse_1 [simp]: "inverse 1 = 1"
93 by (rule inverse_unique) simp
95 lemma nonzero_inverse_mult_distrib:
96 assumes "a \<noteq> 0" and "b \<noteq> 0"
97 shows "inverse (a * b) = inverse b * inverse a"
99 have "a * (b * inverse b) * inverse a = 1" using assms by simp
100 hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc)
101 thus ?thesis by (rule inverse_unique)
104 lemma division_ring_inverse_add:
105 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
106 by (simp add: algebra_simps)
108 lemma division_ring_inverse_diff:
109 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
110 by (simp add: algebra_simps)
112 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
114 assume neq: "b \<noteq> 0"
116 hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)
117 also assume "a / b = 1"
118 finally show "a = b" by simp
121 with neq show "a / b = 1" by (simp add: divide_inverse)
125 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
126 by (simp add: divide_inverse)
128 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
129 by (simp add: divide_inverse)
131 lemma divide_zero_left [simp]: "0 / a = 0"
132 by (simp add: divide_inverse)
134 lemma inverse_eq_divide: "inverse a = 1 / a"
135 by (simp add: divide_inverse)
137 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
138 by (simp add: divide_inverse algebra_simps)
140 lemma divide_1 [simp]: "a / 1 = a"
141 by (simp add: divide_inverse)
143 lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
144 by (simp add: divide_inverse mult_assoc)
146 lemma minus_divide_left: "- (a / b) = (-a) / b"
147 by (simp add: divide_inverse)
149 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
150 by (simp add: divide_inverse nonzero_inverse_minus_eq)
152 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
153 by (simp add: divide_inverse nonzero_inverse_minus_eq)
155 lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
156 by (simp add: divide_inverse)
158 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
159 by (simp add: diff_minus add_divide_distrib)
161 lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
163 assume [simp]: "c \<noteq> 0"
164 have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
165 also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
166 finally show ?thesis .
169 lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
171 assume [simp]: "c \<noteq> 0"
172 have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
173 also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
174 finally show ?thesis .
177 lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
178 by (simp add: divide_inverse mult_assoc)
180 lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
181 by (drule sym) (simp add: divide_inverse mult_assoc)
185 class division_ring_inverse_zero = division_ring +
186 assumes inverse_zero [simp]: "inverse 0 = 0"
189 lemma divide_zero [simp]:
191 by (simp add: divide_inverse)
193 lemma divide_self_if [simp]:
194 "a / a = (if a = 0 then 0 else 1)"
197 lemma inverse_nonzero_iff_nonzero [simp]:
198 "inverse a = 0 \<longleftrightarrow> a = 0"
199 by rule (fact inverse_zero_imp_zero, simp)
201 lemma inverse_minus_eq [simp]:
202 "inverse (- a) = - inverse a"
204 assume "a=0" thus ?thesis by simp
207 thus ?thesis by (simp add: nonzero_inverse_minus_eq)
210 lemma inverse_inverse_eq [simp]:
211 "inverse (inverse a) = a"
213 assume "a=0" thus ?thesis by simp
216 thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
219 lemma inverse_eq_imp_eq:
220 "inverse a = inverse b \<Longrightarrow> a = b"
221 by (drule arg_cong [where f="inverse"], simp)
223 lemma inverse_eq_iff_eq [simp]:
224 "inverse a = inverse b \<longleftrightarrow> a = b"
225 by (force dest!: inverse_eq_imp_eq)
229 subsection {* Fields *}
231 class field = comm_ring_1 + inverse +
232 assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
233 assumes field_divide_inverse: "a / b = a * inverse b"
236 subclass division_ring
239 assume "a \<noteq> 0"
240 thus "inverse a * a = 1" by (rule field_inverse)
241 thus "a * inverse a = 1" by (simp only: mult_commute)
244 show "a / b = a * inverse b" by (rule field_divide_inverse)
249 text{*There is no slick version using division by zero.*}
251 "[| a \<noteq> 0; b \<noteq> 0 |]
252 ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
253 by (simp add: division_ring_inverse_add mult_ac)
255 lemma nonzero_mult_divide_mult_cancel_left [simp, no_atp]:
256 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
258 have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
259 by (simp add: divide_inverse nonzero_inverse_mult_distrib)
260 also have "... = a * inverse b * (inverse c * c)"
261 by (simp only: mult_ac)
262 also have "... = a * inverse b" by simp
263 finally show ?thesis by (simp add: divide_inverse)
266 lemma nonzero_mult_divide_mult_cancel_right [simp, no_atp]:
267 "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
268 by (simp add: mult_commute [of _ c])
270 lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
271 by (simp add: divide_inverse mult_ac)
273 text{*It's not obvious whether @{text times_divide_eq} should be
274 simprules or not. Their effect is to gather terms into one big
275 fraction, like a*b*c / x*y*z. The rationale for that is unclear, but
276 many proofs seem to need them.*}
278 lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
281 assumes "y \<noteq> 0" and "z \<noteq> 0"
282 shows "x / y + w / z = (x * z + w * y) / (y * z)"
284 have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"
286 also have "\<dots> = (x * z + y * w) / (y * z)"
287 by (simp only: add_divide_distrib)
289 by (simp only: mult_commute)
292 text{*Special Cancellation Simprules for Division*}
294 lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
295 "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
296 using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
298 lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
299 "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
300 using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
302 lemma nonzero_divide_mult_cancel_right [simp, no_atp]:
303 "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
304 using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
306 lemma nonzero_divide_mult_cancel_left [simp, no_atp]:
307 "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
308 using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
310 lemma nonzero_mult_divide_mult_cancel_left2 [simp, no_atp]:
311 "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
312 using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
314 lemma nonzero_mult_divide_mult_cancel_right2 [simp, no_atp]:
315 "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
316 using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
318 lemma add_divide_eq_iff [field_simps]:
319 "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
320 by (simp add: add_divide_distrib)
322 lemma divide_add_eq_iff [field_simps]:
323 "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
324 by (simp add: add_divide_distrib)
326 lemma diff_divide_eq_iff [field_simps]:
327 "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
328 by (simp add: diff_divide_distrib)
330 lemma divide_diff_eq_iff [field_simps]:
331 "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
332 by (simp add: diff_divide_distrib)
335 "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
336 by (simp add: field_simps)
339 "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
340 by (simp add: field_simps)
344 class field_inverse_zero = field +
345 assumes field_inverse_zero: "inverse 0 = 0"
348 subclass division_ring_inverse_zero proof
349 qed (fact field_inverse_zero)
351 text{*This version builds in division by zero while also re-orienting
352 the right-hand side.*}
353 lemma inverse_mult_distrib [simp]:
354 "inverse (a * b) = inverse a * inverse b"
356 assume "a \<noteq> 0 & b \<noteq> 0"
357 thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
359 assume "~ (a \<noteq> 0 & b \<noteq> 0)"
360 thus ?thesis by force
363 lemma inverse_divide [simp]:
364 "inverse (a / b) = b / a"
365 by (simp add: divide_inverse mult_commute)
368 text {* Calculations with fractions *}
370 text{* There is a whole bunch of simp-rules just for class @{text
371 field} but none for class @{text field} and @{text nonzero_divides}
372 because the latter are covered by a simproc. *}
374 lemma mult_divide_mult_cancel_left:
375 "c \<noteq> 0 \<Longrightarrow> (c * a) / (c * b) = a / b"
376 apply (cases "b = 0")
380 lemma mult_divide_mult_cancel_right:
381 "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
382 apply (cases "b = 0")
386 lemma divide_divide_eq_right [simp, no_atp]:
387 "a / (b / c) = (a * c) / b"
388 by (simp add: divide_inverse mult_ac)
390 lemma divide_divide_eq_left [simp, no_atp]:
391 "(a / b) / c = a / (b * c)"
392 by (simp add: divide_inverse mult_assoc)
395 text {*Special Cancellation Simprules for Division*}
397 lemma mult_divide_mult_cancel_left_if [simp,no_atp]:
398 shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
399 by (simp add: mult_divide_mult_cancel_left)
402 text {* Division and Unary Minus *}
404 lemma minus_divide_right:
405 "- (a / b) = a / - b"
406 by (simp add: divide_inverse)
408 lemma divide_minus_right [simp, no_atp]:
409 "a / - b = - (a / b)"
410 by (simp add: divide_inverse)
412 lemma minus_divide_divide:
413 "(- a) / (- b) = a / b"
414 apply (cases "b=0", simp)
415 apply (simp add: nonzero_minus_divide_divide)
419 "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)"
420 by (simp add: nonzero_eq_divide_eq)
423 "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)"
424 by (force simp add: nonzero_divide_eq_eq)
426 lemma inverse_eq_1_iff [simp]:
427 "inverse x = 1 \<longleftrightarrow> x = 1"
428 by (insert inverse_eq_iff_eq [of x 1], simp)
430 lemma divide_eq_0_iff [simp, no_atp]:
431 "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
432 by (simp add: divide_inverse)
434 lemma divide_cancel_right [simp, no_atp]:
435 "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
436 apply (cases "c=0", simp)
437 apply (simp add: divide_inverse)
440 lemma divide_cancel_left [simp, no_atp]:
441 "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b"
442 apply (cases "c=0", simp)
443 apply (simp add: divide_inverse)
446 lemma divide_eq_1_iff [simp, no_atp]:
447 "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
448 apply (cases "b=0", simp)
449 apply (simp add: right_inverse_eq)
452 lemma one_eq_divide_iff [simp, no_atp]:
453 "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
454 by (simp add: eq_commute [of 1])
456 lemma times_divide_times_eq:
457 "(x / y) * (z / w) = (x * z) / (y * w)"
461 "y \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y"
462 by (simp add: add_divide_distrib)
465 "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
466 by (simp add: add_divide_distrib add.commute)
471 subsection {* Ordered fields *}
473 class linordered_field = field + linordered_idom
476 lemma positive_imp_inverse_positive:
477 assumes a_gt_0: "0 < a"
478 shows "0 < inverse a"
480 have "0 < a * inverse a"
481 by (simp add: a_gt_0 [THEN less_imp_not_eq2])
483 by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff)
486 lemma negative_imp_inverse_negative:
487 "a < 0 \<Longrightarrow> inverse a < 0"
488 by (insert positive_imp_inverse_positive [of "-a"],
489 simp add: nonzero_inverse_minus_eq less_imp_not_eq)
491 lemma inverse_le_imp_le:
492 assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
494 proof (rule classical)
496 hence "a < b" by (simp add: linorder_not_le)
497 hence bpos: "0 < b" by (blast intro: apos less_trans)
498 hence "a * inverse a \<le> a * inverse b"
499 by (simp add: apos invle less_imp_le mult_left_mono)
500 hence "(a * inverse a) * b \<le> (a * inverse b) * b"
501 by (simp add: bpos less_imp_le mult_right_mono)
502 thus "b \<le> a" by (simp add: mult_assoc apos bpos less_imp_not_eq2)
505 lemma inverse_positive_imp_positive:
506 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
509 have "0 < inverse (inverse a)"
510 using inv_gt_0 by (rule positive_imp_inverse_positive)
512 using nz by (simp add: nonzero_inverse_inverse_eq)
515 lemma inverse_negative_imp_negative:
516 assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
519 have "inverse (inverse a) < 0"
520 using inv_less_0 by (rule negative_imp_inverse_negative)
521 thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
524 lemma linordered_field_no_lb:
525 "\<forall>x. \<exists>y. y < x"
528 have m1: "- (1::'a) < 0" by simp
529 from add_strict_right_mono[OF m1, where c=x]
530 have "(- 1) + x < x" by simp
531 thus "\<exists>y. y < x" by blast
534 lemma linordered_field_no_ub:
535 "\<forall> x. \<exists>y. y > x"
538 have m1: " (1::'a) > 0" by simp
539 from add_strict_right_mono[OF m1, where c=x]
540 have "1 + x > x" by simp
541 thus "\<exists>y. y > x" by blast
544 lemma less_imp_inverse_less:
545 assumes less: "a < b" and apos: "0 < a"
546 shows "inverse b < inverse a"
548 assume "~ inverse b < inverse a"
549 hence "inverse a \<le> inverse b" by simp
551 by (simp add: not_less inverse_le_imp_le [OF _ apos])
552 thus False by (rule notE [OF _ less])
555 lemma inverse_less_imp_less:
556 "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
557 apply (simp add: less_le [of "inverse a"] less_le [of "b"])
558 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
561 text{*Both premises are essential. Consider -1 and 1.*}
562 lemma inverse_less_iff_less [simp,no_atp]:
563 "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
564 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
566 lemma le_imp_inverse_le:
567 "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
568 by (force simp add: le_less less_imp_inverse_less)
570 lemma inverse_le_iff_le [simp,no_atp]:
571 "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
572 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
575 text{*These results refer to both operands being negative. The opposite-sign
576 case is trivial, since inverse preserves signs.*}
577 lemma inverse_le_imp_le_neg:
578 "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
579 apply (rule classical)
580 apply (subgoal_tac "a < 0")
582 apply (insert inverse_le_imp_le [of "-b" "-a"])
583 apply (simp add: nonzero_inverse_minus_eq)
586 lemma less_imp_inverse_less_neg:
587 "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a"
588 apply (subgoal_tac "a < 0")
589 prefer 2 apply (blast intro: less_trans)
590 apply (insert less_imp_inverse_less [of "-b" "-a"])
591 apply (simp add: nonzero_inverse_minus_eq)
594 lemma inverse_less_imp_less_neg:
595 "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
596 apply (rule classical)
597 apply (subgoal_tac "a < 0")
600 apply (insert inverse_less_imp_less [of "-b" "-a"])
601 apply (simp add: nonzero_inverse_minus_eq)
604 lemma inverse_less_iff_less_neg [simp,no_atp]:
605 "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
606 apply (insert inverse_less_iff_less [of "-b" "-a"])
607 apply (simp del: inverse_less_iff_less
608 add: nonzero_inverse_minus_eq)
611 lemma le_imp_inverse_le_neg:
612 "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
613 by (force simp add: le_less less_imp_inverse_less_neg)
615 lemma inverse_le_iff_le_neg [simp,no_atp]:
616 "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
617 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
619 lemma one_less_inverse:
620 "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a"
621 using less_imp_inverse_less [of a 1, unfolded inverse_1] .
623 lemma one_le_inverse:
624 "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
625 using le_imp_inverse_le [of a 1, unfolded inverse_1] .
627 lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
630 hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
631 by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
632 also have "... = (a*c \<le> b)"
633 by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
634 finally show ?thesis .
637 lemma neg_le_divide_eq [field_simps]: "c < 0 ==> (a \<le> b/c) = (b \<le> a*c)"
640 hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
641 by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
642 also have "... = (b \<le> a*c)"
643 by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc)
644 finally show ?thesis .
647 lemma pos_less_divide_eq [field_simps]:
648 "0 < c ==> (a < b/c) = (a*c < b)"
651 hence "(a < b/c) = (a*c < (b/c)*c)"
652 by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
653 also have "... = (a*c < b)"
654 by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
655 finally show ?thesis .
658 lemma neg_less_divide_eq [field_simps]:
659 "c < 0 ==> (a < b/c) = (b < a*c)"
662 hence "(a < b/c) = ((b/c)*c < a*c)"
663 by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
664 also have "... = (b < a*c)"
665 by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc)
666 finally show ?thesis .
669 lemma pos_divide_less_eq [field_simps]:
670 "0 < c ==> (b/c < a) = (b < a*c)"
673 hence "(b/c < a) = ((b/c)*c < a*c)"
674 by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
675 also have "... = (b < a*c)"
676 by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
677 finally show ?thesis .
680 lemma neg_divide_less_eq [field_simps]:
681 "c < 0 ==> (b/c < a) = (a*c < b)"
684 hence "(b/c < a) = (a*c < (b/c)*c)"
685 by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq)
686 also have "... = (a*c < b)"
687 by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc)
688 finally show ?thesis .
691 lemma pos_divide_le_eq [field_simps]: "0 < c ==> (b/c \<le> a) = (b \<le> a*c)"
694 hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
695 by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
696 also have "... = (b \<le> a*c)"
697 by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
698 finally show ?thesis .
701 lemma neg_divide_le_eq [field_simps]: "c < 0 ==> (b/c \<le> a) = (a*c \<le> b)"
704 hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
705 by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq)
706 also have "... = (a*c \<le> b)"
707 by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc)
708 finally show ?thesis .
711 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
712 of positivity/negativity needed for @{text field_simps}. Have not added @{text
713 sign_simps} to @{text field_simps} because the former can lead to case
716 lemmas sign_simps [no_atp] = algebra_simps
717 zero_less_mult_iff mult_less_0_iff
719 lemmas (in -) sign_simps [no_atp] = algebra_simps
720 zero_less_mult_iff mult_less_0_iff
722 (* Only works once linear arithmetic is installed:
724 lemma fixes a b c d e f :: "'a::linordered_field"
725 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
726 ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
727 ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
728 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
729 prefer 2 apply(simp add:sign_simps)
730 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
731 prefer 2 apply(simp add:sign_simps)
732 apply(simp add:field_simps)
736 lemma divide_pos_pos:
737 "0 < x ==> 0 < y ==> 0 < x / y"
738 by(simp add:field_simps)
740 lemma divide_nonneg_pos:
741 "0 <= x ==> 0 < y ==> 0 <= x / y"
742 by(simp add:field_simps)
744 lemma divide_neg_pos:
745 "x < 0 ==> 0 < y ==> x / y < 0"
746 by(simp add:field_simps)
748 lemma divide_nonpos_pos:
749 "x <= 0 ==> 0 < y ==> x / y <= 0"
750 by(simp add:field_simps)
752 lemma divide_pos_neg:
753 "0 < x ==> y < 0 ==> x / y < 0"
754 by(simp add:field_simps)
756 lemma divide_nonneg_neg:
757 "0 <= x ==> y < 0 ==> x / y <= 0"
758 by(simp add:field_simps)
760 lemma divide_neg_neg:
761 "x < 0 ==> y < 0 ==> 0 < x / y"
762 by(simp add:field_simps)
764 lemma divide_nonpos_neg:
765 "x <= 0 ==> y < 0 ==> 0 <= x / y"
766 by(simp add:field_simps)
768 lemma divide_strict_right_mono:
769 "[|a < b; 0 < c|] ==> a / c < b / c"
770 by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
771 positive_imp_inverse_positive)
774 lemma divide_strict_right_mono_neg:
775 "[|b < a; c < 0|] ==> a / c < b / c"
776 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
777 apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric])
780 text{*The last premise ensures that @{term a} and @{term b}
782 lemma divide_strict_left_mono:
783 "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
784 by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
786 lemma divide_left_mono:
787 "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
788 by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
790 lemma divide_strict_left_mono_neg:
791 "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
792 by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
794 lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
796 by (subst pos_divide_le_eq, assumption+)
798 lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==>
800 by(simp add:field_simps)
802 lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==>
804 by(simp add:field_simps)
806 lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==>
808 by(simp add:field_simps)
810 lemma frac_le: "0 <= x ==>
811 x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w"
812 apply (rule mult_imp_div_pos_le)
814 apply (subst times_divide_eq_left)
815 apply (rule mult_imp_le_div_pos, assumption)
816 apply (rule mult_mono)
820 lemma frac_less: "0 <= x ==>
821 x < y ==> 0 < w ==> w <= z ==> x / z < y / w"
822 apply (rule mult_imp_div_pos_less)
824 apply (subst times_divide_eq_left)
825 apply (rule mult_imp_less_div_pos, assumption)
826 apply (erule mult_less_le_imp_less)
830 lemma frac_less2: "0 < x ==>
831 x <= y ==> 0 < w ==> w < z ==> x / z < y / w"
832 apply (rule mult_imp_div_pos_less)
834 apply (rule mult_imp_less_div_pos, assumption)
835 apply (erule mult_le_less_imp_less)
839 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
840 by (simp add: field_simps zero_less_two)
842 lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
843 by (simp add: field_simps zero_less_two)
845 subclass dense_linorder
848 from less_add_one show "\<exists>y. x < y" ..
849 from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
850 then have "x - 1 < x + 1 - 1" by (simp only: diff_minus [symmetric])
851 then have "x - 1 < x" by (simp add: algebra_simps)
852 then show "\<exists>y. y < x" ..
853 show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
856 lemma nonzero_abs_inverse:
857 "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
858 apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq
859 negative_imp_inverse_negative)
860 apply (blast intro: positive_imp_inverse_positive elim: less_asym)
863 lemma nonzero_abs_divide:
864 "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
865 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
867 lemma field_le_epsilon:
868 assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
870 proof (rule dense_le)
872 hence "0 < x - t" by (simp add: less_diff_eq)
873 from e [OF this] have "x + 0 \<le> x + (y - t)" by (simp add: algebra_simps)
874 then have "0 \<le> y - t" by (simp only: add_le_cancel_left)
875 then show "t \<le> y" by (simp add: algebra_simps)
880 class linordered_field_inverse_zero = linordered_field + field_inverse_zero
885 (if 0 < c then a*c \<le> b
886 else if c < 0 then b \<le> a*c
888 apply (cases "c=0", simp)
889 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
892 lemma inverse_positive_iff_positive [simp]:
893 "(0 < inverse a) = (0 < a)"
894 apply (cases "a = 0", simp)
895 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
898 lemma inverse_negative_iff_negative [simp]:
899 "(inverse a < 0) = (a < 0)"
900 apply (cases "a = 0", simp)
901 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
904 lemma inverse_nonnegative_iff_nonnegative [simp]:
905 "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a"
906 by (simp add: not_less [symmetric])
908 lemma inverse_nonpositive_iff_nonpositive [simp]:
909 "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
910 by (simp add: not_less [symmetric])
912 lemma one_less_inverse_iff:
913 "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
916 with inverse_less_iff_less [OF zero_less_one, of x]
919 assume notless: "~ (0 < x)"
920 have "~ (1 < inverse x)"
922 assume "1 < inverse x"
923 also with notless have "... \<le> 0" by simp
924 also have "... < 1" by (rule zero_less_one)
925 finally show False by auto
927 with notless show ?thesis by simp
930 lemma one_le_inverse_iff:
931 "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
932 proof (cases "x = 1")
933 case True then show ?thesis by simp
935 case False then have "inverse x \<noteq> 1" by simp
936 then have "1 \<noteq> inverse x" by blast
937 then have "1 \<le> inverse x \<longleftrightarrow> 1 < inverse x" by (simp add: le_less)
938 with False show ?thesis by (auto simp add: one_less_inverse_iff)
941 lemma inverse_less_1_iff:
942 "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
943 by (simp add: not_le [symmetric] one_le_inverse_iff)
945 lemma inverse_le_1_iff:
946 "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
947 by (simp add: not_less [symmetric] one_less_inverse_iff)
951 (if 0 < c then b \<le> a*c
952 else if c < 0 then a*c \<le> b
954 apply (cases "c=0", simp)
955 apply (force simp add: pos_divide_le_eq neg_divide_le_eq)
958 lemma less_divide_eq:
960 (if 0 < c then a*c < b
961 else if c < 0 then b < a*c
963 apply (cases "c=0", simp)
964 apply (force simp add: pos_less_divide_eq neg_less_divide_eq)
967 lemma divide_less_eq:
969 (if 0 < c then b < a*c
970 else if c < 0 then a*c < b
972 apply (cases "c=0", simp)
973 apply (force simp add: pos_divide_less_eq neg_divide_less_eq)
976 text {*Division and Signs*}
978 lemma zero_less_divide_iff:
979 "(0 < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
980 by (simp add: divide_inverse zero_less_mult_iff)
982 lemma divide_less_0_iff:
984 (0 < a & b < 0 | a < 0 & 0 < b)"
985 by (simp add: divide_inverse mult_less_0_iff)
987 lemma zero_le_divide_iff:
989 (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
990 by (simp add: divide_inverse zero_le_mult_iff)
992 lemma divide_le_0_iff:
994 (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
995 by (simp add: divide_inverse mult_le_0_iff)
997 text {* Division and the Number One *}
999 text{*Simplify expressions equated with 1*}
1001 lemma zero_eq_1_divide_iff [simp,no_atp]:
1002 "(0 = 1/a) = (a = 0)"
1003 apply (cases "a=0", simp)
1004 apply (auto simp add: nonzero_eq_divide_eq)
1007 lemma one_divide_eq_0_iff [simp,no_atp]:
1008 "(1/a = 0) = (a = 0)"
1009 apply (cases "a=0", simp)
1010 apply (insert zero_neq_one [THEN not_sym])
1011 apply (auto simp add: nonzero_divide_eq_eq)
1014 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
1016 lemma zero_le_divide_1_iff [simp, no_atp]:
1017 "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
1018 by (simp add: zero_le_divide_iff)
1020 lemma zero_less_divide_1_iff [simp, no_atp]:
1021 "0 < 1 / a \<longleftrightarrow> 0 < a"
1022 by (simp add: zero_less_divide_iff)
1024 lemma divide_le_0_1_iff [simp, no_atp]:
1025 "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
1026 by (simp add: divide_le_0_iff)
1028 lemma divide_less_0_1_iff [simp, no_atp]:
1029 "1 / a < 0 \<longleftrightarrow> a < 0"
1030 by (simp add: divide_less_0_iff)
1032 lemma divide_right_mono:
1033 "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
1034 by (force simp add: divide_strict_right_mono le_less)
1036 lemma divide_right_mono_neg: "a <= b
1037 ==> c <= 0 ==> b / c <= a / c"
1038 apply (drule divide_right_mono [of _ _ "- c"])
1042 lemma divide_left_mono_neg: "a <= b
1043 ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
1044 apply (drule divide_left_mono [of _ _ "- c"])
1045 apply (auto simp add: mult_commute)
1048 lemma inverse_le_iff:
1049 "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
1052 then have "inverse a < 0" by simp
1053 moreover assume "0 < b"
1054 then have "0 < inverse b" by simp
1055 ultimately have "inverse a < inverse b" by (rule less_trans)
1056 then have "inverse a \<le> inverse b" by simp }
1059 then have "inverse b < 0" by simp
1060 moreover assume "0 < a"
1061 then have "0 < inverse a" by simp
1062 ultimately have "inverse b < inverse a" by (rule less_trans)
1063 then have "\<not> inverse a \<le> inverse b" by simp }
1064 ultimately show ?thesis
1065 by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
1066 (auto simp: not_less zero_less_mult_iff mult_le_0_iff)
1069 lemma inverse_less_iff:
1070 "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
1071 by (subst less_le) (auto simp: inverse_le_iff)
1073 lemma divide_le_cancel:
1074 "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
1075 by (simp add: divide_inverse mult_le_cancel_right)
1077 lemma divide_less_cancel:
1078 "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
1079 by (auto simp add: divide_inverse mult_less_cancel_right)
1081 text{*Simplify quotients that are compared with the value 1.*}
1083 lemma le_divide_eq_1 [no_atp]:
1084 "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
1085 by (auto simp add: le_divide_eq)
1087 lemma divide_le_eq_1 [no_atp]:
1088 "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
1089 by (auto simp add: divide_le_eq)
1091 lemma less_divide_eq_1 [no_atp]:
1092 "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
1093 by (auto simp add: less_divide_eq)
1095 lemma divide_less_eq_1 [no_atp]:
1096 "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
1097 by (auto simp add: divide_less_eq)
1100 text {*Conditional Simplification Rules: No Case Splits*}
1102 lemma le_divide_eq_1_pos [simp,no_atp]:
1103 "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
1104 by (auto simp add: le_divide_eq)
1106 lemma le_divide_eq_1_neg [simp,no_atp]:
1107 "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
1108 by (auto simp add: le_divide_eq)
1110 lemma divide_le_eq_1_pos [simp,no_atp]:
1111 "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
1112 by (auto simp add: divide_le_eq)
1114 lemma divide_le_eq_1_neg [simp,no_atp]:
1115 "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
1116 by (auto simp add: divide_le_eq)
1118 lemma less_divide_eq_1_pos [simp,no_atp]:
1119 "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
1120 by (auto simp add: less_divide_eq)
1122 lemma less_divide_eq_1_neg [simp,no_atp]:
1123 "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
1124 by (auto simp add: less_divide_eq)
1126 lemma divide_less_eq_1_pos [simp,no_atp]:
1127 "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
1128 by (auto simp add: divide_less_eq)
1130 lemma divide_less_eq_1_neg [simp,no_atp]:
1131 "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
1132 by (auto simp add: divide_less_eq)
1134 lemma eq_divide_eq_1 [simp,no_atp]:
1135 "(1 = b/a) = ((a \<noteq> 0 & a = b))"
1136 by (auto simp add: eq_divide_eq)
1138 lemma divide_eq_eq_1 [simp,no_atp]:
1139 "(b/a = 1) = ((a \<noteq> 0 & a = b))"
1140 by (auto simp add: divide_eq_eq)
1142 lemma abs_inverse [simp]:
1143 "\<bar>inverse a\<bar> =
1144 inverse \<bar>a\<bar>"
1145 apply (cases "a=0", simp)
1146 apply (simp add: nonzero_abs_inverse)
1149 lemma abs_divide [simp]:
1150 "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
1151 apply (cases "b=0", simp)
1152 apply (simp add: nonzero_abs_divide)
1155 lemma abs_div_pos: "0 < y ==>
1156 \<bar>x\<bar> / y = \<bar>x / y\<bar>"
1157 apply (subst abs_divide)
1158 apply (simp add: order_less_imp_le)
1161 lemma field_le_mult_one_interval:
1162 assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
1164 proof (cases "0 < x")
1167 using dense_le_bounded[of 0 1 "y/x"] *
1168 unfolding le_divide_eq if_P[OF `0 < x`] by simp
1170 assume "\<not>0 < x" hence "x \<le> 0" by simp
1171 obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1\<Colon>'a"] by auto
1172 hence "x \<le> s * x" using mult_le_cancel_right[of 1 x s] `x \<le> 0` by auto
1174 finally show ?thesis .
1182 code_modulename OCaml
1185 code_modulename Haskell