src/HOL/Transcendental.thy
 changeset 56381 0556204bc230 parent 56371 fb9ae0727548 child 56409 36489d77c484
```     1.1 --- a/src/HOL/Transcendental.thy	Thu Apr 03 17:16:02 2014 +0200
1.2 +++ b/src/HOL/Transcendental.thy	Thu Apr 03 17:56:08 2014 +0200
1.3 @@ -630,7 +630,7 @@
1.4        and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
1.5        and 4: "norm x < norm K"
1.6    shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
1.7 -  unfolding deriv_def
1.8 +  unfolding DERIV_def
1.9  proof (rule LIM_zero_cancel)
1.10    show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
1.11              - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
1.12 @@ -669,7 +669,7 @@
1.13      and "summable L"
1.14      and L_def: "\<And>n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar>f x n - f y n\<bar> \<le> L n * \<bar>x - y\<bar>"
1.15    shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))"
1.16 -  unfolding deriv_def
1.17 +  unfolding DERIV_def
1.18  proof (rule LIM_I)
1.19    fix r :: real
1.20    assume "0 < r" hence "0 < r/3" by auto
1.21 @@ -863,7 +863,7 @@
1.22        {
1.23          fix n
1.24          show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
1.25 -          by (auto intro!: DERIV_intros simp del: power_Suc)
1.26 +          by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def)
1.27        }
1.28        {
1.29          fix x
1.30 @@ -978,7 +978,7 @@
1.31    apply (simp del: of_real_add)
1.32    done
1.33
1.34 -declare DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.35 +declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
1.36
1.37  lemma isCont_exp: "isCont exp x"
1.38    by (rule DERIV_exp [THEN DERIV_isCont])
1.39 @@ -1315,7 +1315,7 @@
1.40  lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
1.41    by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
1.42
1.43 -declare DERIV_ln_divide[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.44 +declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
1.45
1.46  lemma ln_series:
1.47    assumes "0 < x" and "x < 2"
1.48 @@ -1356,7 +1356,7 @@
1.49      hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
1.50        unfolding One_nat_def by auto
1.51      hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)"
1.52 -      unfolding deriv_def repos .
1.53 +      unfolding DERIV_def repos .
1.54      ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
1.55        by (rule DERIV_diff)
1.56      thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
1.57 @@ -1621,7 +1621,7 @@
1.58  proof -
1.59    let ?l = "\<lambda>y. ln y - y + 1"
1.60    have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
1.61 -    by (auto intro!: DERIV_intros)
1.62 +    by (auto intro!: derivative_eq_intros)
1.63
1.64    show ?thesis
1.65    proof (cases rule: linorder_cases)
1.66 @@ -1699,9 +1699,9 @@
1.67    show ?case
1.68    proof (rule lhospital_at_top_at_top)
1.69      show "eventually (\<lambda>x. DERIV (\<lambda>x. x ^ Suc k) x :> (real (Suc k) * x^k)) at_top"
1.70 -      by eventually_elim (intro DERIV_intros, simp, simp)
1.71 +      by eventually_elim (intro derivative_eq_intros, auto)
1.72      show "eventually (\<lambda>x. DERIV exp x :> exp x) at_top"
1.73 -      by eventually_elim (auto intro!: DERIV_intros)
1.74 +      by eventually_elim auto
1.75      show "eventually (\<lambda>x. exp x \<noteq> 0) at_top"
1.76        by auto
1.77      from tendsto_mult[OF tendsto_const Suc, of "real (Suc k)"]
1.78 @@ -1825,12 +1825,12 @@
1.79  proof -
1.80    def lb \<equiv> "1 / ln b"
1.81    moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x"
1.82 -    using `x > 0` by (auto intro!: DERIV_intros)
1.83 +    using `x > 0` by (auto intro!: derivative_eq_intros)
1.84    ultimately show ?thesis
1.85      by (simp add: log_def)
1.86  qed
1.87
1.88 -lemmas DERIV_log[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.89 +lemmas DERIV_log[THEN DERIV_chain2, derivative_intros]
1.90
1.91  lemma powr_log_cancel [simp]: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powr (log a x) = x"
1.92    by (simp add: powr_def log_def)
1.93 @@ -2180,7 +2180,7 @@
1.94      summable_minus summable_sin summable_cos)
1.95    done
1.96
1.97 -declare DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.98 +declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
1.99
1.100  lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
1.101    unfolding cos_def sin_def
1.102 @@ -2189,7 +2189,7 @@
1.103      summable_minus summable_sin summable_cos suminf_minus)
1.104    done
1.105
1.106 -declare DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.107 +declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
1.108
1.109  lemma isCont_sin: "isCont sin x"
1.110    by (rule DERIV_sin [THEN DERIV_isCont])
1.111 @@ -2238,7 +2238,7 @@
1.112  lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
1.113  proof -
1.114    have "\<forall>x. DERIV (\<lambda>x. (sin x)\<^sup>2 + (cos x)\<^sup>2) x :> 0"
1.115 -    by (auto intro!: DERIV_intros)
1.116 +    by (auto intro!: derivative_eq_intros)
1.117    hence "(sin x)\<^sup>2 + (cos x)\<^sup>2 = (sin 0)\<^sup>2 + (cos 0)\<^sup>2"
1.118      by (rule DERIV_isconst_all)
1.119    thus "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" by simp
1.120 @@ -2276,19 +2276,19 @@
1.121
1.122  lemma DERIV_fun_pow: "DERIV g x :> m ==>
1.123        DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
1.124 -  by (auto intro!: DERIV_intros)
1.125 +  by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
1.126
1.127  lemma DERIV_fun_exp:
1.128       "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
1.129 -  by (auto intro!: DERIV_intros)
1.130 +  by (auto intro!: derivative_intros)
1.131
1.132  lemma DERIV_fun_sin:
1.133       "DERIV g x :> m ==> DERIV (\<lambda>x. sin(g x)) x :> cos(g x) * m"
1.134 -  by (auto intro!: DERIV_intros)
1.135 +  by (auto intro!: derivative_intros)
1.136
1.137  lemma DERIV_fun_cos:
1.138       "DERIV g x :> m ==> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
1.139 -  by (auto intro!: DERIV_intros)
1.140 +  by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
1.141
1.143    "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 +
1.144 @@ -2296,7 +2296,7 @@
1.145    (is "?f x = 0")
1.146  proof -
1.147    have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
1.148 -    by (auto intro!: DERIV_intros simp add: algebra_simps)
1.149 +    by (auto intro!: derivative_eq_intros simp add: algebra_simps)
1.150    hence "?f x = ?f 0"
1.151      by (rule DERIV_isconst_all)
1.152    thus ?thesis by simp
1.153 @@ -2312,7 +2312,7 @@
1.154    "(sin(-x) + sin(x))\<^sup>2 + (cos(-x) - cos(x))\<^sup>2 = 0" (is "?f x = 0")
1.155  proof -
1.156    have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0"
1.157 -    by (auto intro!: DERIV_intros simp add: algebra_simps)
1.158 +    by (auto intro!: derivative_eq_intros simp add: algebra_simps)
1.159    hence "?f x = ?f 0"
1.160      by (rule DERIV_isconst_all)
1.161    thus ?thesis by simp
1.162 @@ -2859,7 +2859,7 @@
1.163
1.164  lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
1.165    unfolding tan_def
1.166 -  by (auto intro!: DERIV_intros, simp add: divide_inverse power2_eq_square)
1.167 +  by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
1.168
1.169  lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
1.170    by (rule DERIV_tan [THEN DERIV_isCont])
1.171 @@ -3332,9 +3332,9 @@
1.172    done
1.173
1.174  declare
1.175 -  DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.176 -  DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.177 -  DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.178 +  DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
1.179 +  DERIV_arccos[THEN DERIV_chain2, derivative_intros]
1.180 +  DERIV_arctan[THEN DERIV_chain2, derivative_intros]
1.181
1.182  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
1.183    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
1.184 @@ -3465,7 +3465,7 @@
1.185    done
1.186
1.187  lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
1.188 -  by (auto intro!: DERIV_intros)
1.189 +  by (auto intro!: derivative_eq_intros)
1.190
1.191  lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
1.192    by (auto simp add: sin_zero_iff even_mult_two_ex)
```