# HG changeset patch
# User immler
# Date 1354020520 -3600
# Node ID dea9363887a680c0f87c9869008c1c458aac9daf
# Parent  de72bbe421902b25ac27b0a2bfd4cb68d70890d5
based countable topological basis on Countable_Set

diff -r de72bbe42190 -r dea9363887a6 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -235,6 +235,12 @@
     by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
 qed
 
+lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
+  using finite_list by auto
+
+lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
+  by (simp add: Collect_finite_eq_lists)
+
 subsection {* Misc lemmas *}
 
 lemma countable_all:
diff -r de72bbe42190 -r dea9363887a6 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -10,7 +10,7 @@
 imports
   SEQ
   "~~/src/HOL/Library/Diagonal_Subsequence"
-  "~~/src/HOL/Library/Countable"
+  "~~/src/HOL/Library/Countable_Set"
   Linear_Algebra
   "~~/src/HOL/Library/Glbs"
   Norm_Arith
@@ -71,147 +71,160 @@
   using assms
   by (simp add: topological_basis_def)
 
+lemma basis_dense:
+  fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a"
+  assumes "topological_basis B"
+  assumes choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
+  shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
+proof (intro allI impI)
+  fix X::"'a set" assume "open X" "X \<noteq> {}"
+  from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
+  guess B' . note B' = this
+  thus "\<exists>B'\<in>B. f B' \<in> X" by (auto intro!: choosefrom_basis)
+qed
+
 end
 
-subsection {* Enumerable Basis *}
-
-locale enumerates_basis =
-  fixes f::"nat \<Rightarrow> 'a::topological_space set"
-  assumes enumerable_basis: "topological_basis (range f)"
+subsection {* Countable Basis *}
+
+locale countable_basis =
+  fixes B::"'a::topological_space set set"
+  assumes is_basis: "topological_basis B"
+  assumes countable_basis: "countable B"
 begin
 
-lemma open_enumerable_basis_ex:
-  assumes "open X"
-  shows "\<exists>N. X = (\<Union>n\<in>N. f n)"
-proof -
-  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. f n \<in> B'}. f n)" by auto
-  with `X = Union B'` show ?thesis by blast
-qed
-
-lemma open_enumerable_basisE:
+lemma open_countable_basis_ex:
   assumes "open X"
-  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> 'a. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
+  shows "\<exists>B' \<subseteq> B. X = Union B'"
+  using assms countable_basis is_basis unfolding topological_basis_def by blast
+
+lemma open_countable_basisE:
+  assumes "open X"
+  obtains B' where "B' \<subseteq> B" "X = Union B'"
+  using assms open_countable_basis_ex by (atomize_elim) simp
+
+lemma countable_dense_exists:
+  shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
 proof -
-  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" "f n \<noteq> ({}::'a set)"
-    proof (atomize_elim, rule ccontr, clarsimp)
-      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
-    qed
-    with x N n have "x n \<in> y" by auto
-    thus "\<exists>n. x n \<in> y" ..
-  qed
-  thus ?thesis by blast
+  let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
+  have "countable (?f ` B)" using countable_basis by simp
+  with basis_dense[OF is_basis, of ?f] show ?thesis
+    by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI)
 qed
 
 lemma countable_dense_setE:
-  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, 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)"
+  obtains D :: "'a set"
+  where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
+  using countable_dense_exists by blast
+
+text {* Construction of an increasing sequence approximating open sets,
+  therefore basis which is closed under union. *}
+
+definition union_closed_basis::"'a set set" where
+  "union_closed_basis = (\<lambda>l. \<Union>set l) ` lists B"
+
+lemma basis_union_closed_basis: "topological_basis union_closed_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
+  from topological_basisE[OF is_basis this] guess B' . note B' = this
+  thus "\<exists>B'\<in>union_closed_basis. x \<in> B' \<and> B' \<subseteq> O'" unfolding union_closed_basis_def
+    by (auto intro!: bexI[where x="[B']"])
 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
-  show "{} = enum_basis (to_nat ([]::nat list))" by (simp add: enum_basis_def)
-qed rule
+  fix B' assume "B' \<in> union_closed_basis"
+  thus "open B'"
+    using topological_basis_open[OF is_basis]
+    by (auto simp: union_closed_basis_def)
+qed
+
+lemma countable_union_closed_basis: "countable union_closed_basis"
+  unfolding union_closed_basis_def using countable_basis by simp
+
+lemmas open_union_closed_basis = topological_basis_open[OF basis_union_closed_basis]
+
+lemma union_closed_basis_ex:
+ assumes X: "X \<in> union_closed_basis"
+ shows "\<exists>B'. finite B' \<and> X = \<Union>B' \<and> B' \<subseteq> B"
+proof -
+  from X obtain l where "\<And>x. x\<in>set l \<Longrightarrow> x\<in>B" "X = \<Union>set l" by (auto simp: union_closed_basis_def)
+  thus ?thesis by auto
+qed
+
+lemma union_closed_basisE:
+  assumes "X \<in> union_closed_basis"
+  obtains B' where "finite B'" "X = \<Union>B'" "B' \<subseteq> B" using union_closed_basis_ex[OF assms] by blast
+
+lemma union_closed_basisI:
+  assumes "finite B'" "X = \<Union>B'" "B' \<subseteq> B"
+  shows "X \<in> union_closed_basis"
+proof -
+  from finite_list[OF `finite B'`] guess l ..
+  thus ?thesis using assms unfolding union_closed_basis_def by (auto intro!: image_eqI[where x=l])
+qed
+
+lemma empty_basisI[intro]: "{} \<in> union_closed_basis"
+  by (rule union_closed_basisI[of "{}"]) auto
 
 lemma union_basisI[intro]:
