removing simprule status for divide_minus_left and divide_minus_right
authorpaulson <lp15@cam.ac.uk>
Thu Apr 03 23:51:52 2014 +0100 (2014-04-03)
changeset 5640936489d77c484
parent 56408 3610e0a7693c
child 56410 a14831ac3023
removing simprule status for divide_minus_left and divide_minus_right
src/HOL/Complex.thy
src/HOL/Deriv.thy
src/HOL/Fields.thy
src/HOL/Library/Convex.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/NSA/HDeriv.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Rat.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Complex.thy	Fri Apr 04 16:43:47 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Thu Apr 03 23:51:52 2014 +0100
     1.3 @@ -145,7 +145,7 @@
     1.4    by (simp add: complex_inverse_def)
     1.5  
     1.6  instance
     1.7 -  by intro_classes (simp_all add: complex_mult_def
     1.8 +  by intro_classes (simp_all add: complex_mult_def divide_minus_left
     1.9      distrib_left distrib_right right_diff_distrib left_diff_distrib
    1.10      complex_inverse_def complex_divide_def
    1.11      power2_eq_square add_divide_distrib [symmetric]
    1.12 @@ -656,7 +656,7 @@
    1.13      moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
    1.14        by (metis add_divide_distrib)
    1.15      ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2`
    1.16 -      apply (simp add: complex_divide_def  zero_less_divide_iff less_divide_eq)
    1.17 +      apply (simp add: complex_divide_def divide_minus_left zero_less_divide_iff less_divide_eq)
    1.18        apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left)
    1.19        done
    1.20    qed
    1.21 @@ -844,7 +844,7 @@
    1.22      real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
    1.23        apply (induct n)
    1.24        apply (simp add: cos_coeff_def sin_coeff_def)
    1.25 -      apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
    1.26 +      apply (simp add: sin_coeff_Suc cos_coeff_Suc divide_minus_left del: mult_Suc)
    1.27        done } note * = this
    1.28    show "Re (cis b) = Re (exp (Complex 0 b))"
    1.29      unfolding exp_def cis_def cos_def
     2.1 --- a/src/HOL/Deriv.thy	Fri Apr 04 16:43:47 2014 +0200
     2.2 +++ b/src/HOL/Deriv.thy	Thu Apr 03 23:51:52 2014 +0100
     2.3 @@ -825,7 +825,7 @@
     2.4  
     2.5  lemma DERIV_mirror:
     2.6    "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
     2.7 -  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
     2.8 +  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right divide_minus_right
     2.9                  tendsto_minus_cancel_left field_simps conj_commute)
    2.10  
    2.11  text {* Caratheodory formulation of derivative at a point *}
    2.12 @@ -908,8 +908,8 @@
    2.13      fix h::real
    2.14      assume "0 < h" "h < s"
    2.15      with all [of "-h"] show "f x < f (x-h)"
    2.16 -    proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
    2.17 -      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
    2.18 +    proof (simp add: abs_if pos_less_divide_eq divide_minus_right split add: split_if_asm)
    2.19 +      assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h"
    2.20        with l
    2.21        have "0 < (f (x-h) - f x) / h" by arith
    2.22        thus "f x < f (x-h)"
    2.23 @@ -1628,7 +1628,8 @@
    2.24      ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
    2.25    ((\<lambda> x. f x / g x) ---> y) (at_left x)"
    2.26    unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
    2.27 -  by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
    2.28 +  by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) 
    2.29 +     (auto simp: DERIV_mirror divide_minus_left divide_minus_right)
    2.30  
    2.31  lemma lhopital:
    2.32    "((f::real \<Rightarrow> real) ---> 0) (at x) \<Longrightarrow> (g ---> 0) (at x) \<Longrightarrow>
    2.33 @@ -1739,7 +1740,8 @@
    2.34      ((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
    2.35      ((\<lambda> x. f x / g x) ---> y) (at_left x)"
    2.36    unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
    2.37 -  by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
    2.38 +  by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"])
    2.39 +     (auto simp: divide_minus_left divide_minus_right DERIV_mirror)
    2.40  
    2.41  lemma lhopital_at_top:
    2.42    "LIM x at x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
    2.43 @@ -1796,7 +1798,7 @@
    2.44      unfolding filterlim_at_right_to_top
    2.45      apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim])
    2.46      using eventually_ge_at_top[where c="1::real"]
    2.47 -    by eventually_elim simp
    2.48 +    by eventually_elim (simp add: divide_minus_left divide_minus_right)
    2.49  qed
    2.50  
    2.51  end
     3.1 --- a/src/HOL/Fields.thy	Fri Apr 04 16:43:47 2014 +0200
     3.2 +++ b/src/HOL/Fields.thy	Thu Apr 03 23:51:52 2014 +0100
     3.3 @@ -152,11 +152,11 @@
     3.4  lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
     3.5    by (simp add: divide_inverse nonzero_inverse_minus_eq)
     3.6  
     3.7 -lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
     3.8 +lemma divide_minus_left: "(-a) / b = - (a / b)"
     3.9    by (simp add: divide_inverse)
    3.10  
    3.11  lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
    3.12 -  using add_divide_distrib [of a "- b" c] by simp
    3.13 +  using add_divide_distrib [of a "- b" c] by (simp add: divide_inverse)
    3.14  
    3.15  lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
    3.16  proof -
    3.17 @@ -408,7 +408,7 @@
    3.18    "- (a / b) = a / - b"
    3.19    by (simp add: divide_inverse)
    3.20  
    3.21 -lemma divide_minus_right [simp]:
    3.22 +lemma divide_minus_right:
    3.23    "a / - b = - (a / b)"
    3.24    by (simp add: divide_inverse)
    3.25  
    3.26 @@ -1045,13 +1045,13 @@
    3.27  lemma divide_right_mono_neg: "a <= b 
    3.28      ==> c <= 0 ==> b / c <= a / c"
    3.29  apply (drule divide_right_mono [of _ _ "- c"])
    3.30 -apply auto
    3.31 +apply (auto simp: divide_minus_right)
    3.32  done
    3.33  
    3.34  lemma divide_left_mono_neg: "a <= b 
    3.35      ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
    3.36    apply (drule divide_left_mono [of _ _ "- c"])
    3.37 -  apply (auto simp add: mult_commute)
    3.38 +  apply (auto simp add: divide_minus_left mult_commute)
    3.39  done
    3.40  
    3.41  lemma inverse_le_iff:
     4.1 --- a/src/HOL/Library/Convex.thy	Fri Apr 04 16:43:47 2014 +0200
     4.2 +++ b/src/HOL/Library/Convex.thy	Thu Apr 03 23:51:52 2014 +0100
     4.3 @@ -656,7 +656,7 @@
     4.4  proof -
     4.5    have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
     4.6    then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
     4.7 -    by (auto simp: DERIV_minus)
     4.8 +    by (auto simp: divide_minus_left DERIV_minus)
     4.9    have "\<And>z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
    4.10      using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
    4.11    from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
    4.12 @@ -664,7 +664,7 @@
    4.13      DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
    4.14      by auto
    4.15    then have f''0: "\<And>z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
    4.16 -    unfolding inverse_eq_divide by (auto simp add: mult_assoc)
    4.17 +    by (auto simp add: inverse_eq_divide divide_minus_left mult_assoc)
    4.18    have f''_ge0: "\<And>z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
    4.19      using `b > 1` by (auto intro!:less_imp_le simp add: divide_pos_pos[of 1] mult_pos_pos)
    4.20    from f''_ge0_imp_convex[OF pos_is_convex,
     5.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Fri Apr 04 16:43:47 2014 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Apr 03 23:51:52 2014 +0100
     5.3 @@ -998,7 +998,7 @@
     5.4             f (Suc n) u * (z-u) ^ n / of_nat (fact n) +
     5.5             f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / of_nat (fact (Suc n)) -
     5.6             f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / of_nat (fact (Suc n))"
     5.7 -        using Suc by simp
     5.8 +        using Suc by (simp add: divide_minus_left)
     5.9        also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n))"
    5.10        proof -
    5.11          have "of_nat(fact(Suc n)) *
     6.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 04 16:43:47 2014 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Apr 03 23:51:52 2014 +0100
     6.3 @@ -2277,9 +2277,7 @@
     6.4        using Min_ge_iff[of i 0 ] and obt(1)
     6.5        unfolding t_def i_def
     6.6        using obt(4)[unfolded le_less]
     6.7 -      apply auto
     6.8 -      unfolding divide_le_0_iff
     6.9 -      apply auto
    6.10 +      apply (auto simp: divide_le_0_iff divide_minus_right)
    6.11        done
    6.12      have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
    6.13      proof
    6.14 @@ -2316,7 +2314,7 @@
    6.15  
    6.16      obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
    6.17        using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
    6.18 -    then have a: "a \<in> s" "u a + t * w a = 0" by auto
    6.19 +    then have a: "a \<in> s" "u a + t * w a = 0" by (auto simp: divide_minus_right)
    6.20      have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
    6.21        unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto
    6.22      have "(\<Sum>v\<in>s. u v + t * w v) = 1"
     7.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Apr 04 16:43:47 2014 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Apr 03 23:51:52 2014 +0100
     7.3 @@ -1139,7 +1139,7 @@
     7.4        setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
     7.5        using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps)
     7.6      also have "\<dots> = ?a"
     7.7 -      unfolding scaleR_right.setsum [symmetric] u using uv by simp
     7.8 +      unfolding scaleR_right.setsum [symmetric] u using uv by (simp add: divide_minus_left)
     7.9      finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
    7.10      with th0 have ?lhs
    7.11        unfolding dependent_def span_explicit
    7.12 @@ -2131,7 +2131,7 @@
    7.13      case False
    7.14      with span_mul[OF th, of "- 1/ k"]
    7.15      have th1: "f a \<in> span (f ` b)"
    7.16 -      by auto
    7.17 +      by (auto simp: divide_minus_left)
    7.18      from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
    7.19      have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
    7.20      from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
     8.1 --- a/src/HOL/NSA/HDeriv.thy	Fri Apr 04 16:43:47 2014 +0200
     8.2 +++ b/src/HOL/NSA/HDeriv.thy	Thu Apr 03 23:51:52 2014 +0100
     8.3 @@ -359,7 +359,7 @@
     8.4        have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
     8.5          (inverse (star_of x + h) - inverse (star_of x)) / h"
     8.6        apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
     8.7 -        nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
     8.8 +        nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs divide_minus_left)
     8.9        apply (subst nonzero_inverse_minus_eq [symmetric])
    8.10        using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
    8.11        apply (simp add: field_simps)
     9.1 --- a/src/HOL/Probability/Information.thy	Fri Apr 04 16:43:47 2014 +0200
     9.2 +++ b/src/HOL/Probability/Information.thy	Thu Apr 03 23:51:52 2014 +0100
     9.3 @@ -945,7 +945,7 @@
     9.4    show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
     9.5      log b (measure MX A)"
     9.6      unfolding eq using uniform_distributed_params[OF X]
     9.7 -    by (subst lebesgue_integral_cmult) (auto simp: measure_def)
     9.8 +    by (subst lebesgue_integral_cmult) (auto simp: divide_minus_left measure_def)
     9.9  qed
    9.10  
    9.11  lemma (in information_space) entropy_simple_distributed:
    10.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Apr 04 16:43:47 2014 +0200
    10.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Thu Apr 03 23:51:52 2014 +0100
    10.3 @@ -241,7 +241,7 @@
    10.4        by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
    10.5      from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
    10.6      with S have "?P (S \<inter> X) S n"
    10.7 -      by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
    10.8 +      by (simp add: divide_minus_left measure_restricted sets_eq sets.Int) (metis inf_absorb2)
    10.9      hence "\<exists>A. ?P A S n" .. }
   10.10    note Ex_P = this
   10.11    def A \<equiv> "rec_nat (space M) (\<lambda>n A. SOME B. ?P B A n)"
   10.12 @@ -280,7 +280,7 @@
   10.13        hence "0 < - ?d B" by auto
   10.14        from ex_inverse_of_nat_Suc_less[OF this]
   10.15        obtain n where *: "?d B < - 1 / real (Suc n)"
   10.16 -        by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
   10.17 +        by (auto simp: divide_minus_left real_eq_of_nat inverse_eq_divide field_simps)
   10.18        have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
   10.19        from epsilon[OF B(1) this] *
   10.20        show False by auto
    11.1 --- a/src/HOL/Rat.thy	Fri Apr 04 16:43:47 2014 +0200
    11.2 +++ b/src/HOL/Rat.thy	Thu Apr 03 23:51:52 2014 +0100
    11.3 @@ -665,7 +665,7 @@
    11.4    by transfer (simp add: add_frac_eq)
    11.5  
    11.6  lemma of_rat_minus: "of_rat (- a) = - of_rat a"
    11.7 -  by transfer simp
    11.8 +  by transfer (simp add: divide_minus_left)
    11.9  
   11.10  lemma of_rat_neg_one [simp]:
   11.11    "of_rat (- 1) = - 1"
    12.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Apr 04 16:43:47 2014 +0200
    12.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Apr 03 23:51:52 2014 +0100
    12.3 @@ -1116,10 +1116,10 @@
    12.4  by (simp add: sgn_div_norm divide_inverse)
    12.5  
    12.6  lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
    12.7 -unfolding real_sgn_eq by simp
    12.8 +  by (rule sgn_pos)
    12.9  
   12.10  lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
   12.11 -unfolding real_sgn_eq by simp
   12.12 +  by (rule sgn_neg)
   12.13  
   12.14  lemma norm_conv_dist: "norm x = dist x 0"
   12.15    unfolding dist_norm by simp
    13.1 --- a/src/HOL/Transcendental.thy	Fri Apr 04 16:43:47 2014 +0200
    13.2 +++ b/src/HOL/Transcendental.thy	Thu Apr 03 23:51:52 2014 +0100
    13.3 @@ -2145,7 +2145,7 @@
    13.4  
    13.5  lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
    13.6    unfolding cos_coeff_def sin_coeff_def
    13.7 -  by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
    13.8 +  by (simp del: mult_Suc, auto simp add: divide_minus_left odd_Suc_mult_two_ex)
    13.9  
   13.10  lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
   13.11    unfolding sin_coeff_def
   13.12 @@ -2169,7 +2169,7 @@
   13.13    by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
   13.14  
   13.15  lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
   13.16 -  by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
   13.17 +  by (simp add: divide_minus_left diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
   13.18  
   13.19  text{*Now at last we can get the derivatives of exp, sin and cos*}
   13.20  
   13.21 @@ -3239,7 +3239,7 @@
   13.22      assume "x \<in> {-1..1}"
   13.23      then show "x \<in> sin ` {- pi / 2..pi / 2}"
   13.24        using arcsin_lbound arcsin_ubound
   13.25 -      by (intro image_eqI[where x="arcsin x"]) auto
   13.26 +      by (intro image_eqI[where x="arcsin x"]) (auto simp: divide_minus_left)
   13.27    qed simp
   13.28    finally show ?thesis .
   13.29  qed
   13.30 @@ -3338,12 +3338,14 @@
   13.31  
   13.32  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
   13.33    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
   13.34 -     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   13.35 +     (auto simp: le_less eventually_at dist_real_def divide_minus_left 
   13.36 +           simp del: less_divide_eq_numeral1
   13.37             intro!: tan_monotone exI[of _ "pi/2"])
   13.38  
   13.39  lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
   13.40    by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
   13.41 -     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   13.42 +     (auto simp: le_less eventually_at dist_real_def divide_minus_left 
   13.43 +           simp del: less_divide_eq_numeral1
   13.44             intro!: tan_monotone exI[of _ "pi/2"])
   13.45  
   13.46  lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
   13.47 @@ -3965,7 +3967,7 @@
   13.48    show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
   13.49      unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
   13.50      unfolding sgn_real_def
   13.51 -    by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
   13.52 +    by (simp add: divide_minus_left tan_def cos_arctan sin_arctan sin_diff cos_diff)
   13.53  qed
   13.54  
   13.55  theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")