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@22987: class field = comm_ring_1 + inverse + haftmann@25062: assumes field_inverse: "a \ 0 \ inverse a * a = 1" haftmann@25062: assumes 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) obua@14738: qed haftmann@25230: huffman@27516: subclass idom .. haftmann@25230: haftmann@25230: lemma right_inverse_eq: "b \ 0 \ a / b = 1 \ a = b" haftmann@25230: proof haftmann@25230: assume neq: "b \ 0" haftmann@25230: { haftmann@25230: hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac) haftmann@25230: also assume "a / b = 1" haftmann@25230: finally show "a = b" by simp haftmann@25230: next haftmann@25230: assume "a = b" haftmann@25230: with neq show "a / b = 1" by (simp add: divide_inverse) haftmann@25230: } haftmann@25230: qed haftmann@25230: haftmann@25230: lemma nonzero_inverse_eq_divide: "a \ 0 \ inverse a = 1 / a" nipkow@29667: by (simp add: divide_inverse) haftmann@25230: haftmann@25230: lemma divide_self [simp]: "a \ 0 \ a / a = 1" nipkow@29667: by (simp add: divide_inverse) haftmann@25230: haftmann@25230: lemma divide_zero_left [simp]: "0 / a = 0" nipkow@29667: by (simp add: divide_inverse) haftmann@25230: haftmann@25230: lemma inverse_eq_divide: "inverse a = 1 / a" nipkow@29667: by (simp add: divide_inverse) haftmann@25230: haftmann@25230: lemma add_divide_distrib: "(a+b) / c = a/c + b/c" huffman@30630: by (simp add: divide_inverse algebra_simps) huffman@30630: 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: huffman@30630: lemma nonzero_mult_divide_mult_cancel_left [simp, noatp]: 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: huffman@30630: lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]: huffman@30630: "\b \ 0; c \ 0\ \ (a * c) / (b * c) = a / b" huffman@30630: by (simp add: mult_commute [of _ c]) huffman@30630: huffman@30630: lemma divide_1 [simp]: "a / 1 = a" huffman@30630: by (simp add: divide_inverse) huffman@30630: huffman@30630: lemma times_divide_eq_right: "a * (b / c) = (a * b) / c" huffman@30630: by (simp add: divide_inverse mult_assoc) huffman@30630: huffman@30630: lemma times_divide_eq_left: "(b / c) * a = (b * a) / c" huffman@30630: by (simp add: divide_inverse mult_ac) huffman@30630: huffman@30630: text {* These are later declared as simp rules. *} huffman@30630: lemmas times_divide_eq [noatp] = 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: huffman@30630: lemma nonzero_mult_divide_cancel_right [simp, noatp]: huffman@30630: "b \ 0 \ a * b / b = a" huffman@30630: using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp huffman@30630: huffman@30630: lemma nonzero_mult_divide_cancel_left [simp, noatp]: 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: huffman@30630: lemma nonzero_divide_mult_cancel_right [simp, noatp]: 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: huffman@30630: lemma nonzero_divide_mult_cancel_left [simp, noatp]: 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: huffman@30630: lemma nonzero_mult_divide_mult_cancel_left2 [simp, noatp]: 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: huffman@30630: lemma nonzero_mult_divide_mult_cancel_right2 [simp, noatp]: 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: huffman@30630: lemma minus_divide_left: "- (a / b) = (-a) / b" huffman@30630: by (simp add: divide_inverse) huffman@30630: huffman@30630: lemma nonzero_minus_divide_right: "b \ 0 ==> - (a / b) = a / (- b)" huffman@30630: by (simp add: divide_inverse nonzero_inverse_minus_eq) huffman@30630: huffman@30630: lemma nonzero_minus_divide_divide: "b \ 0 ==> (-a) / (-b) = a / b" huffman@30630: by (simp add: divide_inverse nonzero_inverse_minus_eq) huffman@30630: huffman@30630: lemma divide_minus_left [simp, noatp]: "(-a) / b = - (a / b)" huffman@30630: by (simp add: divide_inverse) huffman@30630: huffman@30630: lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" huffman@30630: by (simp add: diff_minus add_divide_distrib) huffman@30630: huffman@30630: lemma add_divide_eq_iff: huffman@30630: "z \ 0 \ x + y / z = (z * x + y) / z" huffman@30630: by (simp add: add_divide_distrib) huffman@30630: huffman@30630: lemma divide_add_eq_iff: huffman@30630: "z \ 0 \ x / z + y = (x + z * y) / z" huffman@30630: by (simp add: add_divide_distrib) huffman@30630: huffman@30630: lemma diff_divide_eq_iff: huffman@30630: "z \ 0 \ x - y / z = (z * x - y) / z" huffman@30630: by (simp add: diff_divide_distrib) huffman@30630: huffman@30630: lemma divide_diff_eq_iff: huffman@30630: "z \ 0 \ x / z - y = (x - z * y) / z" huffman@30630: by (simp add: diff_divide_distrib) huffman@30630: huffman@30630: lemma nonzero_eq_divide_eq: "c \ 0 \ a = b / c \ a * c = b" huffman@30630: proof - huffman@30630: assume [simp]: "c \ 0" huffman@30630: have "a = b / c \ a * c = (b / c) * c" by simp huffman@30630: also have "... \ a * c = b" by (simp add: divide_inverse mult_assoc) huffman@30630: finally show ?thesis . huffman@30630: qed huffman@30630: huffman@30630: lemma nonzero_divide_eq_eq: "c \ 0 \ b / c = a \ b = a * c" huffman@30630: proof - huffman@30630: assume [simp]: "c \ 0" huffman@30630: have "b / c = a \ (b / c) * c = a * c" by simp huffman@30630: also have "... \ b = a * c" by (simp add: divide_inverse mult_assoc) huffman@30630: finally show ?thesis . huffman@30630: qed huffman@30630: huffman@30630: lemma divide_eq_imp: "c \ 0 \ b = a * c \ b / c = a" huffman@30630: by simp huffman@30630: huffman@30630: lemma eq_divide_imp: "c \ 0 \ a * c = b \ a = b / c" huffman@30630: by (erule subst, simp) huffman@30630: huffman@30630: lemmas field_eq_simps[noatp] = algebra_simps huffman@30630: (* pull / out*) huffman@30630: add_divide_eq_iff divide_add_eq_iff huffman@30630: diff_divide_eq_iff divide_diff_eq_iff huffman@30630: (* multiply eqn *) huffman@30630: nonzero_eq_divide_eq nonzero_divide_eq_eq huffman@30630: (* is added later: huffman@30630: times_divide_eq_left times_divide_eq_right huffman@30630: *) huffman@30630: huffman@30630: text{*An example:*} huffman@30630: lemma "\a\b; c\d; e\f\ \ ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1" huffman@30630: apply(subgoal_tac "(c-d)*(e-f)*(a-b) \ 0") huffman@30630: apply(simp add:field_eq_simps) huffman@30630: apply(simp) huffman@30630: done huffman@30630: huffman@30630: lemma diff_frac_eq: huffman@30630: "y \ 0 \ z \ 0 \ x / y - w / z = (x * z - w * y) / (y * z)" huffman@30630: by (simp add: field_eq_simps times_divide_eq) huffman@30630: huffman@30630: lemma frac_eq_eq: huffman@30630: "y \ 0 \ z \ 0 \ (x / y = w / z) = (x * z = w * y)" huffman@30630: by (simp add: field_eq_simps times_divide_eq) haftmann@25230: haftmann@25230: end haftmann@25230: haftmann@22390: class division_by_zero = zero + inverse + haftmann@25062: assumes inverse_zero [simp]: "inverse 0 = 0" paulson@14265: haftmann@25230: lemma divide_zero [simp]: haftmann@25230: "a / 0 = (0::'a::{field,division_by_zero})" nipkow@29667: by (simp add: divide_inverse) haftmann@25230: haftmann@25230: lemma divide_self_if [simp]: haftmann@25230: "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" nipkow@29667: by simp haftmann@25230: haftmann@35028: class linordered_field = field + linordered_idom haftmann@25230: paulson@14268: lemma inverse_nonzero_iff_nonzero [simp]: huffman@20496: "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))" haftmann@26274: by (force dest: inverse_zero_imp_zero) paulson@14268: paulson@14268: lemma inverse_minus_eq [simp]: huffman@20496: "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})" paulson@14377: proof cases paulson@14377: assume "a=0" thus ?thesis by (simp add: inverse_zero) paulson@14377: next paulson@14377: assume "a\0" paulson@14377: thus ?thesis by (simp add: nonzero_inverse_minus_eq) paulson@14377: qed paulson@14268: paulson@14268: lemma inverse_eq_imp_eq: huffman@20496: "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" haftmann@21328: apply (cases "a=0 | b=0") paulson@14268: apply (force dest!: inverse_zero_imp_zero paulson@14268: simp add: eq_commute [of "0::'a"]) paulson@14268: apply (force dest!: nonzero_inverse_eq_imp_eq) paulson@14268: done paulson@14268: paulson@14268: lemma inverse_eq_iff_eq [simp]: huffman@20496: "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))" huffman@20496: by (force dest!: inverse_eq_imp_eq) paulson@14268: paulson@14270: lemma inverse_inverse_eq [simp]: huffman@20496: "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" paulson@14270: proof cases paulson@14270: assume "a=0" thus ?thesis by simp paulson@14270: next paulson@14270: assume "a\0" paulson@14270: thus ?thesis by (simp add: nonzero_inverse_inverse_eq) paulson@14270: qed paulson@14270: 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]: paulson@14270: "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})" paulson@14270: proof cases paulson@14270: assume "a \ 0 & b \ 0" nipkow@29667: thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute) paulson@14270: next paulson@14270: assume "~ (a \ 0 & b \ 0)" nipkow@29667: thus ?thesis by force paulson@14270: qed paulson@14270: paulson@14365: lemma inverse_divide [simp]: nipkow@23477: "inverse (a/b) = b / (a::'a::{field,division_by_zero})" nipkow@23477: by (simp add: divide_inverse mult_commute) paulson@14365: wenzelm@23389: avigad@16775: subsection {* 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: nipkow@23477: "c\0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})" haftmann@21328: apply (cases "b = 0") nipkow@23413: apply (simp_all add: nonzero_mult_divide_mult_cancel_left) paulson@14277: done paulson@14277: nipkow@23413: lemma mult_divide_mult_cancel_right: nipkow@23477: "c\0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})" haftmann@21328: apply (cases "b = 0") nipkow@23413: apply (simp_all add: nonzero_mult_divide_mult_cancel_right) paulson@14321: done nipkow@23413: paulson@24286: lemma divide_divide_eq_right [simp,noatp]: nipkow@23477: "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})" paulson@14430: by (simp add: divide_inverse mult_ac) paulson@14288: paulson@24286: lemma divide_divide_eq_left [simp,noatp]: nipkow@23477: "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)" paulson@14430: by (simp add: divide_inverse mult_assoc) paulson@14288: wenzelm@23389: paulson@15234: subsubsection{*Special Cancellation Simprules for Division*} paulson@15234: paulson@24427: lemma mult_divide_mult_cancel_left_if[simp,noatp]: nipkow@23477: fixes c :: "'a :: {field,division_by_zero}" nipkow@23477: shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)" nipkow@23413: by (simp add: mult_divide_mult_cancel_left) nipkow@23413: paulson@15234: paulson@14293: subsection {* Division and Unary Minus *} paulson@14293: paulson@14293: lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})" huffman@29407: by (simp add: divide_inverse) paulson@14430: huffman@30630: lemma divide_minus_right [simp, noatp]: huffman@30630: "a / -(b::'a::{field,division_by_zero}) = -(a / b)" huffman@30630: by (simp add: divide_inverse) huffman@30630: huffman@30630: lemma minus_divide_divide: nipkow@23477: "(-a)/(-b) = a / (b::'a::{field,division_by_zero})" 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: nipkow@23482: "((a::'a::{field,division_by_zero}) = b/c) = (if c\0 then a*c = b else a=0)" huffman@30630: by (simp add: nonzero_eq_divide_eq) nipkow@23482: nipkow@23482: lemma divide_eq_eq: nipkow@23482: "(b/c = (a::'a::{field,division_by_zero})) = (if c\0 then b = a*c else a=0)" huffman@30630: by (force simp add: nonzero_divide_eq_eq) paulson@14293: wenzelm@23389: paulson@14268: subsection {* Ordered Fields *} paulson@14268: paulson@14277: lemma positive_imp_inverse_positive: haftmann@35028: assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::linordered_field)" nipkow@23482: proof - paulson@14268: have "0 < a * inverse a" paulson@14268: by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one) paulson@14268: thus "0 < inverse a" paulson@14268: by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff) nipkow@23482: qed paulson@14268: paulson@14277: lemma negative_imp_inverse_negative: haftmann@35028: "a < 0 ==> inverse a < (0::'a::linordered_field)" nipkow@23482: by (insert positive_imp_inverse_positive [of "-a"], nipkow@23482: simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) paulson@14268: paulson@14268: lemma inverse_le_imp_le: nipkow@23482: assumes invle: "inverse a \ inverse b" and apos: "0 < a" haftmann@35028: shows "b \ (a::'a::linordered_field)" nipkow@23482: proof (rule classical) paulson@14268: assume "~ b \ a" nipkow@23482: hence "a < b" by (simp add: linorder_not_le) nipkow@23482: hence bpos: "0 < b" by (blast intro: apos order_less_trans) paulson@14268: hence "a * inverse a \ a * inverse b" paulson@14268: by (simp add: apos invle order_less_imp_le mult_left_mono) paulson@14268: hence "(a * inverse a) * b \ (a * inverse b) * b" paulson@14268: by (simp add: bpos order_less_imp_le mult_right_mono) nipkow@23482: thus "b \ a" by (simp add: mult_assoc apos bpos order_less_imp_not_eq2) nipkow@23482: qed paulson@14268: paulson@14277: lemma inverse_positive_imp_positive: nipkow@23482: assumes inv_gt_0: "0 < inverse a" and nz: "a \ 0" haftmann@35028: shows "0 < (a::'a::linordered_field)" 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: paulson@14277: lemma inverse_positive_iff_positive [simp]: haftmann@35028: "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))" 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_imp_negative: nipkow@23482: assumes inv_less_0: "inverse a < 0" and nz: "a \ 0" haftmann@35028: shows "a < (0::'a::linordered_field)" wenzelm@23389: proof - paulson@14277: have "inverse (inverse a) < 0" wenzelm@23389: using inv_less_0 by (rule negative_imp_inverse_negative) nipkow@23482: thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq) wenzelm@23389: qed paulson@14277: paulson@14277: lemma inverse_negative_iff_negative [simp]: haftmann@35028: "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))" 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@35028: "(0 \ inverse a) = (0 \ (a::'a::{linordered_field,division_by_zero}))" paulson@14277: by (simp add: linorder_not_less [symmetric]) paulson@14277: paulson@14277: lemma inverse_nonpositive_iff_nonpositive [simp]: haftmann@35028: "(inverse a \ 0) = (a \ (0::'a::{linordered_field,division_by_zero}))" paulson@14277: by (simp add: linorder_not_less [symmetric]) paulson@14277: haftmann@35043: lemma linordered_field_no_lb: "\ x. \y. y < (x::'a::linordered_field)" chaieb@23406: proof chaieb@23406: fix x::'a chaieb@23406: have m1: "- (1::'a) < 0" by simp chaieb@23406: from add_strict_right_mono[OF m1, where c=x] chaieb@23406: have "(- 1) + x < x" by simp chaieb@23406: thus "\y. y < x" by blast chaieb@23406: qed chaieb@23406: haftmann@35043: lemma linordered_field_no_ub: "\ x. \y. y > (x::'a::linordered_field)" chaieb@23406: proof chaieb@23406: fix x::'a chaieb@23406: have m1: " (1::'a) > 0" by simp chaieb@23406: from add_strict_right_mono[OF m1, where c=x] chaieb@23406: have "1 + x > x" by simp chaieb@23406: thus "\y. y > x" by blast chaieb@23406: qed paulson@14277: paulson@14277: subsection{*Anti-Monotonicity of @{term inverse}*} paulson@14277: paulson@14268: lemma less_imp_inverse_less: nipkow@23482: assumes less: "a < b" and apos: "0 < a" haftmann@35028: shows "inverse b < inverse (a::'a::linordered_field)" nipkow@23482: proof (rule ccontr) paulson@14268: assume "~ inverse b < inverse a" nipkow@29667: hence "inverse a \ inverse b" by (simp add: linorder_not_less) paulson@14268: hence "~ (a < b)" paulson@14268: by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos]) nipkow@29667: thus False by (rule notE [OF _ less]) nipkow@23482: qed paulson@14268: paulson@14268: lemma inverse_less_imp_less: haftmann@35028: "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::linordered_field)" paulson@14268: apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"]) paulson@14268: apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) paulson@14268: done paulson@14268: paulson@14268: text{*Both premises are essential. Consider -1 and 1.*} paulson@24286: lemma inverse_less_iff_less [simp,noatp]: haftmann@35028: "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))" paulson@14268: by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) paulson@14268: paulson@14268: lemma le_imp_inverse_le: haftmann@35028: "[|a \ b; 0 < a|] ==> inverse b \ inverse (a::'a::linordered_field)" nipkow@23482: by (force simp add: order_le_less less_imp_inverse_less) paulson@14268: paulson@24286: lemma inverse_le_iff_le [simp,noatp]: haftmann@35028: "[|0 < a; 0 < b|] ==> (inverse a \ inverse b) = (b \ (a::'a::linordered_field))" paulson@14268: by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) paulson@14268: paulson@14268: paulson@14268: text{*These results refer to both operands being negative. The opposite-sign paulson@14268: case is trivial, since inverse preserves signs.*} paulson@14268: lemma inverse_le_imp_le_neg: haftmann@35028: "[|inverse a \ inverse b; b < 0|] ==> b \ (a::'a::linordered_field)" nipkow@23482: apply (rule classical) nipkow@23482: apply (subgoal_tac "a < 0") nipkow@23482: prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) nipkow@23482: apply (insert inverse_le_imp_le [of "-b" "-a"]) nipkow@23482: apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) nipkow@23482: done paulson@14268: paulson@14268: lemma less_imp_inverse_less_neg: haftmann@35028: "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::linordered_field)" nipkow@23482: apply (subgoal_tac "a < 0") nipkow@23482: prefer 2 apply (blast intro: order_less_trans) nipkow@23482: apply (insert less_imp_inverse_less [of "-b" "-a"]) nipkow@23482: apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) nipkow@23482: done paulson@14268: paulson@14268: lemma inverse_less_imp_less_neg: haftmann@35028: "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::linordered_field)" nipkow@23482: apply (rule classical) nipkow@23482: apply (subgoal_tac "a < 0") nipkow@23482: prefer 2 nipkow@23482: apply (force simp add: linorder_not_less intro: order_le_less_trans) nipkow@23482: apply (insert inverse_less_imp_less [of "-b" "-a"]) nipkow@23482: apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) nipkow@23482: done paulson@14268: paulson@24286: lemma inverse_less_iff_less_neg [simp,noatp]: haftmann@35028: "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))" nipkow@23482: apply (insert inverse_less_iff_less [of "-b" "-a"]) nipkow@23482: apply (simp del: inverse_less_iff_less nipkow@23482: add: order_less_imp_not_eq nonzero_inverse_minus_eq) nipkow@23482: done paulson@14268: paulson@14268: lemma le_imp_inverse_le_neg: haftmann@35028: "[|a \ b; b < 0|] ==> inverse b \ inverse (a::'a::linordered_field)" nipkow@23482: by (force simp add: order_le_less less_imp_inverse_less_neg) paulson@14268: paulson@24286: lemma inverse_le_iff_le_neg [simp,noatp]: haftmann@35028: "[|a < 0; b < 0|] ==> (inverse a \ inverse b) = (b \ (a::'a::linordered_field))" paulson@14268: by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) paulson@14265: paulson@14277: paulson@14365: subsection{*Inverses and the Number One*} paulson@14365: paulson@14365: lemma one_less_inverse_iff: haftmann@35028: "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))" 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" paulson@14365: also with notless have "... \ 0" by (simp add: linorder_not_less) 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 inverse_eq_1_iff [simp]: nipkow@23482: "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))" paulson@14365: by (insert inverse_eq_iff_eq [of x 1], simp) paulson@14365: paulson@14365: lemma one_le_inverse_iff: haftmann@35028: "(1 \ inverse x) = (0 < x & x \ (1::'a::{linordered_field,division_by_zero}))" paulson@14365: by (force simp add: order_le_less one_less_inverse_iff zero_less_one paulson@14365: eq_commute [of 1]) paulson@14365: paulson@14365: lemma inverse_less_1_iff: haftmann@35028: "(inverse x < 1) = (x \ 0 | 1 < (x::'a::{linordered_field,division_by_zero}))" paulson@14365: by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) paulson@14365: paulson@14365: lemma inverse_le_1_iff: haftmann@35028: "(inverse x \ 1) = (x \ 0 | 1 \ (x::'a::{linordered_field,division_by_zero}))" paulson@14365: by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) paulson@14365: wenzelm@23389: paulson@14288: subsection{*Simplification of Inequalities Involving Literal Divisors*} paulson@14288: haftmann@35028: lemma pos_le_divide_eq: "0 < (c::'a::linordered_field) ==> (a \ b/c) = (a*c \ b)" paulson@14288: proof - paulson@14288: assume less: "0 b/c) = (a*c \ (b/c)*c)" paulson@14288: by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) paulson@14288: also have "... = (a*c \ b)" paulson@14288: by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) paulson@14288: finally show ?thesis . paulson@14288: qed paulson@14288: haftmann@35028: lemma neg_le_divide_eq: "c < (0::'a::linordered_field) ==> (a \ b/c) = (b \ a*c)" paulson@14288: proof - paulson@14288: assume less: "c<0" paulson@14288: hence "(a \ b/c) = ((b/c)*c \ a*c)" paulson@14288: by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) paulson@14288: also have "... = (b \ a*c)" paulson@14288: by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) paulson@14288: finally show ?thesis . paulson@14288: qed paulson@14288: paulson@14288: lemma le_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@35028: else a \ (0::'a::{linordered_field,division_by_zero}))" haftmann@21328: apply (cases "c=0", simp) paulson@14288: apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) paulson@14288: done paulson@14288: haftmann@35028: lemma pos_divide_le_eq: "0 < (c::'a::linordered_field) ==> (b/c \ a) = (b \ a*c)" paulson@14288: proof - paulson@14288: assume less: "0 a) = ((b/c)*c \ a*c)" paulson@14288: by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) paulson@14288: also have "... = (b \ a*c)" paulson@14288: by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) paulson@14288: finally show ?thesis . paulson@14288: qed paulson@14288: haftmann@35028: lemma neg_divide_le_eq: "c < (0::'a::linordered_field) ==> (b/c \ a) = (a*c \ b)" paulson@14288: proof - paulson@14288: assume less: "c<0" paulson@14288: hence "(b/c \ a) = (a*c \ (b/c)*c)" paulson@14288: by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) paulson@14288: also have "... = (a*c \ b)" paulson@14288: by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) paulson@14288: finally show ?thesis . paulson@14288: qed paulson@14288: 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@35028: else 0 \ (a::'a::{linordered_field,division_by_zero}))" haftmann@21328: apply (cases "c=0", simp) paulson@14288: apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) paulson@14288: done paulson@14288: paulson@14288: lemma pos_less_divide_eq: haftmann@35028: "0 < (c::'a::linordered_field) ==> (a < b/c) = (a*c < b)" paulson@14288: proof - paulson@14288: assume less: "0 (a < b/c) = (b < a*c)" paulson@14288: proof - paulson@14288: assume less: "c<0" paulson@14288: hence "(a < b/c) = ((b/c)*c < a*c)" paulson@15234: by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less]) paulson@14288: also have "... = (b < a*c)" paulson@14288: by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) paulson@14288: finally show ?thesis . paulson@14288: qed 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@35028: else a < (0::'a::{linordered_field,division_by_zero}))" haftmann@21328: apply (cases "c=0", simp) paulson@14288: apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) paulson@14288: done paulson@14288: paulson@14288: lemma pos_divide_less_eq: haftmann@35028: "0 < (c::'a::linordered_field) ==> (b/c < a) = (b < a*c)" paulson@14288: proof - paulson@14288: assume less: "0 (b/c < a) = (a*c < b)" paulson@14288: proof - paulson@14288: assume less: "c<0" paulson@14288: hence "(b/c < a) = (a*c < (b/c)*c)" paulson@15234: by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less]) paulson@14288: also have "... = (a*c < b)" paulson@14288: by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) paulson@14288: finally show ?thesis . paulson@14288: qed 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@35028: else 0 < (a::'a::{linordered_field,division_by_zero}))" haftmann@21328: apply (cases "c=0", simp) paulson@14288: apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) paulson@14288: done paulson@14288: nipkow@23482: nipkow@23482: subsection{*Field simplification*} nipkow@23482: nipkow@29667: text{* Lemmas @{text field_simps} multiply with denominators in in(equations) nipkow@29667: if they can be proved to be non-zero (for equations) or positive/negative nipkow@29667: (for inequations). Can be too aggressive and is therefore separate from the nipkow@29667: more benign @{text algebra_simps}. *} paulson@14288: nipkow@29833: lemmas field_simps[noatp] = field_eq_simps nipkow@23482: (* multiply ineqn *) nipkow@23482: pos_divide_less_eq neg_divide_less_eq nipkow@23482: pos_less_divide_eq neg_less_divide_eq nipkow@23482: pos_divide_le_eq neg_divide_le_eq nipkow@23482: pos_le_divide_eq neg_le_divide_eq paulson@14288: nipkow@23482: text{* Lemmas @{text sign_simps} is a first attempt to automate proofs nipkow@23483: of positivity/negativity needed for @{text field_simps}. Have not added @{text nipkow@23482: sign_simps} to @{text field_simps} because the former can lead to case nipkow@23482: explosions. *} paulson@14288: nipkow@29833: lemmas sign_simps[noatp] = group_simps nipkow@23482: zero_less_mult_iff mult_less_0_iff paulson@14288: nipkow@23482: (* Only works once linear arithmetic is installed: nipkow@23482: text{*An example:*} haftmann@35028: lemma fixes a b c d e f :: "'a::linordered_field" nipkow@23482: shows "\a>b; c \ nipkow@23482: ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < nipkow@23482: ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u" nipkow@23482: apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0") nipkow@23482: prefer 2 apply(simp add:sign_simps) nipkow@23482: apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0") nipkow@23482: prefer 2 apply(simp add:sign_simps) nipkow@23482: apply(simp add:field_simps) avigad@16775: done nipkow@23482: *) avigad@16775: wenzelm@23389: avigad@16775: subsection{*Division and Signs*} avigad@16775: avigad@16775: lemma zero_less_divide_iff: haftmann@35028: "((0::'a::{linordered_field,division_by_zero}) < 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@35028: "(a/b < (0::'a::{linordered_field,division_by_zero})) = 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@35028: "((0::'a::{linordered_field,division_by_zero}) \ 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@35028: "(a/b \ (0::'a::{linordered_field,division_by_zero})) = avigad@16775: (0 \ a & b \ 0 | a \ 0 & 0 \ b)" avigad@16775: by (simp add: divide_inverse mult_le_0_iff) avigad@16775: paulson@24286: lemma divide_eq_0_iff [simp,noatp]: avigad@16775: "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))" nipkow@23482: by (simp add: divide_inverse) avigad@16775: nipkow@23482: lemma divide_pos_pos: haftmann@35028: "0 < (x::'a::linordered_field) ==> 0 < y ==> 0 < x / y" nipkow@23482: by(simp add:field_simps) nipkow@23482: avigad@16775: nipkow@23482: lemma divide_nonneg_pos: haftmann@35028: "0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y" nipkow@23482: by(simp add:field_simps) avigad@16775: nipkow@23482: lemma divide_neg_pos: haftmann@35028: "(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0" nipkow@23482: by(simp add:field_simps) avigad@16775: nipkow@23482: lemma divide_nonpos_pos: haftmann@35028: "(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0" nipkow@23482: by(simp add:field_simps) avigad@16775: nipkow@23482: lemma divide_pos_neg: haftmann@35028: "0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0" nipkow@23482: by(simp add:field_simps) avigad@16775: nipkow@23482: lemma divide_nonneg_neg: haftmann@35028: "0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0" nipkow@23482: by(simp add:field_simps) avigad@16775: nipkow@23482: lemma divide_neg_neg: haftmann@35028: "(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y" nipkow@23482: by(simp add:field_simps) avigad@16775: nipkow@23482: lemma divide_nonpos_neg: haftmann@35028: "(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y" nipkow@23482: by(simp add:field_simps) paulson@15234: wenzelm@23389: paulson@14288: subsection{*Cancellation Laws for Division*} paulson@14288: paulson@24286: lemma divide_cancel_right [simp,noatp]: paulson@14288: "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))" nipkow@23482: apply (cases "c=0", simp) nipkow@23496: apply (simp add: divide_inverse) paulson@14288: done paulson@14288: paulson@24286: lemma divide_cancel_left [simp,noatp]: paulson@14288: "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" nipkow@23482: apply (cases "c=0", simp) nipkow@23496: apply (simp add: divide_inverse) paulson@14288: done paulson@14288: wenzelm@23389: paulson@14353: subsection {* Division and the Number One *} paulson@14353: paulson@14353: text{*Simplify expressions equated with 1*} paulson@24286: lemma divide_eq_1_iff [simp,noatp]: paulson@14353: "(a/b = 1) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" nipkow@23482: apply (cases "b=0", simp) nipkow@23482: apply (simp add: right_inverse_eq) paulson@14353: done paulson@14353: paulson@24286: lemma one_eq_divide_iff [simp,noatp]: paulson@14353: "(1 = a/b) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" nipkow@23482: by (simp add: eq_commute [of 1]) paulson@14353: paulson@24286: lemma zero_eq_1_divide_iff [simp,noatp]: haftmann@35028: "((0::'a::{linordered_field,division_by_zero}) = 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: paulson@24286: lemma one_divide_eq_0_iff [simp,noatp]: haftmann@35028: "(1/a = (0::'a::{linordered_field,division_by_zero})) = (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"}*} paulson@18623: lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified] paulson@18623: lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified] paulson@18623: lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified] paulson@18623: lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified] paulson@17085: nipkow@29833: declare zero_less_divide_1_iff [simp,noatp] paulson@24286: declare divide_less_0_1_iff [simp,noatp] nipkow@29833: declare zero_le_divide_1_iff [simp,noatp] paulson@24286: declare divide_le_0_1_iff [simp,noatp] paulson@14353: wenzelm@23389: paulson@14293: subsection {* Ordering Rules for Division *} paulson@14293: paulson@14293: lemma divide_strict_right_mono: haftmann@35028: "[|a < b; 0 < c|] ==> a / c < b / (c::'a::linordered_field)" paulson@14293: by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono nipkow@23482: positive_imp_inverse_positive) paulson@14293: paulson@14293: lemma divide_right_mono: haftmann@35028: "[|a \ b; 0 \ c|] ==> a/c \ b/(c::'a::{linordered_field,division_by_zero})" nipkow@23482: by (force simp add: divide_strict_right_mono order_le_less) paulson@14293: haftmann@35028: lemma divide_right_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= 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: avigad@16775: lemma divide_strict_right_mono_neg: haftmann@35028: "[|b < a; c < 0|] ==> a / c < b / (c::'a::linordered_field)" nipkow@23482: apply (drule divide_strict_right_mono [of _ _ "-c"], simp) nipkow@23482: apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) avigad@16775: done paulson@14293: paulson@14293: text{*The last premise ensures that @{term a} and @{term b} paulson@14293: have the same sign*} paulson@14293: lemma divide_strict_left_mono: haftmann@35028: "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)" nipkow@23482: by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono) paulson@14293: paulson@14293: lemma divide_left_mono: haftmann@35028: "[|b \ a; 0 \ c; 0 < a*b|] ==> c / a \ c / (b::'a::linordered_field)" nipkow@23482: by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono) paulson@14293: haftmann@35028: lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= 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: paulson@14293: lemma divide_strict_left_mono_neg: haftmann@35028: "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)" nipkow@23482: by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg) nipkow@23482: paulson@14293: avigad@16775: text{*Simplify quotients that are compared with the value 1.*} avigad@16775: paulson@24286: lemma le_divide_eq_1 [noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" avigad@16775: shows "(1 \ b / a) = ((0 < a & a \ b) | (a < 0 & b \ a))" avigad@16775: by (auto simp add: le_divide_eq) avigad@16775: paulson@24286: lemma divide_le_eq_1 [noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" avigad@16775: shows "(b / a \ 1) = ((0 < a & b \ a) | (a < 0 & a \ b) | a=0)" avigad@16775: by (auto simp add: divide_le_eq) avigad@16775: paulson@24286: lemma less_divide_eq_1 [noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" avigad@16775: shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" avigad@16775: by (auto simp add: less_divide_eq) avigad@16775: paulson@24286: lemma divide_less_eq_1 [noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" avigad@16775: shows "(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: avigad@16775: subsection{*Conditional Simplification Rules: No Case Splits*} avigad@16775: paulson@24286: lemma le_divide_eq_1_pos [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "0 < a \ (1 \ b/a) = (a \ b)" avigad@16775: by (auto simp add: le_divide_eq) avigad@16775: paulson@24286: lemma le_divide_eq_1_neg [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "a < 0 \ (1 \ b/a) = (b \ a)" avigad@16775: by (auto simp add: le_divide_eq) avigad@16775: paulson@24286: lemma divide_le_eq_1_pos [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "0 < a \ (b/a \ 1) = (b \ a)" avigad@16775: by (auto simp add: divide_le_eq) avigad@16775: paulson@24286: lemma divide_le_eq_1_neg [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "a < 0 \ (b/a \ 1) = (a \ b)" avigad@16775: by (auto simp add: divide_le_eq) avigad@16775: paulson@24286: lemma less_divide_eq_1_pos [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "0 < a \ (1 < b/a) = (a < b)" avigad@16775: by (auto simp add: less_divide_eq) avigad@16775: paulson@24286: lemma less_divide_eq_1_neg [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "a < 0 \ (1 < b/a) = (b < a)" avigad@16775: by (auto simp add: less_divide_eq) avigad@16775: paulson@24286: lemma divide_less_eq_1_pos [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "0 < a \ (b/a < 1) = (b < a)" paulson@18649: by (auto simp add: divide_less_eq) paulson@18649: paulson@24286: lemma divide_less_eq_1_neg [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "a < 0 \ b/a < 1 <-> a < b" avigad@16775: by (auto simp add: divide_less_eq) avigad@16775: paulson@24286: lemma eq_divide_eq_1 [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "(1 = b/a) = ((a \ 0 & a = b))" avigad@16775: by (auto simp add: eq_divide_eq) avigad@16775: paulson@24286: lemma divide_eq_eq_1 [simp,noatp]: haftmann@35028: fixes a :: "'a :: {linordered_field,division_by_zero}" paulson@18649: shows "(b/a = 1) = ((a \ 0 & a = b))" avigad@16775: by (auto simp add: divide_eq_eq) avigad@16775: wenzelm@23389: avigad@16775: subsection {* Reasoning about inequalities with division *} avigad@16775: haftmann@35028: lemma mult_imp_div_pos_le: "0 < (y::'a::linordered_field) ==> x <= z * y ==> haftmann@33319: x / y <= z" haftmann@33319: by (subst pos_divide_le_eq, assumption+) avigad@16775: haftmann@35028: lemma mult_imp_le_div_pos: "0 < (y::'a::linordered_field) ==> z * y <= x ==> nipkow@23482: z <= x / y" nipkow@23482: by(simp add:field_simps) avigad@16775: haftmann@35028: lemma mult_imp_div_pos_less: "0 < (y::'a::linordered_field) ==> x < z * y ==> avigad@16775: x / y < z" nipkow@23482: by(simp add:field_simps) avigad@16775: haftmann@35028: lemma mult_imp_less_div_pos: "0 < (y::'a::linordered_field) ==> z * y < x ==> avigad@16775: z < x / y" nipkow@23482: by(simp add:field_simps) avigad@16775: haftmann@35028: lemma frac_le: "(0::'a::linordered_field) <= x ==> avigad@16775: x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" avigad@16775: apply (rule mult_imp_div_pos_le) haftmann@25230: apply simp haftmann@25230: apply (subst times_divide_eq_left) avigad@16775: apply (rule mult_imp_le_div_pos, assumption) avigad@16775: apply (rule mult_mono) avigad@16775: apply simp_all paulson@14293: done paulson@14293: haftmann@35028: lemma frac_less: "(0::'a::linordered_field) <= x ==> avigad@16775: x < y ==> 0 < w ==> w <= z ==> x / z < y / w" avigad@16775: apply (rule mult_imp_div_pos_less) haftmann@33319: apply simp haftmann@33319: apply (subst times_divide_eq_left) avigad@16775: apply (rule mult_imp_less_div_pos, assumption) avigad@16775: apply (erule mult_less_le_imp_less) avigad@16775: apply simp_all avigad@16775: done avigad@16775: haftmann@35028: lemma frac_less2: "(0::'a::linordered_field) < x ==> avigad@16775: x <= y ==> 0 < w ==> w < z ==> x / z < y / w" avigad@16775: apply (rule mult_imp_div_pos_less) avigad@16775: apply simp_all haftmann@33319: apply (subst times_divide_eq_left) avigad@16775: apply (rule mult_imp_less_div_pos, assumption) avigad@16775: apply (erule mult_le_less_imp_less) avigad@16775: apply simp_all avigad@16775: done avigad@16775: avigad@16775: text{*It's not obvious whether these should be simprules or not. avigad@16775: Their effect is to gather terms into one big fraction, like avigad@16775: a*b*c / x*y*z. The rationale for that is unclear, but many proofs avigad@16775: seem to need them.*} avigad@16775: avigad@16775: declare times_divide_eq [simp] paulson@14293: wenzelm@23389: paulson@14293: subsection {* Ordered Fields are Dense *} paulson@14293: haftmann@35028: lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)" nipkow@23482: by (simp add: field_simps zero_less_two) paulson@14293: haftmann@35028: lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b" nipkow@23482: by (simp add: field_simps zero_less_two) paulson@14293: haftmann@35028: instance linordered_field < dense_linorder haftmann@24422: proof haftmann@24422: fix x y :: 'a haftmann@24422: have "x < x + 1" by simp haftmann@24422: then show "\y. x < y" .. haftmann@24422: have "x - 1 < x" by simp haftmann@24422: then show "\y. y < x" .. haftmann@24422: show "x < y \ \z>x. z < y" by (blast intro!: less_half_sum gt_half_sum) haftmann@24422: qed paulson@14293: paulson@15234: paulson@14293: subsection {* Absolute Value *} paulson@14293: paulson@14294: lemma nonzero_abs_inverse: haftmann@35028: "a \ 0 ==> abs (inverse (a::'a::linordered_field)) = inverse (abs a)" paulson@14294: apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq paulson@14294: negative_imp_inverse_negative) paulson@14294: apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) paulson@14294: done paulson@14294: paulson@14294: lemma abs_inverse [simp]: haftmann@35028: "abs (inverse (a::'a::{linordered_field,division_by_zero})) = paulson@14294: inverse (abs a)" haftmann@21328: apply (cases "a=0", simp) paulson@14294: apply (simp add: nonzero_abs_inverse) paulson@14294: done paulson@14294: paulson@14294: lemma nonzero_abs_divide: haftmann@35028: "b \ 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b" paulson@14294: by (simp add: divide_inverse abs_mult nonzero_abs_inverse) paulson@14294: paulson@15234: lemma abs_divide [simp]: haftmann@35028: "abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b" haftmann@21328: apply (cases "b=0", simp) paulson@14294: apply (simp add: nonzero_abs_divide) paulson@14294: done paulson@14294: haftmann@35028: lemma abs_div_pos: "(0::'a::{division_by_zero,linordered_field}) < y ==> haftmann@25304: abs x / y = abs (x / y)" haftmann@25304: apply (subst abs_divide) haftmann@25304: apply (simp add: order_less_imp_le) haftmann@25304: done avigad@16775: 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