# HG changeset patch
# User wenzelm
# Date 1358199233 -3600
# Node ID a9c1b1428e873ebe5f207e7fa22366b32d2b6ec7
# Parent  2b21b4e2d7cb2af6dbbc9c9a1af3011057dac282# Parent  d55eb82ae77b31d9b262dd2d6d46d317f95dce20
merged

diff -r d55eb82ae77b -r a9c1b1428e87 NEWS
--- a/NEWS	Mon Jan 14 22:24:57 2013 +0100
+++ b/NEWS	Mon Jan 14 22:33:53 2013 +0100
@@ -162,6 +162,14 @@
 switched on by default, and can be switched off by setting the
 configuration quickcheck_optimise_equality to false.
 
+* Quotient: only one quotient can be defined by quotient_type
+INCOMPATIBILITY.
+
+* Lifting:
+  - generation of an abstraction function equation in lift_definition
+  - quot_del attribute
+  - renamed no_abs_code -> no_code (INCOMPATIBILITY.)
+
 * Simproc "finite_Collect" rewrites set comprehensions into pointfree
 expressions.
 
@@ -371,6 +379,19 @@
 with support for mixed, nested recursion and interesting non-free
 datatypes.
 
+* HOL/Finite_Set and Relation: added new set and relation operations 
+expressed by Finite_Set.fold.
+
+* New theory HOL/Library/RBT_Set: implementation of sets by red-black
+trees for the code generator.
+
+* HOL/Library/RBT and HOL/Library/Mapping have been converted to
+Lifting/Transfer.
+possible INCOMPATIBILITY.
+
+* HOL/Set: renamed Set.project -> Set.filter
+INCOMPATIBILITY.
+
 
 *** Document preparation ***
 
diff -r d55eb82ae77b -r a9c1b1428e87 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -1258,7 +1258,7 @@
   corresponding constants and facts on the raw type.
 
   @{rail "
-    @@{command (HOL) quotient_type} (spec + @'and');
+    @@{command (HOL) quotient_type} (spec);
 
     spec: @{syntax typespec} @{syntax mixfix}? '=' \\
      @{syntax type} '/' ('partial' ':')? @{syntax term} \\
@@ -1514,10 +1514,12 @@
     @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
     @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
     @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\
+    @{attribute_def (HOL) "quot_del"} & : & @{text attribute}
   \end{matharray}
 
   @{rail "
-    @@{command (HOL) setup_lifting} ('(' 'no_abs_code' ')')? \\
+    @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \\
       @{syntax thmref} @{syntax thmref}?;
   "}
 
@@ -1548,7 +1550,7 @@
     the theorem is declared as an abstract type in the code
     generator. This allows @{command (HOL) "lift_definition"} to
     register (generated) code certificate theorems as abstract code
-    equations in the code generator.  The option @{text "no_abs_code"}
+    equations in the code generator.  The option @{text "no_code"}
     of the command @{command (HOL) "setup_lifting"} can turn off that
     behavior and causes that code certificate theorems generated by
     @{command (HOL) "lift_definition"} are not registred as abstract
@@ -1568,10 +1570,21 @@
     @{text f.tranfer} for the Transfer package are generated by the
     package.
 
-    Integration with code_abstype: For typedefs (e.g. subtypes
+    For each constant defined through trivial quotients (type copies or
+    subtypes) @{text f.rep_eq} is generated. The equation is a code certificate
+    that defines @{text f} using the representation function.
+
+    For each constant @{text f.abs_eq} is generated. The equation is unconditional
+    for total quotients. The equation defines @{text f} using
+    the abstraction function.
+
+    Integration with code_abstype: For subtypes (e.g.,
     corresponding to a datatype invariant, such as dlist), @{command
-    (HOL) "lift_definition"} generates a code certificate theorem
-    @{text f.rep_eq} and sets up code generation for each constant.
+    (HOL) "lift_definition"} uses a code certificate theorem
+    @{text f.rep_eq} as a code equation.
+
+    Integration with code: For total quotients, @{command
+    (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
 
   \item @{command (HOL) "print_quotmaps"} prints stored quotient map
     theorems.
@@ -1584,7 +1597,7 @@
     "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
     files.
 
-  \item @{attribute (HOL) invariant_commute} registers a theorem which
+  \item @{attribute (HOL) invariant_commute} registers a theorem that
     shows a relationship between the constant @{text
     Lifting.invariant} (used for internal encoding of proper subtypes)
     and a relator.  Such theorems allows the package to hide @{text
@@ -1593,6 +1606,17 @@
     "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
     files.
 
+  \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
+    that a relator respects reflexivity and left-totality. For exampless 
+    see @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
+    The property is used in generation of abstraction function equations.
+
+  \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
+    from the Lifting infrastructure and thus de-register the corresponding quotient. 
+    This effectively causes that @{command (HOL) lift_definition}  will not
+    do any lifting for the corresponding type. It serves mainly for hiding
+    of type construction details when the construction is done. See for example
+    @{file "~~/src/HOL/Int.thy"}.
   \end{description}
 *}
 
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Limits.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -68,6 +68,17 @@
   using assms unfolding eventually_def
   by (rule is_filter.conj [OF is_filter_Rep_filter])
 
+lemma eventually_Ball_finite:
+  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
+  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
+using assms by (induct set: finite, simp, simp add: eventually_conj)
+
+lemma eventually_all_finite:
+  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
+  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
+  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
+using eventually_Ball_finite [of UNIV P] assms by simp
+
 lemma eventually_mp:
   assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   assumes "eventually (\<lambda>x. P x) F"
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -35,7 +35,8 @@
 qed (auto intro!: continuous_intros)
 
 lemma brouwer_compactness_lemma:
-  assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = (0::_::euclidean_space)))"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space"
+  assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = 0))"
   obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)"
 proof (cases "s={}")
   case False
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -210,17 +210,6 @@
 lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
   unfolding isCont_def by (rule tendsto_vec_nth)
 
-lemma eventually_Ball_finite: (* TODO: move *)
-  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
-  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
-using assms by (induct set: finite, simp, simp add: eventually_conj)
-
-lemma eventually_all_finite: (* TODO: move *)
-  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
-  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
-  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
-using eventually_Ball_finite [of UNIV P] assms by simp
-
 lemma vec_tendstoI:
   assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net"
   shows "((\<lambda>x. f x) ---> a) net"
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -57,7 +57,7 @@
   apply (rule convex_connected, rule convex_real_interval)
   done
 
-lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g)"
+lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g :: 'a::metric_space set)"
   unfolding path_def path_image_def
   by (erule compact_continuous_image, rule compact_interval)
 
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -93,6 +93,25 @@
 
 end
 
+lemma topological_basis_prod:
+  assumes A: "topological_basis A" and B: "topological_basis B"
+  shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
+  unfolding topological_basis_def
+proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
+  fix S :: "('a \<times> 'b) set" assume "open S"
+  then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
+  proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
+    fix x y assume "(x, y) \<in> S"
+    from open_prod_elim[OF `open S` this]
+    obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
+      by (metis mem_Sigma_iff)
+    moreover from topological_basisE[OF A a] guess A0 .
+    moreover from topological_basisE[OF B b] guess B0 .
+    ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
+      by (intro UN_I[of "(A0, B0)"]) auto
+  qed auto
+qed (metis A B topological_basis_open open_Times)
+
 subsection {* Countable Basis *}
 
 locale countable_basis =
@@ -220,19 +239,118 @@
 
 end
 
-class countable_basis_space = topological_space +
+class first_countable_topology = topological_space +
+  assumes first_countable_basis:
+    "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
+
+lemma (in first_countable_topology) countable_basis_at_decseq:
+  obtains A :: "nat \<Rightarrow> 'a set" where
+    "\<And>i. open (A i)" "\<And>i. x \<in> (A i)"
+    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
+proof atomize_elim
+  from first_countable_basis[of x] obtain A
+    where "countable A"
+    and nhds: "\<And>a. a \<in> A \<Longrightarrow> open a" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a"
+    and incl: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"  by auto
+  then have "A \<noteq> {}" by auto
+  with `countable A` have r: "A = range (from_nat_into A)" by auto
+  def F \<equiv> "\<lambda>n. \<Inter>i\<le>n. from_nat_into A i"
+  show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and>
+      (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)"
+  proof (safe intro!: exI[of _ F])
+    fix i
+    show "open (F i)" using nhds(1) r by (auto simp: F_def intro!: open_INT)
+    show "x \<in> F i" using nhds(2) r by (auto simp: F_def)
+  next
+    fix S assume "open S" "x \<in> S"
+    from incl[OF this] obtain i where "F i \<subseteq> S"
+      by (subst (asm) r) (auto simp: F_def)
+    moreover have "\<And>j. i \<le> j \<Longrightarrow> F j \<subseteq> F i"
+      by (auto simp: F_def)
+    ultimately show "eventually (\<lambda>i. F i \<subseteq> S) sequentially"
+      by (auto simp: eventually_sequentially)
+  qed
+qed
+
+lemma (in first_countable_topology) first_countable_basisE:
+  obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
+    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
+  using first_countable_basis[of x]
+  by atomize_elim auto
+
+instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
+proof
+  fix x :: "'a \<times> 'b"
+  from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this
+  from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
+  show "\<exists>A::('a\<times>'b) set set. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
+  proof (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
+    fix a b assume x: "a \<in> A" "b \<in> B"
+    with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)"
+      unfolding mem_Times_iff by (auto intro: open_Times)
+  next
+    fix S assume "open S" "x \<in> S"
+    from open_prod_elim[OF this] guess a' b' .
+    moreover with A(4)[of a'] B(4)[of b']
+    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
+    ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
+      by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
+  qed (simp add: A B)
+qed
+
+instance metric_space \<subseteq> first_countable_topology
+proof
+  fix x :: 'a
+  show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
+  proof (intro exI, safe)
+    fix S assume "open S" "x \<in> S"
+    then obtain r where "0 < r" "{y. dist x y < r} \<subseteq> S"
+      by (auto simp: open_dist dist_commute subset_eq)
+    moreover from reals_Archimedean[OF `0 < r`] guess n ..
+    moreover
+    then have "{y. dist x y < inverse (Suc n)} \<subseteq> {y. dist x y < r}"
+      by (auto simp: inverse_eq_divide)
+    ultimately show "\<exists>a\<in>range (\<lambda>n. {y. dist x y < inverse (Suc n)}). a \<subseteq> S"
+      by auto
+  qed (auto intro: open_ball)
+qed
+
+class second_countable_topology = topological_space +
   assumes ex_countable_basis:
     "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
 
