src/HOL/Deriv.thy
changeset 44568 e6f291cb5810
parent 44317 b7e9fa025f15
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Deriv.thy	Sat Aug 27 17:26:14 2011 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Sun Aug 28 09:20:12 2011 -0700
     1.3 @@ -37,18 +37,18 @@
     1.4  by (simp add: deriv_def)
     1.5  
     1.6  lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x :> 0"
     1.7 -by (simp add: deriv_def)
     1.8 +  by (simp add: deriv_def tendsto_const)
     1.9  
    1.10  lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
    1.11 -by (simp add: deriv_def cong: LIM_cong)
    1.12 +  by (simp add: deriv_def tendsto_const cong: LIM_cong)
    1.13  
    1.14  lemma DERIV_add:
    1.15    "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x :> D + E"
    1.16 -by (simp only: deriv_def add_diff_add add_divide_distrib LIM_add)
    1.17 +  by (simp only: deriv_def add_diff_add add_divide_distrib tendsto_add)
    1.18  
    1.19  lemma DERIV_minus:
    1.20    "DERIV f x :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x :> - D"
    1.21 -by (simp only: deriv_def minus_diff_minus divide_minus_left LIM_minus)
    1.22 +  by (simp only: deriv_def minus_diff_minus divide_minus_left tendsto_minus)
    1.23  
    1.24  lemma DERIV_diff:
    1.25    "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
    1.26 @@ -64,7 +64,7 @@
    1.27    hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
    1.28      by (rule DERIV_D)
    1.29    hence "(\<lambda>h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0"
    1.30 -    by (intro LIM_mult LIM_ident)
    1.31 +    by (intro tendsto_mult tendsto_ident_at)
    1.32    hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
    1.33      by simp
    1.34    hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
    1.35 @@ -90,7 +90,7 @@
    1.36    hence "(\<lambda>h. f(x+h) * ((g(x+h) - g x) / h) +
    1.37                ((f(x+h) - f x) / h) * g x)
    1.38            -- 0 --> f x * E + D * g x"
    1.39 -    by (intro LIM_add LIM_mult LIM_const DERIV_D f g)
    1.40 +    by (intro tendsto_intros DERIV_D f g)
    1.41    thus "(\<lambda>h. (f(x+h) * g(x+h) - f x * g x) / h)
    1.42           -- 0 --> f x * E + D * g x"
    1.43      by (simp only: DERIV_mult_lemma)
    1.44 @@ -172,7 +172,7 @@
    1.45        by (unfold DERIV_iff2)
    1.46      thus "(\<lambda>z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x)))
    1.47            -- x --> ?E"
    1.48 -      by (intro LIM_mult LIM_inverse LIM_minus LIM_const lim_f neq)
    1.49 +      by (intro tendsto_intros lim_f neq)
    1.50    qed
    1.51  qed
    1.52  
    1.53 @@ -245,10 +245,10 @@
    1.54    from f have "f -- x --> f x"
    1.55      by (rule DERIV_isCont [unfolded isCont_def])
    1.56    with cont_d have "(\<lambda>z. d (f z)) -- x --> d (f x)"
    1.57 -    by (rule isCont_LIM_compose)
    1.58 +    by (rule isCont_tendsto_compose)
    1.59    hence "(\<lambda>z. d (f z) * ((f z - f x) / (z - x)))
    1.60            -- x --> d (f x) * D"
    1.61 -    by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]])
    1.62 +    by (rule tendsto_mult [OF _ f [unfolded DERIV_iff2]])
    1.63    thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D"
    1.64      by (simp add: d dfx)
    1.65  qed
    1.66 @@ -485,7 +485,7 @@
    1.67  lemma lim_uminus:
    1.68    fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.69    shows "convergent g ==> lim (%x. - g x) = - (lim g)"
    1.70 -apply (rule LIMSEQ_minus [THEN limI])
    1.71 +apply (rule tendsto_minus [THEN limI])
    1.72  apply (simp add: convergent_LIMSEQ_iff)
    1.73  done
    1.74  
    1.75 @@ -521,7 +521,7 @@
    1.76                  ((\<forall>n. l \<le> g(n)) & g ----> l)"
    1.77  apply (drule lemma_nest, auto)
    1.78  apply (subgoal_tac "l = m")
    1.79 -apply (drule_tac [2] f = f in LIMSEQ_diff)
    1.80 +apply (drule_tac [2] f = f in tendsto_diff)
    1.81  apply (auto intro: LIMSEQ_unique)
    1.82  done
    1.83  
    1.84 @@ -599,7 +599,7 @@
    1.85           a \<le> b |]
    1.86        ==> P(a,b)"
    1.87  apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+)
    1.88 -apply (rule LIMSEQ_minus_cancel)
    1.89 +apply (rule tendsto_minus_cancel)
    1.90  apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero)
    1.91  apply (rule ccontr)
    1.92  apply (drule not_P_Bolzano_bisect', assumption+)
    1.93 @@ -1488,7 +1488,7 @@
    1.94      using cont 1 2 by (rule isCont_LIM_compose2)
    1.95    thus "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x)))
    1.96          -- x --> inverse D"
    1.97 -    using neq by (rule LIM_inverse)
    1.98 +    using neq by (rule tendsto_inverse)
    1.99  qed
   1.100  
   1.101