# HG changeset patch # User haftmann # Date 1272043957 -7200 # Node ID f2753d6b085908592e11abfd793c322512d5f718 # Parent 9eaaa05c972c14ac94605bd0192c79d80e2841da# Parent 26eea417ccc4a87447b393e0571bc835e3bdaa54 merged diff -r 9eaaa05c972c -r f2753d6b0859 NEWS --- a/NEWS Fri Apr 23 16:12:57 2010 +0200 +++ b/NEWS Fri Apr 23 19:32:37 2010 +0200 @@ -112,6 +112,13 @@ *** HOL *** +* Abstract algebra: + * class division_by_zero includes division_ring; + * numerous lemmas have been ported from field to division_ring; + * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero. + + INCOMPATIBILITY. + * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT' provides abstract red-black tree type which is backed by RBT_Impl as implementation. INCOMPATIBILTY. diff -r 9eaaa05c972c -r f2753d6b0859 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Fri Apr 23 16:12:57 2010 +0200 +++ b/src/HOL/Big_Operators.thy Fri Apr 23 19:32:37 2010 +0200 @@ -555,7 +555,7 @@ qed lemma setsum_mono2: -fixes f :: "'a \ 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}" +fixes f :: "'a \ 'b :: ordered_comm_monoid_add" assumes fin: "finite B" and sub: "A \ B" and nn: "\b. b \ B-A \ 0 \ f b" shows "setsum f A \ setsum f B" proof - @@ -1030,7 +1030,7 @@ lemma setprod_diff1: "finite A ==> f a \ 0 ==> (setprod f (A - {a}) :: 'a :: {field}) = (if a:A then setprod f A / f a else setprod f A)" -by (erule finite_induct) (auto simp add: insert_Diff_if) + by (erule finite_induct) (auto simp add: insert_Diff_if) lemma setprod_inversef: fixes f :: "'b \ 'a::{field,division_by_zero}" diff -r 9eaaa05c972c -r f2753d6b0859 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Apr 23 16:12:57 2010 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Apr 23 19:32:37 2010 +0200 @@ -33,7 +33,7 @@ @{thm "real_of_nat_number_of"}, @{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"}, @{thm "real_of_int_zero"}, @{thm "real_of_nat_zero"}, - @{thm "Fields.divide_zero"}, + @{thm "divide_zero"}, @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"}, @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, @{thm "diff_def"}, @{thm "minus_divide_left"}] diff -r 9eaaa05c972c -r f2753d6b0859 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Fri Apr 23 16:12:57 2010 +0200 +++ b/src/HOL/Fields.thy Fri Apr 23 19:32:37 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) +lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c" + 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,392 @@ 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] del: times_divide_eq) + 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] del: times_divide_eq) + 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] del: times_divide_eq) + 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] del: times_divide_eq) + 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] del: times_divide_eq) + 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] del: times_divide_eq) + 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 + +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 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 (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.*} + +lemma less_half_sum: "a a < (a+b) / (1+1)" +by (simp add: field_simps zero_less_two) + +lemma gt_half_sum: "a (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 +687,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 +705,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 +717,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 +726,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/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 +744,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 +765,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 +793,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 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 +834,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 +886,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 a < (a+b) / (1+1::'a::linordered_field)" -by (simp add: field_simps zero_less_two) - -lemma gt_half_sum: "a (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 9eaaa05c972c -r f2753d6b0859 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri Apr 23 16:12:57 2010 +0200 +++ b/src/HOL/Groebner_Basis.thy Fri Apr 23 19:32:37 2010 +0200 @@ -627,7 +627,7 @@ val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, @{thm "divide_Numeral1"}, - @{thm "Fields.divide_zero"}, @{thm "divide_Numeral0"}, + @{thm "divide_zero"}, @{thm "divide_Numeral0"}, @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"}, @{thm "mult_num_frac"}, @{thm "mult_frac_num"}, @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"}, diff -r 9eaaa05c972c -r f2753d6b0859 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Fri Apr 23 16:12:57 2010 +0200 +++ b/src/HOL/Groups.thy Fri Apr 23 19:32:37 2010 +0200 @@ -757,7 +757,7 @@ done lemma less_diff_eq[algebra_simps]: "a < c - b \ a + b < c" -apply (subst less_iff_diff_less_0 [of "plus a b"]) +apply (subst less_iff_diff_less_0 [of "a + b"]) apply (subst less_iff_diff_less_0 [of a]) apply (simp add: diff_minus add_ac) done @@ -966,27 +966,26 @@ end --- {* FIXME localize the following *} +context ordered_comm_monoid_add +begin lemma add_increasing: - fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" - shows "[|0\a; b\c|] ==> b \ a + c" -by (insert add_mono [of 0 a b c], simp) + "0 \ a \ b \ c \ b \ a + c" + by (insert add_mono [of 0 a b c], simp) lemma add_increasing2: - fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" - shows "[|0\c; b\a|] ==> b \ a + c" -by (simp add:add_increasing add_commute[of a]) + "0 \ c \ b \ a \ b \ a + c" + by (simp add: add_increasing add_commute [of a]) lemma add_strict_increasing: - fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" - shows "[|0c|] ==> b < a + c" -by (insert add_less_le_mono [of 0 a b c], simp) + "0 < a \ b \ c \ b < a + c" + by (insert add_less_le_mono [of 0 a b c], simp) lemma add_strict_increasing2: - fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}" - shows "[|0\a; b b < a + c" -by (insert add_le_less_mono [of 0 a b c], simp) + "0 \ a \ b < c \ b < a + c" + by (insert add_le_less_mono [of 0 a b c], simp) + +end class abs = fixes abs :: "'a \ 'a" @@ -1036,7 +1035,7 @@ lemma abs_idempotent [simp]: "\\a\\ = \a\" by (rule antisym) - (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"]) + (auto intro!: abs_ge_self abs_leI order_trans [of "- \a\" 0 "\a\"]) lemma abs_eq_0 [simp]: "\a\ = 0 \ a = 0" proof - @@ -1045,7 +1044,7 @@ assume zero: "\a\ = 0" with abs_ge_self show "a \ 0" by auto from zero have "\-a\ = 0" by simp - with abs_ge_self [of "uminus a"] have "- a \ 0" by auto + with abs_ge_self [of "- a"] have "- a \ 0" by auto with neg_le_0_iff_le show "0 \ a" by auto qed then show ?thesis by auto @@ -1114,32 +1113,31 @@ by (insert abs_ge_self, blast intro: order_trans) lemma abs_le_D2: "\a\ \ b \ - a \ b" -by (insert abs_le_D1 [of "uminus a"], simp) +by (insert abs_le_D1 [of "- a"], simp) lemma abs_le_iff: "\a\ \ b \ a \ b \ - a \ b" by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) lemma abs_triangle_ineq2: "\a\ - \b\ \ \a - b\" - apply (simp add: algebra_simps) - apply (subgoal_tac "abs a = abs (plus b (minus a b))") - apply (erule ssubst) - apply (rule abs_triangle_ineq) - apply (rule arg_cong[of _ _ abs]) - apply (simp add: algebra_simps) -done +proof - + have "\a\ = \b + (a - b)\" + by (simp add: algebra_simps add_diff_cancel) + then have "\a\ \ \b\ + \a - b\" + by (simp add: abs_triangle_ineq) + then show ?thesis + by (simp add: algebra_simps) +qed + +lemma abs_triangle_ineq2_sym: "\a\ - \b\ \ \b - a\" + by (simp only: abs_minus_commute [of b] abs_triangle_ineq2) lemma abs_triangle_ineq3: "\\a\ - \b\\ \ \a - b\" - apply (subst abs_le_iff) - apply auto - apply (rule abs_triangle_ineq2) - apply (subst abs_minus_commute) - apply (rule abs_triangle_ineq2) -done + by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym) lemma abs_triangle_ineq4: "\a - b\ \ \a\ + \b\" proof - - have "abs(a - b) = abs(a + - b)" by (subst diff_minus, rule refl) - also have "... <= abs a + abs (- b)" by (rule abs_triangle_ineq) + have "\a - b\ = \a + - b\" by (subst diff_minus, rule refl) + also have "... \ \