-sublocale countable_basis_space < countable_basis "SOME B. countable B \<and> topological_basis B"
+sublocale second_countable_topology < countable_basis "SOME B. countable B \<and> topological_basis B"
   using someI_ex[OF ex_countable_basis] by unfold_locales safe
 
+instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
+proof
+  obtain A :: "'a set set" where "countable A" "topological_basis A"
+    using ex_countable_basis by auto
+  moreover
+  obtain B :: "'b set set" where "countable B" "topological_basis B"
+    using ex_countable_basis by auto
+  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
+    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
+qed
+
+instance second_countable_topology \<subseteq> first_countable_topology
+proof
+  fix x :: 'a
+  def B \<equiv> "SOME B::'a set set. countable B \<and> topological_basis B"
+  then have B: "countable B" "topological_basis B"
+    using countable_basis is_basis
+    by (auto simp: countable_basis is_basis)
+  then show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
+    by (intro exI[of _ "{b\<in>B. x \<in> b}"])
+       (fastforce simp: topological_space_class.topological_basis_def)
+qed
+
 subsection {* Polish spaces *}
 
 text {* Textbooks define Polish spaces as completely metrizable.
   We assume the topology to be complete for a given metric. *}
 
-class polish_space = complete_space + countable_basis_space
+class polish_space = complete_space + second_countable_topology
 
 subsection {* General notion of a topology as a value *}
 
@@ -1320,33 +1438,38 @@
 text{* Another limit point characterization. *}
 
 lemma islimpt_sequential:
