1.1 --- a/src/HOL/Lim.thy	Wed Aug 17 11:39:09 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Wed Aug 17 13:10:11 2011 -0700
     1.3 @@ -543,80 +543,49 @@
     1.4  subsection {* Relation of LIM and LIMSEQ *}
     1.5  
     1.6  lemma LIMSEQ_SEQ_conv1:
     1.7 -  assumes X: "X -- a --> L"
     1.8 -  shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
     1.9 -  using tendsto_compose_eventually [OF X, where F=sequentially] by simp
    1.10 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    1.11 +  assumes f: "f -- a --> l"
    1.12 +  shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
    1.13 +  using tendsto_compose_eventually [OF f, where F=sequentially] by simp
    1.14 +
    1.15 +lemma LIMSEQ_SEQ_conv2_lemma:
    1.16 +  fixes a :: "'a::metric_space"
    1.17 +  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
    1.18 +  shows "eventually P (at a)"
    1.19 +proof (rule ccontr)
    1.20 +  let ?I = "\<lambda>n. inverse (real (Suc n))"
    1.21 +  let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
    1.22 +  assume "\<not> eventually P (at a)"
    1.23 +  hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
    1.24 +    unfolding eventually_at by simp
    1.25 +  hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
    1.26 +  hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
    1.27 +    by (rule someI_ex)
    1.28 +  hence F1: "\<And>n. ?F n \<noteq> a"
    1.29 +    and F2: "\<And>n. dist (?F n) a < ?I n"
    1.30 +    and F3: "\<And>n. \<not> P (?F n)"
    1.31 +    by fast+
    1.32 +  have "?F ----> a"
    1.33 +    using LIMSEQ_inverse_real_of_nat
    1.34 +    by (rule metric_tendsto_imp_tendsto,
    1.35 +      simp add: dist_norm F2 [THEN less_imp_le])
    1.36 +  moreover have "\<forall>n. ?F n \<noteq> a"
    1.37 +    by (rule allI) (rule F1)
    1.38 +  ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
    1.39 +    using assms by simp
    1.40 +  thus "False" by (simp add: F3)
    1.41 +qed
    1.42  
    1.43  lemma LIMSEQ_SEQ_conv2:
    1.44 -  fixes a :: real and L :: "'a::metric_space"
    1.45 -  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
    1.46 -  shows "X -- a --> L"
    1.47 -proof (rule ccontr)
    1.48 -  assume "\<not> (X -- a --> L)"
    1.49 -  hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> dist (X x) L < r)"
    1.50 -    unfolding LIM_def dist_norm .
    1.51 -  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> dist (X x) L < r)" by simp
    1.52 -  hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r)" by (simp add: not_less)
    1.53 -  then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r))" by auto
    1.54 -
    1.55 -  let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
    1.56 -  have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
    1.57 -    using rdef by simp
    1.58 -  hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
    1.59 -    by (rule someI_ex)
    1.60 -  hence F1: "\<And>n. ?F n \<noteq> a"
    1.61 -    and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
    1.62 -    and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
    1.63 -    by fast+
    1.64 -
    1.65 -  have "?F ----> a"
    1.66 -  proof (rule LIMSEQ_I, unfold real_norm_def)
    1.67 -      fix e::real
    1.68 -      assume "0 < e"
    1.69 -        (* choose no such that inverse (real (Suc n)) < e *)
    1.70 -      then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
    1.71 -      then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
    1.72 -      show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
    1.73 -      proof (intro exI allI impI)
    1.74 -        fix n
    1.75 -        assume mlen: "m \<le> n"
    1.76 -        have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
    1.77 -          by (rule F2)
    1.78 -        also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
    1.79 -          using mlen by auto
    1.80 -        also from nodef have
    1.81 -          "inverse (real (Suc m)) < e" .
    1.82 -        finally show "\<bar>?F n - a\<bar> < e" .
    1.83 -      qed
    1.84 -  qed
    1.85 -  
    1.86 -  moreover have "\<forall>n. ?F n \<noteq> a"
    1.87 -    by (rule allI) (rule F1)
    1.88 -
    1.89 -  moreover note `\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
    1.90 -  ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
    1.91 -  
    1.92 -  moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
    1.93 -  proof -
    1.94 -    {
    1.95 -      fix no::nat
    1.96 -      obtain n where "n = no + 1" by simp
    1.97 -      then have nolen: "no \<le> n" by simp
    1.98 -        (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
    1.99 -      have "dist (X (?F n)) L \<ge> r"
   1.100 -        by (rule F3)
   1.101 -      with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
   1.102 -    }
   1.103 -    then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
   1.104 -    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
   1.105 -    thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
   1.106 -  qed
   1.107 -  ultimately show False by simp
   1.108 -qed
   1.109 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   1.110 +  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   1.111 +  shows "f -- a --> l"
   1.112 +  using assms unfolding tendsto_def [where l=l]
   1.113 +  by (simp add: LIMSEQ_SEQ_conv2_lemma)
   1.114  
   1.115  lemma LIMSEQ_SEQ_conv:
   1.116 -  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   1.117 -   (X -- a --> (L::'a::metric_space))"
   1.118 +  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   1.119 +   (X -- a --> (L::'b::topological_space))"
   1.120    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
   1.121  
   1.122  end