--- 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 ***
--- 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}
*}
--- 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"
--- 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
--- 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"
--- 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)
--- 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
--- 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"
--- 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"
--- 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
--- 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
--- 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"