-  fixes x :: "'a::metric_space"
-  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
+  fixes x :: "'a::first_countable_topology"
+  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f ---> x) sequentially)"
     (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
-    unfolding islimpt_approachable
-    using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
-  let ?I = "\<lambda>n. inverse (real (Suc n))"
-  have "\<forall>n. f (?I n) \<in> S - {x}" using f by simp
-  moreover have "(\<lambda>n. f (?I n)) ----> x"
-  proof (rule metric_tendsto_imp_tendsto)
-    show "?I ----> 0"
-      by (rule LIMSEQ_inverse_real_of_nat)
-    show "eventually (\<lambda>n. dist (f (?I n)) x \<le> dist (?I n) 0) sequentially"
-      by (simp add: norm_conv_dist [symmetric] less_imp_le f)
+  from countable_basis_at_decseq[of x] guess A . note A = this
+  def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
+  { fix n
+    from `?lhs` have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
+      unfolding islimpt_def using A(1,2)[of n] by auto
+    then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
+      unfolding f_def by (rule someI_ex)
+    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto }
+  then have "\<forall>n. f n \<in> S - {x}" by auto
+  moreover have "(\<lambda>n. f n) ----> x"
+  proof (rule topological_tendstoI)
+    fix S assume "open S" "x \<in> S"
+    from A(3)[OF this] `\<And>n. f n \<in> A n`
+    show "eventually (\<lambda>x. f x \<in> S) sequentially" by (auto elim!: eventually_elim1)
   qed
   ultimately show ?rhs by fast
 next
   assume ?rhs
-  then obtain f::"nat\<Rightarrow>'a"  where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding LIMSEQ_def by auto
-  { fix e::real assume "e>0"
-    then obtain N where "dist (f N) x < e" using f(2) by auto
-    moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto
-    ultimately have "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" by auto
-  }
-  thus ?lhs unfolding islimpt_approachable by auto
+  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x" by auto
+  show ?lhs
+    unfolding islimpt_def
+  proof safe
+    fix T assume "open T" "x \<in> T"
+    from lim[THEN topological_tendstoD, OF this] f
+    show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
+      unfolding eventually_sequentially by auto
+  qed
 qed
 
 lemma Lim_inv: (* TODO: delete *)
@@ -1596,7 +1719,7 @@
 text{* Useful lemmas on closure and set of possible sequential limits.*}
 
 lemma closure_sequential:
-  fixes l :: "'a::metric_space"
+  fixes l :: "'a::first_countable_topology"
   shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
 proof
   assume "?lhs" moreover
@@ -1613,7 +1736,7 @@
 qed
 
 lemma closed_sequential_limits:
-  fixes S :: "'a::metric_space set"
+  fixes S :: "'a::first_countable_topology set"
   shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
   unfolding closed_limpt
   using closure_sequential [where 'a='a] closure_closed [where 'a='a] closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
@@ -2221,26 +2344,638 @@
   apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
   done
 
-
-subsection {* Equivalent versions of compactness *}
+subsection {* Compactness *}
+
+subsubsection{* Open-cover compactness *}
+
+definition compact :: "'a::topological_space set \<Rightarrow> bool" where
+  compact_eq_heine_borel: -- "This name is used for backwards compatibility"
+    "compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
+
+subsubsection {* Bolzano-Weierstrass property *}
+
+lemma heine_borel_imp_bolzano_weierstrass:
+  assumes "compact s" "infinite t"  "t \<subseteq> s"
+  shows "\<exists>x \<in> s. x islimpt t"
+proof(rule ccontr)
+  assume "\<not> (\<exists>x \<in> s. x islimpt t)"
+  then obtain f where f:"\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)" unfolding islimpt_def
+    using bchoice[of s "\<lambda> x T. x \<in> T \<and> open T \<and> (\<forall>y\<in>t. y \<in> T \<longrightarrow> y = x)"] by auto
+  obtain g where g:"g\<subseteq>{t. \<exists>x. x \<in> s \<and> t = f x}" "finite g" "s \<subseteq> \<Union>g"
+    using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]] using f by auto
+  from g(1,3) have g':"\<forall>x\<in>g. \<exists>xa \<in> s. x = f xa" by auto
+  { fix x y assume "x\<in>t" "y\<in>t" "f x = f y"
+    hence "x \<in> f x"  "y \<in> f x \<longrightarrow> y = x" using f[THEN bspec[where x=x]] and `t\<subseteq>s` by auto
+    hence "x = y" using `f x = f y` and f[THEN bspec[where x=y]] and `y\<in>t` and `t\<subseteq>s` by auto  }
+  hence "inj_on f t" unfolding inj_on_def by simp
+  hence "infinite (f ` t)" using assms(2) using finite_imageD by auto
+  moreover
+  { fix x assume "x\<in>t" "f x \<notin> g"
+    from g(3) assms(3) `x\<in>t` obtain h where "h\<in>g" and "x\<in>h" by auto
+    then obtain y where "y\<in>s" "h = f y" using g'[THEN bspec[where x=h]] by auto
+    hence "y = x" using f[THEN bspec[where x=y]] and `x\<in>t` and `x\<in>h`[unfolded `h = f y`] by auto
+    hence False using `f x \<notin> g` `h\<in>g` unfolding `h = f y` by auto  }
+  hence "f ` t \<subseteq> g" by auto
+  ultimately show False using g(2) using finite_subset by auto
+qed
+
+lemma islimpt_range_imp_convergent_subsequence:
+  fixes l :: "'a :: {t1_space, first_countable_topology}"
+  assumes l: "l islimpt (range f)"
+  shows "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+proof -
+  from first_countable_topology_class.countable_basis_at_decseq[of l] guess A . note A = this
+
+  def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
+  { fix n i
+    have "\<exists>a. i < a \<and> f a \<in> A (Suc n) - (f ` {.. i} - {l})" (is "\<exists>a. _ \<and> _ \<in> ?A")
+      apply (rule l[THEN islimptE, of "?A"])
+      using A(2) apply fastforce
+      using A(1)
+      apply (intro open_Diff finite_imp_closed)
+      apply auto
+      apply (rule_tac x=x in exI)
+      apply auto
+      done
+    then have "\<exists>a. i < a \<and> f a \<in> A (Suc n)" by blast
+    then have "i < s n i" "f (s n i) \<in> A (Suc n)"
+      unfolding s_def by (auto intro: someI2_ex) }
+  note s = this
+  def r \<equiv> "nat_rec (s 0 0) s"
+  have "subseq r"
+    by (auto simp: r_def s subseq_Suc_iff)
+  moreover
+  have "(\<lambda>n. f (r n)) ----> l"
+  proof (rule topological_tendstoI)
+    fix S assume "open S" "l \<in> S"
+    with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially" by auto
+    moreover
+    { fix i assume "Suc 0 \<le> i" then have "f (r i) \<in> A i"
+        by (cases i) (simp_all add: r_def s) }
+    then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially" by (auto simp: eventually_sequentially)
+    ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
+      by eventually_elim auto
+  qed
+  ultimately show "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+    by (auto simp: convergent_def comp_def)
+qed
+
+lemma finite_range_imp_infinite_repeats:
+  fixes f :: "nat \<Rightarrow> 'a"
+  assumes "finite (range f)"
+  shows "\<exists>k. infinite {n. f n = k}"
+proof -
+  { fix A :: "'a set" assume "finite A"
+    hence "\<And>f. infinite {n. f n \<in> A} \<Longrightarrow> \<exists>k. infinite {n. f n = k}"
+    proof (induct)
+      case empty thus ?case by simp
+    next
+      case (insert x A)
+     show ?case
+      proof (cases "finite {n. f n = x}")
+        case True
+        with `infinite {n. f n \<in> insert x A}`
+        have "infinite {n. f n \<in> A}" by simp
+        thus "\<exists>k. infinite {n. f n = k}" by (rule insert)
+      next
+        case False thus "\<exists>k. infinite {n. f n = k}" ..
+      qed
+    qed
+  } note H = this
+  from assms show "\<exists>k. infinite {n. f n = k}"
+    by (rule H) simp
+qed
+
+lemma sequence_infinite_lemma:
+  fixes f :: "nat \<Rightarrow> 'a::t1_space"
+  assumes "\<forall>n. f n \<noteq> l" and "(f ---> l) sequentially"
+  shows "infinite (range f)"
+proof
+  assume "finite (range f)"
+  hence "closed (range f)" by (rule finite_imp_closed)
+  hence "open (- range f)" by (rule open_Compl)
+  from assms(1) have "l \<in> - range f" by auto
+  from assms(2) have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
+    using `open (- range f)` `l \<in> - range f` by (rule topological_tendstoD)
+  thus False unfolding eventually_sequentially by auto
+qed
+
+lemma closure_insert:
+  fixes x :: "'a::t1_space"
+  shows "closure (insert x s) = insert x (closure s)"
+apply (rule closure_unique)
+apply (rule insert_mono [OF closure_subset])
+apply (rule closed_insert [OF closed_closure])
+apply (simp add: closure_minimal)
+done
+
+lemma islimpt_insert:
+  fixes x :: "'a::t1_space"
+  shows "x islimpt (insert a s) \<longleftrightarrow> x islimpt s"
+proof
+  assume *: "x islimpt (insert a s)"
+  show "x islimpt s"
+  proof (rule islimptI)
+    fix t assume t: "x \<in> t" "open t"
+    show "\<exists>y\<in>s. y \<in> t \<and> y \<noteq> x"
+    proof (cases "x = a")
+      case True
+      obtain y where "y \<in> insert a s" "y \<in> t" "y \<noteq> x"
+        using * t by (rule islimptE)
+      with `x = a` show ?thesis by auto
+    next
+      case False
+      with t have t': "x \<in> t - {a}" "open (t - {a})"
+        by (simp_all add: open_Diff)
+      obtain y where "y \<in> insert a s" "y \<in> t - {a}" "y \<noteq> x"
+        using * t' by (rule islimptE)
+      thus ?thesis by auto
+    qed
+  qed
+next
+  assume "x islimpt s" thus "x islimpt (insert a s)"
+    by (rule islimpt_subset) auto
+qed
+
+lemma islimpt_union_finite:
+  fixes x :: "'a::t1_space"
+  shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
+by (induct set: finite, simp_all add: islimpt_insert)
+ 
+lemma sequence_unique_limpt:
+  fixes f :: "nat \<Rightarrow> 'a::t2_space"
+  assumes "(f ---> l) sequentially" and "l' islimpt (range f)"
+  shows "l' = l"
+proof (rule ccontr)
+  assume "l' \<noteq> l"
+  obtain s t where "open s" "open t" "l' \<in> s" "l \<in> t" "s \<inter> t = {}"
+    using hausdorff [OF `l' \<noteq> l`] by auto
+  have "eventually (\<lambda>n. f n \<in> t) sequentially"
+    using assms(1) `open t` `l \<in> t` by (rule topological_tendstoD)
+  then obtain N where "\<forall>n\<ge>N. f n \<in> t"
+    unfolding eventually_sequentially by auto
+
+  have "UNIV = {..<N} \<union> {N..}" by auto
+  hence "l' islimpt (f ` ({..<N} \<union> {N..}))" using assms(2) by simp
+  hence "l' islimpt (f ` {..<N} \<union> f ` {N..})" by (simp add: image_Un)
+  hence "l' islimpt (f ` {N..})" by (simp add: islimpt_union_finite)
+  then obtain y where "y \<in> f ` {N..}" "y \<in> s" "y \<noteq> l'"
+    using `l' \<in> s` `open s` by (rule islimptE)
+  then obtain n where "N \<le> n" "f n \<in> s" "f n \<noteq> l'" by auto
+  with `\<forall>n\<ge>N. f n \<in> t` have "f n \<in> s \<inter> t" by simp
+  with `s \<inter> t = {}` show False by simp
+qed
+
+lemma bolzano_weierstrass_imp_closed:
+  fixes s :: "'a::{first_countable_topology, t2_space} set"
+  assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
+  shows "closed s"
+proof-
+  { fix x l assume as: "\<forall>n::nat. x n \<in> s" "(x ---> l) sequentially"
+    hence "l \<in> s"
+    proof(cases "\<forall>n. x n \<noteq> l")
+      case False thus "l\<in>s" using as(1) by auto
+    next
+      case True note cas = this
+      with as(2) have "infinite (range x)" using sequence_infinite_lemma[of x l] by auto
+      then obtain l' where "l'\<in>s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] 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 fast
+qed
+
+lemma compact_imp_closed:
+  fixes s :: "'a::{first_countable_topology, t2_space} set"
+  shows "compact s \<Longrightarrow> closed 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 "closed s"
+    by (rule bolzano_weierstrass_imp_closed)
+qed
+
+text{* In particular, some common special cases. *}
+
+lemma compact_empty[simp]:
+ "compact {}"
+  unfolding compact_eq_heine_borel
+  by auto
+
+lemma compact_union [intro]:
+  assumes "compact s" "compact t" shows " compact (s \<union> t)"
+  unfolding compact_eq_heine_borel
+proof (intro allI impI)
+  fix f assume *: "Ball f open \<and> s \<union> t \<subseteq> \<Union>f"
+  from * `compact s` obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
+    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
+  moreover from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
+    unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
+  ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
+    by (auto intro!: exI[of _ "s' \<union> t'"])
+qed
+
+lemma compact_Union [intro]: "finite S \<Longrightarrow> (\<And>T. T \<in> S \<Longrightarrow> compact T) \<Longrightarrow> compact (\<Union>S)"
+  by (induct set: finite) auto
+
+lemma compact_UN [intro]:
+  "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
+  unfolding SUP_def by (rule compact_Union) auto
+
+lemma compact_inter_closed [intro]:
+  assumes "compact s" and "closed t"
+  shows "compact (s \<inter> t)"
+  unfolding compact_eq_heine_borel
+proof safe
+  fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
+  from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
+  moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
+  ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
+    using `compact s` unfolding compact_eq_heine_borel by auto
+  then guess D ..
+  then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
+    by (intro exI[of _ "D - {-t}"]) auto
+qed
+
+lemma closed_inter_compact [intro]:
+  assumes "closed s" and "compact t"
+  shows "compact (s \<inter> t)"
+  using compact_inter_closed [of t s] assms
+  by (simp add: Int_commute)
+
+lemma compact_inter [intro]:
+  fixes s t :: "'a :: {t2_space, first_countable_topology} set"
+  assumes "compact s" and "compact t"
+  shows "compact (s \<inter> t)"
+  using assms by (intro compact_inter_closed compact_imp_closed)
+
+lemma compact_sing [simp]: "compact {a}"
+  unfolding compact_eq_heine_borel by auto
+
+lemma compact_insert [simp]:
+  assumes "compact s" shows "compact (insert x s)"
+proof -
+  have "compact ({x} \<union> s)"
+    using compact_sing assms by (rule compact_union)
+  thus ?thesis by simp
+qed
+
+lemma finite_imp_compact:
+  shows "finite s \<Longrightarrow> compact s"
+  by (induct set: finite) simp_all
+
+lemma open_delete:
+  fixes s :: "'a::t1_space set"
+  shows "open s \<Longrightarrow> open (s - {x})"
+  by (simp add: open_Diff)
+
+text{* Finite intersection property *}
+
+lemma inj_setminus: "inj_on uminus (A::'a set set)"
+  by (auto simp: inj_on_def)
+
+lemma compact_fip:
+  "compact U \<longleftrightarrow>
+    (\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})"
+  (is "_ \<longleftrightarrow> ?R")
+proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
+  fix A assume "compact U" and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
+    and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
+  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>uminus`A"
+    by auto
+  with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
+    unfolding compact_eq_heine_borel by (metis subset_image_iff)
+  with fi[THEN spec, of B] show False
+    by (auto dest: finite_imageD intro: inj_setminus)
+next
+  fix A assume ?R and cover: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
+  from cover have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
+    by auto
+  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>uminus`B = {}"
+    by (metis subset_image_iff)
+  then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
+    by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
+qed
+
+lemma compact_imp_fip:
+  "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter> f') \<noteq> {}) \<Longrightarrow>
+    s \<inter> (\<Inter> f) \<noteq> {}"
+  unfolding compact_fip by auto
+
+text{*Compactness expressed with filters*}
+
+definition "filter_from_subbase B = Abs_filter (\<lambda>P. \<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
+
+lemma eventually_filter_from_subbase:
+  "eventually P (filter_from_subbase B) \<longleftrightarrow> (\<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
+    (is "_ \<longleftrightarrow> ?R P")
+  unfolding filter_from_subbase_def
+proof (rule eventually_Abs_filter is_filter.intro)+
+  show "?R (\<lambda>x. True)"
+    by (rule exI[of _ "{}"]) (simp add: le_fun_def)
+next
+  fix P Q assume "?R P" then guess X ..
+  moreover assume "?R Q" then guess Y ..
+  ultimately show "?R (\<lambda>x. P x \<and> Q x)"
+    by (intro exI[of _ "X \<union> Y"]) auto
+next
+  fix P Q
+  assume "?R P" then guess X ..
+  moreover assume "\<forall>x. P x \<longrightarrow> Q x"
+  ultimately show "?R Q"
+    by (intro exI[of _ X]) auto
+qed
+
+lemma eventually_filter_from_subbaseI: "P \<in> B \<Longrightarrow> eventually P (filter_from_subbase B)"
+  by (subst eventually_filter_from_subbase) (auto intro!: exI[of _ "{P}"])
+
+lemma filter_from_subbase_not_bot:
+  "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot"
+  unfolding trivial_limit_def eventually_filter_from_subbase by auto
+
+lemma closure_iff_nhds_not_empty:
+  "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"
+proof safe
+  assume x: "x \<in> closure X"
+  fix S A assume "open S" "x \<in> S" "X \<inter> A = {}" "S \<subseteq> A"
+  then have "x \<notin> closure (-S)" 
+    by (auto simp: closure_complement subset_eq[symmetric] intro: interiorI)
+  with x have "x \<in> closure X - closure (-S)"
+    by auto
+  also have "\<dots> \<subseteq> closure (X \<inter> S)"
+    using `open S` open_inter_closure_subset[of S X] by (simp add: closed_Compl ac_simps)
+  finally have "X \<inter> S \<noteq> {}" by auto
+  then show False using `X \<inter> A = {}` `S \<subseteq> A` by auto
+next
+  assume "\<forall>A S. S \<subseteq> A \<longrightarrow> open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {}"
+  from this[THEN spec, of "- X", THEN spec, of "- closure X"]
+  show "x \<in> closure X"
+    by (simp add: closure_subset open_Compl)
+qed
+
+lemma compact_filter:
+  "compact U \<longleftrightarrow> (\<forall>F. F \<noteq> bot \<longrightarrow> eventually (\<lambda>x. x \<in> U) F \<longrightarrow> (\<exists>x\<in>U. inf (nhds x) F \<noteq> bot))"
+proof (intro allI iffI impI compact_fip[THEN iffD2] notI)
+  fix F assume "compact U" and F: "F \<noteq> bot" "eventually (\<lambda>x. x \<in> U) F"
+  from F have "U \<noteq> {}"
+    by (auto simp: eventually_False)
+
+  def Z \<equiv> "closure ` {A. eventually (\<lambda>x. x \<in> A) F}"
+  then have "\<forall>z\<in>Z. closed z"
+    by auto
+  moreover 
+  have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
+    unfolding Z_def by (auto elim: eventually_elim1 intro: set_mp[OF closure_subset])
+  have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
+  proof (intro allI impI)
+    fix B assume "finite B" "B \<subseteq> Z"
+    with `finite B` ev_Z have "eventually (\<lambda>x. \<forall>b\<in>B. x \<in> b) F"
+      by (auto intro!: eventually_Ball_finite)
+    with F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
+      by eventually_elim auto
+    with F show "U \<inter> \<Inter>B \<noteq> {}"
+      by (intro notI) (simp add: eventually_False)
+  qed
+  ultimately have "U \<inter> \<Inter>Z \<noteq> {}"
+    using `compact U` unfolding compact_fip by blast
+  then obtain x where "x \<in> U" and x: "\<And>z. z \<in> Z \<Longrightarrow> x \<in> z" by auto
+
+  have "\<And>P. eventually P (inf (nhds x) F) \<Longrightarrow> P \<noteq> bot"
+    unfolding eventually_inf eventually_nhds
+  proof safe
+    fix P Q R S
+    assume "eventually R F" "open S" "x \<in> S"
+    with open_inter_closure_eq_empty[of S "{x. R x}"] x[of "closure {x. R x}"]
+    have "S \<inter> {x. R x} \<noteq> {}" by (auto simp: Z_def)
+    moreover assume "Ball S Q" "\<forall>x. Q x \<and> R x \<longrightarrow> bot x"
+    ultimately show False by (auto simp: set_eq_iff)
+  qed
+  with `x \<in> U` show "\<exists>x\<in>U. inf (nhds x) F \<noteq> bot"
+    by (metis eventually_bot)
+next
+  fix A assume A: "\<forall>a\<in>A. closed a" "\<forall>B\<subseteq>A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" "U \<inter> \<Inter>A = {}"
+
+  def P' \<equiv> "(\<lambda>a (x::'a). x \<in> a)"
+  then have inj_P': "\<And>A. inj_on P' A"
+    by (auto intro!: inj_onI simp: fun_eq_iff)
+  def F \<equiv> "filter_from_subbase (P' ` insert U A)"
+  have "F \<noteq> bot"
+    unfolding F_def
+  proof (safe intro!: filter_from_subbase_not_bot)
+    fix X assume "X \<subseteq> P' ` insert U A" "finite X" "Inf X = bot"
+    then obtain B where "B \<subseteq> insert U A" "finite B" and B: "Inf (P' ` B) = bot"
+      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD)
+    with A(2)[THEN spec, of "B - {U}"] have "U \<inter> \<Inter>(B - {U}) \<noteq> {}" by auto
+    with B show False by (auto simp: P'_def fun_eq_iff)
+  qed
+  moreover have "eventually (\<lambda>x. x \<in> U) F"
+    unfolding F_def by (rule eventually_filter_from_subbaseI) (auto simp: P'_def)
+  moreover assume "\<forall>F. F \<noteq> bot \<longrightarrow> eventually (\<lambda>x. x \<in> U) F \<longrightarrow> (\<exists>x\<in>U. inf (nhds x) F \<noteq> bot)"
+  ultimately obtain x where "x \<in> U" and x: "inf (nhds x) F \<noteq> bot"
+    by auto
+
+  { fix V assume "V \<in> A"
+    then have V: "eventually (\<lambda>x. x \<in> V) F"
+      by (auto simp add: F_def image_iff P'_def intro!: eventually_filter_from_subbaseI)
+    have "x \<in> closure V"
+      unfolding closure_iff_nhds_not_empty
+    proof (intro impI allI)
+      fix S A assume "open S" "x \<in> S" "S \<subseteq> A"
+      then have "eventually (\<lambda>x. x \<in> A) (nhds x)" by (auto simp: eventually_nhds)
+      with V have "eventually (\<lambda>x. x \<in> V \<inter> A) (inf (nhds x) F)"
+        by (auto simp: eventually_inf)
+      with x show "V \<inter> A \<noteq> {}"
+        by (auto simp del: Int_iff simp add: trivial_limit_def)
+    qed
+    then have "x \<in> V"
+      using `V \<in> A` A(1) by simp }
+  with `x\<in>U` have "x \<in> U \<inter> \<Inter>A" by auto
+  with `U \<inter> \<Inter>A = {}` show False by auto
+qed
+
+lemma countable_compact:
+  fixes U :: "'a :: second_countable_topology set"
+  shows "compact U \<longleftrightarrow>
+    (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
+proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
+  fix A assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
+  assume *: "\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T)"
+  def B \<equiv> "SOME B::'a set set. countable B \<and> topological_basis B"
+  then have B: "countable B" "topological_basis B"
+    by (auto simp: countable_basis is_basis)
+
+  moreover def C \<equiv> "{b\<in>B. \<exists>a\<in>A. b \<subseteq> a}"
+  ultimately have "countable C" "\<forall>a\<in>C. open a"
+    unfolding C_def by (auto simp: topological_basis_open)
+  moreover
+  have "\<Union>A \<subseteq> \<Union>C"
+  proof safe
+    fix x a assume "x \<in> a" "a \<in> A"
+    with topological_basisE[of B a x] B A
+    obtain b where "x \<in> b" "b \<in> B" "b \<subseteq> a" by metis
+    with `a \<in> A` show "x \<in> \<Union>C" unfolding C_def by auto
+  qed
+  then have "U \<subseteq> \<Union>C" using `U \<subseteq> \<Union>A` by auto
+  ultimately obtain T where "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
+    using * by metis
+  moreover then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<subseteq> a"
+    by (auto simp: C_def)
+  then guess f unfolding bchoice_iff Bex_def ..
+  ultimately show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
+    unfolding C_def by (intro exI[of _ "f`T"]) fastforce
+qed (auto simp: compact_eq_heine_borel)
 
 subsubsection{* Sequential compactness *}
 
 definition
-  compact :: "'a::metric_space set \<Rightarrow> bool" where (* TODO: generalize *)
-  "compact S \<longleftrightarrow>
+  seq_compact :: "'a::topological_space set \<Rightarrow> bool" where
+  "seq_compact S \<longleftrightarrow>
    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow>
        (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially))"
 
-lemma compactI:
+lemma seq_compact_imp_compact:
+  fixes U :: "'a :: second_countable_topology set"
+  assumes "seq_compact U"
+  shows "compact U"
+  unfolding countable_compact
+proof safe
+  fix A assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
+  have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> subseq r \<and> (X \<circ> r) ----> x"
+    using `seq_compact U` by (fastforce simp: seq_compact_def subset_eq)
+  show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
+  proof cases
+    assume "finite A" with A show ?thesis by auto
+  next
+    assume "infinite A"
+    then have "A \<noteq> {}" by auto
+    show ?thesis
+    proof (rule ccontr)
+      assume "\<not> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T)"
+      then have "\<forall>T. \<exists>x. T \<subseteq> A \<and> finite T \<longrightarrow> (x \<in> U - \<Union>T)" by auto
+      then obtain X' where T: "\<And>T. T \<subseteq> A \<Longrightarrow> finite T \<Longrightarrow> X' T \<in> U - \<Union>T" by metis
+      def X \<equiv> "\<lambda>n. X' (from_nat_into A ` {.. n})"
+      have X: "\<And>n. X n \<in> U - (\<Union>i\<le>n. from_nat_into A i)"
+        using `A \<noteq> {}` unfolding X_def SUP_def by (intro T) (auto intro: from_nat_into)
+      then have "range X \<subseteq> U" by auto
+      with subseq[of X] obtain r x where "x \<in> U" and r: "subseq r" "(X \<circ> r) ----> x" by auto
+      from `x\<in>U` `U \<subseteq> \<Union>A` from_nat_into_surj[OF `countable A`]
+      obtain n where "x \<in> from_nat_into A n" by auto
+      with r(2) A(1) from_nat_into[OF `A \<noteq> {}`, of n]
+      have "eventually (\<lambda>i. X (r i) \<in> from_nat_into A n) sequentially"
+        unfolding tendsto_def by (auto simp: comp_def)
+      then obtain N where "\<And>i. N \<le> i \<Longrightarrow> X (r i) \<in> from_nat_into A n"
+        by (auto simp: eventually_sequentially)
+      moreover from X have "\<And>i. n \<le> r i \<Longrightarrow> X (r i) \<notin> from_nat_into A n"
+        by auto
+      moreover from `subseq r`[THEN seq_suble, of "max n N"] have "\<exists>i. n \<le> r i \<and> N \<le> i"
+        by (auto intro!: exI[of _ "max n N"])
+      ultimately show False
+        by auto
+    qed
+  qed
+qed
+
+lemma compact_imp_seq_compact:
+  fixes U :: "'a :: first_countable_topology set"
+  assumes "compact U" shows "seq_compact U"
+  unfolding seq_compact_def
+proof safe
+  fix X :: "nat \<Rightarrow> 'a" assume "\<forall>n. X n \<in> U"
+  then have "eventually (\<lambda>x. x \<in> U) (filtermap X sequentially)"
+    by (auto simp: eventually_filtermap)
+  moreover have "filtermap X sequentially \<noteq> bot"
+    by (simp add: trivial_limit_def eventually_filtermap)
+  ultimately obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
+    using `compact U` by (auto simp: compact_filter)
+
+  from countable_basis_at_decseq[of x] guess A . note A = this
+  def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> X j \<in> A (Suc n)"
+  { fix n i
+    have "\<exists>a. i < a \<and> X a \<in> A (Suc n)"
+    proof (rule ccontr)
+      assume "\<not> (\<exists>a>i. X a \<in> A (Suc n))"
+      then have "\<And>a. Suc i \<le> a \<Longrightarrow> X a \<notin> A (Suc n)" by auto
+      then have "eventually (\<lambda>x. x \<notin> A (Suc n)) (filtermap X sequentially)"
+        by (auto simp: eventually_filtermap eventually_sequentially)
+      moreover have "eventually (\<lambda>x. x \<in> A (Suc n)) (nhds x)"
+        using A(1,2)[of "Suc n"] by (auto simp: eventually_nhds)
+      ultimately have "eventually (\<lambda>x. False) ?F"
+        by (auto simp add: eventually_inf)
+      with x show False
+        by (simp add: eventually_False)
+    qed
+    then have "i < s n i" "X (s n i) \<in> A (Suc n)"
+      unfolding s_def by (auto intro: someI2_ex) }
+  note s = this
+  def r \<equiv> "nat_rec (s 0 0) s"
+  have "subseq r"
+    by (auto simp: r_def s subseq_Suc_iff)
+  moreover
+  have "(\<lambda>n. X (r n)) ----> x"
+  proof (rule topological_tendstoI)
+    fix S assume "open S" "x \<in> S"
+    with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially" by auto
+    moreover
+    { fix i assume "Suc 0 \<le> i" then have "X (r i) \<in> A i"
+        by (cases i) (simp_all add: r_def s) }
+    then have "eventually (\<lambda>i. X (r i) \<in> A i) sequentially" by (auto simp: eventually_sequentially)
+    ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
+      by eventually_elim auto
+  qed
+  ultimately show "\<exists>x \<in> U. \<exists>r. subseq r \<and> (X \<circ> r) ----> x"
+    using `x \<in> U` by (auto simp: convergent_def comp_def)
+qed
+
+lemma seq_compact_eq_compact:
+  fixes U :: "'a :: second_countable_topology set"
+  shows "seq_compact U \<longleftrightarrow> compact U"
+  using compact_imp_seq_compact seq_compact_imp_compact by blast
+
+lemma seq_compactI:
   assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially"
-  shows "compact S"
-  unfolding compact_def using assms by fast
-
-lemma compactE:
-  assumes "compact S" "\<forall>n. f n \<in> S"
+  shows "seq_compact S"
+  unfolding seq_compact_def using assms by fast
+
+lemma seq_compactE:
+  assumes "seq_compact S" "\<forall>n. f n \<in> S"
   obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
-  using assms unfolding compact_def by fast
+  using assms unfolding seq_compact_def by fast
+
+lemma bolzano_weierstrass_imp_seq_compact:
+  fixes s :: "'a::{t1_space, first_countable_topology} set"
+  assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
+  shows "seq_compact s"
+proof -
+  { fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
+    have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+    proof (cases "finite (range f)")
+      case True
+      hence "\<exists>l. infinite {n. f n = l}"
+        by (rule finite_range_imp_infinite_repeats)
+      then obtain l where "infinite {n. f n = l}" ..
+      hence "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> {n. f n = l})"
+        by (rule infinite_enumerate)
+      then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = l" by auto
+      hence "subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+        unfolding o_def by (simp add: fr tendsto_const)
+      hence "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+        by - (rule exI)
+      from f have "\<forall>n. f (r n) \<in> s" by simp
+      hence "l \<in> s" by (simp add: fr)
+      thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+        by (rule rev_bexI) fact
+    next
+      case False
+      with f assms have "\<exists>x\<in>s. x islimpt (range f)" by auto
+      then obtain l where "l \<in> s" "l islimpt (range f)" ..
+      have "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+        using `l islimpt (range f)`
+        by (rule islimpt_range_imp_convergent_subsequence)
+      with `l \<in> s` show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" ..
+    qed
+  }
+  thus ?thesis unfolding seq_compact_def by auto
+qed
 
 text {*
   A metric space (or topological vector space) is said to have the
@@ -2252,10 +2987,10 @@
     "bounded s \<Longrightarrow> \<forall>n. f n \<in> s
       \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
 
-lemma bounded_closed_imp_compact:
+lemma bounded_closed_imp_seq_compact:
   fixes s::"'a::heine_borel set"
-  assumes "bounded s" and "closed s" shows "compact s"
-proof (unfold compact_def, clarify)
+  assumes "bounded s" and "closed s" shows "seq_compact s"
+proof (unfold seq_compact_def, clarify)
   fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
   obtain l r where r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
     using bounded_imp_convergent_subsequence [OF `bounded s` `\<forall>n. f n \<in> s`] by auto
@@ -2537,10 +3272,10 @@
     apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto
 qed
 
-lemma compact_imp_complete: assumes "compact s" shows "complete s"
+lemma seq_compact_imp_complete: assumes "seq_compact s" shows "complete s"
 proof-
   { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
-    from as(1) obtain l r where lr: "l\<in>s" "subseq r" "((f \<circ> r) ---> l) sequentially" using assms unfolding compact_def by blast
+    from as(1) obtain l r where lr: "l\<in>s" "subseq r" "((f \<circ> r) ---> l) sequentially" using assms unfolding seq_compact_def by blast
 
     note lr' = subseq_bigger [OF lr(2)]
 
@@ -2562,10 +3297,10 @@
   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
   hence "bounded (range f)"
     by (rule cauchy_imp_bounded)
-  hence "compact (closure (range f))"
-    using bounded_closed_imp_compact [of "closure (range f)"] by auto
+  hence "seq_compact (closure (range f))"
+    using bounded_closed_imp_seq_compact [of "closure (range f)"] by auto
   hence "complete (closure (range f))"
-    by (rule compact_imp_complete)
+    by (rule seq_compact_imp_complete)
   moreover have "\<forall>n. f n \<in> closure (range f)"
     using closure_subset [of "range f"] by auto
   ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
@@ -2624,8 +3359,8 @@
   "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
 declare helper_1.simps[simp del]
 
-lemma compact_imp_totally_bounded:
-  assumes "compact s"
+lemma seq_compact_imp_totally_bounded:
+  assumes "seq_compact s"
   shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
 proof(rule, rule, rule ccontr)
   fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k)"
@@ -2642,7 +3377,7 @@
       thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" unfolding Q_def by auto
     qed }
   hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
-  then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded compact_def, THEN spec[where x=x]] by auto
+  then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
   from this(3) have "Cauchy (x \<circ> r)" using convergent_imp_cauchy by auto
   then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto
   show False
@@ -2656,7 +3391,7 @@
 text {* Following Burkill \& Burkill vol. 2. *}
 
 lemma heine_borel_lemma: fixes s::"'a::metric_space set"
-  assumes "compact s"  "s \<subseteq> (\<Union> t)"  "\<forall>b \<in> t. open b"
+  assumes "seq_compact s"  "s \<subseteq> (\<Union> t)"  "\<forall>b \<in> t. open b"
   shows "\<exists>e>0. \<forall>x \<in> s. \<exists>b \<in> t. ball x e \<subseteq> b"
 proof(rule ccontr)
   assume "\<not> (\<exists>e>0. \<forall>x\<in>s. \<exists>b\<in>t. ball x e \<subseteq> b)"
@@ -2669,7 +3404,7 @@
     using choice[of "\<lambda>n::nat. \<lambda>x. x\<in>s \<and> (\<forall>xa\<in>t. \<not> ball x (inverse (real (n + 1))) \<subseteq> xa)"] by auto
 
   then obtain l r where l:"l\<in>s" and r:"subseq r" and lr:"((f \<circ> r) ---> l) sequentially"
-    using assms(1)[unfolded compact_def, THEN spec[where x=f]] by auto
+    using assms(1)[unfolded seq_compact_def, THEN spec[where x=f]] by auto
 
   obtain b where "l\<in>b" "b\<in>t" using assms(2) and l by auto
   then obtain e where "e>0" and e:"\<forall>z. dist z l < e \<longrightarrow> z\<in>b"
@@ -2695,16 +3430,19 @@
   thus False using e and `y\<notin>b` by auto
 qed
 
-lemma compact_imp_heine_borel: "compact s ==> (\<forall>f. (\<forall>t \<in> f. open t) \<and> s \<subseteq> (\<Union> f)
-               \<longrightarrow> (\<exists>f'. f' \<subseteq> f \<and> finite f' \<and> s \<subseteq> (\<Union> f')))"
+lemma seq_compact_imp_heine_borel:
+  fixes s :: "'a :: metric_space set"
+  shows "seq_compact s \<Longrightarrow> compact s"
+  unfolding compact_eq_heine_borel
 proof clarify
