# HG changeset patch
# User hoelzl
# Date 1358429892 -3600
# Node ID 03b11adf1f33dee7731d9716b444661a5ac32816
# Parent  88a00a1c7c2ca444f8ccd559f4665a411700c848
simplified prove of compact_imp_bounded

diff -r 88a00a1c7c2c -r 03b11adf1f33 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 13:58:02 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 14:38:12 2013 +0100
@@ -2325,7 +2325,8 @@
 lemma Inf_insert:
   fixes S :: "real set"
   shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" 
-by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal) 
+by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal)
+
 lemma Inf_insert_finite:
   fixes S :: "real set"
   shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
@@ -2349,6 +2350,12 @@
   obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
   using assms unfolding compact_eq_heine_borel by metis
 
+lemma compactE_image:
+  assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
+  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
+  using assms unfolding ball_simps[symmetric] SUP_def
+  by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
+
 subsubsection {* Bolzano-Weierstrass property *}
 
 lemma heine_borel_imp_bolzano_weierstrass:
@@ -2572,6 +2579,29 @@
     by (simp add: eventually_nhds subset_eq)
 qed
 
+lemma compact_imp_bounded:
+  assumes "compact U" shows "bounded U"
+proof -
+  have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)" using assms by auto
+  then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"
+    by (elim compactE_image)
+  def d \<equiv> "SOME d. d \<in> D"
+  show "bounded U"
+    unfolding bounded_def
+  proof (intro exI, safe)
+    fix x assume "x \<in> U"
+    with D obtain d' where "d' \<in> D" "x \<in> ball d' 1" by auto
+    moreover have "dist d x \<le> dist d d' + dist d' x"
+      using dist_triangle[of d x d'] by (simp add: dist_commute)
+    moreover
+    from `x\<in>U` D have "d \<in> D"
+      unfolding d_def by (rule_tac someI_ex) auto
+    ultimately
+    show "dist d x \<le> Max ((\<lambda>d'. dist d d' + 1) ` D)"
+      using D by (subst Max_ge_iff) (auto intro!: bexI[of _ d'])
+  qed
+qed
+
 text{* In particular, some common special cases. *}
 
 lemma compact_empty[simp]:
@@ -3105,8 +3135,6 @@
 
 subsubsection{* Heine-Borel theorem *}
 
-text {* Following Burkill \& Burkill vol. 2. *}
-
 lemma seq_compact_imp_heine_borel:
   fixes s :: "'a :: metric_space set"
   assumes "seq_compact s" shows "compact s"
@@ -3150,6 +3178,22 @@
    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f o r) ----> l))"
   unfolding compact_eq_seq_compact_metric seq_compact_def by auto
 
