--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Nov 15 17:40:46 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 16 11:22:22 2012 +0100
@@ -64,76 +64,51 @@
show "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" using assms by (simp add: Bex_def)
qed
+lemma topological_basis_open:
+ assumes "topological_basis B"
+ assumes "X \<in> B"
+ shows "open X"
+ using assms
+ by (simp add: topological_basis_def)
+
end
subsection {* Enumerable Basis *}
-class enumerable_basis = topological_space +
- assumes ex_enum_basis: "\<exists>f::nat \<Rightarrow> 'a set. topological_basis (range f)"
+locale enumerates_basis =
+ fixes f::"nat \<Rightarrow> 'a::topological_space set"
+ assumes enumerable_basis: "topological_basis (range f)"
begin
-definition enum_basis'::"nat \<Rightarrow> 'a set"
- where "enum_basis' = Eps (topological_basis o range)"
-
-lemma enumerable_basis': "topological_basis (range enum_basis')"
- using ex_enum_basis
- unfolding enum_basis'_def o_def
- by (rule someI_ex)
-
-lemmas enumerable_basisE' = topological_basisE[OF enumerable_basis']
-
-text {* Extend enumeration of basis, such that it is closed under (finite) Union *}
-
-definition enum_basis::"nat \<Rightarrow> 'a set"
- where "enum_basis n = \<Union>(set (map enum_basis' (from_nat n)))"
-
-lemma
- open_enum_basis:
- assumes "B \<in> range enum_basis"
- shows "open B"
- using assms enumerable_basis'
- by (force simp add: topological_basis_def enum_basis_def)
-
-lemma enumerable_basis: "topological_basis (range enum_basis)"
-proof (rule topological_basisI[OF open_enum_basis])
- fix O' x assume "open O'" "x \<in> O'"
- from topological_basisE[OF enumerable_basis' this] guess B' . note B' = this
- moreover then obtain n where "B' = enum_basis' n" by auto
- moreover hence "B' = enum_basis (to_nat [n])" by (auto simp: enum_basis_def)
- ultimately show "\<exists>B'\<in>range enum_basis. x \<in> B' \<and> B' \<subseteq> O'" by blast
-qed
-
-lemmas enumerable_basisE = topological_basisE[OF enumerable_basis]
-
lemma open_enumerable_basis_ex:
assumes "open X"
- shows "\<exists>N. X = (\<Union>n\<in>N. enum_basis n)"
+ shows "\<exists>N. X = (\<Union>n\<in>N. f n)"
proof -
- from enumerable_basis assms obtain B' where "B' \<subseteq> range enum_basis" "X = Union B'"
+ from enumerable_basis assms obtain B' where "B' \<subseteq> range f" "X = Union B'"
unfolding topological_basis_def by blast
- hence "Union B' = (\<Union>n\<in>{n. enum_basis n \<in> B'}. enum_basis n)" by auto
+ hence "Union B' = (\<Union>n\<in>{n. f n \<in> B'}. f n)" by auto
with `X = Union B'` show ?thesis by blast
qed
lemma open_enumerable_basisE:
assumes "open X"
- obtains N where "X = (\<Union>n\<in>N. enum_basis n)"
+ obtains N where "X = (\<Union>n\<in>N. f n)"
using assms open_enumerable_basis_ex by (atomize_elim) simp
lemma countable_dense_set:
- shows "\<exists>x::nat \<Rightarrow> _. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
+ shows "\<exists>x::nat \<Rightarrow> 'a. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
proof -
- def x \<equiv> "\<lambda>n. (SOME x::'a. x \<in> enum_basis n)"
- have x: "\<And>n. enum_basis n \<noteq> ({}::'a set) \<Longrightarrow> x n \<in> enum_basis n" unfolding x_def
+ def x \<equiv> "\<lambda>n. (SOME x::'a. x \<in> f n)"
+ have x: "\<And>n. f n \<noteq> ({}::'a set) \<Longrightarrow> x n \<in> f n" unfolding x_def
by (rule someI_ex) auto
have "\<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
proof (intro allI impI)
fix y::"'a set" assume "open y" "y \<noteq> {}"
from open_enumerable_basisE[OF `open y`] guess N . note N = this
- obtain n where n: "n \<in> N" "enum_basis n \<noteq> ({}::'a set)"
+ obtain n where n: "n \<in> N" "f n \<noteq> ({}::'a set)"
proof (atomize_elim, rule ccontr, clarsimp)
- assume "\<forall>n. n \<in> N \<longrightarrow> enum_basis n = ({}::'a set)"
- hence "(\<Union>n\<in>N. enum_basis n) = (\<Union>n\<in>N. {}::'a set)"
+ assume "\<forall>n. n \<in> N \<longrightarrow> f n = ({}::'a set)"
+ hence "(\<Union>n\<in>N. f n) = (\<Union>n\<in>N. {}::'a set)"
by (intro UN_cong) auto
hence "y = {}" unfolding N by simp
with `y \<noteq> {}` show False by auto
@@ -145,11 +120,30 @@
qed
lemma countable_dense_setE:
- obtains x :: "nat \<Rightarrow> _"
+ obtains x :: "nat \<Rightarrow> 'a"
where "\<And>y. open y \<Longrightarrow> y \<noteq> {} \<Longrightarrow> \<exists>n. x n \<in> y"
using countable_dense_set by blast
-text {* Construction of an Increasing Sequence Approximating Open Sets *}
+text {* Construction of an increasing sequence approximating open sets, therefore enumeration of
+ basis which is closed under union. *}
+
+definition enum_basis::"nat \<Rightarrow> 'a set"
+ where "enum_basis n = \<Union>(set (map f (from_nat n)))"
+
+lemma enum_basis_basis: "topological_basis (range enum_basis)"
+proof (rule topological_basisI)
+ fix O' and x::'a assume "open O'" "x \<in> O'"
+ from topological_basisE[OF enumerable_basis this] guess B' . note B' = this
+ moreover then obtain n where "B' = f n" by auto
+ moreover hence "B' = enum_basis (to_nat [n])" by (auto simp: enum_basis_def)
+ ultimately show "\<exists>B'\<in>range enum_basis. x \<in> B' \<and> B' \<subseteq> O'" by blast
+next
+ fix B' assume "B' \<in> range enum_basis"
+ with topological_basis_open[OF enumerable_basis]
+ show "open B'" by (auto simp add: enum_basis_def intro!: open_UN)
+qed
+
+lemmas open_enum_basis = topological_basis_open[OF enum_basis_basis]
lemma empty_basisI[intro]: "{} \<in> range enum_basis"
proof
@@ -170,7 +164,8 @@
assumes "open X"
shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> range enum_basis"
proof -
- from open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n\<in>N. enum_basis n)" by auto
+ interpret E: enumerates_basis enum_basis proof qed (rule enum_basis_basis)
+ from E.open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n\<in>N. enum_basis n)" by auto
hence X: "X = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
def S \<equiv> "nat_rec (if 0 \<in> N then enum_basis 0 else {})
(\<lambda>n S. if (Suc n) \<in> N then S \<union> enum_basis (Suc n) else S)"
@@ -204,6 +199,13 @@
end
+class enumerable_basis = topological_space +
+ assumes ex_enum_basis: "\<exists>f::nat \<Rightarrow> 'a::topological_space set. topological_basis (range f)"
+
+sublocale enumerable_basis < enumerates_basis "Eps (topological_basis o range)"
+ unfolding o_def
+ proof qed (rule someI_ex[OF ex_enum_basis])
+
subsection {* Polish spaces *}
text {* Textbooks define Polish spaces as completely metrizable.
--- a/src/HOL/Probability/Borel_Space.thy Thu Nov 15 17:40:46 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Fri Nov 16 11:22:22 2012 +0100
@@ -456,21 +456,28 @@
finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
qed simp_all
-lemma borel_eq_enum_basis:
- "borel = sigma UNIV (range enum_basis)"
+lemma borel_eq_enumerated_basis:
+ fixes f::"nat\<Rightarrow>'a::topological_space set"
+ assumes "topological_basis (range f)"
+ shows "borel = sigma UNIV (range f)"
unfolding borel_def
proof (intro sigma_eqI sigma_sets_eqI, safe)
+ interpret enumerates_basis proof qed (rule assms)
fix x::"'a set" assume "open x"
from open_enumerable_basisE[OF this] guess N .
- hence x: "x = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
- also have "\<dots> \<in> sigma_sets UNIV (range enum_basis)" by (rule Union) auto
- finally show "x \<in> sigma_sets UNIV (range enum_basis)" .
+ hence x: "x = (\<Union>n. if n \<in> N then f n else {})" by (auto split: split_if_asm)
+ also have "\<dots> \<in> sigma_sets UNIV (range f)" by (auto intro!: sigma_sets.Empty Union)
+ finally show "x \<in> sigma_sets UNIV (range f)" .
next
fix n
- have "open (enum_basis n)" by (rule open_enum_basis) simp
- thus "enum_basis n \<in> sigma_sets UNIV (Collect open)" by auto
+ have "open (f n)" by (rule topological_basis_open[OF assms]) simp
+ thus "f n \<in> sigma_sets UNIV (Collect open)" by auto
qed simp_all
+lemma borel_eq_enum_basis:
+ "borel = sigma UNIV (range enum_basis)"
+ by (rule borel_eq_enumerated_basis[OF enum_basis_basis])
+
lemma borel_measurable_halfspacesI:
fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
assumes F: "borel = sigma UNIV (range F)"
--- a/src/HOL/Probability/Fin_Map.thy Thu Nov 15 17:40:46 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Fri Nov 16 11:22:22 2012 +0100
@@ -500,7 +500,7 @@
"topological_basis (range (enum_basis_finmap))"
proof (subst topological_basis_iff, safe)
fix n::nat
- show "open (enum_basis_finmap n::('a \<Rightarrow>\<^isub>F 'b) set)" using enumerable_basis
+ show "open (enum_basis_finmap n::('a \<Rightarrow>\<^isub>F 'b) set)" using enum_basis_basis
by (auto intro!: open_Pi'I simp: topological_basis_def enum_basis_finmap_def Let_def)
next
fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
@@ -514,7 +514,7 @@
fix i assume "i \<in> domain x"
have "open (ball (x i) e')" "x i \<in> ball (x i) e'" using e
by (auto simp add: e'_def intro!: divide_pos_pos)
- from enumerable_basisE[OF this] guess b' .
+ from topological_basisE[OF enum_basis_basis this] guess b' .
thus "\<exists>y. x i \<in> enum_basis y \<and>
enum_basis y \<subseteq> ball (x i) e'" by auto
qed