src/HOL/Deriv.thy

 
 lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --> D"
 by (simp add: deriv_def)
 
 lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x :> 0"
-by (simp add: deriv_def)
+  by (simp add: deriv_def tendsto_const)
 
 lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
-by (simp add: deriv_def cong: LIM_cong)
+  by (simp add: deriv_def tendsto_const cong: LIM_cong)
 
 lemma DERIV_add:
   "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x :> D + E"
-by (simp only: deriv_def add_diff_add add_divide_distrib LIM_add)
+  by (simp only: deriv_def add_diff_add add_divide_distrib tendsto_add)
 
 lemma DERIV_minus:
   "DERIV f x :> D \<Longrightarrow> DERIV (\<lambda>x. - f x) x :> - D"
-by (simp only: deriv_def minus_diff_minus divide_minus_left LIM_minus)
+  by (simp only: deriv_def minus_diff_minus divide_minus_left tendsto_minus)
 
 lemma DERIV_diff:
   "\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
 by (simp only: diff_minus DERIV_add DERIV_minus)
 

 proof (unfold isCont_iff)
   assume "DERIV f x :> D"
   hence "(\<lambda>h. (f(x+h) - f(x)) / h) -- 0 --> D"
     by (rule DERIV_D)
   hence "(\<lambda>h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0"
-    by (intro LIM_mult LIM_ident)
+    by (intro tendsto_mult tendsto_ident_at)
   hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
     by simp
   hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
     by (simp cong: LIM_cong)
   thus "(\<lambda>h. f(x+h)) -- 0 --> f(x)"

   hence "(\<lambda>h. f(x+h)) -- 0 --> f x"
     by (simp only: isCont_iff)
   hence "(\<lambda>h. f(x+h) * ((g(x+h) - g x) / h) +
               ((f(x+h) - f x) / h) * g x)
           -- 0 --> f x * E + D * g x"
-    by (intro LIM_add LIM_mult LIM_const DERIV_D f g)
+    by (intro tendsto_intros DERIV_D f g)
   thus "(\<lambda>h. (f(x+h) * g(x+h) - f x * g x) / h)
          -- 0 --> f x * E + D * g x"
     by (simp only: DERIV_mult_lemma)
 qed
 

   next
     from der have "(\<lambda>z. (f z - f x) / (z - x)) -- x --> D"
       by (unfold DERIV_iff2)
     thus "(\<lambda>z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x)))
           -- x --> ?E"
-      by (intro LIM_mult LIM_inverse LIM_minus LIM_const lim_f neq)
+      by (intro tendsto_intros lim_f neq)
   qed
 qed
 
 lemma DERIV_divide:
   "\<lbrakk>DERIV f x :> D; DERIV g x :> E; g x \<noteq> 0\<rbrakk>

     and cont_d: "isCont d (f x)" and dfx: "d (f x) = E"
     using CARAT_DERIV [THEN iffD1, OF g] by fast
   from f have "f -- x --> f x"
     by (rule DERIV_isCont [unfolded isCont_def])
   with cont_d have "(\<lambda>z. d (f z)) -- x --> d (f x)"
-    by (rule isCont_LIM_compose)
+    by (rule isCont_tendsto_compose)
   hence "(\<lambda>z. d (f z) * ((f z - f x) / (z - x)))
           -- x --> d (f x) * D"
-    by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]])
+    by (rule tendsto_mult [OF _ f [unfolded DERIV_iff2]])
   thus "(\<lambda>z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D"
     by (simp add: d dfx)
 qed
 
 text {*

 done
 
 lemma lim_uminus:
   fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "convergent g ==> lim (%x. - g x) = - (lim g)"
-apply (rule LIMSEQ_minus [THEN limI])
+apply (rule tendsto_minus [THEN limI])
 apply (simp add: convergent_LIMSEQ_iff)
 done
 
 lemma g_dec_imp_lim_le:
   fixes g :: "nat \<Rightarrow> real"

          (%n. f(n) - g(n)) ----> 0 |]
       ==> \<exists>l::real. ((\<forall>n. f(n) \<le> l) & f ----> l) &
                 ((\<forall>n. l \<le> g(n)) & g ----> l)"
 apply (drule lemma_nest, auto)
 apply (subgoal_tac "l = m")
-apply (drule_tac [2] f = f in LIMSEQ_diff)
+apply (drule_tac [2] f = f in tendsto_diff)
 apply (auto intro: LIMSEQ_unique)
 done
 
 text{*The universal quantifiers below are required for the declaration
   of @{text Bolzano_nest_unique} below.*}

          \<forall>x. \<exists>d::real. 0 < d &
                 (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b));
          a \<le> b |]
       ==> P(a,b)"
 apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+)
-apply (rule LIMSEQ_minus_cancel)
+apply (rule tendsto_minus_cancel)
 apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero)
 apply (rule ccontr)
 apply (drule not_P_Bolzano_bisect', assumption+)
 apply (rename_tac "l")
 apply (drule_tac x = l in spec, clarify)

   qed
   have "(\<lambda>y. (f (g y) - x) / (g y - g x)) -- x --> D"
     using cont 1 2 by (rule isCont_LIM_compose2)
   thus "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x)))
         -- x --> inverse D"
-    using neq by (rule LIM_inverse)
+    using neq by (rule tendsto_inverse)
 qed
 
 
 subsection {* Generalized Mean Value Theorem *}