# HG changeset patch
# User huffman
# Date 1358310398 28800
# Node ID a5689bb4ed7e418e05999bad307a6fe0b355ad6a
# Parent  8c742f9de9f58b4092edfbfd03e0010e3f104e50
generalize more topology lemmas

diff -r 8c742f9de9f5 -r a5689bb4ed7e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 19:28:48 2013 -0800
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 20:26:38 2013 -0800
@@ -5427,24 +5427,54 @@
 qed
 
 lemma separate_compact_closed:
-  fixes s t :: "'a::{heine_borel, real_normed_vector} set"
-    (* TODO: does this generalize to heine_borel? *)
+  fixes s t :: "'a::heine_borel set"
   assumes "compact s" and "closed t" and "s \<inter> t = {}"
   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof-
-  have "0 \<notin> {x - y |x y. x \<in> s \<and> y \<in> t}" using assms(3) by auto
-  then obtain d where "d>0" and d:"\<forall>x\<in>{x - y |x y. x \<in> s \<and> y \<in> t}. d \<le> dist 0 x"
-    using separate_point_closed[OF compact_closed_differences[OF assms(1,2)], of 0] by auto
-  { fix x y assume "x\<in>s" "y\<in>t"
-    hence "x - y \<in> {x - y |x y. x \<in> s \<and> y \<in> t}" by auto
-    hence "d \<le> dist (x - y) 0" using d[THEN bspec[where x="x - y"]] using dist_commute
-      by (auto  simp add: dist_commute)
-    hence "d \<le> dist x y" unfolding dist_norm by auto  }
-  thus ?thesis using `d>0` by auto
+proof - (* FIXME: long proof *)
+  let ?T = "\<Union>x\<in>s. { ball x (d / 2) | d. 0 < d \<and> (\<forall>y\<in>t. d \<le> dist x y) }"
+  note `compact s`
+  moreover have "\<forall>t\<in>?T. open t" by auto
+  moreover have "s \<subseteq> \<Union>?T"
+    apply auto
+    apply (rule rev_bexI, assumption)
+    apply (subgoal_tac "x \<notin> t")
+    apply (drule separate_point_closed [OF `closed t`])
+    apply clarify
+    apply (rule_tac x="ball x (d / 2)" in exI)
+    apply simp
+    apply fast
+    apply (cut_tac assms(3))
+    apply auto
+    done
+  ultimately obtain U where "U \<subseteq> ?T" and "finite U" and "s \<subseteq> \<Union>U"
+    by (rule compactE)
+  from `finite U` and `U \<subseteq> ?T` have "\<exists>d>0. \<forall>x\<in>\<Union>U. \<forall>y\<in>t. d \<le> dist x y"
+    apply (induct set: finite)
+    apply simp
+    apply (rule exI)
+    apply (rule zero_less_one)
+    apply clarsimp
+    apply (rename_tac y e)
+    apply (rule_tac x="min d (e / 2)" in exI)
+    apply simp
+    apply (subst ball_Un)
+    apply (rule conjI)
+    apply (intro ballI, rename_tac z)
+    apply (rule min_max.le_infI2)
+    apply (simp only: mem_ball)
+    apply (drule (1) bspec)
+    apply (cut_tac x=y and y=x and z=z in dist_triangle, arith)
+    apply simp
+    apply (intro ballI)
+    apply (rule min_max.le_infI1)
+    apply simp
+    done
+  with `s \<subseteq> \<Union>U` show ?thesis
+    by fast
 qed
 
 lemma separate_closed_compact:
-  fixes s t :: "'a::{heine_borel, real_normed_vector} set"
+  fixes s t :: "'a::heine_borel set"
   assumes "closed s" and "compact t" and "s \<inter> t = {}"
   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
 proof-