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.142  lemma sin_cos_add_lemma:
   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)