added divide_nonneg_nonneg and co; made it a simp rule
authorhoelzl
Mon Apr 14 13:08:17 2014 +0200 (2014-04-14)
changeset 56571f4635657d66f
parent 56570 282f3b06fa86
child 56572 5b171d4e1d6e
added divide_nonneg_nonneg and co; made it a simp rule
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Fields.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Float.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon Apr 14 10:55:56 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Apr 14 13:08:17 2014 +0200
     1.3 @@ -778,7 +778,7 @@
     1.4        also have "\<dots> \<le> cos x"
     1.5        proof -
     1.6          from even[OF `even n`] `0 < ?fact` `0 < ?pow`
     1.7 -        have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos)
     1.8 +        have "0 \<le> (?rest / ?fact) * ?pow" by simp
     1.9          thus ?thesis unfolding cos_eq by auto
    1.10        qed
    1.11        finally have "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> cos x" .
    1.12 @@ -891,7 +891,7 @@
    1.13        also have "\<dots> \<le> sin x"
    1.14        proof -
    1.15          from even[OF `even n`] `0 < ?fact` `0 < ?pow`
    1.16 -        have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos less_imp_le)
    1.17 +        have "0 \<le> (?rest / ?fact) * ?pow" by simp
    1.18          thus ?thesis unfolding sin_eq by auto
    1.19        qed
    1.20        finally have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> sin x" .
    1.21 @@ -1344,7 +1344,7 @@
    1.22        obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
    1.23          using Maclaurin_exp_le unfolding atLeast0LessThan by blast
    1.24        moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
    1.25 -        by (auto simp: divide_nonneg_pos zero_le_even_power)
    1.26 +        by (auto simp: zero_le_even_power)
    1.27        ultimately show ?thesis using get_odd exp_gt_zero by auto
    1.28      qed
    1.29      finally have "lb_exp_horner prec (get_even n) 1 1 x \<le> exp x" .
     2.1 --- a/src/HOL/Fields.thy	Mon Apr 14 10:55:56 2014 +0200
     2.2 +++ b/src/HOL/Fields.thy	Mon Apr 14 13:08:17 2014 +0200
     2.3 @@ -1083,6 +1083,21 @@
     2.4    "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
     2.5  by (auto simp add: divide_less_eq)
     2.6  
     2.7 +lemma divide_nonneg_nonneg [simp]:
     2.8 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y"
     2.9 +  by (auto simp add: divide_simps)
    2.10 +
    2.11 +lemma divide_nonpos_nonpos:
    2.12 +  "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> 0 \<le> x / y"
    2.13 +  by (auto simp add: divide_simps)
    2.14 +
    2.15 +lemma divide_nonneg_nonpos:
    2.16 +  "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> x / y \<le> 0"
    2.17 +  by (auto simp add: divide_simps)
    2.18 +
    2.19 +lemma divide_nonpos_nonneg:
    2.20 +  "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x / y \<le> 0"
    2.21 +  by (auto simp add: divide_simps)
    2.22  
    2.23  text {*Conditional Simplification Rules: No Case Splits*}
    2.24  
     3.1 --- a/src/HOL/Library/Convex.thy	Mon Apr 14 10:55:56 2014 +0200
     3.2 +++ b/src/HOL/Library/Convex.thy	Mon Apr 14 13:08:17 2014 +0200
     3.3 @@ -138,7 +138,7 @@
     3.4      with `0 \<le> setsum a s` have "0 < setsum a s" by simp
     3.5      then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
     3.6        using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
     3.7 -      by (simp add: IH divide_nonneg_pos setsum_divide_distrib [symmetric])
     3.8 +      by (simp add: IH setsum_divide_distrib [symmetric])
     3.9      from `convex C` and `y i \<in> C` and this and `0 \<le> a i`
    3.10        and `0 \<le> setsum a s` and `a i + setsum a s = 1`
    3.11      have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
    3.12 @@ -432,9 +432,7 @@
    3.13      then have "a i < 1" using asm by auto
    3.14      then have i0: "1 - a i > 0" by auto
    3.15      let ?a = "\<lambda>j. a j / (1 - a i)"
    3.16 -    { fix j assume "j \<in> s"
    3.17 -      then have "?a j \<ge> 0"
    3.18 -        using i0 asms divide_nonneg_pos
    3.19 +    { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
    3.20          by fastforce }
    3.21      note a_nonneg = this
    3.22      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
     4.1 --- a/src/HOL/Library/Float.thy	Mon Apr 14 10:55:56 2014 +0200
     4.2 +++ b/src/HOL/Library/Float.thy	Mon Apr 14 13:08:17 2014 +0200
     4.3 @@ -1108,7 +1108,7 @@
     4.4    shows "0 \<le> real (lapprox_rat n x y)"
     4.5  using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
     4.6     powr_int[of 2, simplified]
     4.7 -  by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos)
     4.8 +  by auto
     4.9  
    4.10  lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
    4.11    using round_up by (simp add: rapprox_rat_def)
     5.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 14 10:55:56 2014 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 14 13:08:17 2014 +0200
     5.3 @@ -64,11 +64,6 @@
     5.4    apply auto
     5.5    done
     5.6  
     5.7 -lemma divide_nonneg_nonneg:
     5.8 -  fixes a b :: "'a :: {linordered_field, field_inverse_zero}"
     5.9 -  shows "a \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 \<le> a / b"
    5.10 -  by (cases "b = 0") (auto intro!: divide_nonneg_pos)
    5.11 -
    5.12  lemma setsum_Un_disjoint':
    5.13    assumes "finite A"
    5.14      and "finite B"
     6.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 14 10:55:56 2014 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 14 13:08:17 2014 +0200
     6.3 @@ -2262,10 +2262,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 -      done
    6.11 +      by (auto simp: divide_le_0_iff)
    6.12      have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
    6.13      proof
    6.14        fix v
    6.15 @@ -5056,7 +5053,7 @@
    6.16      apply(rule *[OF _ assms(2)])
    6.17      unfolding mem_Collect_eq
    6.18      using `b > 0` assms(3)
    6.19 -    apply (auto intro!: divide_nonneg_pos)
    6.20 +    apply auto
    6.21      done
    6.22    ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
    6.23      "y \<in> ?A" "y \<in> s" "\<forall>z\<in>?A \<inter> s. dist 0 z \<le> dist 0 y"
    6.24 @@ -5218,8 +5215,6 @@
    6.25      from nor have y: "y = norm y *\<^sub>R ((inverse (norm x)) *\<^sub>R x)"
    6.26        unfolding as(3)[unfolded pi_def] by auto
    6.27      have "0 \<le> norm y * inverse (norm x)" and "0 \<le> norm x * inverse (norm y)"
    6.28 -      unfolding divide_inverse[symmetric]
    6.29 -      apply (rule_tac[!] divide_nonneg_pos)
    6.30        using nor
    6.31        apply auto
    6.32        done
    6.33 @@ -5230,7 +5225,7 @@
    6.34        using x y and front_smul[THEN bspec, OF as(1), THEN spec[where x="norm y * (inverse (norm x))"]]
    6.35        using front_smul[THEN bspec, OF as(2), THEN spec[where x="norm x * (inverse (norm y))"]]
    6.36        using xys nor
    6.37 -      apply (auto simp add:field_simps divide_le_eq_1 divide_inverse[symmetric])
    6.38 +      apply (auto simp add: field_simps)
    6.39        done
    6.40      then show "x = y"
    6.41        apply (subst injpi[symmetric])
    6.42 @@ -6412,9 +6407,7 @@
    6.43    next
    6.44      assume as: "dist a b = dist a x + dist x b"
    6.45      have "norm (a - x) / norm (a - b) \<le> 1"
    6.46 -      unfolding divide_le_eq_1_pos[OF Fal2]
    6.47 -      unfolding as[unfolded dist_norm] norm_ge_zero
    6.48 -      by auto
    6.49 +      using Fal2 unfolding as[unfolded dist_norm] norm_ge_zero by auto
    6.50      then show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
    6.51        apply (rule_tac x="dist a x / dist a b" in exI)
    6.52        unfolding dist_norm
    6.53 @@ -6422,8 +6415,7 @@
    6.54        apply rule
    6.55        defer
    6.56        apply rule
    6.57 -      apply (rule divide_nonneg_pos)
    6.58 -      prefer 4
    6.59 +      prefer 3
    6.60        apply rule
    6.61      proof -
    6.62        fix i :: 'a
     7.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Mon Apr 14 10:55:56 2014 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Mon Apr 14 13:08:17 2014 +0200
     7.3 @@ -16,11 +16,6 @@
     7.4  lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
     7.5    by (auto simp add: Basis_vec_def axis_eq_axis)
     7.6  
     7.7 -lemma divide_nonneg_nonneg:
     7.8 -  fixes a b :: "'a :: {linordered_field, field_inverse_zero}"
     7.9 -  shows "a \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 \<le> a / b"
    7.10 -  by (cases "b = 0") (auto intro!: divide_nonneg_pos)
    7.11 -
    7.12  subsection {*Bijections between intervals. *}
    7.13  
    7.14  definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
    7.15 @@ -60,7 +55,7 @@
    7.16    have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
    7.17      using assms(1)[unfolded mem_box] using i by auto
    7.18    have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
    7.19 -    using * x by (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
    7.20 +    using * x by auto
    7.21    then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
    7.22      using * by auto
    7.23    have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
     8.1 --- a/src/HOL/Probability/Distributions.thy	Mon Apr 14 10:55:56 2014 +0200
     8.2 +++ b/src/HOL/Probability/Distributions.thy	Mon Apr 14 13:08:17 2014 +0200
     8.3 @@ -277,7 +277,7 @@
     8.4      unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def)
     8.5    finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
     8.6      ereal (measure lborel (A \<inter> {..a}) / r)" .
     8.7 -qed (auto intro!: divide_nonneg_nonneg measure_nonneg)
     8.8 +qed (auto simp: measure_nonneg)
     8.9  
    8.10  lemma (in prob_space) uniform_distrI_borel_atLeastAtMost:
    8.11    fixes a b :: real
     9.1 --- a/src/HOL/Probability/Information.thy	Mon Apr 14 10:55:56 2014 +0200
     9.2 +++ b/src/HOL/Probability/Information.thy	Mon Apr 14 13:08:17 2014 +0200
     9.3 @@ -130,7 +130,7 @@
     9.4      KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
     9.5      using f g ac by (subst density_density_divide) simp_all
     9.6    also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
     9.7 -    using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density divide_nonneg_nonneg)
     9.8 +    using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density)
     9.9    also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
    9.10      using ac f g `1 < b` by (subst integral_density) (auto intro!: integral_cong_AE)
    9.11    finally show ?thesis .
    9.12 @@ -332,7 +332,7 @@
    9.13      from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
    9.14        by auto
    9.15      show "AE x in density M f. 0 \<le> g x / f x"
    9.16 -      using f g by (auto simp: AE_density divide_nonneg_nonneg)
    9.17 +      using f g by (auto simp: AE_density)
    9.18      show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
    9.19        using `1 < b` f g ac
    9.20        by (subst integral_density)
    9.21 @@ -804,8 +804,7 @@
    9.22      using D
    9.23      apply (subst eq_commute)
    9.24      apply (intro RN_deriv_unique_sigma_finite)
    9.25 -    apply (auto intro: divide_nonneg_nonneg measure_nonneg
    9.26 -             simp: distributed_distr_eq_density[symmetric, OF X] sf)
    9.27 +    apply (auto simp: distributed_distr_eq_density[symmetric, OF X] sf measure_nonneg)
    9.28      done
    9.29  qed
    9.30  
    9.31 @@ -1102,7 +1101,7 @@
    9.32      apply (rule positive_integral_mono_AE)
    9.33      using ae5 ae6 ae7 ae8
    9.34      apply eventually_elim
    9.35 -    apply (auto intro!: divide_nonneg_nonneg)
    9.36 +    apply auto
    9.37      done
    9.38    also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
    9.39      by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
    9.40 @@ -1115,7 +1114,7 @@
    9.41        "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
    9.42      then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
    9.43        by (subst positive_integral_multc)
    9.44 -         (auto intro!: divide_nonneg_nonneg split: prod.split)
    9.45 +         (auto split: prod.split)
    9.46    qed
    9.47    also have "\<dots> = 1"
    9.48      using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
    9.49 @@ -1151,7 +1150,7 @@
    9.50      apply simp
    9.51      using ae5 ae6 ae7 ae8
    9.52      apply eventually_elim
    9.53 -    apply (auto intro!: divide_nonneg_nonneg)
    9.54 +    apply auto
    9.55      done
    9.56  
    9.57    have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
    9.58 @@ -1347,7 +1346,7 @@
    9.59      apply (rule positive_integral_mono_AE)
    9.60      using ae5 ae6 ae7 ae8
    9.61      apply eventually_elim
    9.62 -    apply (auto intro!: divide_nonneg_nonneg)
    9.63 +    apply auto
    9.64      done
    9.65    also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
    9.66      by (subst STP.positive_integral_snd_measurable[symmetric])
    9.67 @@ -1360,7 +1359,7 @@
    9.68      fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
    9.69        "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
    9.70      then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
    9.71 -      by (subst positive_integral_multc) (auto intro!: divide_nonneg_nonneg)
    9.72 +      by (subst positive_integral_multc) auto
    9.73    qed
    9.74    also have "\<dots> = 1"
    9.75      using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
    9.76 @@ -1396,7 +1395,7 @@
    9.77      apply (auto simp: split_beta') []
    9.78      using ae5 ae6 ae7 ae8
    9.79      apply eventually_elim
    9.80 -    apply (auto intro!: divide_nonneg_nonneg)
    9.81 +    apply auto
    9.82      done
    9.83  
    9.84    have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
    10.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Apr 14 10:55:56 2014 +0200
    10.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Mon Apr 14 13:08:17 2014 +0200
    10.3 @@ -303,7 +303,7 @@
    10.4                                       mult_nonpos_nonneg)
    10.5      next
    10.6        fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
    10.7 -      have "\<And>i. 0 \<le> ?g i x" by (auto simp: divide_nonneg_pos)
    10.8 +      have "\<And>i. 0 \<le> ?g i x" by auto
    10.9        from order_trans[OF this *] have "0 \<le> y" by simp
   10.10        show "max 0 (u x) \<le> y"
   10.11        proof (cases y)
   10.12 @@ -330,7 +330,7 @@
   10.13          then show "max 0 (u x) \<le> y" using real ux by simp
   10.14        qed (insert `0 \<le> y`, auto)
   10.15      qed
   10.16 -  qed (auto simp: divide_nonneg_pos)
   10.17 +  qed auto
   10.18  qed
   10.19  
   10.20  lemma borel_measurable_implies_simple_function_sequence':
    11.1 --- a/src/HOL/Rat.thy	Mon Apr 14 10:55:56 2014 +0200
    11.2 +++ b/src/HOL/Rat.thy	Mon Apr 14 13:08:17 2014 +0200
    11.3 @@ -578,7 +578,7 @@
    11.4      by (cases "b = 0", simp, simp add: of_int_rat)
    11.5    moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
    11.6      unfolding Fract_of_int_quotient
    11.7 -    by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
    11.8 +    by (rule linorder_cases [of b 0]) (simp_all add: divide_nonpos_neg)
    11.9    ultimately show ?thesis by simp
   11.10  qed
   11.11  
    12.1 --- a/src/HOL/Real.thy	Mon Apr 14 10:55:56 2014 +0200
    12.2 +++ b/src/HOL/Real.thy	Mon Apr 14 13:08:17 2014 +0200
    12.3 @@ -1136,8 +1136,6 @@
    12.4    apply (simp add: algebra_simps)
    12.5    apply (subst real_of_int_div_aux)
    12.6    apply simp
    12.7 -  apply (subst zero_le_divide_iff)
    12.8 -  apply auto
    12.9    apply (simp add: algebra_simps)
   12.10    apply (subst real_of_int_div_aux)
   12.11    apply simp
   12.12 @@ -1269,8 +1267,6 @@
   12.13  apply (simp add: algebra_simps)
   12.14  apply (subst real_of_nat_div_aux)
   12.15  apply simp
   12.16 -apply (subst zero_le_divide_iff)
   12.17 -apply simp
   12.18  done
   12.19  
   12.20  lemma real_of_nat_div3:
    13.1 --- a/src/HOL/Transcendental.thy	Mon Apr 14 10:55:56 2014 +0200
    13.2 +++ b/src/HOL/Transcendental.thy	Mon Apr 14 13:08:17 2014 +0200
    13.3 @@ -1494,10 +1494,7 @@
    13.4    also have "- (x / (1 - x)) <= ..."
    13.5    proof -
    13.6      have "ln (1 + x / (1 - x)) <= x / (1 - x)"
    13.7 -      apply (rule ln_add_one_self_le_self)
    13.8 -      apply (rule divide_nonneg_pos)
    13.9 -      using a c apply auto
   13.10 -      done
   13.11 +      using a c by (intro ln_add_one_self_le_self) auto
   13.12      thus ?thesis
   13.13        by auto
   13.14    qed
   13.15 @@ -1586,11 +1583,8 @@
   13.16    also have "... = 1 + (y - x) / x"
   13.17      using x a by (simp add: field_simps)
   13.18    also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
   13.19 -    apply (rule mult_left_mono)
   13.20 -    apply (rule ln_add_one_self_le_self)
   13.21 -    apply (rule divide_nonneg_pos)
   13.22 -    using x a apply simp_all
   13.23 -    done
   13.24 +    using x a 
   13.25 +    by (intro mult_left_mono ln_add_one_self_le_self) simp_all
   13.26    also have "... = y - x" using a by simp
   13.27    also have "... = (y - x) * ln (exp 1)" by simp
   13.28    also have "... <= (y - x) * ln x"
   13.29 @@ -3906,9 +3900,6 @@
   13.30    hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
   13.31      by auto
   13.32  
   13.33 -  have divide_nonzero_divide: "\<And>A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)"
   13.34 -    by auto
   13.35 -
   13.36    have "0 < cos y" using cos_gt_zero_pi[OF low high] .
   13.37    hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
   13.38      by auto
   13.39 @@ -3922,7 +3913,7 @@
   13.40    finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
   13.41  
   13.42    have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
   13.43 -    unfolding tan_def divide_nonzero_divide[OF `cos y \<noteq> 0`, symmetric] ..
   13.44 +    unfolding tan_def using `cos y \<noteq> 0` by (simp add: field_simps)
   13.45    also have "\<dots> = tan y / (1 + 1 / cos y)"
   13.46      using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
   13.47    also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"