# HG changeset patch
# User immler
# Date 1353061342 -3600
# Node ID 84ddcf5364b42bc218b96a9ee06cadbdb419582c
# Parent  a2886be4d615171e64365cd7c8a1c20f6a7e76bb
allow arbitrary enumerations of basis in locale for generation of borel sets

diff -r a2886be4d615 -r 84ddcf5364b4 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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.
diff -r a2886be4d615 -r 84ddcf5364b4 src/HOL/Probability/Borel_Space.thy
--- 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)"
diff -r a2886be4d615 -r 84ddcf5364b4 src/HOL/Probability/Fin_Map.thy
--- 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