haftmann@35050: (* Title: HOL/Fields.thy wenzelm@32960: Author: Gertrud Bauer wenzelm@32960: Author: Steven Obua wenzelm@32960: Author: Tobias Nipkow wenzelm@32960: Author: Lawrence C Paulson wenzelm@32960: Author: Markus Wenzel wenzelm@32960: Author: Jeremy Avigad paulson@14265: *) paulson@14265: haftmann@35050: header {* Fields *} haftmann@25152: haftmann@35050: theory Fields haftmann@35050: imports Rings haftmann@25186: begin paulson@14421: huffman@44064: subsection {* Division rings *} huffman@44064: huffman@44064: text {* huffman@44064: A division ring is like a field, but without the commutativity requirement. huffman@44064: *} huffman@44064: huffman@44064: class inverse = huffman@44064: fixes inverse :: "'a \ 'a" huffman@44064: and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) huffman@44064: huffman@44064: class division_ring = ring_1 + inverse + huffman@44064: assumes left_inverse [simp]: "a \ 0 \ inverse a * a = 1" huffman@44064: assumes right_inverse [simp]: "a \ 0 \ a * inverse a = 1" huffman@44064: assumes divide_inverse: "a / b = a * inverse b" huffman@44064: begin huffman@44064: huffman@44064: subclass ring_1_no_zero_divisors huffman@44064: proof huffman@44064: fix a b :: 'a huffman@44064: assume a: "a \ 0" and b: "b \ 0" huffman@44064: show "a * b \ 0" huffman@44064: proof huffman@44064: assume ab: "a * b = 0" huffman@44064: hence "0 = inverse a * (a * b) * inverse b" by simp huffman@44064: also have "\ = (inverse a * a) * (b * inverse b)" huffman@44064: by (simp only: mult_assoc) huffman@44064: also have "\ = 1" using a b by simp huffman@44064: finally show False by simp huffman@44064: qed huffman@44064: qed huffman@44064: huffman@44064: lemma nonzero_imp_inverse_nonzero: huffman@44064: "a \ 0 \ inverse a \ 0" huffman@44064: proof huffman@44064: assume ianz: "inverse a = 0" huffman@44064: assume "a \ 0" huffman@44064: hence "1 = a * inverse a" by simp huffman@44064: also have "... = 0" by (simp add: ianz) huffman@44064: finally have "1 = 0" . huffman@44064: thus False by (simp add: eq_commute) huffman@44064: qed huffman@44064: huffman@44064: lemma inverse_zero_imp_zero: huffman@44064: "inverse a = 0 \ a = 0" huffman@44064: apply (rule classical) huffman@44064: apply (drule nonzero_imp_inverse_nonzero) huffman@44064: apply auto huffman@44064: done huffman@44064: huffman@44064: lemma inverse_unique: huffman@44064: assumes ab: "a * b = 1" huffman@44064: shows "inverse a = b" huffman@44064: proof - huffman@44064: have "a \ 0" using ab by (cases "a = 0") simp_all huffman@44064: moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) huffman@44064: ultimately show ?thesis by (simp add: mult_assoc [symmetric]) huffman@44064: qed huffman@44064: huffman@44064: lemma nonzero_inverse_minus_eq: huffman@44064: "a \ 0 \ inverse (- a) = - inverse a" huffman@44064: by (rule inverse_unique) simp huffman@44064: huffman@44064: lemma nonzero_inverse_inverse_eq: huffman@44064: "a \ 0 \ inverse (inverse a) = a" huffman@44064: by (rule inverse_unique) simp huffman@44064: huffman@44064: lemma nonzero_inverse_eq_imp_eq: huffman@44064: assumes "inverse a = inverse b" and "a \ 0" and "b \ 0" huffman@44064: shows "a = b" huffman@44064: proof - huffman@44064: from `inverse a = inverse b` huffman@44064: have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) huffman@44064: with `a \ 0` and `b \ 0` show "a = b" huffman@44064: by (simp add: nonzero_inverse_inverse_eq) huffman@44064: qed huffman@44064: huffman@44064: lemma inverse_1 [simp]: "inverse 1 = 1" huffman@44064: by (rule inverse_unique) simp huffman@44064: huffman@44064: lemma nonzero_inverse_mult_distrib: huffman@44064: assumes "a \ 0" and "b \ 0" huffman@44064: shows "inverse (a * b) = inverse b * inverse a" huffman@44064: proof - huffman@44064: have "a * (b * inverse b) * inverse a = 1" using assms by simp huffman@44064: hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult_assoc) huffman@44064: thus ?thesis by (rule inverse_unique) huffman@44064: qed huffman@44064: huffman@44064: lemma division_ring_inverse_add: huffman@44064: "a \ 0 \ b \ 0 \ inverse a + inverse b = inverse a * (a + b) * inverse b" huffman@44064: by (simp add: algebra_simps) huffman@44064: huffman@44064: lemma division_ring_inverse_diff: huffman@44064: "a \ 0 \ b \ 0 \ inverse a - inverse b = inverse a * (b - a) * inverse b" huffman@44064: by (simp add: algebra_simps) huffman@44064: huffman@44064: lemma right_inverse_eq: "b \ 0 \ a / b = 1 \ a = b" huffman@44064: proof huffman@44064: assume neq: "b \ 0" huffman@44064: { huffman@44064: hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc) huffman@44064: also assume "a / b = 1" huffman@44064: finally show "a = b" by simp huffman@44064: next huffman@44064: assume "a = b" huffman@44064: with neq show "a / b = 1" by (simp add: divide_inverse) huffman@44064: } huffman@44064: qed huffman@44064: huffman@44064: lemma nonzero_inverse_eq_divide: "a \ 0 \ inverse a = 1 / a" huffman@44064: by (simp add: divide_inverse) huffman@44064: huffman@44064: lemma divide_self [simp]: "a \ 0 \ a / a = 1" huffman@44064: by (simp add: divide_inverse) huffman@44064: huffman@44064: lemma divide_zero_left [simp]: "0 / a = 0" huffman@44064: by (simp add: divide_inverse) huffman@44064: huffman@44064: lemma inverse_eq_divide: "inverse a = 1 / a" huffman@44064: by (simp add: divide_inverse) huffman@44064: huffman@44064: lemma add_divide_distrib: "(a+b) / c = a/c + b/c" huffman@44064: by (simp add: divide_inverse algebra_simps) huffman@44064: huffman@44064: lemma divide_1 [simp]: "a / 1 = a" huffman@44064: by (simp add: divide_inverse) huffman@44064: huffman@44064: lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c" huffman@44064: by (simp add: divide_inverse mult_assoc) huffman@44064: huffman@44064: lemma minus_divide_left: "- (a / b) = (-a) / b" huffman@44064: by (simp add: divide_inverse) huffman@44064: huffman@44064: lemma nonzero_minus_divide_right: "b \ 0 ==> - (a / b) = a / (- b)" huffman@44064: by (simp add: divide_inverse nonzero_inverse_minus_eq) huffman@44064: huffman@44064: lemma nonzero_minus_divide_divide: "b \ 0 ==> (-a) / (-b) = a / b" huffman@44064: by (simp add: divide_inverse nonzero_inverse_minus_eq) huffman@44064: huffman@44064: lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)" huffman@44064: by (simp add: divide_inverse) huffman@44064: huffman@44064: lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" huffman@44064: by (simp add: diff_minus add_divide_distrib) huffman@44064: huffman@44064: lemma nonzero_eq_divide_eq [field_simps]: "c \ 0 \ a = b / c \ a * c = b" huffman@44064: proof - huffman@44064: assume [simp]: "c \ 0" huffman@44064: have "a = b / c \ a * c = (b / c) * c" by simp huffman@44064: also have "... \ a * c = b" by (simp add: divide_inverse mult_assoc) huffman@44064: finally show ?thesis . huffman@44064: qed huffman@44064: huffman@44064: lemma nonzero_divide_eq_eq [field_simps]: "c \ 0 \ b / c = a \ b = a * c" huffman@44064: proof - huffman@44064: assume [simp]: "c \ 0" huffman@44064: have "b / c = a \ (b / c) * c = a * c" by simp huffman@44064: also have "... \ b = a * c" by (simp add: divide_inverse mult_assoc) huffman@44064: finally show ?thesis . huffman@44064: qed huffman@44064: huffman@44064: lemma divide_eq_imp: "c \ 0 \ b = a * c \ b / c = a" huffman@44064: by (simp add: divide_inverse mult_assoc) huffman@44064: huffman@44064: lemma eq_divide_imp: "c \ 0 \ a * c = b \ a = b / c" huffman@44064: by (drule sym) (simp add: divide_inverse mult_assoc) huffman@44064: huffman@44064: end huffman@44064: huffman@44064: class division_ring_inverse_zero = division_ring + huffman@44064: assumes inverse_zero [simp]: "inverse 0 = 0" huffman@44064: begin huffman@44064: huffman@44064: lemma divide_zero [simp]: huffman@44064: "a / 0 = 0" huffman@44064: by (simp add: divide_inverse) huffman@44064: huffman@44064: lemma divide_self_if [simp]: huffman@44064: "a / a = (if a = 0 then 0 else 1)" huffman@44064: by simp huffman@44064: huffman@44064: lemma inverse_nonzero_iff_nonzero [simp]: huffman@44064: "inverse a = 0 \ a = 0" huffman@44064: by rule (fact inverse_zero_imp_zero, simp) huffman@44064: huffman@44064: lemma inverse_minus_eq [simp]: huffman@44064: "inverse (- a) = - inverse a" huffman@44064: proof cases huffman@44064: assume "a=0" thus ?thesis by simp huffman@44064: next huffman@44064: assume "a\0" huffman@44064: thus ?thesis by (simp add: nonzero_inverse_minus_eq) huffman@44064: qed huffman@44064: huffman@44064: lemma inverse_inverse_eq [simp]: huffman@44064: "inverse (inverse a) = a" huffman@44064: proof cases huffman@44064: assume "a=0" thus ?thesis by simp huffman@44064: next huffman@44064: assume "a\0" huffman@44064: thus ?thesis by (simp add: nonzero_inverse_inverse_eq) huffman@44064: qed huffman@44064: huffman@44680: lemma inverse_eq_imp_eq: huffman@44680: "inverse a = inverse b \ a = b" huffman@44680: by (drule arg_cong [where f="inverse"], simp) huffman@44680: huffman@44680: lemma inverse_eq_iff_eq [simp]: huffman@44680: "inverse a = inverse b \ a = b" huffman@44680: by (force dest!: inverse_eq_imp_eq) huffman@44680: huffman@44064: end huffman@44064: huffman@44064: subsection {* Fields *} huffman@44064: huffman@22987: class field = comm_ring_1 + inverse + haftmann@35084: assumes field_inverse: "a \ 0 \ inverse a * a = 1" haftmann@35084: assumes field_divide_inverse: "a / b = a * inverse b" haftmann@25267: begin huffman@20496: haftmann@25267: subclass division_ring haftmann@28823: proof huffman@22987: fix a :: 'a huffman@22987: assume "a \ 0" huffman@22987: thus "inverse a * a = 1" by (rule field_inverse) huffman@22987: thus "a * inverse a = 1" by (simp only: mult_commute) haftmann@35084: next haftmann@35084: fix a b :: 'a haftmann@35084: show "a / b = a * inverse b" by (rule field_divide_inverse) obua@14738: qed haftmann@25230: huffman@27516: subclass idom .. haftmann@25230: huffman@30630: text{*There is no slick version using division by zero.*} huffman@30630: lemma inverse_add: huffman@30630: "[| a \ 0; b \ 0 |] huffman@30630: ==> inverse a + inverse b = (a + b) * inverse a * inverse b" huffman@30630: by (simp add: division_ring_inverse_add mult_ac) huffman@30630: blanchet@35828: lemma nonzero_mult_divide_mult_cancel_left [simp, no_atp]: huffman@30630: assumes [simp]: "b\0" and [simp]: "c\0" shows "(c*a)/(c*b) = a/b" huffman@30630: proof - huffman@30630: have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" huffman@30630: by (simp add: divide_inverse nonzero_inverse_mult_distrib) huffman@30630: also have "... = a * inverse b * (inverse c * c)" huffman@30630: by (simp only: mult_ac) huffman@30630: also have "... = a * inverse b" by simp huffman@30630: finally show ?thesis by (simp add: divide_inverse) huffman@30630: qed huffman@30630: blanchet@35828: lemma nonzero_mult_divide_mult_cancel_right [simp, no_atp]: huffman@30630: "\b \ 0; c \ 0\ \ (a * c) / (b * c) = a / b" huffman@30630: by (simp add: mult_commute [of _ c]) huffman@30630: haftmann@36304: lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c" haftmann@36301: by (simp add: divide_inverse mult_ac) huffman@30630: huffman@44921: text{*It's not obvious whether @{text times_divide_eq} should be huffman@44921: simprules or not. Their effect is to gather terms into one big huffman@44921: fraction, like a*b*c / x*y*z. The rationale for that is unclear, but huffman@44921: many proofs seem to need them.*} huffman@44921: blanchet@35828: lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left huffman@30630: huffman@30630: lemma add_frac_eq: huffman@30630: assumes "y \ 0" and "z \ 0" huffman@30630: shows "x / y + w / z = (x * z + w * y) / (y * z)" huffman@30630: proof - huffman@30630: have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)" huffman@30630: using assms by simp huffman@30630: also have "\ = (x * z + y * w) / (y * z)" huffman@30630: by (simp only: add_divide_distrib) huffman@30630: finally show ?thesis huffman@30630: by (simp only: mult_commute) huffman@30630: qed huffman@30630: huffman@30630: text{*Special Cancellation Simprules for Division*} huffman@30630: blanchet@35828: lemma nonzero_mult_divide_cancel_right [simp, no_atp]: huffman@30630: "b \ 0 \ a * b / b = a" haftmann@36301: using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp huffman@30630: blanchet@35828: lemma nonzero_mult_divide_cancel_left [simp, no_atp]: huffman@30630: "a \ 0 \ a * b / a = b" huffman@30630: using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp huffman@30630: blanchet@35828: lemma nonzero_divide_mult_cancel_right [simp, no_atp]: huffman@30630: "\a \ 0; b \ 0\ \ b / (a * b) = 1 / a" huffman@30630: using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp huffman@30630: blanchet@35828: lemma nonzero_divide_mult_cancel_left [simp, no_atp]: huffman@30630: "\a \ 0; b \ 0\ \ a / (a * b) = 1 / b" huffman@30630: using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp huffman@30630: blanchet@35828: lemma nonzero_mult_divide_mult_cancel_left2 [simp, no_atp]: huffman@30630: "\b \ 0; c \ 0\ \ (c * a) / (b * c) = a / b" huffman@30630: using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac) huffman@30630: blanchet@35828: lemma nonzero_mult_divide_mult_cancel_right2 [simp, no_atp]: huffman@30630: "\b \ 0; c \ 0\ \ (a * c) / (c * b) = a / b" huffman@30630: using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac) huffman@30630: haftmann@36348: lemma add_divide_eq_iff [field_simps]: huffman@30630: "z \ 0 \ x + y / z = (z * x + y) / z" haftmann@36301: by (simp add: add_divide_distrib) huffman@30630: haftmann@36348: lemma divide_add_eq_iff [field_simps]: huffman@30630: "z \ 0 \ x / z + y = (x + z * y) / z" haftmann@36301: by (simp add: add_divide_distrib) huffman@30630: haftmann@36348: lemma diff_divide_eq_iff [field_simps]: huffman@30630: "z \ 0 \ x - y / z = (z * x - y) / z" haftmann@36301: by (simp add: diff_divide_distrib) huffman@30630: haftmann@36348: lemma divide_diff_eq_iff [field_simps]: huffman@30630: "z \ 0 \ x / z - y = (x - z * y) / z" haftmann@36301: by (simp add: diff_divide_distrib) huffman@30630: huffman@30630: lemma diff_frac_eq: huffman@30630: "y \ 0 \ z \ 0 \ x / y - w / z = (x * z - w * y) / (y * z)" haftmann@36348: by (simp add: field_simps) huffman@30630: huffman@30630: lemma frac_eq_eq: huffman@30630: "y \ 0 \ z \ 0 \ (x / y = w / z) = (x * z = w * y)" haftmann@36348: by (simp add: field_simps) haftmann@36348: haftmann@36348: end haftmann@36348: haftmann@36348: class field_inverse_zero = field + haftmann@36348: assumes field_inverse_zero: "inverse 0 = 0" haftmann@36348: begin haftmann@36348: haftmann@36348: subclass division_ring_inverse_zero proof haftmann@36348: qed (fact field_inverse_zero) haftmann@25230: paulson@14270: text{*This version builds in division by zero while also re-orienting paulson@14270: the right-hand side.*} paulson@14270: lemma inverse_mult_distrib [simp]: haftmann@36409: "inverse (a * b) = inverse a * inverse b" haftmann@36409: proof cases haftmann@36409: assume "a \ 0 & b \ 0" haftmann@36409: thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac) haftmann@36409: next haftmann@36409: assume "~ (a \ 0 & b \ 0)" haftmann@36409: thus ?thesis by force haftmann@36409: qed paulson@14270: paulson@14365: lemma inverse_divide [simp]: haftmann@36409: "inverse (a / b) = b / a" haftmann@36301: by (simp add: divide_inverse mult_commute) paulson@14365: wenzelm@23389: haftmann@36301: text {* Calculations with fractions *} avigad@16775: nipkow@23413: text{* There is a whole bunch of simp-rules just for class @{text nipkow@23413: field} but none for class @{text field} and @{text nonzero_divides} nipkow@23413: because the latter are covered by a simproc. *} nipkow@23413: nipkow@23413: lemma mult_divide_mult_cancel_left: haftmann@36409: "c \ 0 \ (c * a) / (c * b) = a / b" haftmann@21328: apply (cases "b = 0") huffman@35216: apply simp_all paulson@14277: done paulson@14277: nipkow@23413: lemma mult_divide_mult_cancel_right: haftmann@36409: "c \ 0 \ (a * c) / (b * c) = a / b" haftmann@21328: apply (cases "b = 0") huffman@35216: apply simp_all paulson@14321: done nipkow@23413: haftmann@36409: lemma divide_divide_eq_right [simp, no_atp]: haftmann@36409: "a / (b / c) = (a * c) / b" haftmann@36409: by (simp add: divide_inverse mult_ac) paulson@14288: haftmann@36409: lemma divide_divide_eq_left [simp, no_atp]: haftmann@36409: "(a / b) / c = a / (b * c)" haftmann@36409: by (simp add: divide_inverse mult_assoc) paulson@14288: wenzelm@23389: haftmann@36301: text {*Special Cancellation Simprules for Division*} paulson@15234: haftmann@36409: lemma mult_divide_mult_cancel_left_if [simp,no_atp]: haftmann@36409: shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)" haftmann@36409: by (simp add: mult_divide_mult_cancel_left) nipkow@23413: paulson@15234: haftmann@36301: text {* Division and Unary Minus *} paulson@14293: haftmann@36409: lemma minus_divide_right: haftmann@36409: "- (a / b) = a / - b" haftmann@36409: by (simp add: divide_inverse) paulson@14430: blanchet@35828: lemma divide_minus_right [simp, no_atp]: haftmann@36409: "a / - b = - (a / b)" haftmann@36409: by (simp add: divide_inverse) huffman@30630: huffman@30630: lemma minus_divide_divide: haftmann@36409: "(- a) / (- b) = a / b" haftmann@21328: apply (cases "b=0", simp) paulson@14293: apply (simp add: nonzero_minus_divide_divide) paulson@14293: done paulson@14293: nipkow@23482: lemma eq_divide_eq: haftmann@36409: "a = b / c \ (if c \ 0 then a * c = b else a = 0)" haftmann@36409: by (simp add: nonzero_eq_divide_eq) nipkow@23482: nipkow@23482: lemma divide_eq_eq: haftmann@36409: "b / c = a \ (if c \ 0 then b = a * c else a = 0)" haftmann@36409: by (force simp add: nonzero_divide_eq_eq) paulson@14293: haftmann@36301: lemma inverse_eq_1_iff [simp]: haftmann@36409: "inverse x = 1 \ x = 1" haftmann@36409: by (insert inverse_eq_iff_eq [of x 1], simp) wenzelm@23389: haftmann@36409: lemma divide_eq_0_iff [simp, no_atp]: haftmann@36409: "a / b = 0 \ a = 0 \ b = 0" haftmann@36409: by (simp add: divide_inverse) haftmann@36301: haftmann@36409: lemma divide_cancel_right [simp, no_atp]: haftmann@36409: "a / c = b / c \ c = 0 \ a = b" haftmann@36409: apply (cases "c=0", simp) haftmann@36409: apply (simp add: divide_inverse) haftmann@36409: done haftmann@36301: haftmann@36409: lemma divide_cancel_left [simp, no_atp]: haftmann@36409: "c / a = c / b \ c = 0 \ a = b" haftmann@36409: apply (cases "c=0", simp) haftmann@36409: apply (simp add: divide_inverse) haftmann@36409: done haftmann@36301: haftmann@36409: lemma divide_eq_1_iff [simp, no_atp]: haftmann@36409: "a / b = 1 \ b \ 0 \ a = b" haftmann@36409: apply (cases "b=0", simp) haftmann@36409: apply (simp add: right_inverse_eq) haftmann@36409: done haftmann@36301: haftmann@36409: lemma one_eq_divide_iff [simp, no_atp]: haftmann@36409: "1 = a / b \ b \ 0 \ a = b" haftmann@36409: by (simp add: eq_commute [of 1]) haftmann@36409: haftmann@36719: lemma times_divide_times_eq: haftmann@36719: "(x / y) * (z / w) = (x * z) / (y * w)" haftmann@36719: by simp haftmann@36719: haftmann@36719: lemma add_frac_num: haftmann@36719: "y \ 0 \ x / y + z = (x + z * y) / y" haftmann@36719: by (simp add: add_divide_distrib) haftmann@36719: haftmann@36719: lemma add_num_frac: haftmann@36719: "y \ 0 \ z + x / y = (x + z * y) / y" haftmann@36719: by (simp add: add_divide_distrib add.commute) haftmann@36719: haftmann@36409: end haftmann@36301: haftmann@36301: huffman@44064: subsection {* Ordered fields *} haftmann@36301: haftmann@36301: class linordered_field = field + linordered_idom haftmann@36301: begin paulson@14268: paulson@14277: lemma positive_imp_inverse_positive: haftmann@36301: assumes a_gt_0: "0 < a" haftmann@36301: shows "0 < inverse a" nipkow@23482: proof - paulson@14268: have "0 < a * inverse a" haftmann@36301: by (simp add: a_gt_0 [THEN less_imp_not_eq2]) paulson@14268: thus "0 < inverse a" haftmann@36301: by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff) nipkow@23482: qed paulson@14268: paulson@14277: lemma negative_imp_inverse_negative: haftmann@36301: "a < 0 \ inverse a < 0" haftmann@36301: by (insert positive_imp_inverse_positive [of "-a"], haftmann@36301: simp add: nonzero_inverse_minus_eq less_imp_not_eq) paulson@14268: paulson@14268: lemma inverse_le_imp_le: haftmann@36301: assumes invle: "inverse a \ inverse b" and apos: "0 < a" haftmann@36301: shows "b \ a" nipkow@23482: proof (rule classical) paulson@14268: assume "~ b \ a" nipkow@23482: hence "a < b" by (simp add: linorder_not_le) haftmann@36301: hence bpos: "0 < b" by (blast intro: apos less_trans) paulson@14268: hence "a * inverse a \ a * inverse b" haftmann@36301: by (simp add: apos invle less_imp_le mult_left_mono) paulson@14268: hence "(a * inverse a) * b \ (a * inverse b) * b" haftmann@36301: by (simp add: bpos less_imp_le mult_right_mono) haftmann@36301: thus "b \ a" by (simp add: mult_assoc apos bpos less_imp_not_eq2) nipkow@23482: qed paulson@14268: paulson@14277: lemma inverse_positive_imp_positive: haftmann@36301: assumes inv_gt_0: "0 < inverse a" and nz: "a \ 0" haftmann@36301: shows "0 < a" wenzelm@23389: proof - paulson@14277: have "0 < inverse (inverse a)" wenzelm@23389: using inv_gt_0 by (rule positive_imp_inverse_positive) paulson@14277: thus "0 < a" wenzelm@23389: using nz by (simp add: nonzero_inverse_inverse_eq) wenzelm@23389: qed paulson@14277: haftmann@36301: lemma inverse_negative_imp_negative: haftmann@36301: assumes inv_less_0: "inverse a < 0" and nz: "a \ 0" haftmann@36301: shows "a < 0" haftmann@36301: proof - haftmann@36301: have "inverse (inverse a) < 0" haftmann@36301: using inv_less_0 by (rule negative_imp_inverse_negative) haftmann@36301: thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq) haftmann@36301: qed haftmann@36301: haftmann@36301: lemma linordered_field_no_lb: haftmann@36301: "\x. \y. y < x" haftmann@36301: proof haftmann@36301: fix x::'a haftmann@36301: have m1: "- (1::'a) < 0" by simp haftmann@36301: from add_strict_right_mono[OF m1, where c=x] haftmann@36301: have "(- 1) + x < x" by simp haftmann@36301: thus "\y. y < x" by blast haftmann@36301: qed haftmann@36301: haftmann@36301: lemma linordered_field_no_ub: haftmann@36301: "\ x. \y. y > x" haftmann@36301: proof haftmann@36301: fix x::'a haftmann@36301: have m1: " (1::'a) > 0" by simp haftmann@36301: from add_strict_right_mono[OF m1, where c=x] haftmann@36301: have "1 + x > x" by simp haftmann@36301: thus "\y. y > x" by blast haftmann@36301: qed haftmann@36301: haftmann@36301: lemma less_imp_inverse_less: haftmann@36301: assumes less: "a < b" and apos: "0 < a" haftmann@36301: shows "inverse b < inverse a" haftmann@36301: proof (rule ccontr) haftmann@36301: assume "~ inverse b < inverse a" haftmann@36301: hence "inverse a \ inverse b" by simp haftmann@36301: hence "~ (a < b)" haftmann@36301: by (simp add: not_less inverse_le_imp_le [OF _ apos]) haftmann@36301: thus False by (rule notE [OF _ less]) haftmann@36301: qed haftmann@36301: haftmann@36301: lemma inverse_less_imp_less: haftmann@36301: "inverse a < inverse b \ 0 < a \ b < a" haftmann@36301: apply (simp add: less_le [of "inverse a"] less_le [of "b"]) haftmann@36301: apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) haftmann@36301: done haftmann@36301: haftmann@36301: text{*Both premises are essential. Consider -1 and 1.*} haftmann@36301: lemma inverse_less_iff_less [simp,no_atp]: haftmann@36301: "0 < a \ 0 < b \ inverse a < inverse b \ b < a" haftmann@36301: by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) haftmann@36301: haftmann@36301: lemma le_imp_inverse_le: haftmann@36301: "a \ b \ 0 < a \ inverse b \ inverse a" haftmann@36301: by (force simp add: le_less less_imp_inverse_less) haftmann@36301: haftmann@36301: lemma inverse_le_iff_le [simp,no_atp]: haftmann@36301: "0 < a \ 0 < b \ inverse a \ inverse b \ b \ a" haftmann@36301: by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) haftmann@36301: haftmann@36301: haftmann@36301: text{*These results refer to both operands being negative. The opposite-sign haftmann@36301: case is trivial, since inverse preserves signs.*} haftmann@36301: lemma inverse_le_imp_le_neg: haftmann@36301: "inverse a \ inverse b \ b < 0 \ b \ a" haftmann@36301: apply (rule classical) haftmann@36301: apply (subgoal_tac "a < 0") haftmann@36301: prefer 2 apply force haftmann@36301: apply (insert inverse_le_imp_le [of "-b" "-a"]) haftmann@36301: apply (simp add: nonzero_inverse_minus_eq) haftmann@36301: done haftmann@36301: haftmann@36301: lemma less_imp_inverse_less_neg: haftmann@36301: "a < b \ b < 0 \ inverse b < inverse a" haftmann@36301: apply (subgoal_tac "a < 0") haftmann@36301: prefer 2 apply (blast intro: less_trans) haftmann@36301: apply (insert less_imp_inverse_less [of "-b" "-a"]) haftmann@36301: apply (simp add: nonzero_inverse_minus_eq) haftmann@36301: done haftmann@36301: haftmann@36301: lemma inverse_less_imp_less_neg: haftmann@36301: "inverse a < inverse b \ b < 0 \ b < a" haftmann@36301: apply (rule classical) haftmann@36301: apply (subgoal_tac "a < 0") haftmann@36301: prefer 2 haftmann@36301: apply force haftmann@36301: apply (insert inverse_less_imp_less [of "-b" "-a"]) haftmann@36301: apply (simp add: nonzero_inverse_minus_eq) haftmann@36301: done haftmann@36301: haftmann@36301: lemma inverse_less_iff_less_neg [simp,no_atp]: haftmann@36301: "a < 0 \ b < 0 \ inverse a < inverse b \ b < a" haftmann@36301: apply (insert inverse_less_iff_less [of "-b" "-a"]) haftmann@36301: apply (simp del: inverse_less_iff_less haftmann@36301: add: nonzero_inverse_minus_eq) haftmann@36301: done haftmann@36301: haftmann@36301: lemma le_imp_inverse_le_neg: haftmann@36301: "a \ b \ b < 0 ==> inverse b \ inverse a" haftmann@36301: by (force simp add: le_less less_imp_inverse_less_neg) haftmann@36301: haftmann@36301: lemma inverse_le_iff_le_neg [simp,no_atp]: haftmann@36301: "a < 0 \ b < 0 \ inverse a \ inverse b \ b \ a" haftmann@36301: by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) haftmann@36301: huffman@36774: lemma one_less_inverse: huffman@36774: "0 < a \ a < 1 \ 1 < inverse a" huffman@36774: using less_imp_inverse_less [of a 1, unfolded inverse_1] . huffman@36774: huffman@36774: lemma one_le_inverse: huffman@36774: "0 < a \ a \ 1 \ 1 \ inverse a" huffman@36774: using le_imp_inverse_le [of a 1, unfolded inverse_1] . huffman@36774: haftmann@36348: lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \ b/c) = (a*c \ b)" haftmann@36301: proof - haftmann@36301: assume less: "0 b/c) = (a*c \ (b/c)*c)" haftmann@36304: by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq) haftmann@36301: also have "... = (a*c \ b)" haftmann@36301: by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) haftmann@36301: finally show ?thesis . haftmann@36301: qed haftmann@36301: haftmann@36348: lemma neg_le_divide_eq [field_simps]: "c < 0 ==> (a \ b/c) = (b \ a*c)" haftmann@36301: proof - haftmann@36301: assume less: "c<0" haftmann@36301: hence "(a \ b/c) = ((b/c)*c \ a*c)" haftmann@36304: by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq) haftmann@36301: also have "... = (b \ a*c)" haftmann@36301: by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) haftmann@36301: finally show ?thesis . haftmann@36301: qed haftmann@36301: haftmann@36348: lemma pos_less_divide_eq [field_simps]: haftmann@36301: "0 < c ==> (a < b/c) = (a*c < b)" haftmann@36301: proof - haftmann@36301: assume less: "0 (a < b/c) = (b < a*c)" haftmann@36301: proof - haftmann@36301: assume less: "c<0" haftmann@36301: hence "(a < b/c) = ((b/c)*c < a*c)" haftmann@36304: by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq) haftmann@36301: also have "... = (b < a*c)" haftmann@36301: by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) haftmann@36301: finally show ?thesis . haftmann@36301: qed haftmann@36301: haftmann@36348: lemma pos_divide_less_eq [field_simps]: haftmann@36301: "0 < c ==> (b/c < a) = (b < a*c)" haftmann@36301: proof - haftmann@36301: assume less: "0 (b/c < a) = (a*c < b)" haftmann@36301: proof - haftmann@36301: assume less: "c<0" haftmann@36301: hence "(b/c < a) = (a*c < (b/c)*c)" haftmann@36304: by (simp add: mult_less_cancel_right_disj less_not_sym [OF less] del: times_divide_eq) haftmann@36301: also have "... = (a*c < b)" haftmann@36301: by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) haftmann@36301: finally show ?thesis . haftmann@36301: qed haftmann@36301: haftmann@36348: lemma pos_divide_le_eq [field_simps]: "0 < c ==> (b/c \ a) = (b \ a*c)" haftmann@36301: proof - haftmann@36301: assume less: "0 a) = ((b/c)*c \ a*c)" haftmann@36304: by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq) haftmann@36301: also have "... = (b \ a*c)" haftmann@36301: by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) haftmann@36301: finally show ?thesis . haftmann@36301: qed haftmann@36301: haftmann@36348: lemma neg_divide_le_eq [field_simps]: "c < 0 ==> (b/c \ a) = (a*c \ b)" haftmann@36301: proof - haftmann@36301: assume less: "c<0" haftmann@36301: hence "(b/c \ a) = (a*c \ (b/c)*c)" haftmann@36304: by (simp add: mult_le_cancel_right less_not_sym [OF less] del: times_divide_eq) haftmann@36301: also have "... = (a*c \ b)" haftmann@36301: by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) haftmann@36301: finally show ?thesis . haftmann@36301: qed haftmann@36301: haftmann@36301: text{* Lemmas @{text sign_simps} is a first attempt to automate proofs haftmann@36301: of positivity/negativity needed for @{text field_simps}. Have not added @{text haftmann@36301: sign_simps} to @{text field_simps} because the former can lead to case haftmann@36301: explosions. *} haftmann@36301: haftmann@36348: lemmas sign_simps [no_atp] = algebra_simps haftmann@36348: zero_less_mult_iff mult_less_0_iff haftmann@36348: haftmann@36348: lemmas (in -) sign_simps [no_atp] = algebra_simps haftmann@36301: zero_less_mult_iff mult_less_0_iff haftmann@36301: haftmann@36301: (* Only works once linear arithmetic is installed: haftmann@36301: text{*An example:*} haftmann@36301: lemma fixes a b c d e f :: "'a::linordered_field" haftmann@36301: shows "\a>b; c \ haftmann@36301: ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < haftmann@36301: ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u" haftmann@36301: apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0") haftmann@36301: prefer 2 apply(simp add:sign_simps) haftmann@36301: apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0") haftmann@36301: prefer 2 apply(simp add:sign_simps) haftmann@36301: apply(simp add:field_simps) haftmann@36301: done haftmann@36301: *) haftmann@36301: haftmann@36301: lemma divide_pos_pos: haftmann@36301: "0 < x ==> 0 < y ==> 0 < x / y" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma divide_nonneg_pos: haftmann@36301: "0 <= x ==> 0 < y ==> 0 <= x / y" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma divide_neg_pos: haftmann@36301: "x < 0 ==> 0 < y ==> x / y < 0" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma divide_nonpos_pos: haftmann@36301: "x <= 0 ==> 0 < y ==> x / y <= 0" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma divide_pos_neg: haftmann@36301: "0 < x ==> y < 0 ==> x / y < 0" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma divide_nonneg_neg: haftmann@36301: "0 <= x ==> y < 0 ==> x / y <= 0" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma divide_neg_neg: haftmann@36301: "x < 0 ==> y < 0 ==> 0 < x / y" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma divide_nonpos_neg: haftmann@36301: "x <= 0 ==> y < 0 ==> 0 <= x / y" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma divide_strict_right_mono: haftmann@36301: "[|a < b; 0 < c|] ==> a / c < b / c" haftmann@36301: by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono haftmann@36301: positive_imp_inverse_positive) haftmann@36301: haftmann@36301: haftmann@36301: lemma divide_strict_right_mono_neg: haftmann@36301: "[|b < a; c < 0|] ==> a / c < b / c" haftmann@36301: apply (drule divide_strict_right_mono [of _ _ "-c"], simp) haftmann@36301: apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric]) haftmann@36301: done haftmann@36301: haftmann@36301: text{*The last premise ensures that @{term a} and @{term b} haftmann@36301: have the same sign*} haftmann@36301: lemma divide_strict_left_mono: haftmann@36301: "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b" huffman@44921: by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono) haftmann@36301: haftmann@36301: lemma divide_left_mono: haftmann@36301: "[|b \ a; 0 \ c; 0 < a*b|] ==> c / a \ c / b" huffman@44921: by (auto simp: field_simps zero_less_mult_iff mult_right_mono) haftmann@36301: haftmann@36301: lemma divide_strict_left_mono_neg: haftmann@36301: "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b" huffman@44921: by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg) haftmann@36301: haftmann@36301: lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==> haftmann@36301: x / y <= z" haftmann@36301: by (subst pos_divide_le_eq, assumption+) haftmann@36301: haftmann@36301: lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==> haftmann@36301: z <= x / y" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==> haftmann@36301: x / y < z" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==> haftmann@36301: z < x / y" haftmann@36301: by(simp add:field_simps) haftmann@36301: haftmann@36301: lemma frac_le: "0 <= x ==> haftmann@36301: x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" haftmann@36301: apply (rule mult_imp_div_pos_le) haftmann@36301: apply simp haftmann@36301: apply (subst times_divide_eq_left) haftmann@36301: apply (rule mult_imp_le_div_pos, assumption) haftmann@36301: apply (rule mult_mono) haftmann@36301: apply simp_all haftmann@36301: done haftmann@36301: haftmann@36301: lemma frac_less: "0 <= x ==> haftmann@36301: x < y ==> 0 < w ==> w <= z ==> x / z < y / w" haftmann@36301: apply (rule mult_imp_div_pos_less) haftmann@36301: apply simp haftmann@36301: apply (subst times_divide_eq_left) haftmann@36301: apply (rule mult_imp_less_div_pos, assumption) haftmann@36301: apply (erule mult_less_le_imp_less) haftmann@36301: apply simp_all haftmann@36301: done haftmann@36301: haftmann@36301: lemma frac_less2: "0 < x ==> haftmann@36301: x <= y ==> 0 < w ==> w < z ==> x / z < y / w" haftmann@36301: apply (rule mult_imp_div_pos_less) haftmann@36301: apply simp_all haftmann@36301: apply (rule mult_imp_less_div_pos, assumption) haftmann@36301: apply (erule mult_le_less_imp_less) haftmann@36301: apply simp_all haftmann@36301: done haftmann@36301: haftmann@36301: lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)" haftmann@36301: by (simp add: field_simps zero_less_two) haftmann@36301: haftmann@36301: lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b" haftmann@36301: by (simp add: field_simps zero_less_two) haftmann@36301: haftmann@36301: subclass dense_linorder haftmann@36301: proof haftmann@36301: fix x y :: 'a haftmann@36301: from less_add_one show "\y. x < y" .. haftmann@36301: from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono) haftmann@36301: then have "x - 1 < x + 1 - 1" by (simp only: diff_minus [symmetric]) haftmann@36301: then have "x - 1 < x" by (simp add: algebra_simps) haftmann@36301: then show "\y. y < x" .. haftmann@36301: show "x < y \ \z>x. z < y" by (blast intro!: less_half_sum gt_half_sum) haftmann@36301: qed haftmann@36301: haftmann@36301: lemma nonzero_abs_inverse: haftmann@36301: "a \ 0 ==> \inverse a\ = inverse \a\" haftmann@36301: apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq haftmann@36301: negative_imp_inverse_negative) haftmann@36301: apply (blast intro: positive_imp_inverse_positive elim: less_asym) haftmann@36301: done haftmann@36301: haftmann@36301: lemma nonzero_abs_divide: haftmann@36301: "b \ 0 ==> \a / b\ = \a\ / \b\" haftmann@36301: by (simp add: divide_inverse abs_mult nonzero_abs_inverse) haftmann@36301: haftmann@36301: lemma field_le_epsilon: haftmann@36301: assumes e: "\e. 0 < e \ x \ y + e" haftmann@36301: shows "x \ y" haftmann@36301: proof (rule dense_le) haftmann@36301: fix t assume "t < x" haftmann@36301: hence "0 < x - t" by (simp add: less_diff_eq) haftmann@36301: from e [OF this] have "x + 0 \ x + (y - t)" by (simp add: algebra_simps) haftmann@36301: then have "0 \ y - t" by (simp only: add_le_cancel_left) haftmann@36301: then show "t \ y" by (simp add: algebra_simps) haftmann@36301: qed haftmann@36301: haftmann@36301: end haftmann@36301: haftmann@36414: class linordered_field_inverse_zero = linordered_field + field_inverse_zero haftmann@36348: begin haftmann@36348: haftmann@36301: lemma le_divide_eq: haftmann@36301: "(a \ b/c) = haftmann@36301: (if 0 < c then a*c \ b haftmann@36301: else if c < 0 then b \ a*c haftmann@36409: else a \ 0)" haftmann@36301: apply (cases "c=0", simp) haftmann@36301: apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) haftmann@36301: done haftmann@36301: paulson@14277: lemma inverse_positive_iff_positive [simp]: haftmann@36409: "(0 < inverse a) = (0 < a)" haftmann@21328: apply (cases "a = 0", simp) paulson@14277: apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) paulson@14277: done paulson@14277: paulson@14277: lemma inverse_negative_iff_negative [simp]: haftmann@36409: "(inverse a < 0) = (a < 0)" haftmann@21328: apply (cases "a = 0", simp) paulson@14277: apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative) paulson@14277: done paulson@14277: paulson@14277: lemma inverse_nonnegative_iff_nonnegative [simp]: haftmann@36409: "0 \ inverse a \ 0 \ a" haftmann@36409: by (simp add: not_less [symmetric]) paulson@14277: paulson@14277: lemma inverse_nonpositive_iff_nonpositive [simp]: haftmann@36409: "inverse a \ 0 \ a \ 0" haftmann@36409: by (simp add: not_less [symmetric]) paulson@14277: paulson@14365: lemma one_less_inverse_iff: haftmann@36409: "1 < inverse x \ 0 < x \ x < 1" nipkow@23482: proof cases paulson@14365: assume "0 < x" paulson@14365: with inverse_less_iff_less [OF zero_less_one, of x] paulson@14365: show ?thesis by simp paulson@14365: next paulson@14365: assume notless: "~ (0 < x)" paulson@14365: have "~ (1 < inverse x)" paulson@14365: proof paulson@14365: assume "1 < inverse x" haftmann@36409: also with notless have "... \ 0" by simp paulson@14365: also have "... < 1" by (rule zero_less_one) paulson@14365: finally show False by auto paulson@14365: qed paulson@14365: with notless show ?thesis by simp paulson@14365: qed paulson@14365: paulson@14365: lemma one_le_inverse_iff: haftmann@36409: "1 \ inverse x \ 0 < x \ x \ 1" haftmann@36409: proof (cases "x = 1") haftmann@36409: case True then show ?thesis by simp haftmann@36409: next haftmann@36409: case False then have "inverse x \ 1" by simp haftmann@36409: then have "1 \ inverse x" by blast haftmann@36409: then have "1 \ inverse x \ 1 < inverse x" by (simp add: le_less) haftmann@36409: with False show ?thesis by (auto simp add: one_less_inverse_iff) haftmann@36409: qed paulson@14365: paulson@14365: lemma inverse_less_1_iff: haftmann@36409: "inverse x < 1 \ x \ 0 \ 1 < x" haftmann@36409: by (simp add: not_le [symmetric] one_le_inverse_iff) paulson@14365: paulson@14365: lemma inverse_le_1_iff: haftmann@36409: "inverse x \ 1 \ x \ 0 \ 1 \ x" haftmann@36409: by (simp add: not_less [symmetric] one_less_inverse_iff) paulson@14365: paulson@14288: lemma divide_le_eq: paulson@14288: "(b/c \ a) = paulson@14288: (if 0 < c then b \ a*c paulson@14288: else if c < 0 then a*c \ b haftmann@36409: else 0 \ a)" haftmann@21328: apply (cases "c=0", simp) haftmann@36409: apply (force simp add: pos_divide_le_eq neg_divide_le_eq) paulson@14288: done paulson@14288: paulson@14288: lemma less_divide_eq: paulson@14288: "(a < b/c) = paulson@14288: (if 0 < c then a*c < b paulson@14288: else if c < 0 then b < a*c haftmann@36409: else a < 0)" haftmann@21328: apply (cases "c=0", simp) haftmann@36409: apply (force simp add: pos_less_divide_eq neg_less_divide_eq) paulson@14288: done paulson@14288: paulson@14288: lemma divide_less_eq: paulson@14288: "(b/c < a) = paulson@14288: (if 0 < c then b < a*c paulson@14288: else if c < 0 then a*c < b haftmann@36409: else 0 < a)" haftmann@21328: apply (cases "c=0", simp) haftmann@36409: apply (force simp add: pos_divide_less_eq neg_divide_less_eq) paulson@14288: done paulson@14288: haftmann@36301: text {*Division and Signs*} avigad@16775: avigad@16775: lemma zero_less_divide_iff: haftmann@36409: "(0 < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" avigad@16775: by (simp add: divide_inverse zero_less_mult_iff) avigad@16775: avigad@16775: lemma divide_less_0_iff: haftmann@36409: "(a/b < 0) = avigad@16775: (0 < a & b < 0 | a < 0 & 0 < b)" avigad@16775: by (simp add: divide_inverse mult_less_0_iff) avigad@16775: avigad@16775: lemma zero_le_divide_iff: haftmann@36409: "(0 \ a/b) = avigad@16775: (0 \ a & 0 \ b | a \ 0 & b \ 0)" avigad@16775: by (simp add: divide_inverse zero_le_mult_iff) avigad@16775: avigad@16775: lemma divide_le_0_iff: haftmann@36409: "(a/b \ 0) = avigad@16775: (0 \ a & b \ 0 | a \ 0 & 0 \ b)" avigad@16775: by (simp add: divide_inverse mult_le_0_iff) avigad@16775: haftmann@36301: text {* Division and the Number One *} paulson@14353: paulson@14353: text{*Simplify expressions equated with 1*} paulson@14353: blanchet@35828: lemma zero_eq_1_divide_iff [simp,no_atp]: haftmann@36409: "(0 = 1/a) = (a = 0)" nipkow@23482: apply (cases "a=0", simp) nipkow@23482: apply (auto simp add: nonzero_eq_divide_eq) paulson@14353: done paulson@14353: blanchet@35828: lemma one_divide_eq_0_iff [simp,no_atp]: haftmann@36409: "(1/a = 0) = (a = 0)" nipkow@23482: apply (cases "a=0", simp) nipkow@23482: apply (insert zero_neq_one [THEN not_sym]) nipkow@23482: apply (auto simp add: nonzero_divide_eq_eq) paulson@14353: done paulson@14353: paulson@14353: text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*} haftmann@36423: haftmann@36423: lemma zero_le_divide_1_iff [simp, no_atp]: haftmann@36423: "0 \ 1 / a \ 0 \ a" haftmann@36423: by (simp add: zero_le_divide_iff) paulson@17085: haftmann@36423: lemma zero_less_divide_1_iff [simp, no_atp]: haftmann@36423: "0 < 1 / a \ 0 < a" haftmann@36423: by (simp add: zero_less_divide_iff) haftmann@36423: haftmann@36423: lemma divide_le_0_1_iff [simp, no_atp]: haftmann@36423: "1 / a \ 0 \ a \ 0" haftmann@36423: by (simp add: divide_le_0_iff) haftmann@36423: haftmann@36423: lemma divide_less_0_1_iff [simp, no_atp]: haftmann@36423: "1 / a < 0 \ a < 0" haftmann@36423: by (simp add: divide_less_0_iff) paulson@14353: paulson@14293: lemma divide_right_mono: haftmann@36409: "[|a \ b; 0 \ c|] ==> a/c \ b/c" haftmann@36409: by (force simp add: divide_strict_right_mono le_less) paulson@14293: haftmann@36409: lemma divide_right_mono_neg: "a <= b avigad@16775: ==> c <= 0 ==> b / c <= a / c" nipkow@23482: apply (drule divide_right_mono [of _ _ "- c"]) nipkow@23482: apply auto avigad@16775: done avigad@16775: haftmann@36409: lemma divide_left_mono_neg: "a <= b avigad@16775: ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" avigad@16775: apply (drule divide_left_mono [of _ _ "- c"]) avigad@16775: apply (auto simp add: mult_commute) avigad@16775: done avigad@16775: hoelzl@42904: lemma inverse_le_iff: hoelzl@42904: "inverse a \ inverse b \ (0 < a * b \ b \ a) \ (a * b \ 0 \ a \ b)" hoelzl@42904: proof - hoelzl@42904: { assume "a < 0" hoelzl@42904: then have "inverse a < 0" by simp hoelzl@42904: moreover assume "0 < b" hoelzl@42904: then have "0 < inverse b" by simp hoelzl@42904: ultimately have "inverse a < inverse b" by (rule less_trans) hoelzl@42904: then have "inverse a \ inverse b" by simp } hoelzl@42904: moreover hoelzl@42904: { assume "b < 0" hoelzl@42904: then have "inverse b < 0" by simp hoelzl@42904: moreover assume "0 < a" hoelzl@42904: then have "0 < inverse a" by simp hoelzl@42904: ultimately have "inverse b < inverse a" by (rule less_trans) hoelzl@42904: then have "\ inverse a \ inverse b" by simp } hoelzl@42904: ultimately show ?thesis hoelzl@42904: by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) hoelzl@42904: (auto simp: not_less zero_less_mult_iff mult_le_0_iff) hoelzl@42904: qed hoelzl@42904: hoelzl@42904: lemma inverse_less_iff: hoelzl@42904: "inverse a < inverse b \ (0 < a * b \ b < a) \ (a * b \ 0 \ a < b)" hoelzl@42904: by (subst less_le) (auto simp: inverse_le_iff) hoelzl@42904: hoelzl@42904: lemma divide_le_cancel: hoelzl@42904: "a / c \ b / c \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" hoelzl@42904: by (simp add: divide_inverse mult_le_cancel_right) hoelzl@42904: hoelzl@42904: lemma divide_less_cancel: hoelzl@42904: "a / c < b / c \ (0 < c \ a < b) \ (c < 0 \ b < a) \ c \ 0" hoelzl@42904: by (auto simp add: divide_inverse mult_less_cancel_right) hoelzl@42904: avigad@16775: text{*Simplify quotients that are compared with the value 1.*} avigad@16775: blanchet@35828: lemma le_divide_eq_1 [no_atp]: haftmann@36409: "(1 \ b / a) = ((0 < a & a \ b) | (a < 0 & b \ a))" avigad@16775: by (auto simp add: le_divide_eq) avigad@16775: blanchet@35828: lemma divide_le_eq_1 [no_atp]: haftmann@36409: "(b / a \ 1) = ((0 < a & b \ a) | (a < 0 & a \ b) | a=0)" avigad@16775: by (auto simp add: divide_le_eq) avigad@16775: blanchet@35828: lemma less_divide_eq_1 [no_atp]: haftmann@36409: "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" avigad@16775: by (auto simp add: less_divide_eq) avigad@16775: blanchet@35828: lemma divide_less_eq_1 [no_atp]: haftmann@36409: "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" avigad@16775: by (auto simp add: divide_less_eq) avigad@16775: wenzelm@23389: haftmann@36301: text {*Conditional Simplification Rules: No Case Splits*} avigad@16775: blanchet@35828: lemma le_divide_eq_1_pos [simp,no_atp]: haftmann@36409: "0 < a \ (1 \ b/a) = (a \ b)" avigad@16775: by (auto simp add: le_divide_eq) avigad@16775: blanchet@35828: lemma le_divide_eq_1_neg [simp,no_atp]: haftmann@36409: "a < 0 \ (1 \ b/a) = (b \ a)" avigad@16775: by (auto simp add: le_divide_eq) avigad@16775: blanchet@35828: lemma divide_le_eq_1_pos [simp,no_atp]: haftmann@36409: "0 < a \ (b/a \ 1) = (b \ a)" avigad@16775: by (auto simp add: divide_le_eq) avigad@16775: blanchet@35828: lemma divide_le_eq_1_neg [simp,no_atp]: haftmann@36409: "a < 0 \ (b/a \ 1) = (a \ b)" avigad@16775: by (auto simp add: divide_le_eq) avigad@16775: blanchet@35828: lemma less_divide_eq_1_pos [simp,no_atp]: haftmann@36409: "0 < a \ (1 < b/a) = (a < b)" avigad@16775: by (auto simp add: less_divide_eq) avigad@16775: blanchet@35828: lemma less_divide_eq_1_neg [simp,no_atp]: haftmann@36409: "a < 0 \ (1 < b/a) = (b < a)" avigad@16775: by (auto simp add: less_divide_eq) avigad@16775: blanchet@35828: lemma divide_less_eq_1_pos [simp,no_atp]: haftmann@36409: "0 < a \ (b/a < 1) = (b < a)" paulson@18649: by (auto simp add: divide_less_eq) paulson@18649: blanchet@35828: lemma divide_less_eq_1_neg [simp,no_atp]: haftmann@36409: "a < 0 \ b/a < 1 <-> a < b" avigad@16775: by (auto simp add: divide_less_eq) avigad@16775: blanchet@35828: lemma eq_divide_eq_1 [simp,no_atp]: haftmann@36409: "(1 = b/a) = ((a \ 0 & a = b))" avigad@16775: by (auto simp add: eq_divide_eq) avigad@16775: blanchet@35828: lemma divide_eq_eq_1 [simp,no_atp]: haftmann@36409: "(b/a = 1) = ((a \ 0 & a = b))" avigad@16775: by (auto simp add: divide_eq_eq) avigad@16775: paulson@14294: lemma abs_inverse [simp]: haftmann@36409: "\inverse a\ = haftmann@36301: inverse \a\" haftmann@21328: apply (cases "a=0", simp) paulson@14294: apply (simp add: nonzero_abs_inverse) paulson@14294: done paulson@14294: paulson@15234: lemma abs_divide [simp]: haftmann@36409: "\a / b\ = \a\ / \b\" haftmann@21328: apply (cases "b=0", simp) paulson@14294: apply (simp add: nonzero_abs_divide) paulson@14294: done paulson@14294: haftmann@36409: lemma abs_div_pos: "0 < y ==> haftmann@36301: \x\ / y = \x / y\" haftmann@25304: apply (subst abs_divide) haftmann@25304: apply (simp add: order_less_imp_le) haftmann@25304: done avigad@16775: hoelzl@35579: lemma field_le_mult_one_interval: hoelzl@35579: assumes *: "\z. \ 0 < z ; z < 1 \ \ z * x \ y" hoelzl@35579: shows "x \ y" hoelzl@35579: proof (cases "0 < x") hoelzl@35579: assume "0 < x" hoelzl@35579: thus ?thesis hoelzl@35579: using dense_le_bounded[of 0 1 "y/x"] * hoelzl@35579: unfolding le_divide_eq if_P[OF `0 < x`] by simp hoelzl@35579: next hoelzl@35579: assume "\0 < x" hence "x \ 0" by simp hoelzl@35579: obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1\'a"] by auto hoelzl@35579: hence "x \ s * x" using mult_le_cancel_right[of 1 x s] `x \ 0` by auto hoelzl@35579: also note *[OF s] hoelzl@35579: finally show ?thesis . hoelzl@35579: qed haftmann@35090: haftmann@36409: end haftmann@36409: haftmann@33364: code_modulename SML haftmann@35050: Fields Arith haftmann@33364: haftmann@33364: code_modulename OCaml haftmann@35050: Fields Arith haftmann@33364: haftmann@33364: code_modulename Haskell haftmann@35050: Fields Arith haftmann@33364: paulson@14265: end