src/HOL/Analysis/Complex_Transcendental.thy
changeset 66447 a1f5c5c26fa6
parent 66252 b73f94b366b7
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 17 14:40:42 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 17 14:52:56 2017 +0200
     1.3 @@ -2420,7 +2420,7 @@
     1.4                 intro!: mult_pos_pos divide_pos_pos always_eventually)
     1.5      thus "summable (\<lambda>n. g n * u^n)"
     1.6        by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
     1.7 -         (auto simp: power_mult subseq_def g_def h_def elim!: oddE)
     1.8 +         (auto simp: power_mult strict_mono_def g_def h_def elim!: oddE)
     1.9    qed (simp add: h_def)
    1.10  
    1.11    have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c"
    1.12 @@ -2436,7 +2436,7 @@
    1.13        by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib)
    1.14      also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)"
    1.15        by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
    1.16 -         (auto elim!: evenE simp: subseq_def power_mult power_mult_distrib)
    1.17 +         (auto elim!: evenE simp: strict_mono_def power_mult power_mult_distrib)
    1.18      also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all
    1.19      hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
    1.20        by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide)
    1.21 @@ -2450,7 +2450,7 @@
    1.22    with c z have "Arctan z = G z" by simp
    1.23    with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff)
    1.24    thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
    1.25 -                              (auto elim!: oddE simp: subseq_def power_mult g_def h_def)
    1.26 +                              (auto elim!: oddE simp: strict_mono_def power_mult g_def h_def)
    1.27  qed
    1.28  
    1.29  text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close>