Simplification of some proofs. Also key lemmas using !! rather than ! in premises
authorpaulson <lp15@cam.ac.uk>
Tue May 02 14:34:06 2017 +0100 (2017-05-02)
changeset 65680378a2f11bec9
parent 65677 7d25b8dbdbfa
child 65681 eba08da54c6b
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Groups_Big.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Limits.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Tue May 02 10:25:27 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue May 02 14:34:06 2017 +0100
     1.3 @@ -444,7 +444,7 @@
     1.4  lemma simple_bochner_integral_nonneg[simp]:
     1.5    fixes f :: "'a \<Rightarrow> real"
     1.6    shows "(\<And>x. 0 \<le> f x) \<Longrightarrow> 0 \<le> simple_bochner_integral M f"
     1.7 -  by (simp add: sum_nonneg simple_bochner_integral_def)
     1.8 +  by (force simp add: simple_bochner_integral_def intro: sum_nonneg)
     1.9  
    1.10  lemma simple_bochner_integral_eq_nn_integral:
    1.11    assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"
     2.1 --- a/src/HOL/Analysis/Caratheodory.thy	Tue May 02 10:25:27 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Tue May 02 14:34:06 2017 +0100
     2.3 @@ -30,7 +30,7 @@
     2.4        then have "a < ?M fst" "b < ?M snd"
     2.5          by (auto intro!: Max_ge le_imp_less_Suc image_eqI) }
     2.6      then have "sum f (prod_decode ` {..<n}) \<le> sum f ({..<?M fst} \<times> {..<?M snd})"
     2.7 -      by (auto intro!: sum_mono3)
     2.8 +      by (auto intro!: sum_mono2)
     2.9      then show "\<exists>a b. sum f (prod_decode ` {..<n}) \<le> sum f ({..<a} \<times> {..<b})" by auto
    2.10    next
    2.11      fix a b
    2.12 @@ -38,7 +38,7 @@
    2.13      { fix a' b' assume "a' < a" "b' < b" then have "(a', b') \<in> ?M"
    2.14          by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) }
    2.15      then have "sum f ({..<a} \<times> {..<b}) \<le> sum f ?M"
    2.16 -      by (auto intro!: sum_mono3)
    2.17 +      by (auto intro!: sum_mono2)
    2.18      then show "\<exists>n. sum f ({..<a} \<times> {..<b}) \<le> sum f (prod_decode ` {..<n})"
    2.19        by auto
    2.20    qed
     3.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue May 02 10:25:27 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue May 02 14:34:06 2017 +0100
     3.3 @@ -1969,23 +1969,7 @@
     3.4        qed auto
     3.5      qed
     3.6      note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
     3.7 -    show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
     3.8 -      unfolding diff_0_right *
     3.9 -      unfolding real_scaleR_def real_norm_def
    3.10 -      apply (subst abs_of_nonneg)
    3.11 -      apply (rule sum_nonneg)
    3.12 -      apply rule
    3.13 -      unfolding split_paired_all split_conv
    3.14 -      apply (rule mult_nonneg_nonneg)
    3.15 -      apply (drule p'(4))
    3.16 -      apply (erule exE)+
    3.17 -      apply(rule_tac b=b in back_subst)
    3.18 -      prefer 2
    3.19 -      apply (subst(asm) eq_commute)
    3.20 -      apply assumption
    3.21 -      apply (subst interval_doublesplit[OF k])
    3.22 -      apply (rule content_pos_le)
    3.23 -      apply (rule indicator_pos_le)
    3.24 +    have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
    3.25      proof -
    3.26        have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
    3.27          (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
    3.28 @@ -2037,11 +2021,14 @@
    3.29        qed
    3.30        finally show "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
    3.31      qed
    3.32 +    then show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
    3.33 +      unfolding * real_norm_def
    3.34 +      apply (subst abs_of_nonneg)
    3.35 +      using measure_nonneg  by (force simp add: indicator_def intro: sum_nonneg)+
    3.36    qed
    3.37  qed
    3.38  
    3.39  
    3.40 -
    3.41  subsection \<open>Hence the main theorem about negligible sets.\<close>
    3.42  
    3.43  lemma has_integral_negligible:
    3.44 @@ -3876,26 +3863,17 @@
    3.45        have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2"
    3.46          by auto
    3.47        case 2
    3.48 -      show ?case
    3.49 -        apply (rule *)
    3.50 -        apply (rule sum_nonneg)
    3.51 -        apply rule
    3.52 -        apply (unfold split_paired_all split_conv)
    3.53 -        defer
    3.54 -        unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
    3.55 -        unfolding sum_distrib_left[symmetric]
    3.56 -        apply (subst additive_tagged_division_1[OF _ as(1)])
    3.57 -        apply (rule assms)
    3.58 +      have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}" for x k
    3.59        proof -
    3.60 -        fix x k
    3.61 -        assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}}"
    3.62 -        note xk=IntD1[OF this]
    3.63 -        from p(4)[OF this] guess u v by (elim exE) note uv=this
    3.64 -        with p(2)[OF xk] have "cbox u v \<noteq> {}"
    3.65 -          by auto
    3.66 +        obtain u v where uv: "k = cbox u v"
    3.67 +          by (meson Int_iff xkp p(4))
    3.68 +        with p(2) that uv have "cbox u v \<noteq> {}"
    3.69 +          by blast
    3.70          then show "0 \<le> e * ((Sup k) - (Inf k))"
    3.71            unfolding uv using e by (auto simp add: field_simps)
    3.72 -      next
    3.73 +      qed
    3.74 +      have **: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b - a) / 2"
    3.75 +      proof -
    3.76          have *: "\<And>s f t e. sum f s = sum f t \<Longrightarrow> norm (sum f t) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
    3.77            by auto
    3.78          show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x -
    3.79 @@ -4122,6 +4100,15 @@
    3.80            qed (insert p(1) ab e, auto simp add: field_simps)
    3.81          qed auto
    3.82        qed
    3.83 +      show ?case
    3.84 +        apply (rule * [OF sum_nonneg])
    3.85 +        using ge0 apply (force simp add: )
    3.86 +        unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric]
    3.87 +        unfolding sum_distrib_left[symmetric]
    3.88 +        apply (subst additive_tagged_division_1[OF _ as(1)])
    3.89 +         apply (rule assms)
    3.90 +        apply (rule **)
    3.91 +        done
    3.92      qed
    3.93    qed
    3.94  qed
     4.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Tue May 02 10:25:27 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Tue May 02 14:34:06 2017 +0100
     4.3 @@ -281,7 +281,7 @@
     4.4      also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon"
     4.5        by auto
     4.6      also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
     4.7 -      using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono3)
     4.8 +      using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2)
     4.9      finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon"
    4.10        using egt0 by (simp add: ennreal_plus[symmetric] sum_nonneg del: ennreal_plus)
    4.11      then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
     5.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue May 02 10:25:27 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue May 02 14:34:06 2017 +0100
     5.3 @@ -1480,12 +1480,6 @@
     5.4      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
     5.5    by (auto simp add: insert_absorb)
     5.6  
     5.7 -lemma sum_norm_le:
     5.8 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     5.9 -  assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
    5.10 -  shows "norm (sum f S) \<le> sum g S"
    5.11 -  by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
    5.12 -
    5.13  lemma sum_norm_bound:
    5.14    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    5.15    assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
     6.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue May 02 10:25:27 2017 +0200
     6.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue May 02 14:34:06 2017 +0100
     6.3 @@ -1143,7 +1143,7 @@
     6.4      unfolding nn_integral_sum[OF f] ..
     6.5    also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
     6.6      by (intro nn_integral_monotone_convergence_SUP_AE[symmetric])
     6.7 -       (elim AE_mp, auto simp: sum_nonneg simp del: sum_lessThan_Suc intro!: AE_I2 sum_mono3)
     6.8 +       (elim AE_mp, auto simp: sum_nonneg simp del: sum_lessThan_Suc intro!: AE_I2 sum_mono2)
     6.9    also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
    6.10      by (intro nn_integral_cong_AE) (auto simp: suminf_eq_SUP)
    6.11    finally show ?thesis by simp
     7.1 --- a/src/HOL/Analysis/Polytope.thy	Tue May 02 10:25:27 2017 +0200
     7.2 +++ b/src/HOL/Analysis/Polytope.thy	Tue May 02 14:34:06 2017 +0100
     7.3 @@ -311,7 +311,7 @@
     7.4      proof (cases "sum c (S - T) = 0")
     7.5        case True
     7.6        have ci0: "\<And>i. i \<in> (S - T) \<Longrightarrow> c i = 0"
     7.7 -        using True cge0 by (simp add: \<open>finite S\<close> sum_nonneg_eq_0_iff)
     7.8 +        using True cge0 fin(2) sum_nonneg_eq_0_iff by auto
     7.9        have a0: "a i = 0" if "i \<in> (S - T)" for i
    7.10          using ci0 [OF that] u01 a [of i] b [of i] that
    7.11          by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
    7.12 @@ -2775,7 +2775,7 @@
    7.13          by (simp add: \<open>0 < e\<close>)
    7.14        finally show ?thesis .
    7.15      qed
    7.16 -  qed (auto simp: eq poly aff face  \<open>finite \<F>'\<close>)
    7.17 +  qed (auto simp: eq poly aff face \<open>finite \<F>'\<close>)
    7.18  qed
    7.19  
    7.20  end
     8.1 --- a/src/HOL/Groups_Big.thy	Tue May 02 10:25:27 2017 +0200
     8.2 +++ b/src/HOL/Groups_Big.thy	Tue May 02 14:34:06 2017 +0100
     8.3 @@ -675,7 +675,7 @@
     8.4  context ordered_comm_monoid_add
     8.5  begin
     8.6  
     8.7 -lemma sum_nonneg: "\<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> 0 \<le> sum f A"
     8.8 +lemma sum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> sum f A"
     8.9  proof (induct A rule: infinite_finite_induct)
    8.10    case infinite
    8.11    then show ?case by simp
    8.12 @@ -688,7 +688,7 @@
    8.13    with insert show ?case by simp
    8.14  qed
    8.15  
    8.16 -lemma sum_nonpos: "\<forall>x\<in>A. f x \<le> 0 \<Longrightarrow> sum f A \<le> 0"
    8.17 +lemma sum_nonpos: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> 0) \<Longrightarrow> sum f A \<le> 0"
    8.18  proof (induct A rule: infinite_finite_induct)
    8.19    case infinite
    8.20    then show ?case by simp
    8.21 @@ -702,7 +702,7 @@
    8.22  qed
    8.23  
    8.24  lemma sum_nonneg_eq_0_iff:
    8.25 -  "finite A \<Longrightarrow> \<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> sum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
    8.26 +  "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> sum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
    8.27    by (induct set: finite) (simp_all add: add_nonneg_eq_0_iff sum_nonneg)
    8.28  
    8.29  lemma sum_nonneg_0:
    8.30 @@ -727,7 +727,7 @@
    8.31    shows "sum f A \<le> sum f B"
    8.32  proof -
    8.33    have "sum f A \<le> sum f A + sum f (B-A)"
    8.34 -    by(simp add: add_increasing2[OF sum_nonneg] nn Ball_def)
    8.35 +    by (auto intro: add_increasing2 [OF sum_nonneg] nn)
    8.36    also from fin finite_subset[OF sub fin] have "\<dots> = sum f (A \<union> (B-A))"
    8.37      by (simp add: sum.union_disjoint del: Un_Diff_cancel)
    8.38    also from sub have "A \<union> (B-A) = B" by blast
    8.39 @@ -755,9 +755,6 @@
    8.40    finally show ?thesis .
    8.41  qed
    8.42  
    8.43 -lemma sum_mono3: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<forall>x\<in>B - A. 0 \<le> f x \<Longrightarrow> sum f A \<le> sum f B"
    8.44 -  by (rule sum_mono2) auto
    8.45 -
    8.46  end
    8.47  
    8.48  lemma (in canonically_ordered_monoid_add) sum_eq_0_iff [simp]:
    8.49 @@ -1210,12 +1207,19 @@
    8.50    for c :: "nat \<Rightarrow> 'a::field"
    8.51    using sum_zero_power [of "\<lambda>i. c i / d i" A] by auto
    8.52  
    8.53 -lemma (in field) prod_inversef:
    8.54 -  "finite A \<Longrightarrow> prod (inverse \<circ> f) A = inverse (prod f A)"
    8.55 -  by (induct A rule: finite_induct) simp_all
    8.56 +lemma (in field) prod_inversef: "prod (inverse \<circ> f) A = inverse (prod f A)"
    8.57 + proof (cases "finite A")
    8.58 +   case True
    8.59 +   then show ?thesis
    8.60 +     by (induct A rule: finite_induct) simp_all
    8.61 + next
    8.62 +   case False
    8.63 +   then show ?thesis
    8.64 +     by auto
    8.65 + qed
    8.66  
    8.67 -lemma (in field) prod_dividef: "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
    8.68 -  using prod_inversef [of A g] by (simp add: divide_inverse prod.distrib)
    8.69 +lemma (in field) prod_dividef: "(\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
    8.70 +  using prod_inversef [of g A] by (simp add: divide_inverse prod.distrib)
    8.71  
    8.72  lemma prod_Un:
    8.73    fixes f :: "'b \<Rightarrow> 'a :: field"
     9.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 02 10:25:27 2017 +0200
     9.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue May 02 14:34:06 2017 +0100
     9.3 @@ -223,7 +223,7 @@
     9.4  lemma suminf_eq_SUP_real:
     9.5    assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
     9.6    by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
     9.7 -     (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono3)
     9.8 +     (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
     9.9  
    9.10  subsection \<open>Defining the extended non-negative reals\<close>
    9.11  
    10.1 --- a/src/HOL/Library/Extended_Real.thy	Tue May 02 10:25:27 2017 +0200
    10.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue May 02 14:34:06 2017 +0100
    10.3 @@ -3394,7 +3394,7 @@
    10.4      also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
    10.5        by (subst sum.reindex) auto
    10.6      also have "\<dots> \<le> sum f {..<n + k}"
    10.7 -      by (intro sum_mono3) (auto simp: f)
    10.8 +      by (intro sum_mono2) (auto simp: f)
    10.9      finally show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}" .
   10.10    qed
   10.11  qed
    11.1 --- a/src/HOL/Limits.thy	Tue May 02 10:25:27 2017 +0200
    11.2 +++ b/src/HOL/Limits.thy	Tue May 02 14:34:06 2017 +0100
    11.3 @@ -824,6 +824,10 @@
    11.4    for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
    11.5    by (induct n) (simp_all add: tendsto_mult)
    11.6  
    11.7 +lemma tendsto_null_power: "\<lbrakk>(f \<longlongrightarrow> 0) F; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F"
    11.8 +    for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra_1}"
    11.9 +  using tendsto_power [of f 0 F n] by (simp add: power_0_left)
   11.10 +
   11.11  lemma continuous_power [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
   11.12    for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   11.13    unfolding continuous_def by (rule tendsto_power)
    12.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue May 02 10:25:27 2017 +0200
    12.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue May 02 14:34:06 2017 +0100
    12.3 @@ -871,7 +871,7 @@
    12.4  
    12.5  lemma sum_norm_le:
    12.6    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    12.7 -  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
    12.8 +  assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
    12.9    shows "norm (sum f S) \<le> sum g S"
   12.10    by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
   12.11  
    13.1 --- a/src/HOL/Series.thy	Tue May 02 10:25:27 2017 +0200
    13.2 +++ b/src/HOL/Series.thy	Tue May 02 14:34:06 2017 +0100
    13.3 @@ -1062,7 +1062,7 @@
    13.4      have "(\<Sum>i<n. f (g i)) = sum f (g ` {..<n})"
    13.5        by (simp add: sum.reindex)
    13.6      also have "\<dots> \<le> (\<Sum>i<m. f i)"
    13.7 -      by (rule sum_mono3) (auto simp add: pos n[rule_format])
    13.8 +      by (rule sum_mono2) (auto simp add: pos n[rule_format])
    13.9      also have "\<dots> \<le> suminf f"
   13.10        using \<open>summable f\<close> by (rule sum_le_suminf) (simp add: pos)
   13.11      finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f"
   13.12 @@ -1097,7 +1097,7 @@
   13.13      also have "\<dots> = (\<Sum>i\<in>g -` {..<n}. (f \<circ> g) i)"
   13.14        by (rule sum.reindex_cong[where l=g])(auto)
   13.15      also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)"
   13.16 -      by (rule sum_mono3)(auto simp add: pos n)
   13.17 +      by (rule sum_mono2)(auto simp add: pos n)
   13.18      also have "\<dots> \<le> suminf (f \<circ> g)"
   13.19        using \<open>summable (f \<circ> g)\<close> by (rule sum_le_suminf) (simp add: pos)
   13.20      finally show "sum f {..<n} \<le> suminf (f \<circ> g)" .
    14.1 --- a/src/HOL/Transcendental.thy	Tue May 02 10:25:27 2017 +0200
    14.2 +++ b/src/HOL/Transcendental.thy	Tue May 02 14:34:06 2017 +0100
    14.3 @@ -197,7 +197,7 @@
    14.4    also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
    14.5      by (cases n) simp_all
    14.6    also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)"
    14.7 -    by (intro sum_mono3) auto
    14.8 +    by (intro sum_mono2) auto
    14.9    also have "\<dots> = (2*n) choose n" by (rule choose_square_sum)
   14.10    also have "(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) \<le> (\<Sum>k\<in>{0<..<2*n}. (2*n) choose n)"
   14.11      by (intro sum_mono binomial_maximum')
   14.12 @@ -1774,13 +1774,13 @@
   14.13    for x :: real
   14.14    by (simp add: order_eq_iff)
   14.15  
   14.16 -lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
   14.17 +lemma ln_add_one_self_le_self: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
   14.18    for x :: real
   14.19    by (rule exp_le_cancel_iff [THEN iffD1]) (simp add: exp_ge_add_one_self_aux)
   14.20  
   14.21  lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
   14.22    for x :: real
   14.23 -  by (rule order_less_le_trans [where y = "ln (1 + x)"]) simp_all
   14.24 +  by (rule order_less_le_trans [where y = "ln (1 + x)"]) (simp_all add: ln_add_one_self_le_self)
   14.25  
   14.26  lemma ln_ge_iff: "\<And>x::real. 0 < x \<Longrightarrow> y \<le> ln x \<longleftrightarrow> exp y \<le> x"
   14.27    using exp_le_cancel_iff exp_total by force