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")
```