src/HOL/Lim.thy
changeset 44532 a2e9b39df938
parent 44314 dbad46932536
child 44568 e6f291cb5810
     1.1 --- a/src/HOL/Lim.thy	Thu Aug 25 19:41:38 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Fri Aug 26 08:12:38 2011 -0700
     1.3 @@ -444,46 +444,51 @@
     1.4  
     1.5  subsection {* Relation of LIM and LIMSEQ *}
     1.6  
     1.7 +lemma sequentially_imp_eventually_within:
     1.8 +  fixes a :: "'a::metric_space"
     1.9 +  assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
    1.10 +    eventually (\<lambda>n. P (f n)) sequentially"
    1.11 +  shows "eventually P (at a within s)"
    1.12 +proof (rule ccontr)
    1.13 +  let ?I = "\<lambda>n. inverse (real (Suc n))"
    1.14 +  def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
    1.15 +  assume "\<not> eventually P (at a within s)"
    1.16 +  hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
    1.17 +    unfolding Limits.eventually_within Limits.eventually_at by fast
    1.18 +  hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
    1.19 +  hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
    1.20 +    unfolding F_def by (rule someI_ex)
    1.21 +  hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
    1.22 +    and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"
    1.23 +    by fast+
    1.24 +  from LIMSEQ_inverse_real_of_nat have "F ----> a"
    1.25 +    by (rule metric_tendsto_imp_tendsto,
    1.26 +      simp add: dist_norm F2 less_imp_le)
    1.27 +  hence "eventually (\<lambda>n. P (F n)) sequentially"
    1.28 +    using assms F0 F1 by simp
    1.29 +  thus "False" by (simp add: F3)
    1.30 +qed
    1.31 +
    1.32 +lemma sequentially_imp_eventually_at:
    1.33 +  fixes a :: "'a::metric_space"
    1.34 +  assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
    1.35 +    eventually (\<lambda>n. P (f n)) sequentially"
    1.36 +  shows "eventually P (at a)"
    1.37 +  using assms sequentially_imp_eventually_within [where s=UNIV]
    1.38 +  unfolding within_UNIV by simp
    1.39 +
    1.40  lemma LIMSEQ_SEQ_conv1:
    1.41    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    1.42    assumes f: "f -- a --> l"
    1.43    shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
    1.44    using tendsto_compose_eventually [OF f, where F=sequentially] by simp
    1.45  
    1.46 -lemma LIMSEQ_SEQ_conv2_lemma:
    1.47 -  fixes a :: "'a::metric_space"
    1.48 -  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
    1.49 -  shows "eventually P (at a)"
    1.50 -proof (rule ccontr)
    1.51 -  let ?I = "\<lambda>n. inverse (real (Suc n))"
    1.52 -  let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
    1.53 -  assume "\<not> eventually P (at a)"
    1.54 -  hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
    1.55 -    unfolding eventually_at by simp
    1.56 -  hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
    1.57 -  hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
    1.58 -    by (rule someI_ex)
    1.59 -  hence F1: "\<And>n. ?F n \<noteq> a"
    1.60 -    and F2: "\<And>n. dist (?F n) a < ?I n"
    1.61 -    and F3: "\<And>n. \<not> P (?F n)"
    1.62 -    by fast+
    1.63 -  have "?F ----> a"
    1.64 -    using LIMSEQ_inverse_real_of_nat
    1.65 -    by (rule metric_tendsto_imp_tendsto,
    1.66 -      simp add: dist_norm F2 [THEN less_imp_le])
    1.67 -  moreover have "\<forall>n. ?F n \<noteq> a"
    1.68 -    by (rule allI) (rule F1)
    1.69 -  ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
    1.70 -    using assms by simp
    1.71 -  thus "False" by (simp add: F3)
    1.72 -qed
    1.73 -
    1.74  lemma LIMSEQ_SEQ_conv2:
    1.75    fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
    1.76    assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
    1.77    shows "f -- a --> l"
    1.78    using assms unfolding tendsto_def [where l=l]
    1.79 -  by (simp add: LIMSEQ_SEQ_conv2_lemma)
    1.80 +  by (simp add: sequentially_imp_eventually_at)
    1.81  
    1.82  lemma LIMSEQ_SEQ_conv:
    1.83    "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =