# HG changeset patch
# User huffman
# Date 1313604452 25200
# Node ID 10362a07eb7c524affd80b7360ff38f0b1df0412
# Parent  d101ed3177b686cb1ab0e10c6c9e6f7ee8fa6d56
Topology_Euclidean_Space.thy: simplify some proofs

diff -r d101ed3177b6 -r 10362a07eb7c src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 17 11:06:39 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 17 11:07:32 2011 -0700
@@ -1237,16 +1237,10 @@
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net"
   shows "(f ---> 0) net"
-proof(simp add: tendsto_iff, rule+)
-  fix e::real assume "0<e"
-  { fix x
-    assume "norm (f x) \<le> g x" "dist (g x) 0 < e"
-    hence "dist (f x) 0 < e" by (simp add: dist_norm)
-  }
-  thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
-    using eventually_conj_iff[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (g x) 0 < e" net]
-    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]
-    using assms `e>0` unfolding tendsto_iff by auto
+proof (rule metric_tendsto_imp_tendsto)
+  show "(g ---> 0) net" by fact
+  show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
+    using assms(1) by (rule eventually_elim1, simp add: dist_norm)
 qed
 
 lemma Lim_transform_bound:
@@ -1254,16 +1248,8 @@
   fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
   shows "(f ---> 0) net"
-proof (rule tendstoI)
-  fix e::real assume "e>0"
-  { fix x
-    assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
-    hence "dist (f x) 0 < e" by (simp add: dist_norm)}
-  thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
-    using eventually_conj_iff[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
-    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]
-    using assms `e>0` unfolding tendsto_iff by blast
-qed
+  using assms(1) tendsto_norm_zero [OF assms(2)]
+  by (rule Lim_null_comparison)
 
 text{* Deducing things about the limit from the elements. *}
 
@@ -1287,60 +1273,45 @@
 lemma Lim_dist_ubound:
   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
   shows "dist a l <= e"
-proof (rule ccontr)
-  assume "\<not> dist a l \<le> e"
-  then have "0 < dist a l - e" by simp
-  with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
-    by (rule tendstoD)
-  with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
-    by (rule eventually_conj)
-  then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
-    using assms(1) eventually_happens by auto
-  hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
-    by (rule add_le_less_mono)
-  hence "dist a (f w) + dist (f w) l < dist a l"
-    by simp
-  also have "\<dots> \<le> dist a (f w) + dist (f w) l"
-    by (rule dist_triangle)
-  finally show False by simp
+proof-
+  have "dist a l \<in> {..e}"
+  proof (rule Lim_in_closed_set)
+    show "closed {..e}" by simp
+    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" by (simp add: assms)
+    show "\<not> trivial_limit net" by fact
+    show "((\<lambda>x. dist a (f x)) ---> dist a l) net" by (intro tendsto_intros assms)
+  qed
+  thus ?thesis by simp
 qed
 
 lemma Lim_norm_ubound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
   shows "norm(l) <= e"
-proof (rule ccontr)
-  assume "\<not> norm l \<le> e"
-  then have "0 < norm l - e" by simp
-  with assms(2) have "eventually (\<lambda>x. dist (f x) l < norm l - e) net"
-    by (rule tendstoD)
-  with assms(3) have "eventually (\<lambda>x. norm (f x) \<le> e \<and> dist (f x) l < norm l - e) net"
-    by (rule eventually_conj)
-  then obtain w where "norm (f w) \<le> e" "dist (f w) l < norm l - e"
-    using assms(1) eventually_happens by auto
-  hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm)
-  hence "norm (f w - l) + norm (f w) < norm l" by simp
-  hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4])
-  thus False using `\<not> norm l \<le> e` by simp
+proof-
+  have "norm l \<in> {..e}"
+  proof (rule Lim_in_closed_set)
+    show "closed {..e}" by simp
+    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" by (simp add: assms)
+    show "\<not> trivial_limit net" by fact
+    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
+  qed
+  thus ?thesis by simp
 qed
 
 lemma Lim_norm_lbound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not> (trivial_limit net)"  "(f ---> l) net"  "eventually (\<lambda>x. e <= norm(f x)) net"
   shows "e \<le> norm l"
-proof (rule ccontr)
-  assume "\<not> e \<le> norm l"
-  then have "0 < e - norm l" by simp
-  with assms(2) have "eventually (\<lambda>x. dist (f x) l < e - norm l) net"
-    by (rule tendstoD)
-  with assms(3) have "eventually (\<lambda>x. e \<le> norm (f x) \<and> dist (f x) l < e - norm l) net"
-    by (rule eventually_conj)
-  then obtain w where "e \<le> norm (f w)" "dist (f w) l < e - norm l"
-    using assms(1) eventually_happens by auto
-  hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm)
-  hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans)
-  hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq])
-  thus False by simp
+proof-
+  have "norm l \<in> {e..}"
+  proof (rule Lim_in_closed_set)
+    show "closed {e..}" by simp
+    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" by (simp add: assms)
+    show "\<not> trivial_limit net" by fact
+    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
+  qed
+  thus ?thesis by simp
 qed
 
 text{* Uniqueness of the limit, when nontrivial. *}
@@ -1371,40 +1342,7 @@
   fixes a :: "'a::real_normed_vector"
   fixes l :: "'b::topological_space"
   shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
-proof
-  assume "?lhs"
-  { fix S assume "open S" "l \<in> S"
-    with `?lhs` have "eventually (\<lambda>x. f x \<in> S) (at a)"
-      by (rule topological_tendstoD)
-    then obtain d where d: "d>0" "\<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S"
-      unfolding Limits.eventually_at by fast
-    { fix x::"'a" assume "x \<noteq> 0 \<and> dist x 0 < d"
-      hence "f (a + x) \<in> S" using d
-      apply(erule_tac x="x+a" in allE)
-      by (auto simp add: add_commute dist_norm dist_commute)
-    }
-    hence "\<exists>d>0. \<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
-      using d(1) by auto
-    hence "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
-      unfolding Limits.eventually_at .
-  }
-  thus "?rhs" by (rule topological_tendstoI)
-next
-  assume "?rhs"
-  { fix S assume "open S" "l \<in> S"
-    with `?rhs` have "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
-      by (rule topological_tendstoD)
-    then obtain d where d: "d>0" "\<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
-      unfolding Limits.eventually_at by fast
-    { fix x::"'a" assume "x \<noteq> a \<and> dist x a < d"
-      hence "f x \<in> S" using d apply(erule_tac x="x-a" in allE)
-        by(auto simp add: add_commute dist_norm dist_commute)
-    }
-    hence "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S" using d(1) by auto
-    hence "eventually (\<lambda>x. f x \<in> S) (at a)" unfolding Limits.eventually_at .
-  }
-  thus "?lhs" by (rule topological_tendstoI)
-qed
+  using LIM_offset_zero LIM_offset_zero_cancel ..
 
 text{* It's also sometimes useful to extract the limit point from the filter. *}
 
@@ -1447,10 +1385,7 @@
   fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
   assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
   shows "(g ---> l) net"
-proof-
-  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
-  thus "?thesis" using tendsto_minus [of "\<lambda> x. - g x" "-l" net] by auto
-qed
+  using tendsto_diff [OF assms(2) assms(1)] by simp
 
 lemma Lim_transform_eventually:
   "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"