-  assumes "A \<in> range enum_basis" "B \<in> range enum_basis"
-  shows "A \<union> B \<in> range enum_basis"
-proof -
-  from assms obtain a b where "A \<union> B = enum_basis a \<union> enum_basis b" by auto
-  also have "\<dots> = enum_basis (to_nat (from_nat a @ from_nat b::nat list))"
-    by (simp add: enum_basis_def)
-  finally show ?thesis by simp
-qed
+  assumes "X \<in> union_closed_basis" "Y \<in> union_closed_basis"
+  shows "X \<union> Y \<in> union_closed_basis"
+  using assms by (auto intro: union_closed_basisI elim!:union_closed_basisE)
 
 lemma open_imp_Union_of_incseq:
   assumes "open X"
-  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> range enum_basis"
+  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> union_closed_basis"
 proof -
-  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)"
-  have S_simps[simp]:
-    "S 0 = (if 0 \<in> N then enum_basis 0 else {})"
-    "\<And>n. S (Suc n) = (if (Suc n) \<in> N then S n \<union> enum_basis (Suc n) else S n)"
-    by (simp_all add: S_def)
-  have "incseq S" by (rule incseq_SucI) auto
-  moreover
-  have "(\<Union>j. S j) = X" unfolding N
-  proof safe
-    fix x n assume "n \<in> N" "x \<in> enum_basis n"
-    hence "x \<in> S n" by (cases n) auto
-    thus "x \<in> (\<Union>j. S j)" by auto
-  next
-    fix x j
-    assume "x \<in> S j"
-    thus "x \<in> UNION N enum_basis" by (induct j) (auto split: split_if_asm)
-  qed
-  moreover have "range S \<subseteq> range enum_basis"
-  proof safe
-    fix j show "S j \<in> range enum_basis" by (induct j) auto
-  qed
-  ultimately show ?thesis by auto
+  from open_countable_basis_ex[OF `open X`]
+  obtain B' where B': "B'\<subseteq>B" "X = \<Union>B'" by auto
+  from this(1) countable_basis have "countable B'" by (rule countable_subset)
+  show ?thesis
+  proof cases
+    assume "B' \<noteq> {}"
+    def S \<equiv> "\<lambda>n. \<Union>i\<in>{0..n}. from_nat_into B' i"
+    have S:"\<And>n. S n = \<Union>{from_nat_into B' i|i. i\<in>{0..n}}" unfolding S_def by force
+    have "incseq S" by (force simp: S_def incseq_Suc_iff)
+    moreover
+    have "(\<Union>j. S j) = X" unfolding B'
+    proof safe
+      fix x X assume "X \<in> B'" "x \<in> X"
+      then obtain n where "X = from_nat_into B' n"
+        by (metis `countable B'` from_nat_into_surj)
+      also have "\<dots> \<subseteq> S n" by (auto simp: S_def)
+      finally show "x \<in> (\<Union>j. S j)" using `x \<in> X` by auto
+    next
+      fix x n
+      assume "x \<in> S n"
+      also have "\<dots> = (\<Union>i\<in>{0..n}. from_nat_into B' i)"
+        by (simp add: S_def)
+      also have "\<dots> \<subseteq> (\<Union>i. from_nat_into B' i)" by auto
+      also have "\<dots> \<subseteq> \<Union>B'" using `B' \<noteq> {}` by (auto intro: from_nat_into)
+      finally show "x \<in> \<Union>B'" .
+    qed
+    moreover have "range S \<subseteq> union_closed_basis" using B'
+      by (auto intro!: union_closed_basisI[OF _ S] simp: from_nat_into `B' \<noteq> {}`)
+    ultimately show ?thesis by auto
+  qed (auto simp: B')
 qed
 
 lemma open_incseqE:
   assumes "open X"
-  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> range enum_basis"
+  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> union_closed_basis"
   using open_imp_Union_of_incseq assms by atomize_elim
 
 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])
+class countable_basis_space = 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"
+  using someI_ex[OF ex_countable_basis] by unfold_locales safe
 
 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 + enumerable_basis
+class polish_space = complete_space + countable_basis_space
 
 subsection {* General notion of a topology as a value *}
 
@@ -5444,35 +5457,36 @@
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
 
-instance ordered_euclidean_space \<subseteq> enumerable_basis
+instance ordered_euclidean_space \<subseteq> countable_basis_space
 proof
   def to_cube \<equiv> "\<lambda>(a, b). {Chi (real_of_rat \<circ> op ! a)<..<Chi (real_of_rat \<circ> op ! b)}::'a set"
-  def enum \<equiv> "\<lambda>n. (to_cube (from_nat n)::'a set)"
-  have "Ball (range enum) open" unfolding enum_def
+  def B \<equiv> "(\<lambda>n. (to_cube (from_nat n)::'a set)) ` UNIV"
+  have "countable B" unfolding B_def by simp
+  moreover
+  have "Ball B open" unfolding B_def
   proof safe
     fix n show "open (to_cube (from_nat n))"
       by (cases "from_nat n::rat list \<times> rat list")
          (simp add: open_interval to_cube_def)
   qed
-  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>range enum. \<Union>B' = x))"
+  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = x))"
   proof safe
     fix x::"'a set" assume "open x"
     def lists \<equiv> "{(a, b) |a b. to_cube (a, b) \<subseteq> x}"
     from open_UNION[OF `open x`]
     have "\<Union>(to_cube ` lists) = x" unfolding lists_def to_cube_def
      by simp
-    moreover have "to_cube ` lists \<subseteq> range enum"
+    moreover have "to_cube ` lists \<subseteq> B"
     proof
       fix x assume "x \<in> to_cube ` lists"
       then obtain l where "l \<in> lists" "x = to_cube l" by auto
-      hence "x = enum (to_nat l)" by (simp add: to_cube_def enum_def)
-      thus "x \<in> range enum" by simp
+      thus "x \<in> B" by (auto simp add: B_def intro!: image_eqI[where x="to_nat l"])
     qed
     ultimately
-    show "\<exists>B'\<subseteq>range enum. \<Union>B' = x" by blast
+    show "\<exists>B'\<subseteq>B. \<Union>B' = x" by blast
   qed
   ultimately
-  show "\<exists>f::nat\<Rightarrow>'a set. topological_basis (range f)" unfolding topological_basis_def by blast
+  show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
 qed
 
 instance ordered_euclidean_space \<subseteq> polish_space ..
diff -r de72bbe42190 -r dea9363887a6 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -462,27 +462,32 @@
   finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
 qed simp_all
 
-lemma borel_eq_enumerated_basis:
-  fixes f::"nat\<Rightarrow>'a::topological_space set"
-  assumes "topological_basis (range f)"
-  shows "borel = sigma UNIV (range f)"
+lemma borel_eq_countable_basis:
+  fixes B::"'a::topological_space set set"
+  assumes "countable B"
+  assumes "topological_basis B"
+  shows "borel = sigma UNIV B"
   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 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)" .
+  interpret countable_basis using assms by unfold_locales
+  fix X::"'a set" assume "open X"
+  from open_countable_basisE[OF this] guess B' . note B' = this
+  show "X \<in> sigma_sets UNIV B"
+  proof cases
+    assume "B' \<noteq> {}"
+    thus "X \<in> sigma_sets UNIV B" using assms B'
+      by (metis from_nat_into Union_image_eq countable_subset range_from_nat_into
+        in_mono sigma_sets.Basic sigma_sets.Union)
+  qed (simp add: sigma_sets.Empty B')
 next
-  fix n
-  have "open (f n)" by (rule topological_basis_open[OF assms]) simp
-  thus "f n \<in> sigma_sets UNIV (Collect open)" by auto
+  fix b assume "b \<in> B"
+  hence "open b" by (rule topological_basis_open[OF assms(2)])
+  thus "b \<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_eq_union_closed_basis:
+  "borel = sigma UNIV union_closed_basis"
+  by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
 
 lemma borel_measurable_halfspacesI:
   fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
diff -r de72bbe42190 -r dea9363887a6 src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -48,15 +48,17 @@
   thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
 qed
 
-instance discrete :: (countable) enumerable_basis
+instance discrete :: (countable) countable_basis_space
 proof
-  have "topological_basis (range (\<lambda>n::nat. {from_nat n::'a discrete}))"
+  let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
+  have "topological_basis ?B"
   proof (intro topological_basisI)
     fix x::"'a discrete" and O' assume "open O'" "x \<in> O'"
     thus "\<exists>B'\<in>range (\<lambda>n. {from_nat n}). x \<in> B' \<and> B' \<subseteq> O'"
       by (auto intro: exI[where x="to_nat x"])
   qed (simp add: open_discrete_def)
-  thus "\<exists>f::nat\<Rightarrow>'a discrete set. topological_basis (range f)" by blast
+  moreover have "countable ?B" by simp
+  ultimately show "\<exists>B::'a discrete set set. countable B \<and> topological_basis B" by blast
 qed
 
 instance discrete :: (countable) polish_space ..
diff -r de72bbe42190 -r dea9363887a6 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -450,40 +450,41 @@
 instantiation finmap :: (countable, polish_space) polish_space
 begin
 
-definition enum_basis_finmap :: "nat \<Rightarrow> ('a \<Rightarrow>\<^isub>F 'b) set" where
-  "enum_basis_finmap n =
-  (let m = from_nat n::('a \<Rightarrow>\<^isub>F nat) in Pi' (domain m) (enum_basis o (m)\<^isub>F))"
+definition basis_finmap::"('a \<Rightarrow>\<^isub>F 'b) set set"
+  where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> union_closed_basis)}"
+
+lemma in_basis_finmapI:
+  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
+  shows "Pi' I S \<in> basis_finmap"
+  using assms unfolding basis_finmap_def by auto
+
+lemma in_basis_finmapE:
+  assumes "x \<in> basis_finmap"
+  obtains I S where "x = Pi' I S" "finite I" "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
+  using assms unfolding basis_finmap_def by auto
 
