# HG changeset patch
# User huffman
# Date 1312841014 25200
# Node ID e3a744a157d42c6e4f330ca992c4ebc510635da6
# Parent  efd1ea744101e25cd3169c9d4663b07be693be81
generalize compactness equivalence lemmas

diff -r efd1ea744101 -r e3a744a157d4 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 08 14:59:01 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 08 15:03:34 2011 -0700
@@ -2955,26 +2955,26 @@
 text{* Hence express everything as an equivalence.   *}
 
 lemma compact_eq_heine_borel:
-  fixes s :: "'a::heine_borel set"
+  fixes s :: "'a::metric_space set"
   shows "compact s \<longleftrightarrow>
            (\<forall>f. (\<forall>t \<in> f. open t) \<and> s \<subseteq> (\<Union> f)
                --> (\<exists>f'. f' \<subseteq> f \<and> finite f' \<and> s \<subseteq> (\<Union> f')))" (is "?lhs = ?rhs")
 proof
-  assume ?lhs thus ?rhs using compact_imp_heine_borel[of s] by blast
+  assume ?lhs thus ?rhs by (rule compact_imp_heine_borel)
 next
   assume ?rhs
   hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. x islimpt t)"
     by (blast intro: heine_borel_imp_bolzano_weierstrass[of s])
-  thus ?lhs using bolzano_weierstrass_imp_bounded[of s] bolzano_weierstrass_imp_closed[of s] bounded_closed_imp_compact[of s] by blast
+  thus ?lhs by (rule bolzano_weierstrass_imp_compact)
 qed
 
 lemma compact_eq_bolzano_weierstrass:
-  fixes s :: "'a::heine_borel set"
+  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 unfolding compact_eq_heine_borel using heine_borel_imp_bolzano_weierstrass[of s] by auto
 next
-  assume ?rhs thus ?lhs using bolzano_weierstrass_imp_bounded bolzano_weierstrass_imp_closed bounded_closed_imp_compact by auto
+  assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
 qed
 
 lemma compact_eq_bounded_closed: