src/HOL/Transcendental.thy

   assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \<noteq> 0"
   shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
   unfolding powr_def
 proof (rule filterlim_If)
   from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
-    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
+    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds)
 qed (insert f g a, auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
 
 lemma continuous_powr:
   assumes "continuous F f"
     and "continuous F g"

   assumes f: "(f ---> a) F" and g: "(g ---> b) F" and f_nonneg: "\<forall>\<^sub>F x in F. 0 \<le> f x" and b: "0 < b"
   shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
   unfolding powr_def
 proof (rule filterlim_If)
   from f show "((\<lambda>x. 0) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))"
-    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_elim1 dest: t1_space_nhds)
+    by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds)
 next
   { assume "a = 0"
     with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0"
       by (auto simp add: filterlim_at eventually_inf_principal le_less
-               elim: eventually_elim1 intro: tendsto_mono inf_le1)
+               elim: eventually_mono intro: tendsto_mono inf_le1)
     then have "((\<lambda>x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \<noteq> 0}))"
       by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0]
                        filterlim_tendsto_pos_mult_at_bot[OF _ \<open>0 < b\<close>]
                intro: tendsto_mono inf_le1 g) }
   then show "((\<lambda>x. exp (g x * ln (f x))) ---> (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \<noteq> 0}))"

   then show ?thesis
   proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated])
     from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
       unfolding isCont_def by (rule order_tendstoD(1))
     with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
-      by (auto simp: eventually_at_filter powr_def elim: eventually_elim1)
+      by (auto simp: eventually_at_filter powr_def elim: eventually_mono)
   qed
 qed
 
 lemma DERIV_fun_powr:
   fixes r::real

   have "((\<lambda>x. exp (s * ln (f x))) ---> (0::real)) F" (is "?X")
     by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_top]
                      filterlim_tendsto_neg_mult_at_bot assms)
   also have "?X \<longleftrightarrow> ((\<lambda>x. f x powr s) ---> (0::real)) F"
     using f filterlim_at_top_dense[of f F]
-    by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_elim1)
+    by (intro filterlim_cong[OF refl refl]) (auto simp: neq_iff powr_def elim: eventually_mono)
   finally show ?thesis .
 qed
 
 lemma tendsto_exp_limit_at_right:
   fixes x :: real

     apply (rule add_pos_nonneg, auto intro: divide_nonneg_nonneg)
     apply (subgoal_tac "x / real xa > -1")
     apply (auto simp add: field_simps)
     done
   then show "eventually (\<lambda>n. (1 + x / n) powr n = (1 + x / n) ^ n) at_top"
-    by (rule eventually_elim1) (erule powr_realpow)
+    by (rule eventually_mono) (erule powr_realpow)
   show "(\<lambda>n. (1 + x / real n) powr real n) ----> exp x"
     by (rule filterlim_compose [OF tendsto_exp_limit_at_top filterlim_real_sequentially])
 qed auto
 
 subsection \<open>Sine and Cosine\<close>