1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 17 11:06:39 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 17 11:07:32 2011 -0700
     1.3 @@ -1237,16 +1237,10 @@
     1.4    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     1.5    assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net"
     1.6    shows "(f ---> 0) net"
     1.7 -proof(simp add: tendsto_iff, rule+)
     1.8 -  fix e::real assume "0<e"
     1.9 -  { fix x
    1.10 -    assume "norm (f x) \<le> g x" "dist (g x) 0 < e"
    1.11 -    hence "dist (f x) 0 < e" by (simp add: dist_norm)
    1.12 -  }
    1.13 -  thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
    1.14 -    using eventually_conj_iff[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net]
    1.15 -    using eventually_mono[of "(\<lambda>x. norm (f x) \<le> g x \<and> dist (g x) 0 < e)" "(\<lambda>x. dist (f x) 0 < e)" net]
    1.16 -    using assms `e>0` unfolding tendsto_iff by auto
    1.17 +proof (rule metric_tendsto_imp_tendsto)
    1.18 +  show "(g ---> 0) net" by fact
    1.19 +  show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
    1.20 +    using assms(1) by (rule eventually_elim1, simp add: dist_norm)
    1.21  qed
    1.22  
    1.23  lemma Lim_transform_bound:
    1.24 @@ -1254,16 +1248,8 @@
    1.25    fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
    1.26    assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
    1.27    shows "(f ---> 0) net"
    1.28 -proof (rule tendstoI)
    1.29 -  fix e::real assume "e>0"
    1.30 -  { fix x
    1.31 -    assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
    1.32 -    hence "dist (f x) 0 < e" by (simp add: dist_norm)}
    1.33 -  thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
    1.34 -    using eventually_conj_iff[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
    1.35 -    using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
    1.36 -    using assms `e>0` unfolding tendsto_iff by blast
    1.37 -qed
    1.38 +  using assms(1) tendsto_norm_zero [OF assms(2)]
    1.39 +  by (rule Lim_null_comparison)
    1.40  
    1.41  text{* Deducing things about the limit from the elements. *}
    1.42  
    1.43 @@ -1287,60 +1273,45 @@
    1.44  lemma Lim_dist_ubound:
    1.45    assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
    1.46    shows "dist a l <= e"
    1.47 -proof (rule ccontr)
    1.48 -  assume "\<not> dist a l \<le> e"
    1.49 -  then have "0 < dist a l - e" by simp
    1.50 -  with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
    1.51 -    by (rule tendstoD)
    1.52 -  with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
    1.53 -    by (rule eventually_conj)
    1.54 -  then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
    1.55 -    using assms(1) eventually_happens by auto
    1.56 -  hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
    1.57 -    by (rule add_le_less_mono)
    1.58 -  hence "dist a (f w) + dist (f w) l < dist a l"
    1.59 -    by simp
    1.60 -  also have "\<dots> \<le> dist a (f w) + dist (f w) l"
    1.61 -    by (rule dist_triangle)
    1.62 -  finally show False by simp
    1.63 +proof-
    1.64 +  have "dist a l \<in> {..e}"
    1.65 +  proof (rule Lim_in_closed_set)
    1.66 +    show "closed {..e}" by simp
    1.67 +    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" by (simp add: assms)
    1.68 +    show "\<not> trivial_limit net" by fact
    1.69 +    show "((\<lambda>x. dist a (f x)) ---> dist a l) net" by (intro tendsto_intros assms)
    1.70 +  qed
    1.71 +  thus ?thesis by simp
    1.72  qed
    1.73  
    1.74  lemma Lim_norm_ubound:
    1.75    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    1.76    assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
    1.77    shows "norm(l) <= e"
    1.78 -proof (rule ccontr)
    1.79 -  assume "\<not> norm l \<le> e"
    1.80 -  then have "0 < norm l - e" by simp
    1.81 -  with assms(2) have "eventually (\<lambda>x. dist (f x) l < norm l - e) net"
    1.82 -    by (rule tendstoD)
    1.83 -  with assms(3) have "eventually (\<lambda>x. norm (f x) \<le> e \<and> dist (f x) l < norm l - e) net"
    1.84 -    by (rule eventually_conj)
    1.85 -  then obtain w where "norm (f w) \<le> e" "dist (f w) l < norm l - e"
    1.86 -    using assms(1) eventually_happens by auto
    1.87 -  hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm)
    1.88 -  hence "norm (f w - l) + norm (f w) < norm l" by simp
    1.89 -  hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4])
    1.90 -  thus False using `\<not> norm l \<le> e` by simp
    1.91 +proof-
    1.92 +  have "norm l \<in> {..e}"
    1.93 +  proof (rule Lim_in_closed_set)
    1.94 +    show "closed {..e}" by simp
    1.95 +    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" by (simp add: assms)
    1.96 +    show "\<not> trivial_limit net" by fact
    1.97 +    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
    1.98 +  qed
    1.99 +  thus ?thesis by simp
   1.100  qed
   1.101  
   1.102  lemma Lim_norm_lbound:
   1.103    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.104    assumes "\<not> (trivial_limit net)"  "(f ---> l) net"  "eventually (\<lambda>x. e <= norm(f x)) net"
   1.105    shows "e \<le> norm l"
   1.106 -proof (rule ccontr)
   1.107 -  assume "\<not> e \<le> norm l"
   1.108 -  then have "0 < e - norm l" by simp
   1.109 -  with assms(2) have "eventually (\<lambda>x. dist (f x) l < e - norm l) net"
   1.110 -    by (rule tendstoD)
   1.111 -  with assms(3) have "eventually (\<lambda>x. e \<le> norm (f x) \<and> dist (f x) l < e - norm l) net"
   1.112 -    by (rule eventually_conj)
   1.113 -  then obtain w where "e \<le> norm (f w)" "dist (f w) l < e - norm l"
   1.114 -    using assms(1) eventually_happens by auto
   1.115 -  hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm)
   1.116 -  hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans)
   1.117 -  hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq])
   1.118 -  thus False by simp
   1.119 +proof-
   1.120 +  have "norm l \<in> {e..}"
   1.121 +  proof (rule Lim_in_closed_set)
   1.122 +    show "closed {e..}" by simp
   1.123 +    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" by (simp add: assms)
   1.124 +    show "\<not> trivial_limit net" by fact
   1.125 +    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
   1.126 +  qed
   1.127 +  thus ?thesis by simp
   1.128  qed
   1.129  
   1.130  text{* Uniqueness of the limit, when nontrivial. *}
   1.131 @@ -1371,40 +1342,7 @@
   1.132    fixes a :: "'a::real_normed_vector"
   1.133    fixes l :: "'b::topological_space"
   1.134    shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
   1.135 -proof
   1.136 -  assume "?lhs"
   1.137 -  { fix S assume "open S" "l \<in> S"
   1.138 -    with `?lhs` have "eventually (\<lambda>x. f x \<in> S) (at a)"
   1.139 -      by (rule topological_tendstoD)
   1.140 -    then obtain d where d: "d>0" "\<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S"
   1.141 -      unfolding Limits.eventually_at by fast
   1.142 -    { fix x::"'a" assume "x \<noteq> 0 \<and> dist x 0 < d"
   1.143 -      hence "f (a + x) \<in> S" using d
   1.144 -      apply(erule_tac x="x+a" in allE)
   1.145 -      by (auto simp add: add_commute dist_norm dist_commute)
   1.146 -    }
   1.147 -    hence "\<exists>d>0. \<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
   1.148 -      using d(1) by auto
   1.149 -    hence "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
   1.150 -      unfolding Limits.eventually_at .
   1.151 -  }
   1.152 -  thus "?rhs" by (rule topological_tendstoI)
   1.153 -next
   1.154 -  assume "?rhs"
   1.155 -  { fix S assume "open S" "l \<in> S"
   1.156 -    with `?rhs` have "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
   1.157 -      by (rule topological_tendstoD)
   1.158 -    then obtain d where d: "d>0" "\<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
   1.159 -      unfolding Limits.eventually_at by fast
   1.160 -    { fix x::"'a" assume "x \<noteq> a \<and> dist x a < d"
   1.161 -      hence "f x \<in> S" using d apply(erule_tac x="x-a" in allE)
   1.162 -        by(auto simp add: add_commute dist_norm dist_commute)
   1.163 -    }
   1.164 -    hence "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S" using d(1) by auto
   1.165 -    hence "eventually (\<lambda>x. f x \<in> S) (at a)" unfolding Limits.eventually_at .
   1.166 -  }
   1.167 -  thus "?lhs" by (rule topological_tendstoI)
   1.168 -qed
   1.169 +  using LIM_offset_zero LIM_offset_zero_cancel ..
   1.170  
   1.171  text{* It's also sometimes useful to extract the limit point from the filter. *}
   1.172  
   1.173 @@ -1447,10 +1385,7 @@
   1.174    fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
   1.175    assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
   1.176    shows "(g ---> l) net"
   1.177 -proof-
   1.178 -  from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using tendsto_diff[of "\<lambda>x. f x - g x" 0 net f l] by auto
   1.179 -  thus "?thesis" using tendsto_minus [of "\<lambda> x. - g x" "-l" net] by auto
   1.180 -qed
   1.181 +  using tendsto_diff [OF assms(2) assms(1)] by simp
   1.182  
   1.183  lemma Lim_transform_eventually:
   1.184    "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"