# HG changeset patch # User haftmann # Date 1272028679 -7200 # Node ID 6984744e6b3427f4d7e489803f24b9a0c3808812 # Parent 80e3f43306cf07eed68b76ef50ec1615cbf61252 less special treatment of times_divide_eq [simp] diff -r 80e3f43306cf -r 6984744e6b34 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Fri Apr 23 15:17:59 2010 +0200 +++ b/src/HOL/Fields.thy Fri Apr 23 15:17:59 2010 +0200 @@ -52,7 +52,7 @@ "\b \ 0; c \ 0\ \ (a * c) / (b * c) = a / b" by (simp add: mult_commute [of _ c]) -lemma times_divide_eq_left: "(b / c) * a = (b * a) / c" +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. *} @@ -395,7 +395,7 @@ proof - assume less: "0 b/c) = (a*c \ (b/c)*c)" - by (simp add: mult_le_cancel_right less_not_sym [OF less]) + 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 . @@ -405,7 +405,7 @@ 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]) + 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 . @@ -416,7 +416,7 @@ proof - assume less: "0 a) = ((b/c)*c \ a*c)" - by (simp add: mult_le_cancel_right less_not_sym [OF less]) + 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 . @@ -469,7 +469,7 @@ 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]) + 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 . @@ -487,8 +487,6 @@ 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 @@ -609,7 +607,6 @@ 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 @@ -620,8 +617,6 @@ 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) diff -r 80e3f43306cf -r 6984744e6b34 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Fri Apr 23 15:17:59 2010 +0200 +++ b/src/HOL/Rings.thy Fri Apr 23 15:17:59 2010 +0200 @@ -518,7 +518,7 @@ lemma divide_1 [simp]: "a / 1 = a" by (simp add: divide_inverse) -lemma times_divide_eq_right: "a * (b / c) = (a * b) / c" +lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c" by (simp add: divide_inverse mult_assoc) lemma minus_divide_left: "- (a / b) = (-a) / b"