-  fix f assume "compact s" " \<forall>t\<in>f. open t" "s \<subseteq> \<Union>f"
+  fix f assume "seq_compact s" " \<forall>t\<in>f. open t" "s \<subseteq> \<Union>f"
   then obtain e::real where "e>0" and "\<forall>x\<in>s. \<exists>b\<in>f. ball x e \<subseteq> b" using heine_borel_lemma[of s f] by auto
   hence "\<forall>x\<in>s. \<exists>b. b\<in>f \<and> ball x e \<subseteq> b" by auto
   hence "\<exists>bb. \<forall>x\<in>s. bb x \<in>f \<and> ball x e \<subseteq> bb x" using bchoice[of s "\<lambda>x b. b\<in>f \<and> ball x e \<subseteq> b"] by auto
   then obtain  bb where bb:"\<forall>x\<in>s. (bb x) \<in> f \<and> ball x e \<subseteq> (bb x)" by blast
 
-  from `compact s` have  "\<exists> k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" using compact_imp_totally_bounded[of s] `e>0` by auto
+  from `seq_compact s` have  "\<exists> k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
+    using seq_compact_imp_totally_bounded[of s] `e>0` by auto
   then obtain k where k:"finite k" "k \<subseteq> s" "s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" by auto
 
   have "finite (bb ` k)" using k(1) by auto
