1.1 --- a/src/HOL/Lim.thy	Wed Aug 17 11:07:32 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Wed Aug 17 11:39:09 2011 -0700
     1.3 @@ -254,27 +254,7 @@
     1.4    assumes g: "g -- b --> c"
     1.5    assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
     1.6    shows "(\<lambda>x. g (f x)) -- a --> c"
     1.7 -proof (rule topological_tendstoI)
     1.8 -  fix C assume C: "open C" "c \<in> C"
     1.9 -  obtain B where B: "open B" "b \<in> B"
    1.10 -    and gC: "\<And>y. y \<in> B \<Longrightarrow> y \<noteq> b \<Longrightarrow> g y \<in> C"
    1.11 -    using topological_tendstoD [OF g C]
    1.12 -    unfolding eventually_at_topological by fast
    1.13 -  obtain A where A: "open A" "a \<in> A"
    1.14 -    and fB: "\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x \<in> B"
    1.15 -    using topological_tendstoD [OF f B]
    1.16 -    unfolding eventually_at_topological by fast
    1.17 -  have "eventually (\<lambda>x. f x \<noteq> b \<longrightarrow> g (f x) \<in> C) (at a)"
    1.18 -  unfolding eventually_at_topological
    1.19 -  proof (intro exI conjI ballI impI)
    1.20 -    show "open A" and "a \<in> A" using A .
    1.21 -  next
    1.22 -    fix x assume "x \<in> A" and "x \<noteq> a" and "f x \<noteq> b"
    1.23 -    then show "g (f x) \<in> C" by (simp add: gC fB)
    1.24 -  qed
    1.25 -  with inj show "eventually (\<lambda>x. g (f x) \<in> C) (at a)"
    1.26 -    by (rule eventually_rev_mp)
    1.27 -qed
    1.28 +  using g f inj by (rule tendsto_compose_eventually)
    1.29  
    1.30  lemma metric_LIM_compose2:
    1.31    assumes f: "f -- a --> b"
    1.32 @@ -563,25 +543,9 @@
    1.33  subsection {* Relation of LIM and LIMSEQ *}
    1.34  
    1.35  lemma LIMSEQ_SEQ_conv1:
    1.36 -  fixes a :: "'a::metric_space" and L :: "'b::metric_space"
    1.37    assumes X: "X -- a --> L"
    1.38    shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
    1.39 -proof (safe intro!: metric_LIMSEQ_I)
    1.40 -  fix S :: "nat \<Rightarrow> 'a"
    1.41 -  fix r :: real
    1.42 -  assume rgz: "0 < r"
    1.43 -  assume as: "\<forall>n. S n \<noteq> a"
    1.44 -  assume S: "S ----> a"
    1.45 -  from metric_LIM_D [OF X rgz] obtain s
    1.46 -    where sgz: "0 < s"
    1.47 -    and aux: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> dist (X x) L < r"
    1.48 -    by fast
    1.49 -  from metric_LIMSEQ_D [OF S sgz]
    1.50 -  obtain no where "\<forall>n\<ge>no. dist (S n) a < s" by blast
    1.51 -  hence "\<forall>n\<ge>no. dist (X (S n)) L < r" by (simp add: aux as)
    1.52 -  thus "\<exists>no. \<forall>n\<ge>no. dist (X (S n)) L < r" ..
    1.53 -qed
    1.54 -
    1.55 +  using tendsto_compose_eventually [OF X, where F=sequentially] by simp
    1.56  
    1.57  lemma LIMSEQ_SEQ_conv2:
    1.58    fixes a :: real and L :: "'a::metric_space"
    1.59 @@ -653,12 +617,6 @@
    1.60  lemma LIMSEQ_SEQ_conv:
    1.61    "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
    1.62     (X -- a --> (L::'a::metric_space))"
    1.63 -proof
    1.64 -  assume "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
    1.65 -  thus "X -- a --> L" by (rule LIMSEQ_SEQ_conv2)
    1.66 -next
    1.67 -  assume "(X -- a --> L)"
    1.68 -  thus "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by (rule LIMSEQ_SEQ_conv1)
    1.69 -qed
    1.70 +  using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
    1.71  
    1.72  end

     2.1 --- a/src/HOL/Limits.thy	Wed Aug 17 11:07:32 2011 -0700
     2.2 +++ b/src/HOL/Limits.thy	Wed Aug 17 11:39:09 2011 -0700
     2.3 @@ -627,6 +627,22 @@
     2.4      by (rule eventually_mono)
     2.5  qed
     2.6  
     2.7 +lemma tendsto_compose_eventually:
     2.8 +  assumes g: "(g ---> m) (at l)"
     2.9 +  assumes f: "(f ---> l) F"
    2.10 +  assumes inj: "eventually (\<lambda>x. f x \<noteq> l) F"
    2.11 +  shows "((\<lambda>x. g (f x)) ---> m) F"
    2.12 +proof (rule topological_tendstoI)
    2.13 +  fix B assume B: "open B" "m \<in> B"
    2.14 +  obtain A where A: "open A" "l \<in> A"
    2.15 +    and gB: "\<And>y. y \<in> A \<Longrightarrow> y \<noteq> l \<Longrightarrow> g y \<in> B"
    2.16 +    using topological_tendstoD [OF g B]
    2.17 +    unfolding eventually_at_topological by fast
    2.18 +  show "eventually (\<lambda>x. g (f x) \<in> B) F"
    2.19 +    using topological_tendstoD [OF f A] inj
    2.20 +    by (rule eventually_elim2) (simp add: gB)
    2.21 +qed
    2.22 +
    2.23  lemma metric_tendsto_imp_tendsto:
    2.24    assumes f: "(f ---> a) F"
    2.25    assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F"