author huffman Mon, 08 Jun 2009 19:18:47 -0700 changeset 31534 0de814d2ff95 parent 31533 2cce9283ba72 child 31535 f5bde0d3c385
```--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 17:15:22 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 19:18:47 2009 -0700
@@ -2451,16 +2451,23 @@
thus "\<exists>l. (f ---> l) sequentially" unfolding LIMSEQ_conv_tendsto .
qed

+lemma complete_imp_closed: assumes "complete s" shows "closed s"
+proof -
+  { fix x assume "x islimpt s"
+    then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially"
+      unfolding islimpt_sequential by auto
+    then obtain l where l: "l\<in>s" "(f ---> l) sequentially"
+      using `complete s`[unfolded complete_def] using convergent_imp_cauchy[of f x] by auto
+    hence "x \<in> s"  using Lim_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
+  }
+  thus "closed s" unfolding closed_limpt by auto
+qed
+
lemma complete_eq_closed:
fixes s :: "'a::complete_space set"
shows "complete s \<longleftrightarrow> closed s" (is "?lhs = ?rhs")
proof
-  assume ?lhs
-  { fix x assume "x islimpt s"
-    then obtain f where f:"\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially" unfolding islimpt_sequential by auto
-    then obtain l where l: "l\<in>s" "(f ---> l) sequentially" using `?lhs`[unfolded complete_def]  using convergent_imp_cauchy[of f x] by auto
-    hence "x \<in> s"  using Lim_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto  }
-  thus ?rhs unfolding closed_limpt by auto
+  assume ?lhs thus ?rhs by (rule complete_imp_closed)
next
assume ?rhs
{ fix f assume as:"\<forall>n::nat. f n \<in> s" "Cauchy f"
@@ -2725,7 +2732,7 @@
then obtain l' where "l'\<in>s" "l' islimpt {y. \<exists>n. y = x n}" using assms[THEN spec[where x="{y. \<exists>n. y = x n}"]] as(1) by auto
thus "l\<in>s" using sequence_unique_limpt[of x l l'] using as cas by auto
qed  }
-  thus ?thesis unfolding closed_sequential_limits by auto (* FIXME: simp_depth_limit exceeded *)
+  thus ?thesis unfolding closed_sequential_limits by fast
qed

text{* Hence express everything as an equivalence.   *}```