@@ -2717,169 +3455,8 @@
   ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f'" using bb k(2) by (rule_tac x="bb ` k" in exI) auto
 qed
 
-subsubsection {* Bolzano-Weierstrass property *}
-
-lemma heine_borel_imp_bolzano_weierstrass:
-  assumes "\<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'))"
-          "infinite t"  "t \<subseteq> s"
-  shows "\<exists>x \<in> s. x islimpt t"
-proof(rule ccontr)
-  assume "\<not> (\<exists>x \<in> s. x islimpt t)"
-  then obtain f where f:"\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)" unfolding islimpt_def
-    using bchoice[of s "\<lambda> x T. x \<in> T \<and> open T \<and> (\<forall>y\<in>t. y \<in> T \<longrightarrow> y = x)"] by auto
-  obtain g where g:"g\<subseteq>{t. \<exists>x. x \<in> s \<and> t = f x}" "finite g" "s \<subseteq> \<Union>g"
-    using assms(1)[THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]] using f by auto
-  from g(1,3) have g':"\<forall>x\<in>g. \<exists>xa \<in> s. x = f xa" by auto
-  { fix x y assume "x\<in>t" "y\<in>t" "f x = f y"
-    hence "x \<in> f x"  "y \<in> f x \<longrightarrow> y = x" using f[THEN bspec[where x=x]] and `t\<subseteq>s` by auto
-    hence "x = y" using `f x = f y` and f[THEN bspec[where x=y]] and `y\<in>t` and `t\<subseteq>s` by auto  }
-  hence "inj_on f t" unfolding inj_on_def by simp
-  hence "infinite (f ` t)" using assms(2) using finite_imageD by auto
-  moreover
-  { fix x assume "x\<in>t" "f x \<notin> g"
-    from g(3) assms(3) `x\<in>t` obtain h where "h\<in>g" and "x\<in>h" by auto
-    then obtain y where "y\<in>s" "h = f y" using g'[THEN bspec[where x=h]] by auto
-    hence "y = x" using f[THEN bspec[where x=y]] and `x\<in>t` and `x\<in>h`[unfolded `h = f y`] by auto
-    hence False using `f x \<notin> g` `h\<in>g` unfolding `h = f y` by auto  }
-  hence "f ` t \<subseteq> g" by auto
-  ultimately show False using g(2) using finite_subset by auto
-qed
-
 subsubsection {* Complete the chain of compactness variants *}
 
