src/HOL/Lim.thy
 changeset 44253 c073a0bd8458 parent 44251 d101ed3177b6 child 44254 336dd390e4a4
```     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
```