author huffman Wed Aug 17 13:10:11 2011 -0700 (2011-08-17) changeset 44254 336dd390e4a4 parent 44253 c073a0bd8458 child 44255 e37e1ef33bb8
Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
 src/HOL/Lim.thy file | annotate | diff | revisions
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.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.15 -lemma LIMSEQ_SEQ_conv2:
1.16 -  fixes a :: real and L :: "'a::metric_space"
1.17 -  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
1.18 -  shows "X -- a --> L"
1.19 +lemma LIMSEQ_SEQ_conv2_lemma:
1.20 +  fixes a :: "'a::metric_space"
1.21 +  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
1.22 +  shows "eventually P (at a)"
1.23  proof (rule ccontr)
1.24 -  assume "\<not> (X -- a --> L)"
1.25 -  hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> dist (X x) L < r)"
1.26 -    unfolding LIM_def dist_norm .
1.27 -  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.28 -  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.29 -  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.30 -
1.31 -  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.32 -  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.33 -    using rdef by simp
1.34 -  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.35 +  let ?I = "\<lambda>n. inverse (real (Suc n))"
1.36 +  let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
1.37 +  assume "\<not> eventually P (at a)"
1.38 +  hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
1.39 +    unfolding eventually_at by simp
1.40 +  hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
1.41 +  hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
1.42      by (rule someI_ex)
1.43    hence F1: "\<And>n. ?F n \<noteq> a"
1.44 -    and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
1.45 -    and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
1.46 +    and F2: "\<And>n. dist (?F n) a < ?I n"
1.47 +    and F3: "\<And>n. \<not> P (?F n)"
1.48      by fast+
1.49 -
1.50    have "?F ----> a"
1.51 -  proof (rule LIMSEQ_I, unfold real_norm_def)
1.52 -      fix e::real
1.53 -      assume "0 < e"
1.54 -        (* choose no such that inverse (real (Suc n)) < e *)
1.55 -      then have "\<exists>no. inverse (real (Suc no)) < e" by (rule reals_Archimedean)
1.56 -      then obtain m where nodef: "inverse (real (Suc m)) < e" by auto
1.57 -      show "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e"
1.58 -      proof (intro exI allI impI)
1.59 -        fix n
1.60 -        assume mlen: "m \<le> n"
1.61 -        have "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
1.62 -          by (rule F2)
1.63 -        also have "inverse (real (Suc n)) \<le> inverse (real (Suc m))"
1.64 -          using mlen by auto
1.65 -        also from nodef have
1.66 -          "inverse (real (Suc m)) < e" .
1.67 -        finally show "\<bar>?F n - a\<bar> < e" .
1.68 -      qed
1.69 -  qed
1.70 -
1.71 +    using LIMSEQ_inverse_real_of_nat
1.72 +    by (rule metric_tendsto_imp_tendsto,
1.73 +      simp add: dist_norm F2 [THEN less_imp_le])
1.74    moreover have "\<forall>n. ?F n \<noteq> a"
1.75      by (rule allI) (rule F1)
1.76 -
1.77 -  moreover note `\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
1.78 -  ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
1.79 -
1.80 -  moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
1.81 -  proof -
1.82 -    {
1.83 -      fix no::nat
1.84 -      obtain n where "n = no + 1" by simp
1.85 -      then have nolen: "no \<le> n" by simp
1.86 -        (* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
1.87 -      have "dist (X (?F n)) L \<ge> r"
1.88 -        by (rule F3)
1.89 -      with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
1.90 -    }
1.91 -    then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
1.92 -    with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
1.93 -    thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
1.94 -  qed
1.95 -  ultimately show False by simp
1.96 +  ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
1.97 +    using assms by simp
1.98 +  thus "False" by (simp add: F3)
1.99  qed
1.101 +lemma LIMSEQ_SEQ_conv2:
1.102 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
1.103 +  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
1.104 +  shows "f -- a --> l"
1.105 +  using assms unfolding tendsto_def [where l=l]
1.106 +  by (simp add: LIMSEQ_SEQ_conv2_lemma)
1.108  lemma LIMSEQ_SEQ_conv:
1.109 -  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::real) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
1.110 -   (X -- a --> (L::'a::metric_space))"
1.111 +  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
1.112 +   (X -- a --> (L::'b::topological_space))"
1.113    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
1.115  end