-lemma range_enum_basis_eq:
-  "range enum_basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> range enum_basis)}"
-proof (auto simp: enum_basis_finmap_def[abs_def])
-  fix S::"('a \<Rightarrow> 'b set)" and I
-  assume "\<forall>i\<in>I. S i \<in> range enum_basis"
-  hence "\<forall>i\<in>I. \<exists>n. S i = enum_basis n" by auto
-  then obtain n where n: "\<forall>i\<in>I. S i = enum_basis (n i)"
-    unfolding bchoice_iff by blast
-  assume [simp]: "finite I"
-  have "\<exists>fm. domain fm = I \<and> (\<forall>i\<in>I. n i = (fm i))"
-    by (rule finmap_choice) auto
-  then obtain m where "Pi' I S = Pi' (domain m) (enum_basis o m)"
-    using n by (auto simp: Pi'_def)
-  hence "Pi' I S = (let m = from_nat (to_nat m) in Pi' (domain m) (enum_basis \<circ> m))"
-    by simp
-  thus "Pi' I S \<in> range (\<lambda>n. let m = from_nat n in Pi' (domain m) (enum_basis \<circ> m))"
-    by blast
-qed (metis finite_domain o_apply rangeI)
+lemma basis_finmap_eq:
+  "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into union_closed_basis ((f)\<^isub>F i))) `
+    (UNIV::('a \<Rightarrow>\<^isub>F nat) set)" (is "_ = ?f ` _")
+  unfolding basis_finmap_def
+proof safe
+  fix I::"'a set" and S::"'a \<Rightarrow> 'b set"
+  assume "finite I" "\<forall>i\<in>I. S i \<in> union_closed_basis"
+  hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on union_closed_basis (S x)))"
+    by (force simp: Pi'_def countable_union_closed_basis)
+  thus "Pi' I S \<in> range ?f" by simp
+qed (metis (mono_tags) empty_basisI equals0D finite_domain from_nat_into)
 
-lemma in_enum_basis_finmapI:
-  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> range enum_basis"
-  shows "Pi' I S \<in> range enum_basis_finmap"
-  using assms unfolding range_enum_basis_eq by auto
+lemma countable_basis_finmap: "countable basis_finmap"
+  unfolding basis_finmap_eq by simp
 
 lemma finmap_topological_basis:
-  "topological_basis (range (enum_basis_finmap))"
+  "topological_basis basis_finmap"
 proof (subst topological_basis_iff, safe)
-  fix n::nat
-  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)
+  fix B' assume "B' \<in> basis_finmap"
+  thus "open B'"
+    by (auto intro!: open_Pi'I topological_basis_open[OF basis_union_closed_basis]
+      simp: topological_basis_def basis_finmap_def Let_def)
 next
   fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
   assume "open O'" "x \<in> O'"
@@ -491,19 +492,18 @@
   def e' \<equiv> "e / (card (domain x) + 1)"
 
   have "\<exists>B.
-    (\<forall>i\<in>domain x. x i \<in> enum_basis (B i) \<and> enum_basis (B i) \<subseteq> ball (x i) e')"
+    (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> ball (x i) e' \<and> B i \<in> union_closed_basis)"
   proof (rule bchoice, safe)
     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 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
+    from topological_basisE[OF basis_union_closed_basis this] guess b' .
+    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> ball (x i) e' \<and> y \<in> union_closed_basis" by auto
   qed
   then guess B .. note B = this
-  def B' \<equiv> "Pi' (domain x) (\<lambda>i. enum_basis (B i)::'b set)"
-  hence "B' \<in> range enum_basis_finmap" unfolding B'_def
-    by (intro in_enum_basis_finmapI) auto
+  def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)"
+  hence "B' \<in> basis_finmap" unfolding B'_def using B
+    by (intro in_basis_finmapI) auto
   moreover have "x \<in> B'" unfolding B'_def using B by auto
   moreover have "B' \<subseteq> O'"
   proof
@@ -516,7 +516,7 @@
       also have "\<dots> \<le> (\<Sum>i \<in> domain x. e')"
       proof (rule setsum_mono)
         fix i assume "i \<in> domain x"
-        with `y \<in> B'` B have "y i \<in> enum_basis (B i)"
+        with `y \<in> B'` B have "y i \<in> B i"
           by (simp add: Pi'_def B'_def)
         hence "y i \<in> ball (x i) e'" using B `domain y = domain x` `i \<in> domain x`
           by force
@@ -528,73 +528,15 @@
     qed
   qed
   ultimately
-  show "\<exists>B'\<in>range enum_basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" by blast
+  show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" by blast
 qed
 
 lemma range_enum_basis_finmap_imp_open:
-  assumes "x \<in> range enum_basis_finmap"
+  assumes "x \<in> basis_finmap"
   shows "open x"
   using finmap_topological_basis assms by (auto simp: topological_basis_def)
 
-lemma open_imp_ex_UNION_of_enum:
-  fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
-  assumes "open X" assumes "X \<noteq> {}"
-  shows "\<exists>A::nat\<Rightarrow>'a set. \<exists>B::nat\<Rightarrow>('a \<Rightarrow> 'b set) . X = UNION UNIV (\<lambda>i. Pi' (A i) (B i)) \<and>
-    (\<forall>n. \<forall>i\<in>A n. (B n) i \<in> range enum_basis) \<and> (\<forall>n. finite (A n))"
-proof -
-  from `open X` obtain B' where B': "B'\<subseteq>range enum_basis_finmap" "\<Union>B' = X"
-    using finmap_topological_basis by (force simp add: topological_basis_def)
-  then obtain B where B: "B' = enum_basis_finmap ` B" by (auto simp: subset_image_iff)
-  show ?thesis
-  proof cases
-    assume "B = {}" with B have "B' = {}" by simp hence False using B' assms by simp
-    thus ?thesis by simp
-  next
-    assume "B \<noteq> {}" then obtain b where b: "b \<in> B" by auto
-    def NA \<equiv> "\<lambda>n::nat. if n \<in> B
-      then domain ((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) n)
-      else domain ((from_nat::_\<Rightarrow>'a\<Rightarrow>\<^isub>F nat) b)"
-    def NB \<equiv> "\<lambda>n::nat. if n \<in> B
-      then (\<lambda>i. (enum_basis::nat\<Rightarrow>'b set) (((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) n) i))
-      else (\<lambda>i. (enum_basis::nat\<Rightarrow>'b set) (((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) b) i))"
-    have "X = UNION UNIV (\<lambda>i. Pi' (NA i) (NB i))" unfolding B'(2)[symmetric] using b
-      unfolding B
-      by safe
-         (auto simp add: NA_def NB_def enum_basis_finmap_def Let_def o_def split: split_if_asm)
-    moreover
-    have "(\<forall>n. \<forall>i\<in>NA n. (NB n) i \<in> range enum_basis)"
-      using enumerable_basis by (auto simp: topological_basis_def NA_def NB_def)
-    moreover have "(\<forall>n. finite (NA n))" by (simp add: NA_def)
-    ultimately show ?thesis by auto
-  qed
-qed
-
-lemma open_imp_ex_UNION:
-  fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
-  assumes "open X" assumes "X \<noteq> {}"
-  shows "\<exists>A::nat\<Rightarrow>'a set. \<exists>B::nat\<Rightarrow>('a \<Rightarrow> 'b set) . X = UNION UNIV (\<lambda>i. Pi' (A i) (B i)) \<and>
-    (\<forall>n. \<forall>i\<in>A n. open ((B n) i)) \<and> (\<forall>n. finite (A n))"
-  using open_imp_ex_UNION_of_enum[OF assms]
-  apply auto
-  apply (rule_tac x = A in exI)
-  apply (rule_tac x = B in exI)
-  apply (auto simp: open_enum_basis)
-  done
-
-lemma open_basisE:
-  assumes "open X" assumes "X \<noteq> {}"
-  obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
-  "X = UNION UNIV (\<lambda>i. Pi' (A i) (B i))" "\<And>n i. i\<in>A n \<Longrightarrow> open ((B n) i)" "\<And>n. finite (A n)"
-  using open_imp_ex_UNION[OF assms] by auto
-
-lemma open_basis_of_enumE:
-  assumes "open X" assumes "X \<noteq> {}"
-  obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
-  "X = UNION UNIV (\<lambda>i. Pi' (A i) (B i))" "\<And>n i. i\<in>A n \<Longrightarrow> (B n) i \<in> range enum_basis"
-  "\<And>n. finite (A n)"
-  using open_imp_ex_UNION_of_enum[OF assms] by auto
-
-instance proof qed (blast intro: finmap_topological_basis)
+instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap)
 
 end
 
@@ -746,16 +688,12 @@
 proof safe
   fix y assume "y \<in> sets N"
   have "A -` y = (\<Union>{A -` y \<inter> {x. domain x = J}|J. finite J})" by auto
-  hence "A -` y \<inter> space (PiF I M) = (\<Union>n. A -` y \<inter> space (PiF ({set (from_nat n)}\<inter>I) M))"
-    apply (auto simp: space_PiF Pi'_def)
-  proof -
-    case goal1
+  { fix x::"'a \<Rightarrow>\<^isub>F 'b"
     from finite_list[of "domain x"] obtain xs where "set xs = domain x" by auto
-    thus ?case
-      apply (intro exI[where x="to_nat xs"])
-      apply auto
-      done
-  qed
+    hence "\<exists>n. domain x = set (from_nat n)"
+      by (intro exI[where x="to_nat xs"]) auto }
+  hence "A -` y \<inter> space (PiF I M) = (\<Union>n. A -` y \<inter> space (PiF ({set (from_nat n)}\<inter>I) M))"
+    by (auto simp: space_PiF Pi'_def)
   also have "\<dots> \<in> sets (PiF I M)"
     apply (intro sets.Int sets.countable_nat_UN subsetI, safe)
     apply (case_tac "set (from_nat i) \<in> I")
@@ -928,16 +866,6 @@
   qed simp
 qed
 
-lemma sets_subspaceI:
-  assumes "A \<inter> space M \<in> sets M"
-  assumes "B \<in> sets M"
-  shows "A \<inter> B \<in> sets M" using assms
-proof -
-  have "A \<inter> B = (A \<inter> space M) \<inter> B"
-    using assms sets.sets_into_space by auto
-  thus ?thesis using assms by auto
-qed
-
 lemma space_PiF_singleton_eq_product:
   assumes "finite I"
   shows "space (PiF {I} M) = (\<Pi>' i\<in>I. space (M i))"
@@ -1075,49 +1003,49 @@
     by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
 qed
 
-lemma enumerable_sigma_fprod_algebra_sigma_eq:
+lemma sets_PiF_eq_sigma_union_closed_basis_single:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
   shows "sets (PiF {I} (\<lambda>_. borel)) = sigma_sets (space (PiF {I} (\<lambda>_. borel)))
-    {Pi' I F |F. (\<forall>i\<in>I. F i \<in> range enum_basis)}"
+    {Pi' I F |F. (\<forall>i\<in>I. F i \<in> union_closed_basis)}"
 proof -
   from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   show ?thesis
   proof (rule sigma_fprod_algebra_sigma_eq)
     show "finite I" by simp
     show "I \<noteq> {}" by fact
-    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> range enum_basis"
+    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
       using S by simp_all
-    show "range enum_basis \<subseteq> Pow (space borel)" by simp
-    show "sets borel = sigma_sets (space borel) (range enum_basis)"
-      by (simp add: borel_eq_enum_basis)
+    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
+    show "sets borel = sigma_sets (space borel) union_closed_basis"
+      by (simp add: borel_eq_union_closed_basis)
   qed
 qed
 
-text {* adapted from @{thm enumerable_sigma_fprod_algebra_sigma_eq} *}
+text {* adapted from @{thm sets_PiF_eq_sigma_union_closed_basis_single} *}
 
-lemma enumerable_sigma_prod_algebra_sigma_eq:
+lemma sets_PiM_eq_sigma_union_closed_basis:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
   shows "sets (PiM I (\<lambda>_. borel)) = sigma_sets (space (PiM I (\<lambda>_. borel)))
-    {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> range enum_basis}"
+    {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> union_closed_basis}"
 proof -
   from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   show ?thesis
   proof (rule sigma_prod_algebra_sigma_eq)
     show "finite I" by simp note[[show_types]]
-    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> range enum_basis"
+    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
       using S by simp_all
-    show "range enum_basis \<subseteq> Pow (space borel)" by simp
-    show "sets borel = sigma_sets (space borel) (range enum_basis)"
-      by (simp add: borel_eq_enum_basis)
+    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
+    show "sets borel = sigma_sets (space borel) union_closed_basis"
+      by (simp add: borel_eq_union_closed_basis)
   qed
 qed
 
 lemma product_open_generates_sets_PiF_single:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
-  shows "sets (PiF {I} (\<lambda>_. borel::'b::enumerable_basis measure)) =
+  shows "sets (PiF {I} (\<lambda>_. borel::'b::countable_basis_space 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
@@ -1126,7 +1054,7 @@
     show "finite I" by simp
     show "I \<noteq> {}" by fact
     show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
-      using S by (auto simp: open_enum_basis)
+      using S by (auto simp: open_union_closed_basis)
     show "Collect open \<subseteq> Pow (space borel)" by simp
     show "sets borel = sigma_sets (space borel) (Collect open)"
       by (simp add: borel_def)
@@ -1136,7 +1064,7 @@
 lemma product_open_generates_sets_PiM:
   assumes "I \<noteq> {}"
   assumes [simp]: "finite I"
-  shows "sets (PiM I (\<lambda>_. borel::'b::enumerable_basis measure)) =
+  shows "sets (PiM I (\<lambda>_. borel::'b::countable_basis_space 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
@@ -1144,7 +1072,7 @@
   proof (rule sigma_prod_algebra_sigma_eq)
     show "finite I" by simp note[[show_types]]
     fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
-      using S by (auto simp: open_enum_basis)
+      using S by (auto simp: open_union_closed_basis)
     show "Collect open \<subseteq> Pow (space borel)" by simp
     show "sets borel = sigma_sets (space borel) (Collect open)"
       by (simp add: borel_def)
@@ -1155,88 +1083,62 @@
 
 lemma borel_eq_PiF_borel:
   shows "(borel :: ('i::countable \<Rightarrow>\<^isub>F 'a::polish_space) measure) =
-  PiF (Collect finite) (\<lambda>_. borel :: 'a measure)"
-proof (rule measure_eqI)
-  have C: "Collect finite \<noteq> {}" by auto
-  show "sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure) = sets (PiF (Collect finite) (\<lambda>_. borel))"
-  proof
-    show "sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure) \<subseteq> sets (PiF (Collect finite) (\<lambda>_. borel))"
-      apply (simp add: borel_def sets_PiF)
-    proof (rule sigma_sets_mono, safe, cases)
-      fix X::"('i \<Rightarrow>\<^isub>F 'a) set" assume "open X" "X \<noteq> {}"
-      from open_basisE[OF this] guess NA NB . note N = this
-      hence "X = (\<Union>i. Pi' (NA i) (NB i))" by simp
-      also have "\<dots> \<in>
-        sigma_sets UNIV {Pi' J S |S J. finite J \<and> S \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
-        using N by (intro Union sigma_sets.Basic) blast
-      finally show "X \<in> sigma_sets UNIV
-        {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}" .
-    qed (auto simp: Empty)
+    PiF (Collect finite) (\<lambda>_. borel :: 'a measure)"
+  unfolding borel_def PiF_def
+proof (rule measure_eqI, clarsimp, rule sigma_sets_eqI)
+  fix a::"('i \<Rightarrow>\<^isub>F 'a) set" assume "a \<in> Collect open" hence "open a" by simp
+  then obtain B' where B': "B'\<subseteq>basis_finmap" "a = \<Union>B'"
+    using finmap_topological_basis by (force simp add: topological_basis_def)
+  have "a \<in> sigma UNIV {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
+    unfolding `a = \<Union>B'`
+  proof (rule sets.countable_Union)
+    from B' countable_basis_finmap show "countable B'" by (metis countable_subset)
   next
-    show "sets (PiF (Collect finite) (\<lambda>_. borel)) \<subseteq> sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure)"
+    show "B' \<subseteq> sets (sigma UNIV
+      {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)})" (is "_ \<subseteq> sets ?s")
     proof
-      fix x assume x: "x \<in> sets (PiF (Collect finite::'i set set) (\<lambda>_. borel::'a measure))"
-      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets.sets_into_space)
-      let ?x = "\<lambda>J. x \<inter> {x. domain x = J}"
-      have "x = \<Union>{?x J |J. finite J}" by auto
-      also have "\<dots> \<in> sets borel"
-      proof (rule countable_finite_comprehension, assumption)
-        fix J::"'i set" assume "finite J"
-        { assume ef: "J = {}"
-          { assume e: "?x J = {}"
-            hence "?x J \<in> sets borel" by simp
-          } moreover {
-            assume "?x J \<noteq> {}"
-            then obtain f where "f \<in> x" "domain f = {}" using ef by auto
-            hence "?x J = {f}" using `J = {}`
-              by (auto simp: finmap_eq_iff)
-            also have "{f} \<in> sets borel" by simp
-            finally have "?x J \<in> sets borel" .
-          } ultimately have "?x J \<in> sets borel" by blast
-        } moreover {
-          assume "J \<noteq> ({}::'i set)"
-          from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'a set" . note S = this
-          have "(?x J) = x \<inter> {m. domain m \<in> {J}}" by auto
-          also have "\<dots> \<in> sets (PiF {J} (\<lambda>_. borel))"
-            using x by (rule restrict_sets_measurable) (auto simp: `finite J`)
-          also have "\<dots> = sigma_sets (space (PiF {J} (\<lambda>_. borel)))
-            {Pi' (J) F |F. (\<forall>j\<in>J. F j \<in> range enum_basis)}"
-            (is "_ = sigma_sets _ ?P")
-            by (rule enumerable_sigma_fprod_algebra_sigma_eq[OF `J \<noteq> {}` `finite J`])
-          also have "\<dots> \<subseteq> sets borel"
-          proof
-            fix x
-            assume "x \<in> sigma_sets (space (PiF {J} (\<lambda>_. borel))) ?P"
-            thus "x \<in> sets borel"
-            proof (rule sigma_sets.induct, safe)
-              fix F::"'i \<Rightarrow> 'a set"
-              assume "\<forall>j\<in>J. F j \<in> range enum_basis"
-              hence "Pi' J F \<in> range enum_basis_finmap"
-                unfolding range_enum_basis_eq
-                by (auto simp: `finite J` intro!: exI[where x=J] exI[where x=F])
-              hence "open (Pi' (J) F)" by (rule range_enum_basis_finmap_imp_open)
-              thus "Pi' (J) F \<in> sets borel" by simp
-            next
-              fix a::"('i \<Rightarrow>\<^isub>F 'a) set"
-              have "space (PiF {J::'i set} (\<lambda>_. borel::'a measure)) =
-                Pi' (J) (\<lambda>_. UNIV)"
-                by (auto simp: space_PiF product_def)
-              moreover have "open (Pi' (J::'i set) (\<lambda>_. UNIV::'a set))"
-                by (intro open_Pi'I) auto
-              ultimately
-              have "space (PiF {J::'i set} (\<lambda>_. borel::'a measure)) \<in> sets borel"
-                by simp
-              moreover
-              assume "a \<in> sets borel"
-              ultimately show "space (PiF {J} (\<lambda>_. borel)) - a \<in> sets borel" ..
-            qed auto
-          qed
-          finally have "(?x J) \<in> sets borel" .
-        } ultimately show "(?x J) \<in> sets borel" by blast
-      qed
-      finally show "x \<in> sets (borel)" .
+      fix x assume "x \<in> B'" with B' have "x \<in> basis_finmap" by auto
+      then obtain J X where "x = Pi' J X" "finite J" "X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)"
+        by (auto simp: basis_finmap_def open_union_closed_basis)
+      thus "x \<in> sets ?s" by auto
     qed
   qed
+  thus "a \<in> sigma_sets UNIV {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
+    by simp
+next
+  fix b::"('i \<Rightarrow>\<^isub>F 'a) set"
+  assume "b \<in> {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
+  hence b': "b \<in> sets (Pi\<^isub>F (Collect finite) (\<lambda>_. borel))" by (auto simp: sets_PiF borel_def)
+  let ?b = "\<lambda>J. b \<inter> {x. domain x = J}"
+  have "b = \<Union>((\<lambda>J. ?b J) ` Collect finite)" by auto
+  also have "\<dots> \<in> sets borel"
+  proof (rule sets.countable_Union, safe)
+    fix J::"'i set" assume "finite J"
+    { assume ef: "J = {}"
+      have "?b J \<in> sets borel"
+      proof cases
+        assume "?b J \<noteq> {}"
+        then obtain f where "f \<in> b" "domain f = {}" using ef by auto
+        hence "?b J = {f}" using `J = {}`
+          by (auto simp: finmap_eq_iff)
+        also have "{f} \<in> sets borel" by simp
+        finally show ?thesis .
+      qed simp
+    } moreover {
+      assume "J \<noteq> ({}::'i set)"
+      have "(?b J) = b \<inter> {m. domain m \<in> {J}}" by auto
+      also have "\<dots> \<in> sets (PiF {J} (\<lambda>_. borel))"
+        using b' by (rule restrict_sets_measurable) (auto simp: `finite J`)
+      also have "\<dots> = sigma_sets (space (PiF {J} (\<lambda>_. borel)))
+        {Pi' (J) F |F. (\<forall>j\<in>J. F j \<in> Collect open)}"
+        (is "_ = sigma_sets _ ?P")
+       by (rule product_open_generates_sets_PiF_single[OF `J \<noteq> {}` `finite J`])
+      also have "\<dots> \<subseteq> sigma_sets UNIV (Collect open)"
+        by (intro sigma_sets_mono'') (auto intro!: open_Pi'I simp: space_PiF)
+      finally have "(?b J) \<in> sets borel" by (simp add: borel_def)
+    } ultimately show "(?b J) \<in> sets borel" by blast
+  qed (simp add: countable_Collect_finite)
+  finally show "b \<in> sigma_sets UNIV (Collect open)" by (simp add: borel_def)
 qed (simp add: emeasure_sigma borel_def PiF_def)
 
 subsection {* Isomorphism between Functions and Finite Maps *}
diff -r de72bbe42190 -r dea9363887a6 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -178,7 +178,7 @@
 
 lemma prod_algebra_sets_into_space:
   "prod_algebra I M \<subseteq> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
-  using assms by (auto simp: prod_emb_def prod_algebra_def)
+  by (auto simp: prod_emb_def prod_algebra_def)
 
 lemma prod_algebra_eq_finite:
   assumes I: "finite I"
diff -r de72bbe42190 -r dea9363887a6 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -550,7 +550,7 @@
 hide_const (open) finmap_of
 hide_const (open) proj
 hide_const (open) domain
-hide_const (open) enum_basis_finmap
+hide_const (open) basis_finmap
 
 sublocale polish_projective \<subseteq> P!: prob_space "(lim\<^isub>B I P)"
 proof
diff -r de72bbe42190 -r dea9363887a6 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Probability/Regularity.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -104,7 +104,7 @@
 qed
 
 lemma
-  fixes M::"'a::{enumerable_basis, complete_space} measure"
+  fixes M::"'a::{countable_basis_space, complete_space} measure"
   assumes sb: "sets M = sets borel"
   assumes "emeasure M (space M) \<noteq> \<infinity>"
   assumes "B \<in> sets borel"
@@ -124,43 +124,48 @@
     (\<And>e. e > 0 \<Longrightarrow> \<exists>B. A \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M A + ereal e) \<Longrightarrow> ?outer A"
     by (rule ereal_approx_INF)
        (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
-  from countable_dense_setE guess x::"nat \<Rightarrow> 'a"  . note x = this
+  from countable_dense_setE guess X::"'a set"  . note X = this
   {
     fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
-    with x[OF this]
-    have x: "space M = (\<Union>n. cball (x n) r)"
+    with X(2)[OF this]
+    have x: "space M = (\<Union>x\<in>X. cball x r)"
       by (auto simp add: sU) (metis dist_commute order_less_imp_le)
-    have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r))"
+    let ?U = "\<Union>k. (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)"
+    have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) ----> M ?U"
       by (rule Lim_emeasure_incseq)
         (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
-    also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
-      unfolding x by force
-    finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
+    also have "?U = space M"
+    proof safe
+      fix x from X(2)[OF open_ball[of x r]] `r > 0` obtain d where d: "d\<in>X" "d \<in> ball x r" by auto
+      show "x \<in> ?U"
+        using X(1) d by (auto intro!: exI[where x="to_nat_on X d"] simp: dist_commute Bex_def)
+    qed (simp add: sU)
+    finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) ----> M (space M)" .
   } note M_space = this
   {
     fix e ::real and n :: nat assume "e > 0" "n > 0"
     hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
     from M_space[OF `1/n>0`]
-    have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
+    have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)"
       unfolding emeasure_eq_measure by simp
     from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
-    obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
+    obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) <
       e * 2 powr -n"
       by auto
-    hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
+    hence "measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>
       measure M (space M) - e * 2 powr -real n"
       by (auto simp: dist_real_def)
-    hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
+    hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>
       measure M (space M) - e * 2 powr - real n" ..
   } note k=this
   hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
-    measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
+    measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
     by blast
   then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
-    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
+    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
     apply atomize_elim unfolding bchoice_iff .
   hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
-    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
+    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
     unfolding Ball_def by blast
   have approx_space:
     "\<And>e. e > 0 \<Longrightarrow>
@@ -168,7 +173,7 @@
       (is "\<And>e. _ \<Longrightarrow> ?thesis e")
   proof -
     fix e :: real assume "e > 0"
-    def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
+    def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n)"
     have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
     hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
     from k[OF `e > 0` zero_less_Suc]
@@ -202,7 +207,7 @@
       show "complete K" using `closed K` by (simp add: complete_eq_closed)
       fix e'::real assume "0 < e'"
       from nat_approx_posE[OF this] guess n . note n = this
-      let ?k = "x ` {0..k e (Suc n)}"
+      let ?k = "from_nat_into X ` {0..k e (Suc n)}"
       have "finite ?k" by simp
       moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
       ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
diff -r de72bbe42190 -r dea9363887a6 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 27 11:29:47 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 27 13:48:40 2012 +0100
@@ -10,7 +10,7 @@
 theory Sigma_Algebra
 imports
   Complex_Main
-  "~~/src/HOL/Library/Countable"
+  "~~/src/HOL/Library/Countable_Set"
   "~~/src/HOL/Library/FuncSet"
   "~~/src/HOL/Library/Indicator_Function"
   "~~/src/HOL/Library/Extended_Real"
@@ -298,6 +298,17 @@
   show ?thesis unfolding * ** ..
 qed
 
+lemma (in sigma_algebra) countable_Union [intro]:
+  assumes "countable X" "X \<subseteq> M" shows "Union X \<in> M"
+proof cases
+  assume "X \<noteq> {}"
+  hence "\<Union>X = (\<Union>n. from_nat_into X n)"
+    using assms by (auto intro: from_nat_into) (metis from_nat_into_surj)
+  also have "\<dots> \<in> M" using assms
+    by (auto intro!: countable_nat_UN) (metis `X \<noteq> {}` from_nat_into set_mp)
+  finally show ?thesis .
+qed simp
+
 lemma (in sigma_algebra) countable_UN[intro]:
   fixes A :: "'i::countable \<Rightarrow> 'a set"
   assumes "A`X \<subseteq> M"
@@ -1100,6 +1111,30 @@
   "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
   by (auto intro!: sigma_sets_subseteq)
 
+lemma sigma_sets_mono'':
+  assumes "A \<in> sigma_sets C D"
+  assumes "B \<subseteq> D"
+  assumes "D \<subseteq> Pow C"
+  shows "sigma_sets A B \<subseteq> sigma_sets C D"
+proof
+  fix x assume "x \<in> sigma_sets A B"
+  thus "x \<in> sigma_sets C D"
+  proof induct
+    case (Basic a) with assms have "a \<in> D" by auto
+    thus ?case ..
+  next
+    case Empty show ?case by (rule sigma_sets.Empty)
+  next
+    from assms have "A \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`])
+    moreover case (Compl a) hence "a \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`])
+    ultimately have "A - a \<in> sets (sigma C D)" ..
+    thus ?case by (subst (asm) sets_measure_of[OF `D \<subseteq> Pow C`])
+  next
+    case (Union a)
+    thus ?case by (intro sigma_sets.Union)
+  qed
+qed
+
 lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
   by auto