src/HOL/Transcendental.thy
changeset 31790 05c92381363c
parent 31338 d41a8ba25b67
child 31880 6fb86c61747c
     1.1 --- a/src/HOL/Transcendental.thy	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -2242,7 +2242,7 @@
     1.4  lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x" 
     1.5  proof (induct n arbitrary: x)
     1.6    case (Suc n)
     1.7 -  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
     1.8 +  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
     1.9    show ?case unfolding split_pi_off using Suc by auto
    1.10  qed auto
    1.11  
    1.12 @@ -2779,12 +2779,12 @@
    1.13      show ?thesis
    1.14      proof (cases "0 \<le> x")
    1.15        case True from mono[OF this `x \<le> 1`, THEN allI]
    1.16 -      show ?thesis unfolding Suc_plus1[symmetric] by (rule mono_SucI2)
    1.17 +      show ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI2)
    1.18      next
    1.19        case False hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
    1.20        from mono[OF this]
    1.21        have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge> 1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
    1.22 -      thus ?thesis unfolding Suc_plus1[symmetric] by (rule mono_SucI1[OF allI])
    1.23 +      thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
    1.24      qed
    1.25    qed
    1.26  qed
    1.27 @@ -2800,13 +2800,13 @@
    1.28      case True hence "norm x < 1" by auto
    1.29      from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
    1.30      have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
    1.31 -      unfolding inverse_eq_divide Suc_plus1 by simp
    1.32 +      unfolding inverse_eq_divide Suc_eq_plus1 by simp
    1.33      then show ?thesis using pos2 by (rule LIMSEQ_linear)
    1.34    next
    1.35      case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
    1.36      hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
    1.37      from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
    1.38 -    show ?thesis unfolding n_eq Suc_plus1 by auto
    1.39 +    show ?thesis unfolding n_eq Suc_eq_plus1 by auto
    1.40    qed
    1.41  qed
    1.42  
    1.43 @@ -2921,7 +2921,7 @@
    1.44      qed
    1.45      
    1.46      have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
    1.47 -      unfolding Suc_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero by auto
    1.48 +      unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero by auto
    1.49      
    1.50      have "suminf (?c x) - arctan x = 0"
    1.51      proof (cases "x = 0")