# HG changeset patch # User haftmann # Date 1272023894 -7200 # Node ID 72f4d079ebf82b1fa8555cd0370916af73eaef9d # Parent c805033ad0327d27f94635f97309594193401ec1 more localization; factored out lemmas for division_ring diff -r c805033ad032 -r 72f4d079ebf8 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Fri Apr 23 13:58:14 2010 +0200 +++ b/src/HOL/Fields.thy Fri Apr 23 13:58:14 2010 +0200 @@ -31,34 +31,6 @@ subclass idom .. -lemma right_inverse_eq: "b \ 0 \ a / b = 1 \ a = b" -proof - assume neq: "b \ 0" - { - hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac) - also assume "a / b = 1" - finally show "a = b" by simp - next - assume "a = b" - with neq show "a / b = 1" by (simp add: divide_inverse) - } -qed - -lemma nonzero_inverse_eq_divide: "a \ 0 \ inverse a = 1 / a" -by (simp add: divide_inverse) - -lemma divide_self [simp]: "a \ 0 \ a / a = 1" -by (simp add: divide_inverse) - -lemma divide_zero_left [simp]: "0 / a = 0" -by (simp add: divide_inverse) - -lemma inverse_eq_divide: "inverse a = 1 / a" -by (simp add: divide_inverse) - -lemma add_divide_distrib: "(a+b) / c = a/c + b/c" -by (simp add: divide_inverse algebra_simps) - text{*There is no slick version using division by zero.*} lemma inverse_add: "[| a \ 0; b \ 0 |] @@ -80,14 +52,8 @@ "\b \ 0; c \ 0\ \ (a * c) / (b * c) = a / b" by (simp add: mult_commute [of _ c]) -lemma divide_1 [simp]: "a / 1 = a" -by (simp add: divide_inverse) - -lemma times_divide_eq_right: "a * (b / c) = (a * b) / c" -by (simp add: divide_inverse mult_assoc) - lemma times_divide_eq_left: "(b / c) * a = (b * a) / c" -by (simp add: divide_inverse mult_ac) + by (simp add: divide_inverse mult_ac) text {* These are later declared as simp rules. *} lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left @@ -108,7 +74,7 @@ lemma nonzero_mult_divide_cancel_right [simp, no_atp]: "b \ 0 \ a * b / b = a" -using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp + using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp lemma nonzero_mult_divide_cancel_left [simp, no_atp]: "a \ 0 \ a * b / a = b" @@ -130,58 +96,21 @@ "\b \ 0; c \ 0\ \ (a * c) / (c * b) = a / b" using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac) -lemma minus_divide_left: "- (a / b) = (-a) / b" -by (simp add: divide_inverse) - -lemma nonzero_minus_divide_right: "b \ 0 ==> - (a / b) = a / (- b)" -by (simp add: divide_inverse nonzero_inverse_minus_eq) - -lemma nonzero_minus_divide_divide: "b \ 0 ==> (-a) / (-b) = a / b" -by (simp add: divide_inverse nonzero_inverse_minus_eq) - -lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)" -by (simp add: divide_inverse) - -lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" -by (simp add: diff_minus add_divide_distrib) - lemma add_divide_eq_iff: "z \ 0 \ x + y / z = (z * x + y) / z" -by (simp add: add_divide_distrib) + by (simp add: add_divide_distrib) lemma divide_add_eq_iff: "z \ 0 \ x / z + y = (x + z * y) / z" -by (simp add: add_divide_distrib) + by (simp add: add_divide_distrib) lemma diff_divide_eq_iff: "z \ 0 \ x - y / z = (z * x - y) / z" -by (simp add: diff_divide_distrib) + by (simp add: diff_divide_distrib) lemma divide_diff_eq_iff: "z \ 0 \ x / z - y = (x - z * y) / z" -by (simp add: diff_divide_distrib) - -lemma nonzero_eq_divide_eq: "c \ 0 \ a = b / c \ a * c = b" -proof - - assume [simp]: "c \ 0" - have "a = b / c \ a * c = (b / c) * c" by simp - also have "... \ a * c = b" by (simp add: divide_inverse mult_assoc) - finally show ?thesis . -qed - -lemma nonzero_divide_eq_eq: "c \ 0 \ b / c = a \ b = a * c" -proof - - assume [simp]: "c \ 0" - have "b / c = a \ (b / c) * c = a * c" by simp - also have "... \ b = a * c" by (simp add: divide_inverse mult_assoc) - finally show ?thesis . -qed - -lemma divide_eq_imp: "c \ 0 \ b = a * c \ b / c = a" -by simp - -lemma eq_divide_imp: "c \ 0 \ a * c = b \ a = b / c" -by (erule subst, simp) + by (simp add: diff_divide_distrib) lemmas field_eq_simps[no_atp] = algebra_simps (* pull / out*) @@ -189,9 +118,7 @@ diff_divide_eq_iff divide_diff_eq_iff (* multiply eqn *) nonzero_eq_divide_eq nonzero_divide_eq_eq -(* is added later: times_divide_eq_left times_divide_eq_right -*) text{*An example:*} lemma "\a\b; c\d; e\f\ \ ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1" @@ -202,68 +129,21 @@ lemma diff_frac_eq: "y \ 0 \ z \ 0 \ x / y - w / z = (x * z - w * y) / (y * z)" -by (simp add: field_eq_simps times_divide_eq) + by (simp add: field_eq_simps times_divide_eq) lemma frac_eq_eq: "y \ 0 \ z \ 0 \ (x / y = w / z) = (x * z = w * y)" -by (simp add: field_eq_simps times_divide_eq) + by (simp add: field_eq_simps times_divide_eq) end -class division_by_zero = zero + inverse + - assumes inverse_zero [simp]: "inverse 0 = 0" - -lemma divide_zero [simp]: - "a / 0 = (0::'a::{field,division_by_zero})" -by (simp add: divide_inverse) - -lemma divide_self_if [simp]: - "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)" -by simp - -class linordered_field = field + linordered_idom - -lemma inverse_nonzero_iff_nonzero [simp]: - "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))" -by (force dest: inverse_zero_imp_zero) - -lemma inverse_minus_eq [simp]: - "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})" -proof cases - assume "a=0" thus ?thesis by simp -next - assume "a\0" - thus ?thesis by (simp add: nonzero_inverse_minus_eq) -qed - -lemma inverse_eq_imp_eq: - "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})" -apply (cases "a=0 | b=0") - apply (force dest!: inverse_zero_imp_zero - simp add: eq_commute [of "0::'a"]) -apply (force dest!: nonzero_inverse_eq_imp_eq) -done - -lemma inverse_eq_iff_eq [simp]: - "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))" -by (force dest!: inverse_eq_imp_eq) - -lemma inverse_inverse_eq [simp]: - "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a" - proof cases - assume "a=0" thus ?thesis by simp - next - assume "a\0" - thus ?thesis by (simp add: nonzero_inverse_inverse_eq) - qed - text{*This version builds in division by zero while also re-orienting the right-hand side.*} lemma inverse_mult_distrib [simp]: "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})" proof cases assume "a \ 0 & b \ 0" - thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute) + thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac) next assume "~ (a \ 0 & b \ 0)" thus ?thesis by force @@ -271,10 +151,10 @@ lemma inverse_divide [simp]: "inverse (a/b) = b / (a::'a::{field,division_by_zero})" -by (simp add: divide_inverse mult_commute) + by (simp add: divide_inverse mult_commute) -subsection {* Calculations with fractions *} +text {* Calculations with fractions *} text{* There is a whole bunch of simp-rules just for class @{text field} but none for class @{text field} and @{text nonzero_divides} @@ -301,7 +181,7 @@ by (simp add: divide_inverse mult_assoc) -subsubsection{*Special Cancellation Simprules for Division*} +text {*Special Cancellation Simprules for Division*} lemma mult_divide_mult_cancel_left_if[simp,no_atp]: fixes c :: "'a :: {field,division_by_zero}" @@ -309,7 +189,7 @@ by (simp add: mult_divide_mult_cancel_left) -subsection {* Division and Unary Minus *} +text {* Division and Unary Minus *} lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})" by (simp add: divide_inverse) @@ -332,40 +212,74 @@ "(b/c = (a::'a::{field,division_by_zero})) = (if c\0 then b = a*c else a=0)" by (force simp add: nonzero_divide_eq_eq) +lemma inverse_eq_1_iff [simp]: + "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))" +by (insert inverse_eq_iff_eq [of x 1], simp) -subsection {* Ordered Fields *} +lemma divide_eq_0_iff [simp,no_atp]: + "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))" +by (simp add: divide_inverse) + +lemma divide_cancel_right [simp,no_atp]: + "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))" +apply (cases "c=0", simp) +apply (simp add: divide_inverse) +done + +lemma divide_cancel_left [simp,no_atp]: + "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" +apply (cases "c=0", simp) +apply (simp add: divide_inverse) +done + +lemma divide_eq_1_iff [simp,no_atp]: + "(a/b = 1) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" +apply (cases "b=0", simp) +apply (simp add: right_inverse_eq) +done + +lemma one_eq_divide_iff [simp,no_atp]: + "(1 = a/b) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" +by (simp add: eq_commute [of 1]) + + +text {* Ordered Fields *} + +class linordered_field = field + linordered_idom +begin lemma positive_imp_inverse_positive: -assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::linordered_field)" + assumes a_gt_0: "0 < a" + shows "0 < inverse a" proof - have "0 < a * inverse a" - by (simp add: a_gt_0 [THEN order_less_imp_not_eq2]) + by (simp add: a_gt_0 [THEN less_imp_not_eq2]) thus "0 < inverse a" - by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff) + by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff) qed lemma negative_imp_inverse_negative: - "a < 0 ==> inverse a < (0::'a::linordered_field)" -by (insert positive_imp_inverse_positive [of "-a"], - simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) + "a < 0 \ inverse a < 0" + by (insert positive_imp_inverse_positive [of "-a"], + simp add: nonzero_inverse_minus_eq less_imp_not_eq) lemma inverse_le_imp_le: -assumes invle: "inverse a \ inverse b" and apos: "0 < a" -shows "b \ (a::'a::linordered_field)" + assumes invle: "inverse a \ inverse b" and apos: "0 < a" + shows "b \ a" proof (rule classical) assume "~ b \ a" hence "a < b" by (simp add: linorder_not_le) - hence bpos: "0 < b" by (blast intro: apos order_less_trans) + hence bpos: "0 < b" by (blast intro: apos less_trans) hence "a * inverse a \ a * inverse b" - by (simp add: apos invle order_less_imp_le mult_left_mono) + by (simp add: apos invle less_imp_le mult_left_mono) hence "(a * inverse a) * b \ (a * inverse b) * b" - by (simp add: bpos order_less_imp_le mult_right_mono) - thus "b \ a" by (simp add: mult_assoc apos bpos order_less_imp_not_eq2) + by (simp add: bpos less_imp_le mult_right_mono) + thus "b \ a" by (simp add: mult_assoc apos bpos less_imp_not_eq2) qed lemma inverse_positive_imp_positive: -assumes inv_gt_0: "0 < inverse a" and nz: "a \ 0" -shows "0 < (a::'a::linordered_field)" + assumes inv_gt_0: "0 < inverse a" and nz: "a \ 0" + shows "0 < a" proof - have "0 < inverse (inverse a)" using inv_gt_0 by (rule positive_imp_inverse_positive) @@ -373,21 +287,397 @@ using nz by (simp add: nonzero_inverse_inverse_eq) qed +lemma inverse_negative_imp_negative: + assumes inv_less_0: "inverse a < 0" and nz: "a \ 0" + shows "a < 0" +proof - + have "inverse (inverse a) < 0" + using inv_less_0 by (rule negative_imp_inverse_negative) + thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq) +qed + +lemma linordered_field_no_lb: + "\x. \y. y < x" +proof + fix x::'a + have m1: "- (1::'a) < 0" by simp + from add_strict_right_mono[OF m1, where c=x] + have "(- 1) + x < x" by simp + thus "\y. y < x" by blast +qed + +lemma linordered_field_no_ub: + "\ x. \y. y > x" +proof + fix x::'a + have m1: " (1::'a) > 0" by simp + from add_strict_right_mono[OF m1, where c=x] + have "1 + x > x" by simp + thus "\y. y > x" by blast +qed + +lemma less_imp_inverse_less: + assumes less: "a < b" and apos: "0 < a" + shows "inverse b < inverse a" +proof (rule ccontr) + assume "~ inverse b < inverse a" + hence "inverse a \ inverse b" by simp + hence "~ (a < b)" + by (simp add: not_less inverse_le_imp_le [OF _ apos]) + thus False by (rule notE [OF _ less]) +qed + +lemma inverse_less_imp_less: + "inverse a < inverse b \ 0 < a \ b < a" +apply (simp add: less_le [of "inverse a"] less_le [of "b"]) +apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) +done + +text{*Both premises are essential. Consider -1 and 1.*} +lemma inverse_less_iff_less [simp,no_atp]: + "0 < a \ 0 < b \ inverse a < inverse b \ b < a" + by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) + +lemma le_imp_inverse_le: + "a \ b \ 0 < a \ inverse b \ inverse a" + by (force simp add: le_less less_imp_inverse_less) + +lemma inverse_le_iff_le [simp,no_atp]: + "0 < a \ 0 < b \ inverse a \ inverse b \ b \ a" + by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) + + +text{*These results refer to both operands being negative. The opposite-sign +case is trivial, since inverse preserves signs.*} +lemma inverse_le_imp_le_neg: + "inverse a \ inverse b \ b < 0 \ b \ a" +apply (rule classical) +apply (subgoal_tac "a < 0") + prefer 2 apply force +apply (insert inverse_le_imp_le [of "-b" "-a"]) +apply (simp add: nonzero_inverse_minus_eq) +done + +lemma less_imp_inverse_less_neg: + "a < b \ b < 0 \ inverse b < inverse a" +apply (subgoal_tac "a < 0") + prefer 2 apply (blast intro: less_trans) +apply (insert less_imp_inverse_less [of "-b" "-a"]) +apply (simp add: nonzero_inverse_minus_eq) +done + +lemma inverse_less_imp_less_neg: + "inverse a < inverse b \ b < 0 \ b < a" +apply (rule classical) +apply (subgoal_tac "a < 0") + prefer 2 + apply force +apply (insert inverse_less_imp_less [of "-b" "-a"]) +apply (simp add: nonzero_inverse_minus_eq) +done + +lemma inverse_less_iff_less_neg [simp,no_atp]: + "a < 0 \ b < 0 \ inverse a < inverse b \ b < a" +apply (insert inverse_less_iff_less [of "-b" "-a"]) +apply (simp del: inverse_less_iff_less + add: nonzero_inverse_minus_eq) +done + +lemma le_imp_inverse_le_neg: + "a \ b \ b < 0 ==> inverse b \ inverse a" + by (force simp add: le_less less_imp_inverse_less_neg) + +lemma inverse_le_iff_le_neg [simp,no_atp]: + "a < 0 \ b < 0 \ inverse a \ inverse b \ b \ a" + by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) + +lemma pos_le_divide_eq: "0 < c ==> (a \ b/c) = (a*c \ b)" +proof - + assume less: "0 b/c) = (a*c \ (b/c)*c)" + by (simp add: mult_le_cancel_right less_not_sym [OF less]) + also have "... = (a*c \ b)" + by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma neg_le_divide_eq: "c < 0 ==> (a \ b/c) = (b \ a*c)" +proof - + assume less: "c<0" + hence "(a \ b/c) = ((b/c)*c \ a*c)" + by (simp add: mult_le_cancel_right less_not_sym [OF less]) + also have "... = (b \ a*c)" + by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma pos_less_divide_eq: + "0 < c ==> (a < b/c) = (a*c < b)" +proof - + assume less: "0 (a < b/c) = (b < a*c)" +proof - + assume less: "c<0" + hence "(a < b/c) = ((b/c)*c < a*c)" + by (simp add: mult_less_cancel_right_disj less_not_sym [OF less]) + also have "... = (b < a*c)" + by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma pos_divide_less_eq: + "0 < c ==> (b/c < a) = (b < a*c)" +proof - + assume less: "0 (b/c < a) = (a*c < b)" +proof - + assume less: "c<0" + hence "(b/c < a) = (a*c < (b/c)*c)" + by (simp add: mult_less_cancel_right_disj less_not_sym [OF less]) + also have "... = (a*c < b)" + by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma pos_divide_le_eq: "0 < c ==> (b/c \ a) = (b \ a*c)" +proof - + assume less: "0 a) = ((b/c)*c \ a*c)" + by (simp add: mult_le_cancel_right less_not_sym [OF less]) + also have "... = (b \ a*c)" + by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma neg_divide_le_eq: "c < 0 ==> (b/c \ a) = (a*c \ b)" +proof - + assume less: "c<0" + hence "(b/c \ a) = (a*c \ (b/c)*c)" + by (simp add: mult_le_cancel_right less_not_sym [OF less]) + also have "... = (a*c \ b)" + by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc) + finally show ?thesis . +qed + +text{* Lemmas @{text field_simps} multiply with denominators in in(equations) +if they can be proved to be non-zero (for equations) or positive/negative +(for inequations). Can be too aggressive and is therefore separate from the +more benign @{text algebra_simps}. *} + +lemmas field_simps[no_atp] = field_eq_simps + (* multiply ineqn *) + pos_divide_less_eq neg_divide_less_eq + pos_less_divide_eq neg_less_divide_eq + pos_divide_le_eq neg_divide_le_eq + pos_le_divide_eq neg_le_divide_eq + +thm field_eq_simps + +text{* Lemmas @{text sign_simps} is a first attempt to automate proofs +of positivity/negativity needed for @{text field_simps}. Have not added @{text +sign_simps} to @{text field_simps} because the former can lead to case +explosions. *} + +lemmas sign_simps[no_atp] = group_simps + zero_less_mult_iff mult_less_0_iff + +(* Only works once linear arithmetic is installed: +text{*An example:*} +lemma fixes a b c d e f :: "'a::linordered_field" +shows "\a>b; c \ + ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < + ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u" +apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0") + prefer 2 apply(simp add:sign_simps) +apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0") + prefer 2 apply(simp add:sign_simps) +apply(simp add:field_simps) +done +*) + +lemma divide_pos_pos: + "0 < x ==> 0 < y ==> 0 < x / y" +by(simp add:field_simps) + +lemma divide_nonneg_pos: + "0 <= x ==> 0 < y ==> 0 <= x / y" +by(simp add:field_simps) + +lemma divide_neg_pos: + "x < 0 ==> 0 < y ==> x / y < 0" +by(simp add:field_simps) + +lemma divide_nonpos_pos: + "x <= 0 ==> 0 < y ==> x / y <= 0" +by(simp add:field_simps) + +lemma divide_pos_neg: + "0 < x ==> y < 0 ==> x / y < 0" +by(simp add:field_simps) + +lemma divide_nonneg_neg: + "0 <= x ==> y < 0 ==> x / y <= 0" +by(simp add:field_simps) + +lemma divide_neg_neg: + "x < 0 ==> y < 0 ==> 0 < x / y" +by(simp add:field_simps) + +lemma divide_nonpos_neg: + "x <= 0 ==> y < 0 ==> 0 <= x / y" +by(simp add:field_simps) + +lemma divide_strict_right_mono: + "[|a < b; 0 < c|] ==> a / c < b / c" +by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono + positive_imp_inverse_positive) + + +lemma divide_strict_right_mono_neg: + "[|b < a; c < 0|] ==> a / c < b / c" +apply (drule divide_strict_right_mono [of _ _ "-c"], simp) +apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric]) +done + +text{*The last premise ensures that @{term a} and @{term b} + have the same sign*} +lemma divide_strict_left_mono: + "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b" +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono) + +lemma divide_left_mono: + "[|b \ a; 0 \ c; 0 < a*b|] ==> c / a \ c / b" +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono) + +lemma divide_strict_left_mono_neg: + "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b" +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg) + +lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==> + x / y <= z" +by (subst pos_divide_le_eq, assumption+) + +lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==> + z <= x / y" +by(simp add:field_simps) + +lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==> + x / y < z" +by(simp add:field_simps) + +lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==> + z < x / y" +by(simp add:field_simps) + +lemma frac_le: "0 <= x ==> + x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" + apply (rule mult_imp_div_pos_le) + apply simp + apply (subst times_divide_eq_left) + apply (rule mult_imp_le_div_pos, assumption) + apply (rule mult_mono) + apply simp_all +done + +lemma frac_less: "0 <= x ==> + x < y ==> 0 < w ==> w <= z ==> x / z < y / w" + apply (rule mult_imp_div_pos_less) + apply simp + apply (subst times_divide_eq_left) + apply (rule mult_imp_less_div_pos, assumption) + apply (erule mult_less_le_imp_less) + apply simp_all +done + +lemma frac_less2: "0 < x ==> + x <= y ==> 0 < w ==> w < z ==> x / z < y / w" + apply (rule mult_imp_div_pos_less) + apply simp_all + apply (subst times_divide_eq_left) + apply (rule mult_imp_less_div_pos, assumption) + apply (erule mult_le_less_imp_less) + apply simp_all +done + +text{*It's not obvious whether these should be simprules or not. + Their effect is to gather terms into one big fraction, like + a*b*c / x*y*z. The rationale for that is unclear, but many proofs + seem to need them.*} + +declare times_divide_eq [simp] + +lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)" +by (simp add: field_simps zero_less_two) + +lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b" +by (simp add: field_simps zero_less_two) + +subclass dense_linorder +proof + fix x y :: 'a + from less_add_one show "\y. x < y" .. + from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono) + then have "x - 1 < x + 1 - 1" by (simp only: diff_minus [symmetric]) + then have "x - 1 < x" by (simp add: algebra_simps) + then show "\y. y < x" .. + show "x < y \ \z>x. z < y" by (blast intro!: less_half_sum gt_half_sum) +qed + +lemma nonzero_abs_inverse: + "a \ 0 ==> \inverse a\ = inverse \a\" +apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq + negative_imp_inverse_negative) +apply (blast intro: positive_imp_inverse_positive elim: less_asym) +done + +lemma nonzero_abs_divide: + "b \ 0 ==> \a / b\ = \a\ / \b\" + by (simp add: divide_inverse abs_mult nonzero_abs_inverse) + +lemma field_le_epsilon: + assumes e: "\e. 0 < e \ x \ y + e" + shows "x \ y" +proof (rule dense_le) + fix t assume "t < x" + hence "0 < x - t" by (simp add: less_diff_eq) + from e [OF this] have "x + 0 \ x + (y - t)" by (simp add: algebra_simps) + then have "0 \ y - t" by (simp only: add_le_cancel_left) + then show "t \ y" by (simp add: algebra_simps) +qed + +end + +lemma le_divide_eq: + "(a \ b/c) = + (if 0 < c then a*c \ b + else if c < 0 then b \ a*c + else a \ (0::'a::{linordered_field,division_by_zero}))" +apply (cases "c=0", simp) +apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) +done + lemma inverse_positive_iff_positive [simp]: "(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))" apply (cases "a = 0", simp) apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) done -lemma inverse_negative_imp_negative: -assumes inv_less_0: "inverse a < 0" and nz: "a \ 0" -shows "a < (0::'a::linordered_field)" -proof - - have "inverse (inverse a) < 0" - using inv_less_0 by (rule negative_imp_inverse_negative) - thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq) -qed - lemma inverse_negative_iff_negative [simp]: "(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))" apply (cases "a = 0", simp) @@ -402,104 +692,6 @@ "(inverse a \ 0) = (a \ (0::'a::{linordered_field,division_by_zero}))" by (simp add: linorder_not_less [symmetric]) -lemma linordered_field_no_lb: "\ x. \y. y < (x::'a::linordered_field)" -proof - fix x::'a - have m1: "- (1::'a) < 0" by simp - from add_strict_right_mono[OF m1, where c=x] - have "(- 1) + x < x" by simp - thus "\y. y < x" by blast -qed - -lemma linordered_field_no_ub: "\ x. \y. y > (x::'a::linordered_field)" -proof - fix x::'a - have m1: " (1::'a) > 0" by simp - from add_strict_right_mono[OF m1, where c=x] - have "1 + x > x" by simp - thus "\y. y > x" by blast -qed - -subsection{*Anti-Monotonicity of @{term inverse}*} - -lemma less_imp_inverse_less: -assumes less: "a < b" and apos: "0 < a" -shows "inverse b < inverse (a::'a::linordered_field)" -proof (rule ccontr) - assume "~ inverse b < inverse a" - hence "inverse a \ inverse b" by (simp add: linorder_not_less) - hence "~ (a < b)" - by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos]) - thus False by (rule notE [OF _ less]) -qed - -lemma inverse_less_imp_less: - "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::linordered_field)" -apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"]) -apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) -done - -text{*Both premises are essential. Consider -1 and 1.*} -lemma inverse_less_iff_less [simp,no_atp]: - "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))" -by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) - -lemma le_imp_inverse_le: - "[|a \ b; 0 < a|] ==> inverse b \ inverse (a::'a::linordered_field)" -by (force simp add: order_le_less less_imp_inverse_less) - -lemma inverse_le_iff_le [simp,no_atp]: - "[|0 < a; 0 < b|] ==> (inverse a \ inverse b) = (b \ (a::'a::linordered_field))" -by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) - - -text{*These results refer to both operands being negative. The opposite-sign -case is trivial, since inverse preserves signs.*} -lemma inverse_le_imp_le_neg: - "[|inverse a \ inverse b; b < 0|] ==> b \ (a::'a::linordered_field)" -apply (rule classical) -apply (subgoal_tac "a < 0") - prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) -apply (insert inverse_le_imp_le [of "-b" "-a"]) -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) -done - -lemma less_imp_inverse_less_neg: - "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::linordered_field)" -apply (subgoal_tac "a < 0") - prefer 2 apply (blast intro: order_less_trans) -apply (insert less_imp_inverse_less [of "-b" "-a"]) -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) -done - -lemma inverse_less_imp_less_neg: - "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::linordered_field)" -apply (rule classical) -apply (subgoal_tac "a < 0") - prefer 2 - apply (force simp add: linorder_not_less intro: order_le_less_trans) -apply (insert inverse_less_imp_less [of "-b" "-a"]) -apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) -done - -lemma inverse_less_iff_less_neg [simp,no_atp]: - "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))" -apply (insert inverse_less_iff_less [of "-b" "-a"]) -apply (simp del: inverse_less_iff_less - add: order_less_imp_not_eq nonzero_inverse_minus_eq) -done - -lemma le_imp_inverse_le_neg: - "[|a \ b; b < 0|] ==> inverse b \ inverse (a::'a::linordered_field)" -by (force simp add: order_le_less less_imp_inverse_less_neg) - -lemma inverse_le_iff_le_neg [simp,no_atp]: - "[|a < 0; b < 0|] ==> (inverse a \ inverse b) = (b \ (a::'a::linordered_field))" -by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) - - -subsection{*Inverses and the Number One*} - lemma one_less_inverse_iff: "(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))" proof cases @@ -518,10 +710,6 @@ with notless show ?thesis by simp qed -lemma inverse_eq_1_iff [simp]: - "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))" -by (insert inverse_eq_iff_eq [of x 1], simp) - lemma one_le_inverse_iff: "(1 \ inverse x) = (0 < x & x \ (1::'a::{linordered_field,division_by_zero}))" by (force simp add: order_le_less one_less_inverse_iff) @@ -534,58 +722,6 @@ "(inverse x \ 1) = (x \ 0 | 1 \ (x::'a::{linordered_field,division_by_zero}))" by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) - -subsection{*Simplification of Inequalities Involving Literal Divisors*} - -lemma pos_le_divide_eq: "0 < (c::'a::linordered_field) ==> (a \ b/c) = (a*c \ b)" -proof - - assume less: "0 b/c) = (a*c \ (b/c)*c)" - by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) - also have "... = (a*c \ b)" - by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) - finally show ?thesis . -qed - -lemma neg_le_divide_eq: "c < (0::'a::linordered_field) ==> (a \ b/c) = (b \ a*c)" -proof - - assume less: "c<0" - hence "(a \ b/c) = ((b/c)*c \ a*c)" - by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) - also have "... = (b \ a*c)" - by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) - finally show ?thesis . -qed - -lemma le_divide_eq: - "(a \ b/c) = - (if 0 < c then a*c \ b - else if c < 0 then b \ a*c - else a \ (0::'a::{linordered_field,division_by_zero}))" -apply (cases "c=0", simp) -apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff) -done - -lemma pos_divide_le_eq: "0 < (c::'a::linordered_field) ==> (b/c \ a) = (b \ a*c)" -proof - - assume less: "0 a) = ((b/c)*c \ a*c)" - by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) - also have "... = (b \ a*c)" - by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) - finally show ?thesis . -qed - -lemma neg_divide_le_eq: "c < (0::'a::linordered_field) ==> (b/c \ a) = (a*c \ b)" -proof - - assume less: "c<0" - hence "(b/c \ a) = (a*c \ (b/c)*c)" - by (simp add: mult_le_cancel_right order_less_not_sym [OF less]) - also have "... = (a*c \ b)" - by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) - finally show ?thesis . -qed - lemma divide_le_eq: "(b/c \ a) = (if 0 < c then b \ a*c @@ -595,28 +731,6 @@ apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) done -lemma pos_less_divide_eq: - "0 < (c::'a::linordered_field) ==> (a < b/c) = (a*c < b)" -proof - - assume less: "0 (a < b/c) = (b < a*c)" -proof - - assume less: "c<0" - hence "(a < b/c) = ((b/c)*c < a*c)" - by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less]) - also have "... = (b < a*c)" - by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) - finally show ?thesis . -qed - lemma less_divide_eq: "(a < b/c) = (if 0 < c then a*c < b @@ -626,28 +740,6 @@ apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff) done -lemma pos_divide_less_eq: - "0 < (c::'a::linordered_field) ==> (b/c < a) = (b < a*c)" -proof - - assume less: "0 (b/c < a) = (a*c < b)" -proof - - assume less: "c<0" - hence "(b/c < a) = (a*c < (b/c)*c)" - by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less]) - also have "... = (a*c < b)" - by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) - finally show ?thesis . -qed - lemma divide_less_eq: "(b/c < a) = (if 0 < c then b < a*c @@ -657,45 +749,7 @@ apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) done - -subsection{*Field simplification*} - -text{* Lemmas @{text field_simps} multiply with denominators in in(equations) -if they can be proved to be non-zero (for equations) or positive/negative -(for inequations). Can be too aggressive and is therefore separate from the -more benign @{text algebra_simps}. *} - -lemmas field_simps[no_atp] = field_eq_simps - (* multiply ineqn *) - pos_divide_less_eq neg_divide_less_eq - pos_less_divide_eq neg_less_divide_eq - pos_divide_le_eq neg_divide_le_eq - pos_le_divide_eq neg_le_divide_eq - -text{* Lemmas @{text sign_simps} is a first attempt to automate proofs -of positivity/negativity needed for @{text field_simps}. Have not added @{text -sign_simps} to @{text field_simps} because the former can lead to case -explosions. *} - -lemmas sign_simps[no_atp] = group_simps - zero_less_mult_iff mult_less_0_iff - -(* Only works once linear arithmetic is installed: -text{*An example:*} -lemma fixes a b c d e f :: "'a::linordered_field" -shows "\a>b; c \ - ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) < - ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u" -apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0") - prefer 2 apply(simp add:sign_simps) -apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0") - prefer 2 apply(simp add:sign_simps) -apply(simp add:field_simps) -done -*) - - -subsection{*Division and Signs*} +text {*Division and Signs*} lemma zero_less_divide_iff: "((0::'a::{linordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" @@ -716,71 +770,9 @@ (0 \ a & b \ 0 | a \ 0 & 0 \ b)" by (simp add: divide_inverse mult_le_0_iff) -lemma divide_eq_0_iff [simp,no_atp]: - "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))" -by (simp add: divide_inverse) - -lemma divide_pos_pos: - "0 < (x::'a::linordered_field) ==> 0 < y ==> 0 < x / y" -by(simp add:field_simps) - - -lemma divide_nonneg_pos: - "0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y" -by(simp add:field_simps) - -lemma divide_neg_pos: - "(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0" -by(simp add:field_simps) - -lemma divide_nonpos_pos: - "(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0" -by(simp add:field_simps) - -lemma divide_pos_neg: - "0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0" -by(simp add:field_simps) - -lemma divide_nonneg_neg: - "0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0" -by(simp add:field_simps) - -lemma divide_neg_neg: - "(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y" -by(simp add:field_simps) - -lemma divide_nonpos_neg: - "(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y" -by(simp add:field_simps) - - -subsection{*Cancellation Laws for Division*} - -lemma divide_cancel_right [simp,no_atp]: - "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))" -apply (cases "c=0", simp) -apply (simp add: divide_inverse) -done - -lemma divide_cancel_left [simp,no_atp]: - "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" -apply (cases "c=0", simp) -apply (simp add: divide_inverse) -done - - -subsection {* Division and the Number One *} +text {* Division and the Number One *} text{*Simplify expressions equated with 1*} -lemma divide_eq_1_iff [simp,no_atp]: - "(a/b = 1) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" -apply (cases "b=0", simp) -apply (simp add: right_inverse_eq) -done - -lemma one_eq_divide_iff [simp,no_atp]: - "(1 = a/b) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" -by (simp add: eq_commute [of 1]) lemma zero_eq_1_divide_iff [simp,no_atp]: "((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)" @@ -806,49 +798,22 @@ declare zero_le_divide_1_iff [simp,no_atp] declare divide_le_0_1_iff [simp,no_atp] - -subsection {* Ordering Rules for Division *} - -lemma divide_strict_right_mono: - "[|a < b; 0 < c|] ==> a / c < b / (c::'a::linordered_field)" -by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono - positive_imp_inverse_positive) - lemma divide_right_mono: "[|a \ b; 0 \ c|] ==> a/c \ b/(c::'a::{linordered_field,division_by_zero})" by (force simp add: divide_strict_right_mono order_le_less) -lemma divide_right_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b +lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= b ==> c <= 0 ==> b / c <= a / c" apply (drule divide_right_mono [of _ _ "- c"]) apply auto done -lemma divide_strict_right_mono_neg: - "[|b < a; c < 0|] ==> a / c < b / (c::'a::linordered_field)" -apply (drule divide_strict_right_mono [of _ _ "-c"], simp) -apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) -done - -text{*The last premise ensures that @{term a} and @{term b} - have the same sign*} -lemma divide_strict_left_mono: - "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)" -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono) - -lemma divide_left_mono: - "[|b \ a; 0 \ c; 0 < a*b|] ==> c / a \ c / (b::'a::linordered_field)" -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono) - -lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b +lemma divide_left_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= b ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" apply (drule divide_left_mono [of _ _ "- c"]) apply (auto simp add: mult_commute) done -lemma divide_strict_left_mono_neg: - "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)" -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg) text{*Simplify quotients that are compared with the value 1.*} @@ -874,7 +839,7 @@ by (auto simp add: divide_less_eq) -subsection{*Conditional Simplification Rules: No Case Splits*} +text {*Conditional Simplification Rules: No Case Splits*} lemma le_divide_eq_1_pos [simp,no_atp]: fixes a :: "'a :: {linordered_field,division_by_zero}" @@ -926,125 +891,25 @@ shows "(b/a = 1) = ((a \ 0 & a = b))" by (auto simp add: divide_eq_eq) - -subsection {* Reasoning about inequalities with division *} - -lemma mult_imp_div_pos_le: "0 < (y::'a::linordered_field) ==> x <= z * y ==> - x / y <= z" -by (subst pos_divide_le_eq, assumption+) - -lemma mult_imp_le_div_pos: "0 < (y::'a::linordered_field) ==> z * y <= x ==> - z <= x / y" -by(simp add:field_simps) - -lemma mult_imp_div_pos_less: "0 < (y::'a::linordered_field) ==> x < z * y ==> - x / y < z" -by(simp add:field_simps) - -lemma mult_imp_less_div_pos: "0 < (y::'a::linordered_field) ==> z * y < x ==> - z < x / y" -by(simp add:field_simps) - -lemma frac_le: "(0::'a::linordered_field) <= x ==> - x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" - apply (rule mult_imp_div_pos_le) - apply simp - apply (subst times_divide_eq_left) - apply (rule mult_imp_le_div_pos, assumption) - apply (rule mult_mono) - apply simp_all -done - -lemma frac_less: "(0::'a::linordered_field) <= x ==> - x < y ==> 0 < w ==> w <= z ==> x / z < y / w" - apply (rule mult_imp_div_pos_less) - apply simp - apply (subst times_divide_eq_left) - apply (rule mult_imp_less_div_pos, assumption) - apply (erule mult_less_le_imp_less) - apply simp_all -done - -lemma frac_less2: "(0::'a::linordered_field) < x ==> - x <= y ==> 0 < w ==> w < z ==> x / z < y / w" - apply (rule mult_imp_div_pos_less) - apply simp_all - apply (subst times_divide_eq_left) - apply (rule mult_imp_less_div_pos, assumption) - apply (erule mult_le_less_imp_less) - apply simp_all -done - -text{*It's not obvious whether these should be simprules or not. - Their effect is to gather terms into one big fraction, like - a*b*c / x*y*z. The rationale for that is unclear, but many proofs - seem to need them.*} - -declare times_divide_eq [simp] - - -subsection {* Ordered Fields are Dense *} - -lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)" -by (simp add: field_simps zero_less_two) - -lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b" -by (simp add: field_simps zero_less_two) - -instance linordered_field < dense_linorder -proof - fix x y :: 'a - have "x < x + 1" by simp - then show "\y. x < y" .. - have "x - 1 < x" by simp - then show "\y. y < x" .. - show "x < y \ \z>x. z < y" by (blast intro!: less_half_sum gt_half_sum) -qed - - -subsection {* Absolute Value *} - -lemma nonzero_abs_inverse: - "a \ 0 ==> abs (inverse (a::'a::linordered_field)) = inverse (abs a)" -apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq - negative_imp_inverse_negative) -apply (blast intro: positive_imp_inverse_positive elim: order_less_asym) -done - lemma abs_inverse [simp]: - "abs (inverse (a::'a::{linordered_field,division_by_zero})) = - inverse (abs a)" + "\inverse (a::'a::{linordered_field,division_by_zero})\ = + inverse \a\" apply (cases "a=0", simp) apply (simp add: nonzero_abs_inverse) done -lemma nonzero_abs_divide: - "b \ 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b" -by (simp add: divide_inverse abs_mult nonzero_abs_inverse) - lemma abs_divide [simp]: - "abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b" + "\a / (b::'a::{linordered_field,division_by_zero})\ = \a\ / \b\" apply (cases "b=0", simp) apply (simp add: nonzero_abs_divide) done -lemma abs_div_pos: "(0::'a::{division_by_zero,linordered_field}) < y ==> - abs x / y = abs (x / y)" +lemma abs_div_pos: "(0::'a::{linordered_field,division_by_zero}) < y ==> + \x\ / y = \x / y\" apply (subst abs_divide) apply (simp add: order_less_imp_le) done -lemma field_le_epsilon: - fixes x y :: "'a\linordered_field" - assumes e: "\e. 0 < e \ x \ y + e" - shows "x \ y" -proof (rule dense_le) - fix t assume "t < x" - hence "0 < x - t" by (simp add: less_diff_eq) - from e[OF this] - show "t \ y" by (simp add: field_simps) -qed - lemma field_le_mult_one_interval: fixes x :: "'a\{linordered_field,division_by_zero}" assumes *: "\z. \ 0 < z ; z < 1 \ \ z * x \ y" diff -r c805033ad032 -r 72f4d079ebf8 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Fri Apr 23 13:58:14 2010 +0200 +++ b/src/HOL/Rings.thy Fri Apr 23 13:58:14 2010 +0200 @@ -487,6 +487,125 @@ "a \ 0 \ b \ 0 \ inverse a - inverse b = inverse a * (b - a) * inverse b" by (simp add: algebra_simps) +lemma right_inverse_eq: "b \ 0 \ a / b = 1 \ a = b" +proof + assume neq: "b \ 0" + { + hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc) + also assume "a / b = 1" + finally show "a = b" by simp + next + assume "a = b" + with neq show "a / b = 1" by (simp add: divide_inverse) + } +qed + +lemma nonzero_inverse_eq_divide: "a \ 0 \ inverse a = 1 / a" +by (simp add: divide_inverse) + +lemma divide_self [simp]: "a \ 0 \ a / a = 1" +by (simp add: divide_inverse) + +lemma divide_zero_left [simp]: "0 / a = 0" +by (simp add: divide_inverse) + +lemma inverse_eq_divide: "inverse a = 1 / a" +by (simp add: divide_inverse) + +lemma add_divide_distrib: "(a+b) / c = a/c + b/c" +by (simp add: divide_inverse algebra_simps) + +lemma divide_1 [simp]: "a / 1 = a" + by (simp add: divide_inverse) + +lemma times_divide_eq_right: "a * (b / c) = (a * b) / c" + by (simp add: divide_inverse mult_assoc) + +lemma minus_divide_left: "- (a / b) = (-a) / b" + by (simp add: divide_inverse) + +lemma nonzero_minus_divide_right: "b \ 0 ==> - (a / b) = a / (- b)" + by (simp add: divide_inverse nonzero_inverse_minus_eq) + +lemma nonzero_minus_divide_divide: "b \ 0 ==> (-a) / (-b) = a / b" + by (simp add: divide_inverse nonzero_inverse_minus_eq) + +lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)" + by (simp add: divide_inverse) + +lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" + by (simp add: diff_minus add_divide_distrib) + +lemma nonzero_eq_divide_eq: "c \ 0 \ a = b / c \ a * c = b" +proof - + assume [simp]: "c \ 0" + have "a = b / c \ a * c = (b / c) * c" by simp + also have "... \ a * c = b" by (simp add: divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma nonzero_divide_eq_eq: "c \ 0 \ b / c = a \ b = a * c" +proof - + assume [simp]: "c \ 0" + have "b / c = a \ (b / c) * c = a * c" by simp + also have "... \ b = a * c" by (simp add: divide_inverse mult_assoc) + finally show ?thesis . +qed + +lemma divide_eq_imp: "c \ 0 \ b = a * c \ b / c = a" + by (simp add: divide_inverse mult_assoc) + +lemma eq_divide_imp: "c \ 0 \ a * c = b \ a = b / c" + by (drule sym) (simp add: divide_inverse mult_assoc) + +end + +class division_by_zero = division_ring + + assumes inverse_zero [simp]: "inverse 0 = 0" +begin + +lemma divide_zero [simp]: + "a / 0 = 0" + by (simp add: divide_inverse) + +lemma divide_self_if [simp]: + "a / a = (if a = 0 then 0 else 1)" + by simp + +lemma inverse_nonzero_iff_nonzero [simp]: + "inverse a = 0 \ a = 0" + by rule (fact inverse_zero_imp_zero, simp) + +lemma inverse_minus_eq [simp]: + "inverse (- a) = - inverse a" +proof cases + assume "a=0" thus ?thesis by simp +next + assume "a\0" + thus ?thesis by (simp add: nonzero_inverse_minus_eq) +qed + +lemma inverse_eq_imp_eq: + "inverse a = inverse b \ a = b" +apply (cases "a=0 | b=0") + apply (force dest!: inverse_zero_imp_zero + simp add: eq_commute [of "0::'a"]) +apply (force dest!: nonzero_inverse_eq_imp_eq) +done + +lemma inverse_eq_iff_eq [simp]: + "inverse a = inverse b \ a = b" + by (force dest!: inverse_eq_imp_eq) + +lemma inverse_inverse_eq [simp]: + "inverse (inverse a) = a" +proof cases + assume "a=0" thus ?thesis by simp +next + assume "a\0" + thus ?thesis by (simp add: nonzero_inverse_inverse_eq) +qed + end class mult_mono = times + zero + ord + @@ -533,17 +652,17 @@ subclass ordered_semiring .. lemma mult_nonneg_nonneg: "0 \ a \ 0 \ b \ 0 \ a * b" -using mult_left_mono [of zero b a] by simp +using mult_left_mono [of 0 b a] by simp lemma mult_nonneg_nonpos: "0 \ a \ b \ 0 \ a * b \ 0" -using mult_left_mono [of b zero a] by simp +using mult_left_mono [of b 0 a] by simp lemma mult_nonpos_nonneg: "a \ 0 \ 0 \ b \ a * b \ 0" -using mult_right_mono [of a zero b] by simp +using mult_right_mono [of a 0 b] by simp text {* Legacy - use @{text mult_nonpos_nonneg} *} lemma mult_nonneg_nonpos2: "0 \ a \ b \ 0 \ b * a \ 0" -by (drule mult_right_mono [of b zero], auto) +by (drule mult_right_mono [of b 0], auto) lemma split_mult_neg_le: "(0 \ a & b \ 0) | (a \ 0 & 0 \ b) \ a * b \ 0" by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) @@ -597,17 +716,17 @@ by (force simp add: mult_strict_right_mono not_less [symmetric]) lemma mult_pos_pos: "0 < a \ 0 < b \ 0 < a * b" -using mult_strict_left_mono [of zero b a] by simp +using mult_strict_left_mono [of 0 b a] by simp lemma mult_pos_neg: "0 < a \ b < 0 \ a * b < 0" -using mult_strict_left_mono [of b zero a] by simp +using mult_strict_left_mono [of b 0 a] by simp lemma mult_neg_pos: "a < 0 \ 0 < b \ a * b < 0" -using mult_strict_right_mono [of a zero b] by simp +using mult_strict_right_mono [of a 0 b] by simp text {* Legacy - use @{text mult_neg_pos} *} lemma mult_pos_neg2: "0 < a \ b < 0 \ b * a < 0" -by (drule mult_strict_right_mono [of b zero], auto) +by (drule mult_strict_right_mono [of b 0], auto) lemma zero_less_mult_pos: "0 < a * b \ 0 < a \ 0 < b" @@ -763,18 +882,18 @@ lemma mult_left_mono_neg: "b \ a \ c \ 0 \ c * a \ c * b" - apply (drule mult_left_mono [of _ _ "uminus c"]) + apply (drule mult_left_mono [of _ _ "- c"]) apply simp_all done lemma mult_right_mono_neg: "b \ a \ c \ 0 \ a * c \ b * c" - apply (drule mult_right_mono [of _ _ "uminus c"]) + apply (drule mult_right_mono [of _ _ "- c"]) apply simp_all done lemma mult_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a * b" -using mult_right_mono_neg [of a zero b] by simp +using mult_right_mono_neg [of a 0 b] by simp lemma split_mult_pos_le: "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a * b" @@ -821,7 +940,7 @@ using mult_strict_right_mono [of b a "- c"] by simp lemma mult_neg_neg: "a < 0 \ b < 0 \ 0 < a * b" -using mult_strict_right_mono_neg [of a zero b] by simp +using mult_strict_right_mono_neg [of a 0 b] by simp subclass ring_no_zero_divisors proof @@ -973,7 +1092,7 @@ lemma pos_add_strict: shows "0 < a \ b < c \ b < a + c" - using add_strict_mono [of zero a b c] by simp + using add_strict_mono [of 0 a b c] by simp lemma zero_le_one [simp]: "0 \ 1" by (rule zero_less_one [THEN less_imp_le]) @@ -1074,7 +1193,7 @@ "sgn (a * b) = sgn a * sgn b" by (auto simp add: sgn_if zero_less_mult_iff) -lemma abs_sgn: "abs k = k * sgn k" +lemma abs_sgn: "\k\ = k * sgn k" unfolding sgn_if abs_if by auto lemma sgn_greater [simp]: @@ -1085,14 +1204,14 @@ "sgn a < 0 \ a < 0" unfolding sgn_if by auto -lemma abs_dvd_iff [simp]: "(abs m) dvd k \ m dvd k" +lemma abs_dvd_iff [simp]: "\m\ dvd k \ m dvd k" by (simp add: abs_if) -lemma dvd_abs_iff [simp]: "m dvd (abs k) \ m dvd k" +lemma dvd_abs_iff [simp]: "m dvd \k\ \ m dvd k" by (simp add: abs_if) lemma dvd_if_abs_eq: - "abs l = abs (k) \ l dvd k" + "\l\ = \k\ \ l dvd k" by(subst abs_dvd_iff[symmetric]) simp end @@ -1110,17 +1229,7 @@ mult_cancel_right1 mult_cancel_right2 mult_cancel_left1 mult_cancel_left2 --- {* FIXME continue localization here *} - -subsection {* Reasoning about inequalities with division *} - -lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1 - ==> x * y <= x" -by (auto simp add: mult_le_cancel_left2) - -lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1 - ==> y * x <= x" -by (auto simp add: mult_le_cancel_right2) +text {* Reasoning about inequalities with division *} context linordered_semidom begin @@ -1137,20 +1246,34 @@ end +context linordered_idom +begin -subsection {* Absolute Value *} +lemma mult_right_le_one_le: + "0 \ x \ 0 \ y \ y \ 1 \ x * y \ x" + by (auto simp add: mult_le_cancel_left2) + +lemma mult_left_le_one_le: + "0 \ x \ 0 \ y \ y \ 1 \ y * x \ x" + by (auto simp add: mult_le_cancel_right2) + +end + +text {* Absolute Value *} context linordered_idom begin -lemma mult_sgn_abs: "sgn x * abs x = x" +lemma mult_sgn_abs: + "sgn x * \x\ = x" unfolding abs_if sgn_if by auto +lemma abs_one [simp]: + "\1\ = 1" + by (simp add: abs_if zero_less_one [THEN less_not_sym]) + end -lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)" -by (simp add: abs_if zero_less_one [THEN order_less_not_sym]) - class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs + assumes abs_eq_mult: "(0 \ a \ a \ 0) \ (0 \ b \ b \ 0) \ \a * b\ = \a\ * \b\" @@ -1162,39 +1285,35 @@ qed (auto simp add: abs_if not_less mult_less_0_iff) lemma abs_mult: - "abs (a * b) = abs a * abs b" + "\a * b\ = \a\ * \b\" by (rule abs_eq_mult) auto lemma abs_mult_self: - "abs a * abs a = a * a" + "\a\ * \a\ = a * a" by (simp add: abs_if) -end - lemma abs_mult_less: - "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)" + "\a\ < c \ \b\ < d \ \a\ * \b\ < c * d" proof - - assume ac: "abs a < c" - hence cpos: "0a\ < c" + hence cpos: "0b\ < d" thus ?thesis by (simp add: ac cpos mult_strict_mono) qed -lemmas eq_minus_self_iff[no_atp] = equal_neg_zero - -lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))" - unfolding order_less_le less_eq_neg_nonpos equal_neg_zero .. +lemma less_minus_self_iff: + "a < - a \ a < 0" + by (simp only: less_le less_eq_neg_nonpos equal_neg_zero) -lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))" -apply (simp add: order_less_le abs_le_iff) -apply (auto simp add: abs_if) -done +lemma abs_less_iff: + "\a\ < b \ a < b \ - a < b" + by (simp add: less_le abs_le_iff) (auto simp add: abs_if) -lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==> - (abs y) * x = abs (y * x)" - apply (subst abs_mult) - apply simp -done +lemma abs_mult_pos: + "0 \ x \ \y\ * x = \y * x\" + by (simp add: abs_mult) + +end code_modulename SML Rings Arith