New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
authorpaulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578e4997c181cce
parent 65577 32d4117ad6e8
child 65579 52eafedaf196
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Poly_Roots.thy
src/HOL/Analysis/Summation_Tests.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
src/HOL/Complex.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Filter.thy
src/HOL/Limits.thy
src/HOL/Probability/Sinc_Integral.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set_Interval.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -1727,8 +1727,7 @@
     1.4  next
     1.5    case False
     1.6    then have k: "0 < k" "k < 1" "complex_of_real k \<noteq> 1"
     1.7 -    using assms apply auto
     1.8 -    using of_real_eq_iff by fastforce
     1.9 +    using assms by auto
    1.10    have c': "c = k *\<^sub>R (b - a) + a"
    1.11      by (metis diff_add_cancel c)
    1.12    have bc: "(b - c) = (1 - k) *\<^sub>R (b - a)"
    1.13 @@ -3871,7 +3870,7 @@
    1.14    shows
    1.15    "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
    1.16      \<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
    1.17 -   \<Longrightarrow> \<bar>Re(winding_number \<gamma> z)\<bar> < 1"
    1.18 +   \<Longrightarrow> Re(winding_number \<gamma> z) < 1"
    1.19     by (auto simp: not_less dest: winding_number_big_meets)
    1.20  
    1.21  text\<open>One way of proving that WN=1 for a loop.\<close>
    1.22 @@ -6532,6 +6531,21 @@
    1.23  apply (force simp add: summable_Re o_def nonneg_Reals_cmod_eq_Re image_subset_iff)
    1.24  done
    1.25  
    1.26 +text\<open>Sometimes convenient to compare with a complex series of positive reals. (?)\<close>
    1.27 +lemma series_differentiable_comparison_complex:
    1.28 +  fixes S :: "complex set"
    1.29 +  assumes S: "open S"
    1.30 +    and hfd: "\<And>n x. x \<in> S \<Longrightarrow> f n field_differentiable (at x)"
    1.31 +    and to_g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>d h. 0 < d \<and> summable h \<and> range h \<subseteq> \<real>\<^sub>\<ge>\<^sub>0 \<and> (\<forall>\<^sub>F n in sequentially. \<forall>y\<in>ball x d \<inter> S. cmod(f n y) \<le> cmod (h n))"
    1.32 +  obtains g where "\<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> g field_differentiable (at x)"
    1.33 +proof -
    1.34 +  have hfd': "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative deriv (f n) x) (at x)"
    1.35 +    using hfd field_differentiable_derivI by blast
    1.36 +  have "\<exists>g g'. \<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. deriv (f n) x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
    1.37 +    by (metis series_and_derivative_comparison_complex [OF S hfd' to_g])
    1.38 +  then show ?thesis
    1.39 +    using field_differentiable_def that by blast
    1.40 +qed
    1.41  
    1.42  text\<open>In particular, a power series is analytic inside circle of convergence.\<close>
    1.43  
    1.44 @@ -7441,5 +7455,4 @@
    1.45                           homotopic_paths_imp_homotopic_loops)
    1.46  using valid_path_imp_path by blast
    1.47  
    1.48 -
    1.49  end
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 08:38:23 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 16:39:54 2017 +0100
     2.3 @@ -709,6 +709,7 @@
     2.4    apply (simp only: pos_le_divide_eq [symmetric], linarith)
     2.5    done
     2.6  
     2.7 +text\<open>An odd contrast with the much more easily proved @{thm exp_le}\<close>
     2.8  lemma e_less_3: "exp 1 < (3::real)"
     2.9    using e_approx_32
    2.10    by (simp add: abs_if split: if_split_asm)
    2.11 @@ -1752,7 +1753,7 @@
    2.12  declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
    2.13  
    2.14  
    2.15 -lemma has_field_derivative_powr_right:
    2.16 +lemma has_field_derivative_powr_right [derivative_intros]:
    2.17      "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
    2.18    apply (simp add: powr_def)
    2.19    apply (intro derivative_eq_intros | simp)+
     3.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Apr 25 08:38:23 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Apr 25 16:39:54 2017 +0100
     3.3 @@ -1244,7 +1244,7 @@
     3.4          by (meson Tsb min.cobounded1 order_trans r subset_ball)
     3.5        ultimately have False
     3.6          using inj_onD [OF injf, of y0 y1] \<open>y0 \<in> T\<close> \<open>y1 \<in> T\<close>
     3.7 -        using fd [of y0] fd [of y1] complex_root_unity [of n 1]
     3.8 +        using fd [of y0] fd [of y1] complex_root_unity [of n 1] n_ne
     3.9          apply (simp add: y0 y1 power_mult_distrib)
    3.10          apply (force simp: algebra_simps)
    3.11          done
     4.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Tue Apr 25 08:38:23 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Tue Apr 25 16:39:54 2017 +0100
     4.3 @@ -1880,7 +1880,7 @@
     4.4    show "G x \<ge> Gamma x"
     4.5    proof (rule tendsto_upperbound)
     4.6      from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
     4.7 -      using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
     4.8 +      using  x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "1::nat"]])
     4.9    qed (simp_all add: Gamma_series_LIMSEQ)
    4.10  next
    4.11    show "G x \<le> Gamma x"
    4.12 @@ -1891,7 +1891,7 @@
    4.13      thus "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x" by simp
    4.14    next
    4.15      from G_upper[of x] show "eventually (\<lambda>n. Gamma_series x n * (1 + x / real n) \<ge> G x) sequentially"
    4.16 -      using eventually_ge_at_top[of "2::nat"] x by (auto elim!: eventually_mono)
    4.17 +      using x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "2::nat"]])
    4.18    qed simp_all
    4.19  qed
    4.20  
    4.21 @@ -2472,9 +2472,9 @@
    4.22    let ?r' = "\<lambda>n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))"
    4.23    from z have z': "z \<noteq> 0" by auto
    4.24  
    4.25 -  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" using eventually_gt_at_top[of "0::nat"]
    4.26 +  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" 
    4.27      using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac
    4.28 -                     elim!: eventually_mono dest: pochhammer_eq_0_imp_nonpos_Int)
    4.29 +                     intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int)
    4.30    moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
    4.31      by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all
    4.32    ultimately show "?r \<longlonglongrightarrow> 1" by (force dest!: Lim_transform_eventually)
     5.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Apr 25 08:38:23 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Apr 25 16:39:54 2017 +0100
     5.3 @@ -2578,36 +2578,38 @@
     5.4  proof (rule integrable_uniform_limit, safe)
     5.5    fix e :: real
     5.6    assume e: "e > 0"
     5.7 -  from compact_uniformly_continuous[OF assms compact_cbox,unfolded uniformly_continuous_on_def,rule_format,OF e] guess d ..
     5.8 -  note d=conjunctD2[OF this,rule_format]
     5.9 -  from fine_division_exists[OF gauge_ball[OF d(1)], of a b] guess p . note p=this
    5.10 -  note p' = tagged_division_ofD[OF p(1)]
    5.11 +  then obtain d where "0 < d" and d: "\<And>x x'. \<lbrakk>x \<in> cbox a b; x' \<in> cbox a b; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
    5.12 +    using compact_uniformly_continuous[OF assms compact_cbox] unfolding uniformly_continuous_on_def by metis
    5.13 +  obtain p where ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x d) fine p"
    5.14 +    using fine_division_exists[OF gauge_ball[OF \<open>0 < d\<close>], of a b] .
    5.15    have *: "\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
    5.16    proof (safe, unfold snd_conv)
    5.17      fix x l
    5.18      assume as: "(x, l) \<in> p"
    5.19 -    from p'(4)[OF this] guess a b by (elim exE) note l=this
    5.20 +    obtain a b where l: "l = cbox a b"
    5.21 +      using as ptag by blast
    5.22 +    then have x: "x \<in> cbox a b"
    5.23 +      using as ptag by auto
    5.24      show "\<exists>g. (\<forall>x\<in>l. norm (f x - g x) \<le> e) \<and> g integrable_on l"
    5.25        apply (rule_tac x="\<lambda>y. f x" in exI)
    5.26      proof safe
    5.27        show "(\<lambda>y. f x) integrable_on l"
    5.28 -        unfolding integrable_on_def l
    5.29 -        apply rule
    5.30 -        apply (rule has_integral_const)
    5.31 -        done
    5.32 +        unfolding integrable_on_def l by blast
    5.33 +    next
    5.34        fix y
    5.35        assume y: "y \<in> l"
    5.36 -      note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
    5.37 -      note d(2)[OF _ _ this[unfolded mem_ball]]
    5.38 +      then have "y \<in> ball x d"
    5.39 +        using as finep by fastforce
    5.40        then show "norm (f y - f x) \<le> e"
    5.41 -        using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce
    5.42 +        using d x y as l
    5.43 +        by (metis dist_commute dist_norm less_imp_le mem_ball ptag subsetCE tagged_division_ofD(3))
    5.44      qed
    5.45    qed
    5.46    from e have "e \<ge> 0"
    5.47      by auto
    5.48 -  from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
    5.49 -  then show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
    5.50 -    by auto
    5.51 +  from approximable_on_division[OF this division_of_tagged_division[OF ptag] *]
    5.52 +  show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
    5.53 +    by metis
    5.54  qed
    5.55  
    5.56  lemma integrable_continuous_interval:
    5.57 @@ -6278,89 +6280,6 @@
    5.58  qed
    5.59  
    5.60  
    5.61 -subsection \<open>Geometric progression\<close>
    5.62 -
    5.63 -text \<open>FIXME: Should one or more of these theorems be moved to
    5.64 -  \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
    5.65 -
    5.66 -lemma sum_gp_basic:
    5.67 -  fixes x :: "'a::ring_1"
    5.68 -  shows "(1 - x) * sum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
    5.69 -proof -
    5.70 -  define y where "y = 1 - x"
    5.71 -  have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
    5.72 -    by (induct n) (simp_all add: algebra_simps)
    5.73 -  then show ?thesis
    5.74 -    unfolding y_def by simp
    5.75 -qed
    5.76 -
    5.77 -lemma sum_gp_multiplied:
    5.78 -  assumes mn: "m \<le> n"
    5.79 -  shows "((1::'a::{field}) - x) * sum (op ^ x) {m..n} = x^m - x^ Suc n"
    5.80 -  (is "?lhs = ?rhs")
    5.81 -proof -
    5.82 -  let ?S = "{0..(n - m)}"
    5.83 -  from mn have mn': "n - m \<ge> 0"
    5.84 -    by arith
    5.85 -  let ?f = "op + m"
    5.86 -  have i: "inj_on ?f ?S"
    5.87 -    unfolding inj_on_def by auto
    5.88 -  have f: "?f ` ?S = {m..n}"
    5.89 -    using mn
    5.90 -    apply (auto simp add: image_iff Bex_def)
    5.91 -    apply presburger
    5.92 -    done
    5.93 -  have th: "op ^ x \<circ> op + m = (\<lambda>i. x^m * x^i)"
    5.94 -    by (rule ext) (simp add: power_add power_mult)
    5.95 -  from sum.reindex[OF i, of "op ^ x", unfolded f th sum_distrib_left[symmetric]]
    5.96 -  have "?lhs = x^m * ((1 - x) * sum (op ^ x) {0..n - m})"
    5.97 -    by simp
    5.98 -  then show ?thesis
    5.99 -    unfolding sum_gp_basic
   5.100 -    using mn
   5.101 -    by (simp add: field_simps power_add[symmetric])
   5.102 -qed
   5.103 -
   5.104 -lemma sum_gp:
   5.105 -  "sum (op ^ (x::'a::{field})) {m .. n} =
   5.106 -    (if n < m then 0
   5.107 -     else if x = 1 then of_nat ((n + 1) - m)
   5.108 -     else (x^ m - x^ (Suc n)) / (1 - x))"
   5.109 -proof -
   5.110 -  {
   5.111 -    assume nm: "n < m"
   5.112 -    then have ?thesis by simp
   5.113 -  }
   5.114 -  moreover
   5.115 -  {
   5.116 -    assume "\<not> n < m"
   5.117 -    then have nm: "m \<le> n"
   5.118 -      by arith
   5.119 -    {
   5.120 -      assume x: "x = 1"
   5.121 -      then have ?thesis
   5.122 -        by simp
   5.123 -    }
   5.124 -    moreover
   5.125 -    {
   5.126 -      assume x: "x \<noteq> 1"
   5.127 -      then have nz: "1 - x \<noteq> 0"
   5.128 -        by simp
   5.129 -      from sum_gp_multiplied[OF nm, of x] nz have ?thesis
   5.130 -        by (simp add: field_simps)
   5.131 -    }
   5.132 -    ultimately have ?thesis by blast
   5.133 -  }
   5.134 -  ultimately show ?thesis by blast
   5.135 -qed
   5.136 -
   5.137 -lemma sum_gp_offset:
   5.138 -  "sum (op ^ (x::'a::{field})) {m .. m+n} =
   5.139 -    (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
   5.140 -  unfolding sum_gp[of x m "m + n"] power_Suc
   5.141 -  by (simp add: field_simps power_add)
   5.142 -
   5.143 -
   5.144  subsection \<open>Monotone convergence (bounded interval first)\<close>
   5.145  
   5.146  lemma monotone_convergence_interval:
     6.1 --- a/src/HOL/Analysis/Poly_Roots.thy	Tue Apr 25 08:38:23 2017 +0200
     6.2 +++ b/src/HOL/Analysis/Poly_Roots.thy	Tue Apr 25 16:39:54 2017 +0100
     6.3 @@ -8,73 +8,6 @@
     6.4  imports Complex_Main
     6.5  begin
     6.6  
     6.7 -subsection\<open>Geometric progressions\<close>
     6.8 -
     6.9 -lemma sum_gp_basic:
    6.10 -  fixes x :: "'a::{comm_ring,monoid_mult}"
    6.11 -  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
    6.12 -  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
    6.13 -
    6.14 -lemma sum_gp0:
    6.15 -  fixes x :: "'a::{comm_ring,division_ring}"
    6.16 -  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
    6.17 -  using sum_gp_basic[of x n]
    6.18 -  by (simp add: mult.commute divide_simps)
    6.19 -
    6.20 -lemma sum_power_add:
    6.21 -  fixes x :: "'a::{comm_ring,monoid_mult}"
    6.22 -  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
    6.23 -  by (simp add: sum_distrib_left power_add)
    6.24 -
    6.25 -lemma sum_power_shift:
    6.26 -  fixes x :: "'a::{comm_ring,monoid_mult}"
    6.27 -  assumes "m \<le> n"
    6.28 -  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
    6.29 -proof -
    6.30 -  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
    6.31 -    by (simp add: sum_distrib_left power_add [symmetric])
    6.32 -  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
    6.33 -    using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
    6.34 -  finally show ?thesis .
    6.35 -qed
    6.36 -
    6.37 -lemma sum_gp_multiplied:
    6.38 -  fixes x :: "'a::{comm_ring,monoid_mult}"
    6.39 -  assumes "m \<le> n"
    6.40 -  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
    6.41 -proof -
    6.42 -  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
    6.43 -    by (metis mult.assoc mult.commute assms sum_power_shift)
    6.44 -  also have "... =x^m * (1 - x^Suc(n-m))"
    6.45 -    by (metis mult.assoc sum_gp_basic)
    6.46 -  also have "... = x^m - x^Suc n"
    6.47 -    using assms
    6.48 -    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
    6.49 -  finally show ?thesis .
    6.50 -qed
    6.51 -
    6.52 -lemma sum_gp:
    6.53 -  fixes x :: "'a::{comm_ring,division_ring}"
    6.54 -  shows   "(\<Sum>i=m..n. x^i) =
    6.55 -               (if n < m then 0
    6.56 -                else if x = 1 then of_nat((n + 1) - m)
    6.57 -                else (x^m - x^Suc n) / (1 - x))"
    6.58 -using sum_gp_multiplied [of m n x]
    6.59 -apply auto
    6.60 -by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
    6.61 -
    6.62 -lemma sum_gp_offset:
    6.63 -  fixes x :: "'a::{comm_ring,division_ring}"
    6.64 -  shows   "(\<Sum>i=m..m+n. x^i) =
    6.65 -       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
    6.66 -  using sum_gp [of x m "m+n"]
    6.67 -  by (auto simp: power_add algebra_simps)
    6.68 -
    6.69 -lemma sum_gp_strict:
    6.70 -  fixes x :: "'a::{comm_ring,division_ring}"
    6.71 -  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
    6.72 -  by (induct n) (auto simp: algebra_simps divide_simps)
    6.73 -
    6.74  subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
    6.75  
    6.76  lemma sub_polyfun:
     7.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Tue Apr 25 08:38:23 2017 +0200
     7.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Tue Apr 25 16:39:54 2017 +0100
     7.3 @@ -246,9 +246,9 @@
     7.4  proof (cases "Re s \<le> 0")
     7.5    let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
     7.6    case False
     7.7 -  with eventually_gt_at_top[of "0::nat"]
     7.8 -    have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
     7.9 -    by (auto intro!: ge_one_powr_ge_zero elim!: eventually_mono)
    7.10 +  have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
    7.11 +    apply (rule eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
    7.12 +    using False ge_one_powr_ge_zero by auto
    7.13    from summable_comparison_test_ev[OF this] False show ?thesis by (auto simp: summable_const_iff)
    7.14  next
    7.15    let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
    7.16 @@ -387,11 +387,11 @@
    7.17      by (auto simp: eventually_at_top_linorder)
    7.18    hence A: "p n * f n < p (Suc n) * f (Suc n)" if "n \<ge> N" for n using that N[of n] N[of "Suc n"]
    7.19      by (simp add: field_simps)
    7.20 -  have "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
    7.21 -      by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
    7.22 -  from eventually_ge_at_top[of N] N this
    7.23 -    have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
    7.24 -    by (auto elim!: eventually_mono simp: field_simps abs_of_pos)
    7.25 +  have B: "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
    7.26 +    by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
    7.27 +  have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
    7.28 +    apply (rule eventually_mono [OF eventually_ge_at_top[of N]])
    7.29 +    using B N  by (auto  simp: field_simps abs_of_pos)
    7.30    from this and \<open>summable f\<close> have "summable (\<lambda>n. p N * f N * inverse (p n))"
    7.31      by (rule summable_comparison_test_ev)
    7.32    from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl]
    7.33 @@ -779,9 +779,8 @@
    7.34  proof -
    7.35    have "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
    7.36            limsup (\<lambda>n. ereal (norm c) * ereal (root n (norm (f n))))"
    7.37 -    using eventually_gt_at_top[of "0::nat"]
    7.38 -    by (intro Limsup_eq)
    7.39 -       (auto elim!: eventually_mono simp: norm_mult norm_power real_root_mult real_root_power)
    7.40 +    by (intro Limsup_eq eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
    7.41 +       (auto simp: norm_mult norm_power real_root_mult real_root_power)
    7.42    also have "\<dots> = ereal (norm c) * limsup (\<lambda>n. ereal (root n (norm (f n))))"
    7.43      using assms by (subst Limsup_ereal_mult_left[symmetric]) simp_all
    7.44    finally have A: "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
     8.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 08:38:23 2017 +0200
     8.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 16:39:54 2017 +0100
     8.3 @@ -398,12 +398,17 @@
     8.4      using \<open>k>0\<close> \<open>\<delta>>0\<close> NN  k\<delta>
     8.5      apply (force simp add: field_simps)+
     8.6      done
     8.7 -  have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e"
     8.8 -    apply (subst Transcendental.ln_less_cancel_iff [symmetric])
     8.9 -      prefer 3 apply (subst ln_realpow)
    8.10 -    using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
    8.11 -    apply (force simp add: field_simps ln_div)+
    8.12 -    done
    8.13 +  have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e
    8.14 +  proof -
    8.15 +    have "0 < ln (real k) + ln \<delta>"
    8.16 +      using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero by fastforce
    8.17 +    then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e"
    8.18 +      using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps)
    8.19 +    then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
    8.20 +      by (metis exp_less_mono exp_ln that)
    8.21 +    then show ?thesis
    8.22 +      by (simp add: \<delta>01(1) \<open>0 < k\<close>)
    8.23 +  qed
    8.24    { fix t and e::real
    8.25      assume "e>0"
    8.26      have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e"
     9.1 --- a/src/HOL/Complex.thy	Tue Apr 25 08:38:23 2017 +0200
     9.2 +++ b/src/HOL/Complex.thy	Tue Apr 25 16:39:54 2017 +0100
     9.3 @@ -138,7 +138,7 @@
     9.4  end
     9.5  
     9.6  
     9.7 -subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>
     9.8 +subsection \<open>Numerals, Arithmetic, and Embedding from \<real>\<close>
     9.9  
    9.10  abbreviation complex_of_real :: "real \<Rightarrow> complex"
    9.11    where "complex_of_real \<equiv> of_real"
    9.12 @@ -649,10 +649,10 @@
    9.13  lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
    9.14    by (simp add: Im_divide power2_eq_square)
    9.15  
    9.16 -lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
    9.17 +lemma Re_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Re (z / r) = Re z / Re r"
    9.18    by (metis Re_divide_of_real of_real_Re)
    9.19  
    9.20 -lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
    9.21 +lemma Im_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Im (z / r) = Im z / Re r"
    9.22    by (metis Im_divide_of_real of_real_Re)
    9.23  
    9.24  lemma Re_sum[simp]: "Re (sum f s) = (\<Sum>x\<in>s. Re (f x))"
    9.25 @@ -691,6 +691,12 @@
    9.26  lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm z = \<bar>Re z\<bar>"
    9.27    by (simp add: complex_is_Real_iff norm_complex_def)
    9.28  
    9.29 +lemma Re_Reals_divide: "r \<in> \<real> \<Longrightarrow> Re (r / z) = Re r * Re z / (norm z)\<^sup>2"
    9.30 +  by (simp add: Re_divide complex_is_Real_iff cmod_power2)
    9.31 +
    9.32 +lemma Im_Reals_divide: "r \<in> \<real> \<Longrightarrow> Im (r / z) = -Re r * Im z / (norm z)\<^sup>2"
    9.33 +  by (simp add: Im_divide complex_is_Real_iff cmod_power2)
    9.34 +
    9.35  lemma series_comparison_complex:
    9.36    fixes f:: "nat \<Rightarrow> 'a::banach"
    9.37    assumes sg: "summable g"
    10.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Apr 25 08:38:23 2017 +0200
    10.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Apr 25 16:39:54 2017 +0100
    10.3 @@ -913,7 +913,7 @@
    10.4    then have "exp (real k * ln y + ln x) > exp 0"
    10.5      by (simp add: ac_simps)
    10.6    then have "y ^ k * x > 1"
    10.7 -    unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
    10.8 +    unfolding exp_zero exp_add exp_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
    10.9      by simp
   10.10    then have "x > (1 / y)^k" using yp
   10.11      by (simp add: field_simps)
    11.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Apr 25 08:38:23 2017 +0200
    11.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Apr 25 16:39:54 2017 +0100
    11.3 @@ -1987,7 +1987,7 @@
    11.4        have "exp x = exp (?num * (x / ?num))"
    11.5          using \<open>real ?num \<noteq> 0\<close> by auto
    11.6        also have "\<dots> = exp (x / ?num) ^ ?num"
    11.7 -        unfolding exp_real_of_nat_mult ..
    11.8 +        unfolding exp_of_nat_mult ..
    11.9        also have "\<dots> \<le> exp (float_divr prec x (- floor_fl x)) ^ ?num"
   11.10          unfolding num_eq fl_eq
   11.11          by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
   11.12 @@ -2023,7 +2023,7 @@
   11.13            unfolding num_eq fl_eq
   11.14            using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
   11.15          also have "\<dots> = exp (?num * (x / ?num))"
   11.16 -          unfolding exp_real_of_nat_mult ..
   11.17 +          unfolding exp_of_nat_mult ..
   11.18          also have "\<dots> = exp x"
   11.19            using \<open>real ?num \<noteq> 0\<close> by auto
   11.20          finally show ?thesis
   11.21 @@ -2050,7 +2050,7 @@
   11.22          hence "real_of_float (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
   11.23            by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
   11.24          also have "\<dots> = exp x"
   11.25 -          unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric]
   11.26 +          unfolding num_eq fl_eq exp_of_nat_mult[symmetric]
   11.27            using \<open>real_of_float (floor_fl x) \<noteq> 0\<close> by auto
   11.28          finally show ?thesis
   11.29            unfolding lb_exp.simps if_not_P[OF \<open>\<not> 0 < x\<close>] if_P[OF \<open>x < - 1\<close>]
    12.1 --- a/src/HOL/Filter.thy	Tue Apr 25 08:38:23 2017 +0200
    12.2 +++ b/src/HOL/Filter.thy	Tue Apr 25 16:39:54 2017 +0100
    12.3 @@ -624,7 +624,7 @@
    12.4    shows "eventually P at_top"
    12.5    using assms by (auto simp: eventually_at_top_linorder)
    12.6  
    12.7 -lemma eventually_ge_at_top:
    12.8 +lemma eventually_ge_at_top [simp]:
    12.9    "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   12.10    unfolding eventually_at_top_linorder by auto
   12.11  
   12.12 @@ -638,10 +638,10 @@
   12.13    finally show ?thesis .
   12.14  qed
   12.15  
   12.16 -lemma eventually_at_top_not_equal: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
   12.17 +lemma eventually_at_top_not_equal [simp]: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
   12.18    unfolding eventually_at_top_dense by auto
   12.19  
   12.20 -lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
   12.21 +lemma eventually_gt_at_top [simp]: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
   12.22    unfolding eventually_at_top_dense by auto
   12.23  
   12.24  lemma eventually_all_ge_at_top:
   12.25 @@ -664,7 +664,7 @@
   12.26    unfolding at_bot_def
   12.27    by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
   12.28  
   12.29 -lemma eventually_le_at_bot:
   12.30 +lemma eventually_le_at_bot [simp]:
   12.31    "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
   12.32    unfolding eventually_at_bot_linorder by auto
   12.33  
   12.34 @@ -678,10 +678,10 @@
   12.35    finally show ?thesis .
   12.36  qed
   12.37  
   12.38 -lemma eventually_at_bot_not_equal: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
   12.39 +lemma eventually_at_bot_not_equal [simp]: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
   12.40    unfolding eventually_at_bot_dense by auto
   12.41  
   12.42 -lemma eventually_gt_at_bot:
   12.43 +lemma eventually_gt_at_bot [simp]:
   12.44    "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   12.45    unfolding eventually_at_bot_dense by auto
   12.46  
    13.1 --- a/src/HOL/Limits.thy	Tue Apr 25 08:38:23 2017 +0200
    13.2 +++ b/src/HOL/Limits.thy	Tue Apr 25 16:39:54 2017 +0100
    13.3 @@ -1799,10 +1799,12 @@
    13.4    using assms by simp
    13.5  
    13.6  text \<open>An unbounded sequence's inverse tends to 0.\<close>
    13.7 -lemma LIMSEQ_inverse_zero: "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
    13.8 +lemma LIMSEQ_inverse_zero:
    13.9 +  assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n"
   13.10 +  shows "(\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
   13.11    apply (rule filterlim_compose[OF tendsto_inverse_0])
   13.12    apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
   13.13 -  apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
   13.14 +  apply (metis assms abs_le_D1 linorder_le_cases linorder_not_le)
   13.15    done
   13.16  
   13.17  text \<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\<close>
   13.18 @@ -2189,16 +2191,16 @@
   13.19    using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
   13.20  
   13.21  lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F"
   13.22 -  for f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   13.23 +  for f :: "'a \<Rightarrow> 'b::real_normed_vector"
   13.24    unfolding tendsto_iff dist_norm by simp
   13.25  
   13.26  lemma LIM_zero_cancel:
   13.27 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   13.28 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   13.29    shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F"
   13.30  unfolding tendsto_iff dist_norm by simp
   13.31  
   13.32  lemma LIM_zero_iff: "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F = (f \<longlongrightarrow> l) F"
   13.33 -  for f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   13.34 +  for f :: "'a \<Rightarrow> 'b::real_normed_vector"
   13.35    unfolding tendsto_iff dist_norm by simp
   13.36  
   13.37  lemma LIM_imp_LIM:
    14.1 --- a/src/HOL/Probability/Sinc_Integral.thy	Tue Apr 25 08:38:23 2017 +0200
    14.2 +++ b/src/HOL/Probability/Sinc_Integral.thy	Tue Apr 25 16:39:54 2017 +0100
    14.3 @@ -219,12 +219,11 @@
    14.4      have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real
    14.5        by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
    14.6           (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
    14.7 -    then have **: "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
    14.8 +    then have "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
    14.9          by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right
   14.10                   intro!:  mult_mono)
   14.11 -
   14.12 -    show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
   14.13 -      using eventually_ge_at_top[of "1::real"] ** by (auto elim: eventually_mono)
   14.14 +    then show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
   14.15 +      by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"])
   14.16      show "AE x in lborel. 0 < x \<longrightarrow> (?F x \<longlongrightarrow> 0) at_top"
   14.17      proof (intro always_eventually impI allI)
   14.18        fix x :: real assume "0 < x"
    15.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Apr 25 08:38:23 2017 +0200
    15.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Apr 25 16:39:54 2017 +0100
    15.3 @@ -364,6 +364,7 @@
    15.4    by (auto intro: injI)
    15.5  
    15.6  lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
    15.7 +lemmas of_real_eq_1_iff [simp] = of_real_eq_iff [of _ 1, simplified]
    15.8  
    15.9  lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
   15.10    by (rule ext) (simp add: of_real_def)
    16.1 --- a/src/HOL/Set_Interval.thy	Tue Apr 25 08:38:23 2017 +0200
    16.2 +++ b/src/HOL/Set_Interval.thy	Tue Apr 25 16:39:54 2017 +0100
    16.3 @@ -1892,7 +1892,7 @@
    16.4    by (induction m) (simp_all add: algebra_simps)
    16.5  
    16.6  
    16.7 -subsubsection \<open>The formula for geometric sums\<close>
    16.8 +subsection \<open>The formula for geometric sums\<close>
    16.9  
   16.10  lemma geometric_sum:
   16.11    assumes "x \<noteq> 1"
   16.12 @@ -1947,6 +1947,71 @@
   16.13    shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
   16.14  by (metis one_diff_power_eq' [of n x] nat_diff_sum_reindex)
   16.15  
   16.16 +lemma sum_gp_basic:
   16.17 +  fixes x :: "'a::{comm_ring,monoid_mult}"
   16.18 +  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
   16.19 +  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
   16.20 +
   16.21 +lemma sum_power_shift:
   16.22 +  fixes x :: "'a::{comm_ring,monoid_mult}"
   16.23 +  assumes "m \<le> n"
   16.24 +  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
   16.25 +proof -
   16.26 +  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
   16.27 +    by (simp add: sum_distrib_left power_add [symmetric])
   16.28 +  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
   16.29 +    using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
   16.30 +  finally show ?thesis .
   16.31 +qed
   16.32 +
   16.33 +lemma sum_gp_multiplied:
   16.34 +  fixes x :: "'a::{comm_ring,monoid_mult}"
   16.35 +  assumes "m \<le> n"
   16.36 +  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
   16.37 +proof -
   16.38 +  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
   16.39 +    by (metis mult.assoc mult.commute assms sum_power_shift)
   16.40 +  also have "... =x^m * (1 - x^Suc(n-m))"
   16.41 +    by (metis mult.assoc sum_gp_basic)
   16.42 +  also have "... = x^m - x^Suc n"
   16.43 +    using assms
   16.44 +    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
   16.45 +  finally show ?thesis .
   16.46 +qed
   16.47 +
   16.48 +lemma sum_gp:
   16.49 +  fixes x :: "'a::{comm_ring,division_ring}"
   16.50 +  shows   "(\<Sum>i=m..n. x^i) =
   16.51 +               (if n < m then 0
   16.52 +                else if x = 1 then of_nat((n + 1) - m)
   16.53 +                else (x^m - x^Suc n) / (1 - x))"
   16.54 +using sum_gp_multiplied [of m n x] apply auto
   16.55 +by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
   16.56 +
   16.57 +subsection\<open>Geometric progressions\<close>
   16.58 +
   16.59 +lemma sum_gp0:
   16.60 +  fixes x :: "'a::{comm_ring,division_ring}"
   16.61 +  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
   16.62 +  using sum_gp_basic[of x n]
   16.63 +  by (simp add: mult.commute divide_simps)
   16.64 +
   16.65 +lemma sum_power_add:
   16.66 +  fixes x :: "'a::{comm_ring,monoid_mult}"
   16.67 +  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
   16.68 +  by (simp add: sum_distrib_left power_add)
   16.69 +
   16.70 +lemma sum_gp_offset:
   16.71 +  fixes x :: "'a::{comm_ring,division_ring}"
   16.72 +  shows   "(\<Sum>i=m..m+n. x^i) =
   16.73 +       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
   16.74 +  using sum_gp [of x m "m+n"]
   16.75 +  by (auto simp: power_add algebra_simps)
   16.76 +
   16.77 +lemma sum_gp_strict:
   16.78 +  fixes x :: "'a::{comm_ring,division_ring}"
   16.79 +  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
   16.80 +  by (induct n) (auto simp: algebra_simps divide_simps)
   16.81  
   16.82  subsubsection \<open>The formula for arithmetic sums\<close>
   16.83  
    17.1 --- a/src/HOL/Transcendental.thy	Tue Apr 25 08:38:23 2017 +0200
    17.2 +++ b/src/HOL/Transcendental.thy	Tue Apr 25 16:39:54 2017 +0100
    17.3 @@ -1506,7 +1506,7 @@
    17.4    finally show False by simp
    17.5  qed
    17.6  
    17.7 -lemma exp_minus_inverse: "exp x * exp (- x) = 1"
    17.8 +lemma exp_minus_inverse [simp]: "exp x * exp (- x) = 1"
    17.9    by (simp add: exp_add_commuting[symmetric])
   17.10  
   17.11  lemma exp_minus: "exp (- x) = inverse (exp x)"
   17.12 @@ -1517,17 +1517,18 @@
   17.13    for x :: "'a::{real_normed_field,banach}"
   17.14    using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
   17.15  
   17.16 -lemma exp_of_nat_mult: "exp (of_nat n * x) = exp x ^ n"
   17.17 +lemma exp_of_nat_mult [simp]: "exp (of_nat n * x) = exp x ^ n"
   17.18    for x :: "'a::{real_normed_field,banach}"
   17.19    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
   17.20  
   17.21 -corollary exp_real_of_nat_mult: "exp (real n * x) = exp x ^ n"
   17.22 -  by (simp add: exp_of_nat_mult)
   17.23 +corollary exp_of_nat2_mult [simp]: "exp (x * of_nat n) = exp x ^ n"
   17.24 +  for x :: "'a::{real_normed_field,banach}"
   17.25 +  by (metis exp_of_nat_mult mult_of_nat_commute)
   17.26  
   17.27  lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = prod (\<lambda>x. exp (f x)) I"
   17.28    by (induct I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
   17.29  
   17.30 -lemma exp_divide_power_eq:
   17.31 +lemma exp_divide_power_eq [simp]:
   17.32    fixes x :: "'a::{real_normed_field,banach}"
   17.33    assumes "n > 0"
   17.34    shows "exp (x / of_nat n) ^ n = exp x"
   17.35 @@ -1742,7 +1743,7 @@
   17.36    for x :: real
   17.37    by (erule subst) (rule ln_exp)
   17.38  
   17.39 -lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   17.40 +lemma ln_mult [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   17.41    for x :: real
   17.42    by (rule ln_unique) (simp add: exp_add)
   17.43  
   17.44 @@ -1750,7 +1751,7 @@
   17.45    for f :: "'a \<Rightarrow> real"
   17.46    by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
   17.47  
   17.48 -lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   17.49 +lemma ln_inverse [simp]: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   17.50    for x :: real
   17.51    by (rule ln_unique) (simp add: exp_minus)
   17.52  
   17.53 @@ -1758,8 +1759,8 @@
   17.54    for x :: real
   17.55    by (rule ln_unique) (simp add: exp_diff)
   17.56  
   17.57 -lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
   17.58 -  by (rule ln_unique) (simp add: exp_real_of_nat_mult)
   17.59 +lemma ln_realpow [simp]: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
   17.60 +  by (rule ln_unique) simp
   17.61  
   17.62  lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   17.63    for x :: real
   17.64 @@ -1781,6 +1782,9 @@
   17.65    for x :: real
   17.66    by (rule order_less_le_trans [where y = "ln (1 + x)"]) simp_all
   17.67  
   17.68 +lemma ln_ge_iff: "\<And>x::real. 0 < x \<Longrightarrow> y \<le> ln x \<longleftrightarrow> exp y \<le> x"
   17.69 +  using exp_le_cancel_iff exp_total by force
   17.70 +
   17.71  lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
   17.72    for x :: real
   17.73    using ln_le_cancel_iff [of 1 x] by simp
   17.74 @@ -2298,7 +2302,7 @@
   17.75    also from assms False have "ln (1 + x / real n) \<le> x / real n"
   17.76      by (intro ln_add_one_self_le_self2) (simp_all add: field_simps)
   17.77    with assms have "exp (of_nat n * ln (1 + x / of_nat n)) \<le> exp x"
   17.78 -    by (simp add: field_simps)
   17.79 +    by (simp add: field_simps del: exp_of_nat_mult)
   17.80    finally show ?thesis .
   17.81  next
   17.82    case True
   17.83 @@ -2701,7 +2705,7 @@
   17.84  lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
   17.85    by (induct n) (simp_all add: ac_simps powr_add)
   17.86  
   17.87 -lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   17.88 +lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   17.89    by (metis of_nat_numeral powr_realpow)
   17.90  
   17.91  lemma numeral_powr_numeral[simp]:
   17.92 @@ -2841,14 +2845,26 @@
   17.93    for x :: real
   17.94    by (simp add: powr_def)
   17.95  
   17.96 -lemma powr_mono2: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> x powr a \<le> y powr a"
   17.97 +lemma powr_mono2: "x powr a \<le> y powr a" if "0 \<le> a" "0 \<le> x" "x \<le> y"
   17.98    for x :: real
   17.99 -  apply (case_tac "a = 0")
  17.100 -   apply simp
  17.101 -  apply (case_tac "x = y")
  17.102 -   apply simp
  17.103 -  apply (metis dual_order.strict_iff_order powr_less_mono2)
  17.104 -  done
  17.105 +proof (cases "a = 0")
  17.106 +  case True
  17.107 +  with that show ?thesis by simp
  17.108 +next
  17.109 +  case False show ?thesis
  17.110 +  proof (cases "x = y")
  17.111 +    case True
  17.112 +    then show ?thesis by simp
  17.113 +  next
  17.114 +    case False
  17.115 +    then show ?thesis
  17.116 +      by (metis dual_order.strict_iff_order powr_less_mono2 that \<open>a \<noteq> 0\<close>)
  17.117 +  qed
  17.118 +qed
  17.119 +
  17.120 +lemma powr_le1: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr a \<le> 1"
  17.121 +  for x :: real
  17.122 +  using powr_mono2 by fastforce
  17.123  
  17.124  lemma powr_mono2':
  17.125    fixes a x y :: real
  17.126 @@ -2861,6 +2877,12 @@
  17.127      by (auto simp add: powr_minus field_simps)
  17.128  qed
  17.129  
  17.130 +lemma powr_mono_both:
  17.131 +  fixes x :: real
  17.132 +  assumes "0 \<le> a" "a \<le> b" "1 \<le> x" "x \<le> y"
  17.133 +    shows "x powr a \<le> y powr b"
  17.134 +  by (meson assms order.trans powr_mono powr_mono2 zero_le_one)
  17.135 +
  17.136  lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  17.137    for x :: real
  17.138    unfolding powr_def exp_inj_iff by simp