-lemma islimpt_range_imp_convergent_subsequence:
-  fixes f :: "nat \<Rightarrow> 'a::metric_space"
-  assumes "l islimpt (range f)"
-  shows "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-proof (intro exI conjI)
-  have *: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. 0 < dist (f n) l \<and> dist (f n) l < e"
-    using assms unfolding islimpt_def
-    by (drule_tac x="ball l e" in spec)
-       (auto simp add: zero_less_dist_iff dist_commute)
-
-  def t \<equiv> "\<lambda>e. LEAST n. 0 < dist (f n) l \<and> dist (f n) l < e"
-  have f_t_neq: "\<And>e. 0 < e \<Longrightarrow> 0 < dist (f (t e)) l"
-    unfolding t_def by (rule LeastI2_ex [OF * conjunct1])
-  have f_t_closer: "\<And>e. 0 < e \<Longrightarrow> dist (f (t e)) l < e"
-    unfolding t_def by (rule LeastI2_ex [OF * conjunct2])
-  have t_le: "\<And>n e. 0 < dist (f n) l \<Longrightarrow> dist (f n) l < e \<Longrightarrow> t e \<le> n"
-    unfolding t_def by (simp add: Least_le)
-  have less_tD: "\<And>n e. n < t e \<Longrightarrow> 0 < dist (f n) l \<Longrightarrow> e \<le> dist (f n) l"
-    unfolding t_def by (drule not_less_Least) simp
-  have t_antimono: "\<And>e e'. 0 < e \<Longrightarrow> e \<le> e' \<Longrightarrow> t e' \<le> t e"
-    apply (rule t_le)
-    apply (erule f_t_neq)
-    apply (erule (1) less_le_trans [OF f_t_closer])
-    done
-  have t_dist_f_neq: "\<And>n. 0 < dist (f n) l \<Longrightarrow> t (dist (f n) l) \<noteq> n"
-    by (drule f_t_closer) auto
-  have t_less: "\<And>e. 0 < e \<Longrightarrow> t e < t (dist (f (t e)) l)"
-    apply (subst less_le)
-    apply (rule conjI)
-    apply (rule t_antimono)
-    apply (erule f_t_neq)
-    apply (erule f_t_closer [THEN less_imp_le])
-    apply (rule t_dist_f_neq [symmetric])
-    apply (erule f_t_neq)
-    done
-  have dist_f_t_less':
-    "\<And>e e'. 0 < e \<Longrightarrow> 0 < e' \<Longrightarrow> t e \<le> t e' \<Longrightarrow> dist (f (t e')) l < e"
-    apply (simp add: le_less)
-    apply (erule disjE)
-    apply (rule less_trans)
-    apply (erule f_t_closer)
-    apply (rule le_less_trans)
-    apply (erule less_tD)
-    apply (erule f_t_neq)
-    apply (erule f_t_closer)
-    apply (erule subst)
-    apply (erule f_t_closer)
-    done
-
-  def r \<equiv> "nat_rec (t 1) (\<lambda>_ x. t (dist (f x) l))"
-  have r_simps: "r 0 = t 1" "\<And>n. r (Suc n) = t (dist (f (r n)) l)"
-    unfolding r_def by simp_all
-  have f_r_neq: "\<And>n. 0 < dist (f (r n)) l"
-    by (induct_tac n) (simp_all add: r_simps f_t_neq)
-
-  show "subseq r"
-    unfolding subseq_Suc_iff
-    apply (rule allI)
-    apply (case_tac n)
-    apply (simp_all add: r_simps)
-    apply (rule t_less, rule zero_less_one)
-    apply (rule t_less, rule f_r_neq)
-    done
-  show "((f \<circ> r) ---> l) sequentially"
-    unfolding LIMSEQ_def o_def
-    apply (clarify, rename_tac e, rule_tac x="t e" in exI, clarify)
-    apply (drule le_trans, rule seq_suble [OF `subseq r`])
-    apply (case_tac n, simp_all add: r_simps dist_f_t_less' f_r_neq)
-    done
-qed
-
-lemma finite_range_imp_infinite_repeats:
-  fixes f :: "nat \<Rightarrow> 'a"
-  assumes "finite (range f)"
-  shows "\<exists>k. infinite {n. f n = k}"
-proof -
-  { fix A :: "'a set" assume "finite A"
-    hence "\<And>f. infinite {n. f n \<in> A} \<Longrightarrow> \<exists>k. infinite {n. f n = k}"
-    proof (induct)
-      case empty thus ?case by simp
-    next
-      case (insert x A)
-     show ?case
-      proof (cases "finite {n. f n = x}")
-        case True
-        with `infinite {n. f n \<in> insert x A}`
-        have "infinite {n. f n \<in> A}" by simp
-        thus "\<exists>k. infinite {n. f n = k}" by (rule insert)
-      next
-        case False thus "\<exists>k. infinite {n. f n = k}" ..
-      qed
-    qed
-  } note H = this
-  from assms show "\<exists>k. infinite {n. f n = k}"
-    by (rule H) simp
-qed
-
-lemma bolzano_weierstrass_imp_compact:
-  fixes s :: "'a::metric_space set"
-  assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
-  shows "compact s"
-proof -
-  { fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
-    have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-    proof (cases "finite (range f)")
-      case True
-      hence "\<exists>l. infinite {n. f n = l}"
-        by (rule finite_range_imp_infinite_repeats)
-      then obtain l where "infinite {n. f n = l}" ..
-      hence "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> {n. f n = l})"
-        by (rule infinite_enumerate)
-      then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = l" by auto
-      hence "subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-        unfolding o_def by (simp add: fr tendsto_const)
-      hence "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-        by - (rule exI)
-      from f have "\<forall>n. f (r n) \<in> s" by simp
-      hence "l \<in> s" by (simp add: fr)
-      thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-        by (rule rev_bexI) fact
-    next
-      case False
-      with f assms have "\<exists>x\<in>s. x islimpt (range f)" by auto
-      then obtain l where "l \<in> s" "l islimpt (range f)" ..
-      have "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-        using `l islimpt (range f)`
-        by (rule islimpt_range_imp_convergent_subsequence)
-      with `l \<in> s` show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" ..
-    qed
-  }
-  thus ?thesis unfolding compact_def by auto
-qed
-
 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 )"
@@ -2944,127 +3521,26 @@
   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
 