+subsubsection {* Complete the chain of compactness variants *}
+
+lemma compact_eq_bolzano_weierstrass:
+  fixes s :: "'a::metric_space set"
+  shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")
+proof
+  assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto
+next
+  assume ?rhs thus ?lhs
+    unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
+qed
+
+lemma bolzano_weierstrass_imp_bounded:
+  "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
+  using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
+
 text {*
   A metric space (or topological vector space) is said to have the
   Heine-Borel property if every closed and bounded subset is compact.
@@ -3174,6 +3218,17 @@
     using `l \<in> s` r l by blast
 qed
 
+lemma compact_eq_bounded_closed:
+  fixes s :: "'a::heine_borel set"
+  shows "compact s \<longleftrightarrow> bounded s \<and> closed s"  (is "?lhs = ?rhs")
+proof
+  assume ?lhs thus ?rhs
+    using compact_imp_closed compact_imp_bounded by blast
+next
+  assume ?rhs thus ?lhs
+    using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
+qed
+
 lemma lim_subseq:
   "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
 unfolding tendsto_def eventually_sequentially o_def
@@ -3498,84 +3553,6 @@
   shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
   by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
 
-subsubsection {* Complete the chain of compactness variants *}
-
-primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
-  "helper_2 beyond 0 = beyond 0" |
-  "helper_2 beyond (Suc n) = beyond (dist undefined (helper_2 beyond n) + 1 )"
-
-lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::metric_space set"
-  assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
-  shows "bounded s"
-proof(rule ccontr)
-  assume "\<not> bounded s"
-  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist undefined (beyond a) \<le> a"
-    unfolding bounded_any_center [where a=undefined]
-    apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist undefined x \<le> a"] by auto
-  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist undefined (beyond a) > a"
-    unfolding linorder_not_le by auto
-  def x \<equiv> "helper_2 beyond"
-
-  { fix m n ::nat assume "m<n"
-    hence "dist undefined (x m) + 1 < dist undefined (x n)"
-    proof(induct n)
-      case 0 thus ?case by auto
-    next
-      case (Suc n)
-      have *:"dist undefined (x n) + 1 < dist undefined (x (Suc n))"
-        unfolding x_def and helper_2.simps
-        using beyond(2)[of "dist undefined (helper_2 beyond n) + 1"] by auto
-      thus ?case proof(cases "m < n")
-        case True thus ?thesis using Suc and * by auto
-      next
-        case False hence "m = n" using Suc(2) by auto
-        thus ?thesis using * by auto
-      qed
-    qed  } note * = this
-  { fix m n ::nat assume "m\<noteq>n"
-    have "1 < dist (x m) (x n)"
-    proof(cases "m<n")
-      case True
-      hence "1 < dist undefined (x n) - dist undefined (x m)" using *[of m n] by auto
-      thus ?thesis using dist_triangle [of undefined "x n" "x m"] by arith
-    next
-      case False hence "n<m" using `m\<noteq>n` by auto
-      hence "1 < dist undefined (x m) - dist undefined (x n)" using *[of n m] by auto
-      thus ?thesis using dist_triangle2 [of undefined "x m" "x n"] by arith
-    qed  } note ** = this
-  { fix a b assume "x a = x b" "a \<noteq> b"
-    hence False using **[of a b] by auto  }
-  hence "inj x" unfolding inj_on_def by auto
-  moreover
-  { fix n::nat
-    have "x n \<in> s"
-    proof(cases "n = 0")
-      case True thus ?thesis unfolding x_def using beyond by auto
-    next
-      case False then obtain z where "n = Suc z" using not0_implies_Suc by auto
-      thus ?thesis unfolding x_def using beyond by auto
-    qed  }
-  ultimately have "infinite (range x) \<and> range x \<subseteq> s" unfolding x_def using range_inj_infinite[of "helper_2 beyond"] using beyond(1) by auto
-
-  then obtain l where "l\<in>s" and l:"l islimpt range x" using assms[THEN spec[where x="range x"]] by auto
-  then obtain y where "x y \<noteq> l" and y:"dist (x y) l < 1/2" unfolding islimpt_approachable apply(erule_tac x="1/2" in allE) by auto
-  then obtain z where "x z \<noteq> l" and z:"dist (x z) l < dist (x y) l" using l[unfolded islimpt_approachable, THEN spec[where x="dist (x y) l"]]
-    unfolding dist_nz by auto
-  show False using y and z and dist_triangle_half_l[of "x y" l 1 "x z"] and **[of y z] by auto
-qed
-
-text {* Hence express everything as an equivalence. *}
-
-lemma compact_eq_bolzano_weierstrass:
-  fixes s :: "'a::metric_space set"
-  shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")
-proof
-  assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto
-next
-  assume ?rhs thus ?lhs
-    unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
-qed
-
 lemma nat_approx_posE:
   fixes e::real
   assumes "0 < e"
@@ -3724,28 +3701,6 @@
   qed
 qed
 
-lemma compact_eq_bounded_closed:
-  fixes s :: "'a::heine_borel set"
-  shows "compact s \<longleftrightarrow> bounded s \<and> closed s"  (is "?lhs = ?rhs")
-proof
-  assume ?lhs thus ?rhs
-    unfolding compact_eq_bolzano_weierstrass using bolzano_weierstrass_imp_bounded bolzano_weierstrass_imp_closed by auto
-next
-  assume ?rhs thus ?lhs
-    using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
-qed
-
-lemma compact_imp_bounded:
-  fixes s :: "'a::metric_space set"
-  shows "compact s \<Longrightarrow> bounded s"
-proof -
-  assume "compact s"
-  hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"
-    using heine_borel_imp_bolzano_weierstrass[of s] by auto
-  thus "bounded s"
-    by (rule bolzano_weierstrass_imp_bounded)
-qed
-
 lemma compact_cball[simp]:
   fixes x :: "'a::heine_borel"
   shows "compact(cball x e)"
@@ -4938,8 +4893,8 @@
 proof (cases, safe)
   fix e :: real assume "0 < e" "s \<noteq> {}"
   def [simp]: R \<equiv> "{(y, d). y \<in> s \<and> 0 < d \<and> ball y d \<inter> s \<subseteq> {x \<in> s. f x \<in> ball (f y) (e/2) } }"
-  let ?C = "(\<lambda>(y, d). ball y (d/2)) ` R"
-  have "(\<forall>r\<in>?C. open r) \<and> s \<subseteq> \<Union>?C"
+  let ?b = "(\<lambda>(y, d). ball y (d/2))"
+  have "(\<forall>r\<in>R. open (?b r))" "s \<subseteq> (\<Union>r\<in>R. ?b r)"
   proof safe
     fix y assume "y \<in> s"
     from continuous_open_in_preimage[OF f open_ball]
@@ -4947,11 +4902,11 @@
       unfolding openin_subtopology open_openin by metis
     then obtain d where "ball y d \<subseteq> T" "0 < d"
       using `0 < e` `y \<in> s` by (auto elim!: openE)
-    with T `y \<in> s` show "y \<in> \<Union>(\<lambda>(y, d). ball y (d/2)) ` R"
-      by (intro UnionI[where X="ball y (d/2)"]) auto
+    with T `y \<in> s` show "y \<in> (\<Union>r\<in>R. ?b r)"
+      by (intro UN_I[of "(y, d)"]) auto
   qed auto
-  then obtain D where D: "finite D" "D \<subseteq> R" "s \<subseteq> (\<Union>(y, d)\<in>D. ball y (d/2))"
-    by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s] s Union_image_eq)
+  with s obtain D where D: "finite D" "D \<subseteq> R" "s \<subseteq> (\<Union>(y, d)\<in>D. ball y (d/2))"
+    by (rule compactE_image)
   with `s \<noteq> {}` have [simp]: "\<And>x. x < Min (snd ` D) \<longleftrightarrow> (\<forall>(y, d)\<in>D. x < d)"
     by (subst Min_gr_iff) auto
   show "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"