\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def) diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Deriv.thy Wed Apr 09 09:37:47 2014 +0200 @@ -825,7 +825,7 @@ lemma DERIV_mirror: "(DERIV f (- x) :> y) \ (DERIV (\x. f (- x::real) :: real) x :> - y)" - by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right divide_minus_right + by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right tendsto_minus_cancel_left field_simps conj_commute) text {* Caratheodory formulation of derivative at a point *} @@ -908,8 +908,8 @@ fix h::real assume "0 < h" "h < s" with all [of "-h"] show "f x < f (x-h)" - proof (simp add: abs_if pos_less_divide_eq divide_minus_right split add: split_if_asm) - assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h" + proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm) + assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h" with l have "0 < (f (x-h) - f x) / h" by arith thus "f x < f (x-h)" @@ -1628,8 +1628,7 @@ ((\ x. (f' x / g' x)) ---> y) (at_left x) \ ((\ x. f x / g x) ---> y) (at_left x)" unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror - by (rule lhopital_right[where f'="\x. - f' (- x)"]) - (auto simp: DERIV_mirror divide_minus_left divide_minus_right) + by (rule lhopital_right[where f'="\x. - f' (- x)"]) (auto simp: DERIV_mirror) lemma lhopital: "((f::real \ real) ---> 0) (at x) \ (g ---> 0) (at x) \ @@ -1740,8 +1739,7 @@ ((\ x. (f' x / g' x)) ---> y) (at_left x) \ ((\ x. f x / g x) ---> y) (at_left x)" unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror - by (rule lhopital_right_at_top[where f'="\x. - f' (- x)"]) - (auto simp: divide_minus_left divide_minus_right DERIV_mirror) + by (rule lhopital_right_at_top[where f'="\x. - f' (- x)"]) (auto simp: DERIV_mirror) lemma lhopital_at_top: "LIM x at x. (g::real \ real) x :> at_top \ @@ -1798,7 +1796,7 @@ unfolding filterlim_at_right_to_top apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim]) using eventually_ge_at_top[where c="1::real"] - by eventually_elim (simp add: divide_minus_left divide_minus_right) + by eventually_elim simp qed end diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Fields.thy Wed Apr 09 09:37:47 2014 +0200 @@ -152,11 +152,11 @@ lemma nonzero_minus_divide_divide: "b \ 0 ==> (-a) / (-b) = a / b" by (simp add: divide_inverse nonzero_inverse_minus_eq) -lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)" +lemma divide_minus_left [simp]: "(-a) / b = - (a / b)" by (simp add: divide_inverse) lemma diff_divide_distrib: "(a - b) / c = a / c - b / c" - using add_divide_distrib [of a "- b" c] by (simp add: divide_inverse) + using add_divide_distrib [of a "- b" c] by simp lemma nonzero_eq_divide_eq [field_simps]: "c \ 0 \ a = b / c \ a * c = b" proof - @@ -416,11 +416,11 @@ "- (a / b) = a / - b" by (simp add: divide_inverse) -lemma divide_minus_right [field_simps]: +lemma divide_minus_right [simp]: "a / - b = - (a / b)" by (simp add: divide_inverse) -lemma minus_divide_divide [simp]: +lemma minus_divide_divide: "(- a) / (- b) = a / b" apply (cases "b=0", simp) apply (simp add: nonzero_minus_divide_divide) @@ -1053,13 +1053,13 @@ lemma divide_right_mono_neg: "a <= b ==> c <= 0 ==> b / c <= a / c" apply (drule divide_right_mono [of _ _ "- c"]) -apply (auto simp: divide_minus_right) +apply auto done lemma divide_left_mono_neg: "a <= b ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" apply (drule divide_left_mono [of _ _ "- c"]) - apply (auto simp add: divide_minus_left mult_commute) + apply (auto simp add: mult_commute) done lemma inverse_le_iff: diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Library/Convex.thy --- a/src/HOL/Library/Convex.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Library/Convex.thy Wed Apr 09 09:37:47 2014 +0200 @@ -656,7 +656,7 @@ proof - have "\z. z > 0 \ DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto then have f': "\z. z > 0 \ DERIV (\ z. - log b z) z :> - 1 / (ln b * z)" - by (auto simp: divide_minus_left DERIV_minus) + by (auto simp: DERIV_minus) have "\z :: real. z > 0 \ DERIV inverse z :> - (inverse z ^ Suc (Suc 0))" using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto from this[THEN DERIV_cmult, of _ "- 1 / ln b"] @@ -664,7 +664,7 @@ DERIV (\ z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))" by auto then have f''0: "\z :: real. z > 0 \ DERIV (\ z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)" - by (auto simp add: inverse_eq_divide divide_minus_left mult_assoc) + unfolding inverse_eq_divide by (auto simp add: mult_assoc) have f''_ge0: "\z :: real. z > 0 \ 1 / (ln b * z * z) \ 0" using `b > 1` by (auto intro!:less_imp_le simp add: divide_pos_pos[of 1] mult_pos_pos) from f''_ge0_imp_convex[OF pos_is_convex, diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Library/Float.thy Wed Apr 09 09:37:47 2014 +0200 @@ -637,7 +637,7 @@ qed thus ?thesis using `\ b dvd a` by simp qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric] - floor_divide_eq_div dvd_neg_div del: real_of_int_minus) + floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus) lemma compute_float_up[code]: "float_up p (Float m e) = @@ -1004,7 +1004,7 @@ else (if 0 < y then - (rapprox_posrat prec (nat (-x)) (nat y)) else lapprox_posrat prec (nat (-x)) (nat (-y))))" - by transfer (auto simp: round_up_def divide_minus_left divide_minus_right round_down_def ceiling_def ac_simps) + by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps) hide_fact (open) compute_lapprox_rat lift_definition rapprox_rat :: "nat \ int \ int \ float" is @@ -1019,7 +1019,7 @@ else (if 0 < y then - (lapprox_posrat prec (nat (-x)) (nat y)) else rapprox_posrat prec (nat (-x)) (nat (-y))))" - by transfer (auto simp: round_up_def round_down_def divide_minus_left divide_minus_right ceiling_def ac_simps) + by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps) hide_fact (open) compute_rapprox_rat subsection {* Division *} diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 09 09:37:47 2014 +0200 @@ -3635,7 +3635,7 @@ done lemma fps_sin_even: "fps_sin (- c) = - fps_sin c" - by (auto simp add: divide_minus_left fps_eq_iff fps_sin_def) + by (auto simp add: fps_eq_iff fps_sin_def) lemma fps_cos_odd: "fps_cos (- c) = fps_cos c" by (auto simp add: fps_eq_iff fps_cos_def) diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Apr 09 09:37:47 2014 +0200 @@ -998,7 +998,7 @@ f (Suc n) u * (z-u) ^ n / of_nat (fact n) + f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / of_nat (fact (Suc n)) - f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / of_nat (fact (Suc n))" - using Suc by (simp add: divide_minus_left) + using Suc by simp also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n))" proof - have "of_nat(fact(Suc n)) * diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 09 09:37:47 2014 +0200 @@ -2277,7 +2277,9 @@ using Min_ge_iff[of i 0 ] and obt(1) unfolding t_def i_def using obt(4)[unfolded le_less] - apply (auto simp: divide_le_0_iff divide_minus_right) + apply auto + unfolding divide_le_0_iff + apply auto done have t: "\v\s. u v + t * w v \ 0" proof @@ -2314,7 +2316,7 @@ obtain a where "a \ s" and "t = (\v. (u v) / (- w v)) a" and "w a < 0" using Min_in[OF _ `i\{}`] and obt(1) unfolding i_def t_def by auto - then have a: "a \ s" "u a + t * w a = 0" by (auto simp: divide_minus_right) + then have a: "a \ s" "u a + t * w a = 0" by auto have *: "\f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)" unfolding setsum_diff1'[OF obt(1) `a\s`] by auto have "(\v\s. u v + t * w v) = 1" diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 09 09:37:47 2014 +0200 @@ -1149,7 +1149,7 @@ setsum (\v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v" using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps) also have "\ = ?a" - unfolding scaleR_right.setsum [symmetric] u using uv by (simp add: divide_minus_left) + unfolding scaleR_right.setsum [symmetric] u using uv by simp finally have "setsum (\v. ?u v *\<^sub>R v) ?S = ?a" . with th0 have ?lhs unfolding dependent_def span_explicit @@ -2143,7 +2143,7 @@ case False with span_mul[OF th, of "- 1/ k"] have th1: "f a \ span (f ` b)" - by (auto simp: divide_minus_left) + by auto from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric] have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"] diff -r 92345da2349f -r 91958d4b30f7 src/HOL/NSA/HDeriv.thy --- a/src/HOL/NSA/HDeriv.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/NSA/HDeriv.thy Wed Apr 09 09:37:47 2014 +0200 @@ -359,7 +359,7 @@ have "inverse (- (h * star_of x) + - (star_of x * star_of x)) = (inverse (star_of x + h) - inverse (star_of x)) / h" apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric] - nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs divide_minus_left) + nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs) apply (subst nonzero_inverse_minus_eq [symmetric]) using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp apply (simp add: field_simps) diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Probability/Information.thy Wed Apr 09 09:37:47 2014 +0200 @@ -945,7 +945,7 @@ show "- (\ x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \MX) = log b (measure MX A)" unfolding eq using uniform_distributed_params[OF X] - by (subst lebesgue_integral_cmult) (auto simp: divide_minus_left measure_def) + by (subst lebesgue_integral_cmult) (auto simp: measure_def) qed lemma (in information_space) entropy_simple_distributed: diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Apr 09 09:37:47 2014 +0200 @@ -241,7 +241,7 @@ by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq) from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this with S have "?P (S \ X) S n" - by (simp add: divide_minus_left measure_restricted sets_eq sets.Int) (metis inf_absorb2) + by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2) hence "\A. ?P A S n" .. } note Ex_P = this def A \ "rec_nat (space M) (\n A. SOME B. ?P B A n)" @@ -280,7 +280,7 @@ hence "0 < - ?d B" by auto from ex_inverse_of_nat_Suc_less[OF this] obtain n where *: "?d B < - 1 / real (Suc n)" - by (auto simp: divide_minus_left real_eq_of_nat inverse_eq_divide field_simps) + by (auto simp: real_eq_of_nat inverse_eq_divide field_simps) have "B \ A (Suc n)" using B by (auto simp del: nat.rec(2)) from epsilon[OF B(1) this] * show False by auto diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Rat.thy Wed Apr 09 09:37:47 2014 +0200 @@ -665,7 +665,7 @@ by transfer (simp add: add_frac_eq) lemma of_rat_minus: "of_rat (- a) = - of_rat a" - by transfer (simp add: divide_minus_left) + by transfer simp lemma of_rat_neg_one [simp]: "of_rat (- 1) = - 1" diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Apr 09 09:37:47 2014 +0200 @@ -1116,10 +1116,10 @@ by (simp add: sgn_div_norm divide_inverse) lemma real_sgn_pos: "0 < (x::real) \ sgn x = 1" - by (rule sgn_pos) +unfolding real_sgn_eq by simp lemma real_sgn_neg: "(x::real) < 0 \ sgn x = -1" - by (rule sgn_neg) +unfolding real_sgn_eq by simp lemma norm_conv_dist: "norm x = dist x 0" unfolding dist_norm by simp diff -r 92345da2349f -r 91958d4b30f7 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Apr 08 23:16:00 2014 +0200 +++ b/src/HOL/Transcendental.thy Wed Apr 09 09:37:47 2014 +0200 @@ -2145,7 +2145,7 @@ lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)" unfolding cos_coeff_def sin_coeff_def - by (simp del: mult_Suc, auto simp add: divide_minus_left odd_Suc_mult_two_ex) + by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex) lemma summable_sin: "summable (\n. sin_coeff n * x ^ n)" unfolding sin_coeff_def @@ -2169,7 +2169,7 @@ by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc) lemma diffs_cos_coeff: "diffs cos_coeff = (\n. - sin_coeff n)" - by (simp add: divide_minus_left diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc) + by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc) text{*Now at last we can get the derivatives of exp, sin and cos*} @@ -3239,7 +3239,7 @@ assume "x \ {-1..1}" then show "x \ sin ` {- pi / 2..pi / 2}" using arcsin_lbound arcsin_ubound - by (intro image_eqI[where x="arcsin x"]) (auto simp: divide_minus_left) + by (intro image_eqI[where x="arcsin x"]) auto qed simp finally show ?thesis . qed @@ -3338,14 +3338,12 @@ lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))" by (rule filterlim_at_bot_at_right[where Q="\x. - pi/2 < x \ x < pi/2" and P="\x. True" and g=arctan]) - (auto simp: le_less eventually_at dist_real_def divide_minus_left - simp del: less_divide_eq_numeral1 + (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 intro!: tan_monotone exI[of _ "pi/2"]) lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))" by (rule filterlim_at_top_at_left[where Q="\x. - pi/2 < x \ x < pi/2" and P="\x. True" and g=arctan]) - (auto simp: le_less eventually_at dist_real_def divide_minus_left - simp del: less_divide_eq_numeral1 + (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1 intro!: tan_monotone exI[of _ "pi/2"]) lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top" @@ -3967,7 +3965,7 @@ show "tan (sgn x * pi / 2 - arctan x) = 1 / x" unfolding tan_inverse [of "arctan x", unfolded tan_arctan] unfolding sgn_real_def - by (simp add: divide_minus_left tan_def cos_arctan sin_arctan sin_diff cos_diff) + by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff) qed theorem pi_series: "pi / 4 = (\ k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")