-lemma sequence_infinite_lemma:
-  fixes f :: "nat \<Rightarrow> 'a::t1_space"
-  assumes "\<forall>n. f n \<noteq> l" and "(f ---> l) sequentially"
-  shows "infinite (range f)"
-proof
-  assume "finite (range f)"
-  hence "closed (range f)" by (rule finite_imp_closed)
-  hence "open (- range f)" by (rule open_Compl)
-  from assms(1) have "l \<in> - range f" by auto
-  from assms(2) have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
-    using `open (- range f)` `l \<in> - range f` by (rule topological_tendstoD)
-  thus False unfolding eventually_sequentially by auto
-qed
-
-lemma closure_insert:
-  fixes x :: "'a::t1_space"
-  shows "closure (insert x s) = insert x (closure s)"
-apply (rule closure_unique)
-apply (rule insert_mono [OF closure_subset])
-apply (rule closed_insert [OF closed_closure])
-apply (simp add: closure_minimal)
-done
-
-lemma islimpt_insert:
-  fixes x :: "'a::t1_space"
-  shows "x islimpt (insert a s) \<longleftrightarrow> x islimpt s"
-proof
-  assume *: "x islimpt (insert a s)"
-  show "x islimpt s"
-  proof (rule islimptI)
-    fix t assume t: "x \<in> t" "open t"
-    show "\<exists>y\<in>s. y \<in> t \<and> y \<noteq> x"
-    proof (cases "x = a")
-      case True
-      obtain y where "y \<in> insert a s" "y \<in> t" "y \<noteq> x"
-        using * t by (rule islimptE)
-      with `x = a` show ?thesis by auto
-    next
-      case False
-      with t have t': "x \<in> t - {a}" "open (t - {a})"
-        by (simp_all add: open_Diff)
-      obtain y where "y \<in> insert a s" "y \<in> t - {a}" "y \<noteq> x"
-        using * t' by (rule islimptE)
-      thus ?thesis by auto
-    qed
-  qed
-next
-  assume "x islimpt s" thus "x islimpt (insert a s)"
-    by (rule islimpt_subset) auto
-qed
-
-lemma islimpt_union_finite:
-  fixes x :: "'a::t1_space"
-  shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
-by (induct set: finite, simp_all add: islimpt_insert)
- 
-lemma sequence_unique_limpt:
-  fixes f :: "nat \<Rightarrow> 'a::t2_space"
-  assumes "(f ---> l) sequentially" and "l' islimpt (range f)"
-  shows "l' = l"
-proof (rule ccontr)
-  assume "l' \<noteq> l"
-  obtain s t where "open s" "open t" "l' \<in> s" "l \<in> t" "s \<inter> t = {}"
-    using hausdorff [OF `l' \<noteq> l`] by auto
-  have "eventually (\<lambda>n. f n \<in> t) sequentially"
-    using assms(1) `open t` `l \<in> t` by (rule topological_tendstoD)
-  then obtain N where "\<forall>n\<ge>N. f n \<in> t"
-    unfolding eventually_sequentially by auto
-
-  have "UNIV = {..<N} \<union> {N..}" by auto
-  hence "l' islimpt (f ` ({..<N} \<union> {N..}))" using assms(2) by simp
-  hence "l' islimpt (f ` {..<N} \<union> f ` {N..})" by (simp add: image_Un)
-  hence "l' islimpt (f ` {N..})" by (simp add: islimpt_union_finite)
-  then obtain y where "y \<in> f ` {N..}" "y \<in> s" "y \<noteq> l'"
-    using `l' \<in> s` `open s` by (rule islimptE)
-  then obtain n where "N \<le> n" "f n \<in> s" "f n \<noteq> l'" by auto
-  with `\<forall>n\<ge>N. f n \<in> t` have "f n \<in> s \<inter> t" by simp
-  with `s \<inter> t = {}` show False by simp
-qed
-
-lemma bolzano_weierstrass_imp_closed:
-  fixes s :: "'a::metric_space set" (* TODO: can this be generalized? *)
-  assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
-  shows "closed s"
-proof-
-  { fix x l assume as: "\<forall>n::nat. x n \<in> s" "(x ---> l) sequentially"
-    hence "l \<in> s"
-    proof(cases "\<forall>n. x n \<noteq> l")
-      case False thus "l\<in>s" using as(1) by auto
-    next
-      case True note cas = this
-      with as(2) have "infinite (range x)" using sequence_infinite_lemma[of x l] by auto
-      then obtain l' where "l'\<in>s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] 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 fast
-qed
-
 text {* Hence express everything as an equivalence. *}
 
-lemma compact_eq_heine_borel:
-  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 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 by (rule bolzano_weierstrass_imp_compact)
-qed
+lemma compact_eq_seq_compact_metric:
+  "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
+  using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
+
+lemma compact_def:
+  "compact (S :: 'a::metric_space set) \<longleftrightarrow>
+   (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow>
+       (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially)) "
+  unfolding compact_eq_seq_compact_metric seq_compact_def by auto
 
 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 unfolding compact_eq_heine_borel using heine_borel_imp_bolzano_weierstrass[of s] by auto
+  assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto
 next
-  assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
+  assume ?rhs thus ?lhs
+    unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
 qed
 
 lemma nat_approx_posE:
@@ -3081,8 +3557,8 @@
 qed
 
 lemma compact_eq_totally_bounded:
-  shows "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
-proof (safe intro!: compact_imp_complete)
+  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
+proof (safe intro!: seq_compact_imp_complete[unfolded  compact_eq_seq_compact_metric[symmetric]])
   fix e::real
   def f \<equiv> "(\<lambda>x::'a. ball x e) ` UNIV"
   assume "0 < e" "compact s"
@@ -3219,124 +3695,24 @@
   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
+  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_compact by auto
+  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 ==> bounded s"
+  shows "compact s \<Longrightarrow> bounded s"
 proof -
   assume "compact s"
-  hence "\<forall>f. (\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
-    by (rule compact_imp_heine_borel)
   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_imp_closed:
-  fixes s :: "'a::metric_space set"
-  shows "compact s ==> closed s"
-proof -
-  assume "compact s"
-  hence "\<forall>f. (\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
-    by (rule compact_imp_heine_borel)
-  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 "closed s"
-    by (rule bolzano_weierstrass_imp_closed)
-qed
-
-text{* In particular, some common special cases. *}
-
-lemma compact_empty[simp]:
- "compact {}"
-  unfolding compact_def
-  by simp
-
-lemma compact_union [intro]:
-  assumes "compact s" and "compact t"
-  shows "compact (s \<union> t)"
-proof (rule compactI)
-  fix f :: "nat \<Rightarrow> 'a"
-  assume "\<forall>n. f n \<in> s \<union> t"
-  hence "infinite {n. f n \<in> s \<union> t}" by simp
-  hence "infinite {n. f n \<in> s} \<or> infinite {n. f n \<in> t}" by simp
-  thus "\<exists>l\<in>s \<union> t. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-  proof
-    assume "infinite {n. f n \<in> s}"
-    from infinite_enumerate [OF this]
-    obtain q where "subseq q" "\<forall>n. (f \<circ> q) n \<in> s" by auto
-    obtain r l where "l \<in> s" "subseq r" "((f \<circ> q \<circ> r) ---> l) sequentially"
-      using `compact s` `\<forall>n. (f \<circ> q) n \<in> s` by (rule compactE)
-    hence "l \<in> s \<union> t" "subseq (q \<circ> r)" "((f \<circ> (q \<circ> r)) ---> l) sequentially"
-      using `subseq q` by (simp_all add: subseq_o o_assoc)
-    thus ?thesis by auto
-  next
-    assume "infinite {n. f n \<in> t}"
-    from infinite_enumerate [OF this]
-    obtain q where "subseq q" "\<forall>n. (f \<circ> q) n \<in> t" by auto
-    obtain r l where "l \<in> t" "subseq r" "((f \<circ> q \<circ> r) ---> l) sequentially"
-      using `compact t` `\<forall>n. (f \<circ> q) n \<in> t` by (rule compactE)
-    hence "l \<in> s \<union> t" "subseq (q \<circ> r)" "((f \<circ> (q \<circ> r)) ---> l) sequentially"
-      using `subseq q` by (simp_all add: subseq_o o_assoc)
-    thus ?thesis by auto
-  qed
-qed
-
-lemma compact_Union [intro]: "finite S \<Longrightarrow> (\<And>T. T \<in> S \<Longrightarrow> compact T) \<Longrightarrow> compact (\<Union>S)"
-  by (induct set: finite) auto
-
-lemma compact_UN [intro]:
-  "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
-  unfolding SUP_def by (rule compact_Union) auto
-
-lemma compact_inter_closed [intro]:
-  assumes "compact s" and "closed t"
-  shows "compact (s \<inter> t)"
-proof (rule compactI)
-  fix f :: "nat \<Rightarrow> 'a"
-  assume "\<forall>n. f n \<in> s \<inter> t"
-  hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t" by simp_all
-  obtain l r where "l \<in> s" "subseq r" "((f \<circ> r) ---> l) sequentially"
-    using `compact s` `\<forall>n. f n \<in> s` by (rule compactE)
-  moreover
-  from `closed t` `\<forall>n. f n \<in> t` `((f \<circ> r) ---> l) sequentially` have "l \<in> t"
-    unfolding closed_sequential_limits o_def by fast
-  ultimately show "\<exists>l\<in>s \<inter> t. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-    by auto
-qed
-
-lemma closed_inter_compact [intro]:
-  assumes "closed s" and "compact t"
-  shows "compact (s \<inter> t)"
-  using compact_inter_closed [of t s] assms
-  by (simp add: Int_commute)
-
-lemma compact_inter [intro]:
-  assumes "compact s" and "compact t"
-  shows "compact (s \<inter> t)"
-  using assms by (intro compact_inter_closed compact_imp_closed)
-
-lemma compact_sing [simp]: "compact {a}"
-  unfolding compact_def o_def subseq_def
-  by (auto simp add: tendsto_const)
-
-lemma compact_insert [simp]:
-  assumes "compact s" shows "compact (insert x s)"
-proof -
-  have "compact ({x} \<union> s)"
-    using compact_sing assms by (rule compact_union)
-  thus ?thesis by simp
-qed
-
-lemma finite_imp_compact:
-  shows "finite s \<Longrightarrow> compact s"
-  by (induct set: finite) simp_all
-
 lemma compact_cball[simp]:
   fixes x :: "'a::heine_borel"
   shows "compact(cball x e)"
@@ -3362,28 +3738,6 @@
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
 
-lemma open_delete:
-  fixes s :: "'a::t1_space set"
-  shows "open s \<Longrightarrow> open (s - {x})"
-  by (simp add: open_Diff)
-
-text{* Finite intersection property. I could make it an equivalence in fact. *}
-
-lemma compact_imp_fip:
-  assumes "compact s"  "\<forall>t \<in> f. closed t"
-        "\<forall>f'. finite f' \<and> f' \<subseteq> f --> (s \<inter> (\<Inter> f') \<noteq> {})"
-  shows "s \<inter> (\<Inter> f) \<noteq> {}"
-proof
-  assume as:"s \<inter> (\<Inter> f) = {}"
-  hence "s \<subseteq> \<Union> uminus ` f" by auto
-  moreover have "Ball (uminus ` f) open" using open_Diff closed_Diff using assms(2) by auto
-  ultimately obtain f' where f':"f' \<subseteq> uminus ` f"  "finite f'"  "s \<subseteq> \<Union>f'" using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="(\<lambda>t. - t) ` f"]] by auto
-  hence "finite (uminus ` f') \<and> uminus ` f' \<subseteq> f" by(auto simp add: Diff_Diff_Int)
-  hence "s \<inter> \<Inter>uminus ` f' \<noteq> {}" using assms(3)[THEN spec[where x="uminus ` f'"]] by auto
-  thus False using f'(3) unfolding subset_eq and Union_iff by blast
-qed
-
-
 subsection {* Bounded closed nest property (proof does not use Heine-Borel) *}
 
 lemma bounded_closed_nest:
@@ -3392,10 +3746,10 @@
   shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s(n)"
 proof-
   from assms(2) obtain x where x:"\<forall>n::nat. x n \<in> s n" using choice[of "\<lambda>n x. x\<in> s n"] by auto
