src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 50949 a5689bb4ed7e
parent 50948 8c742f9de9f5
child 50955 ada575c605e1
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 19:28:48 2013 -0800
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 20:26:38 2013 -0800
     1.3 @@ -5427,24 +5427,54 @@
     1.4  qed
     1.5  
     1.6  lemma separate_compact_closed:
     1.7 -  fixes s t :: "'a::{heine_borel, real_normed_vector} set"
     1.8 -    (* TODO: does this generalize to heine_borel? *)
     1.9 +  fixes s t :: "'a::heine_borel set"
    1.10    assumes "compact s" and "closed t" and "s \<inter> t = {}"
    1.11    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
    1.12 -proof-
    1.13 -  have "0 \<notin> {x - y |x y. x \<in> s \<and> y \<in> t}" using assms(3) by auto
    1.14 -  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"
    1.15 -    using separate_point_closed[OF compact_closed_differences[OF assms(1,2)], of 0] by auto
    1.16 -  { fix x y assume "x\<in>s" "y\<in>t"
    1.17 -    hence "x - y \<in> {x - y |x y. x \<in> s \<and> y \<in> t}" by auto
    1.18 -    hence "d \<le> dist (x - y) 0" using d[THEN bspec[where x="x - y"]] using dist_commute
    1.19 -      by (auto  simp add: dist_commute)
    1.20 -    hence "d \<le> dist x y" unfolding dist_norm by auto  }
    1.21 -  thus ?thesis using `d>0` by auto
    1.22 +proof - (* FIXME: long proof *)
    1.23 +  let ?T = "\<Union>x\<in>s. { ball x (d / 2) | d. 0 < d \<and> (\<forall>y\<in>t. d \<le> dist x y) }"
    1.24 +  note `compact s`
    1.25 +  moreover have "\<forall>t\<in>?T. open t" by auto
    1.26 +  moreover have "s \<subseteq> \<Union>?T"
    1.27 +    apply auto
    1.28 +    apply (rule rev_bexI, assumption)
    1.29 +    apply (subgoal_tac "x \<notin> t")
    1.30 +    apply (drule separate_point_closed [OF `closed t`])
    1.31 +    apply clarify
    1.32 +    apply (rule_tac x="ball x (d / 2)" in exI)
    1.33 +    apply simp
    1.34 +    apply fast
    1.35 +    apply (cut_tac assms(3))
    1.36 +    apply auto
    1.37 +    done
    1.38 +  ultimately obtain U where "U \<subseteq> ?T" and "finite U" and "s \<subseteq> \<Union>U"
    1.39 +    by (rule compactE)
    1.40 +  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"
    1.41 +    apply (induct set: finite)
    1.42 +    apply simp
    1.43 +    apply (rule exI)
    1.44 +    apply (rule zero_less_one)
    1.45 +    apply clarsimp
    1.46 +    apply (rename_tac y e)
    1.47 +    apply (rule_tac x="min d (e / 2)" in exI)
    1.48 +    apply simp
    1.49 +    apply (subst ball_Un)
    1.50 +    apply (rule conjI)
    1.51 +    apply (intro ballI, rename_tac z)
    1.52 +    apply (rule min_max.le_infI2)
    1.53 +    apply (simp only: mem_ball)
    1.54 +    apply (drule (1) bspec)
    1.55 +    apply (cut_tac x=y and y=x and z=z in dist_triangle, arith)
    1.56 +    apply simp
    1.57 +    apply (intro ballI)
    1.58 +    apply (rule min_max.le_infI1)
    1.59 +    apply simp
    1.60 +    done
    1.61 +  with `s \<subseteq> \<Union>U` show ?thesis
    1.62 +    by fast
    1.63  qed
    1.64  
    1.65  lemma separate_closed_compact:
    1.66 -  fixes s t :: "'a::{heine_borel, real_normed_vector} set"
    1.67 +  fixes s t :: "'a::heine_borel set"
    1.68    assumes "closed s" and "compact t" and "s \<inter> t = {}"
    1.69    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
    1.70  proof-