-  from assms(4,1) have *:"compact (s 0)" using bounded_closed_imp_compact[of "s 0"] by auto
+  from assms(4,1) have *:"seq_compact (s 0)" using bounded_closed_imp_seq_compact[of "s 0"] by auto
 
   then obtain l r where lr:"l\<in>s 0" "subseq r" "((x \<circ> r) ---> l) sequentially"
-    unfolding compact_def apply(erule_tac x=x in allE)  using x using assms(3) by blast
+    unfolding seq_compact_def apply(erule_tac x=x in allE)  using x using assms(3) by blast
 
   { fix n::nat
     { fix e::real assume "e>0"
@@ -3406,7 +3760,7 @@
       hence "(x \<circ> r) (max N n) \<in> s n"
         using x apply(erule_tac x=n in allE)
         using x apply(erule_tac x="r (max N n)" in allE)
-        using assms(3) apply(erule_tac x=n in allE)apply( erule_tac x="r (max N n)" in allE) by auto
+        using assms(3) apply(erule_tac x=n in allE) apply(erule_tac x="r (max N n)" in allE) by auto
       ultimately have "\<exists>y\<in>s n. dist y l < e" by auto
     }
     hence "l \<in> s n" using closed_approachable[of "s n" l] assms(1) by blast
@@ -4445,6 +4799,7 @@
 text {* Preservation of compactness and connectedness under continuous function. *}
 
 lemma compact_continuous_image:
+  fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
   assumes "continuous_on s f"  "compact s"
   shows "compact(f ` s)"
 proof-
@@ -4452,7 +4807,8 @@
     then obtain y where y:"\<forall>n. y n \<in> s \<and> x n = f (y n)" unfolding image_iff Bex_def using choice[of "\<lambda>n xa. xa \<in> s \<and> x n = f xa"] by auto
     then obtain l r where "l\<in>s" and r:"subseq r" and lr:"((y \<circ> r) ---> l) sequentially" using assms(2)[unfolded compact_def, THEN spec[where x=y]] by auto
     { fix e::real assume "e>0"
-      then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' l < d \<longrightarrow> dist (f x') (f l) < e" using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\<in>s`] by auto
+      then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' l < d \<longrightarrow> dist (f x') (f l) < e"
+        using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\<in>s`] by auto
       then obtain N::nat where N:"\<forall>n\<ge>N. dist ((y \<circ> r) n) l < d" using lr[unfolded LIMSEQ_def, THEN spec[where x=d]] by auto
       { fix n::nat assume "n\<ge>N" hence "dist ((x \<circ> r) n) (f l) < e" using N[THEN spec[where x=n]] d[THEN bspec[where x="y (r n)"]] y[THEN spec[where x="r n"]] by auto  }
       hence "\<exists>N. \<forall>n\<ge>N. dist ((x \<circ> r) n) (f l) < e" by auto  }
@@ -4493,7 +4849,8 @@
     hence "s \<subseteq> \<Union>{ball x (d x (e / 2)) |x. x \<in> s}" unfolding subset_eq by auto
     moreover
     { fix b assume "b\<in>{ball x (d x (e / 2)) |x. x \<in> s}" hence "open b" by auto  }
-    ultimately obtain ea where "ea>0" and ea:"\<forall>x\<in>s. \<exists>b\<in>{ball x (d x (e / 2)) |x. x \<in> s}. ball x ea \<subseteq> b" using heine_borel_lemma[OF assms(2), of "{ball x (d x (e / 2)) | x. x\<in>s }"] by auto
+    ultimately obtain ea where "ea>0" and ea:"\<forall>x\<in>s. \<exists>b\<in>{ball x (d x (e / 2)) |x. x \<in> s}. ball x ea \<subseteq> b"
+      using heine_borel_lemma[OF assms(2)[unfolded compact_eq_seq_compact_metric], of "{ball x (d x (e / 2)) | x. x\<in>s }"] by auto
 
     { fix x y assume "x\<in>s" "y\<in>s" and as:"dist y x < ea"
       obtain z where "z\<in>s" and z:"ball x ea \<subseteq> ball z (d z (e / 2))" using ea[THEN bspec[where x=x]] and `x\<in>s` by auto
@@ -4720,8 +5077,8 @@
 lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
 by (induct x) simp
 
-lemma compact_Times: "compact s \<Longrightarrow> compact t \<Longrightarrow> compact (s \<times> t)"
-unfolding compact_def
+lemma seq_compact_Times: "seq_compact s \<Longrightarrow> seq_compact t \<Longrightarrow> seq_compact (s \<times> t)"
+unfolding seq_compact_def
 apply clarify
 apply (drule_tac x="fst \<circ> f" in spec)
 apply (drule mp, simp add: mem_Times_iff)
@@ -4737,6 +5094,12 @@
 apply (simp add: o_def)
 done
 
+text {* Generalize to @{class topological_space} *}
+lemma compact_Times: 
+  fixes s :: "'a::metric_space set" and t :: "'b::metric_space set"
+  shows "compact s \<Longrightarrow> compact t \<Longrightarrow> compact (s \<times> t)"
+  unfolding compact_eq_seq_compact_metric by (rule seq_compact_Times)
+
 text{* Hence some useful properties follow quite easily. *}
 
 lemma compact_scaling:
@@ -5256,8 +5619,8 @@
   using bounded_interval[of a b] by auto
 
 lemma compact_interval: fixes a :: "'a::ordered_euclidean_space" shows "compact {a .. b}"
-  using bounded_closed_imp_compact[of "{a..b}"] using bounded_interval[of a b]
-  by auto
+  using bounded_closed_imp_seq_compact[of "{a..b}"] using bounded_interval[of a b]
+  by (auto simp: compact_eq_seq_compact_metric)
 
 lemma open_interval_midpoint: fixes a :: "'a::ordered_euclidean_space"
   assumes "{a<..<b} \<noteq> {}" shows "((1/2) *\<^sub>R (a + b)) \<in> {a<..<b}"
@@ -5411,7 +5774,7 @@
   finally show ?thesis .
 qed
 
-instance euclidean_space \<subseteq> countable_basis_space
+instance euclidean_space \<subseteq> second_countable_topology
 proof
   def a \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. fst (f i) *\<^sub>R i"
   then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f" by simp
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -153,38 +153,8 @@
   "borel = sigma UNIV union_closed_basis"
   by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
 
-lemma topological_basis_prod:
-  assumes A: "topological_basis A" and B: "topological_basis B"
-  shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
-  unfolding topological_basis_def
-proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
-  fix S :: "('a \<times> 'b) set" assume "open S"
-  then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
-  proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
-    fix x y assume "(x, y) \<in> S"
-    from open_prod_elim[OF `open S` this]
-    obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
-      by (metis mem_Sigma_iff)
-    moreover from topological_basisE[OF A a] guess A0 .
-    moreover from topological_basisE[OF B b] guess B0 .
-    ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
-      by (intro UN_I[of "(A0, B0)"]) auto
-  qed auto
-qed (metis A B topological_basis_open open_Times)
-
-instance prod :: (countable_basis_space, countable_basis_space) countable_basis_space
-proof
-  obtain A :: "'a set set" where "countable A" "topological_basis A"
-    using ex_countable_basis by auto
-  moreover
-  obtain B :: "'b set set" where "countable B" "topological_basis B"
-    using ex_countable_basis by auto
-  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
-    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
-qed
-
 lemma borel_measurable_Pair[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
+  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
   shows "(\<lambda>x. (f x, g x)) \<in> borel_measurable M"
@@ -257,7 +227,7 @@
 qed
 
 lemma borel_measurable_continuous_Pair:
-  fixes f :: "'a \<Rightarrow> 'b::countable_basis_space" and g :: "'a \<Rightarrow> 'c::countable_basis_space"
+  fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes [measurable]: "f \<in> borel_measurable M"
   assumes [measurable]: "g \<in> borel_measurable M"
   assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
@@ -271,7 +241,7 @@
 section "Borel spaces on euclidean spaces"
 
 lemma borel_measurable_inner[measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> 'b::{countable_basis_space, real_inner}"
+  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -48,7 +48,7 @@
   thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
 qed
 
-instance discrete :: (countable) countable_basis_space
+instance discrete :: (countable) second_countable_topology
 proof
   let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
   have "topological_basis ?B"
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -1045,7 +1045,7 @@
 lemma product_open_generates_sets_PiF_single:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
-  shows "sets (PiF {I} (\<lambda>_. borel::'b::countable_basis_space measure)) =
+  shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
     sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
 proof -
   from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
@@ -1064,7 +1064,7 @@
 lemma product_open_generates_sets_PiM:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
-  shows "sets (PiM I (\<lambda>_. borel::'b::countable_basis_space measure)) =
+  shows "sets (PiM I (\<lambda>_. borel::'b::second_countable_topology measure)) =
     sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
 proof -
   from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -46,12 +46,13 @@
 end
 
 lemma compactE':
+  fixes S :: "'a :: metric_space set"
   assumes "compact S" "\<forall>n\<ge>m. f n \<in> S"
   obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
 proof atomize_elim
   have "subseq (op + m)" by (simp add: subseq_def)
   have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto
-  from compactE[OF `compact S` this] guess l r .
+  from seq_compactE[OF `compact S`[unfolded compact_eq_seq_compact_metric] this] guess l r .
   hence "l \<in> S" "subseq ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) ----> l"
     using subseq_o[OF `subseq (op + m)` `subseq r`] by (auto simp: o_def)
   thus "\<exists>l r. l \<in> S \<and> subseq r \<and> (f \<circ> r) ----> l" by blast
diff -r d55eb82ae77b -r a9c1b1428e87 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Mon Jan 14 22:24:57 2013 +0100
+++ b/src/HOL/Probability/Regularity.thy	Mon Jan 14 22:33:53 2013 +0100
@@ -104,7 +104,7 @@
 qed
 
 lemma
-  fixes M::"'a::{countable_basis_space, complete_space} measure"
+  fixes M::"'a::{second_countable_topology, complete_space} measure"
   assumes sb: "sets M = sets borel"
   assumes "emeasure M (space M) \<noteq> \<infinity>"
   assumes "B \<in> sets borel"