based countable topological basis on Countable_Set
authorimmler
Tue Nov 27 13:48:40 2012 +0100 (2012-11-27)
changeset 50245dea9363887a6
parent 50244 de72bbe42190
child 50246 4df875d326ee
child 50247 491c5c81c2e8
based countable topological basis on Countable_Set
src/HOL/Library/Countable_Set.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Discrete_Topology.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/Probability/Regularity.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Library/Countable_Set.thy	Tue Nov 27 11:29:47 2012 +0100
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue Nov 27 13:48:40 2012 +0100
     1.3 @@ -235,6 +235,12 @@
     1.4      by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
     1.5  qed
     1.6  
     1.7 +lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
     1.8 +  using finite_list by auto
     1.9 +
    1.10 +lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
    1.11 +  by (simp add: Collect_finite_eq_lists)
    1.12 +
    1.13  subsection {* Misc lemmas *}
    1.14  
    1.15  lemma countable_all:
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 27 11:29:47 2012 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 27 13:48:40 2012 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4  imports
     2.5    SEQ
     2.6    "~~/src/HOL/Library/Diagonal_Subsequence"
     2.7 -  "~~/src/HOL/Library/Countable"
     2.8 +  "~~/src/HOL/Library/Countable_Set"
     2.9    Linear_Algebra
    2.10    "~~/src/HOL/Library/Glbs"
    2.11    Norm_Arith
    2.12 @@ -71,147 +71,160 @@
    2.13    using assms
    2.14    by (simp add: topological_basis_def)
    2.15  
    2.16 +lemma basis_dense:
    2.17 +  fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a"
    2.18 +  assumes "topological_basis B"
    2.19 +  assumes choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
    2.20 +  shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
    2.21 +proof (intro allI impI)
    2.22 +  fix X::"'a set" assume "open X" "X \<noteq> {}"
    2.23 +  from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
    2.24 +  guess B' . note B' = this
    2.25 +  thus "\<exists>B'\<in>B. f B' \<in> X" by (auto intro!: choosefrom_basis)
    2.26 +qed
    2.27 +
    2.28  end
    2.29  
    2.30 -subsection {* Enumerable Basis *}
    2.31 -
    2.32 -locale enumerates_basis =
    2.33 -  fixes f::"nat \<Rightarrow> 'a::topological_space set"
    2.34 -  assumes enumerable_basis: "topological_basis (range f)"
    2.35 +subsection {* Countable Basis *}
    2.36 +
    2.37 +locale countable_basis =
    2.38 +  fixes B::"'a::topological_space set set"
    2.39 +  assumes is_basis: "topological_basis B"
    2.40 +  assumes countable_basis: "countable B"
    2.41  begin
    2.42  
    2.43 -lemma open_enumerable_basis_ex:
    2.44 -  assumes "open X"
    2.45 -  shows "\<exists>N. X = (\<Union>n\<in>N. f n)"
    2.46 -proof -
    2.47 -  from enumerable_basis assms obtain B' where "B' \<subseteq> range f" "X = Union B'"
    2.48 -    unfolding topological_basis_def by blast
    2.49 -  hence "Union B' = (\<Union>n\<in>{n. f n \<in> B'}. f n)" by auto
    2.50 -  with `X = Union B'` show ?thesis by blast
    2.51 -qed
    2.52 -
    2.53 -lemma open_enumerable_basisE:
    2.54 +lemma open_countable_basis_ex:
    2.55    assumes "open X"
    2.56 -  obtains N where "X = (\<Union>n\<in>N. f n)"
    2.57 -  using assms open_enumerable_basis_ex by (atomize_elim) simp
    2.58 -
    2.59 -lemma countable_dense_set:
    2.60 -  shows "\<exists>x::nat \<Rightarrow> 'a. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
    2.61 +  shows "\<exists>B' \<subseteq> B. X = Union B'"
    2.62 +  using assms countable_basis is_basis unfolding topological_basis_def by blast
    2.63 +
    2.64 +lemma open_countable_basisE:
    2.65 +  assumes "open X"
    2.66 +  obtains B' where "B' \<subseteq> B" "X = Union B'"
    2.67 +  using assms open_countable_basis_ex by (atomize_elim) simp
    2.68 +
    2.69 +lemma countable_dense_exists:
    2.70 +  shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
    2.71  proof -
    2.72 -  def x \<equiv> "\<lambda>n. (SOME x::'a. x \<in> f n)"
    2.73 -  have x: "\<And>n. f n \<noteq> ({}::'a set) \<Longrightarrow> x n \<in> f n" unfolding x_def
    2.74 -    by (rule someI_ex) auto
    2.75 -  have "\<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
    2.76 -  proof (intro allI impI)
    2.77 -    fix y::"'a set" assume "open y" "y \<noteq> {}"
    2.78 -    from open_enumerable_basisE[OF `open y`] guess N . note N = this
    2.79 -    obtain n where n: "n \<in> N" "f n \<noteq> ({}::'a set)"
    2.80 -    proof (atomize_elim, rule ccontr, clarsimp)
    2.81 -      assume "\<forall>n. n \<in> N \<longrightarrow> f n = ({}::'a set)"
    2.82 -      hence "(\<Union>n\<in>N. f n) = (\<Union>n\<in>N. {}::'a set)"
    2.83 -        by (intro UN_cong) auto
    2.84 -      hence "y = {}" unfolding N by simp
    2.85 -      with `y \<noteq> {}` show False by auto
    2.86 -    qed
    2.87 -    with x N n have "x n \<in> y" by auto
    2.88 -    thus "\<exists>n. x n \<in> y" ..
    2.89 -  qed
    2.90 -  thus ?thesis by blast
    2.91 +  let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
    2.92 +  have "countable (?f ` B)" using countable_basis by simp
    2.93 +  with basis_dense[OF is_basis, of ?f] show ?thesis
    2.94 +    by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI)
    2.95  qed
    2.96  
    2.97  lemma countable_dense_setE:
    2.98 -  obtains x :: "nat \<Rightarrow> 'a"
    2.99 -  where "\<And>y. open y \<Longrightarrow> y \<noteq> {} \<Longrightarrow> \<exists>n. x n \<in> y"
   2.100 -  using countable_dense_set by blast
   2.101 -
   2.102 -text {* Construction of an increasing sequence approximating open sets, therefore enumeration of
   2.103 -  basis which is closed under union. *}
   2.104 -
   2.105 -definition enum_basis::"nat \<Rightarrow> 'a set"
   2.106 -  where "enum_basis n = \<Union>(set (map f (from_nat n)))"
   2.107 -
   2.108 -lemma enum_basis_basis: "topological_basis (range enum_basis)"
   2.109 +  obtains D :: "'a set"
   2.110 +  where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
   2.111 +  using countable_dense_exists by blast
   2.112 +
   2.113 +text {* Construction of an increasing sequence approximating open sets,
   2.114 +  therefore basis which is closed under union. *}
   2.115 +
   2.116 +definition union_closed_basis::"'a set set" where
   2.117 +  "union_closed_basis = (\<lambda>l. \<Union>set l) ` lists B"
   2.118 +
   2.119 +lemma basis_union_closed_basis: "topological_basis union_closed_basis"
   2.120  proof (rule topological_basisI)
   2.121    fix O' and x::'a assume "open O'" "x \<in> O'"
   2.122 -  from topological_basisE[OF enumerable_basis this] guess B' . note B' = this
   2.123 -  moreover then obtain n where "B' = f n" by auto
   2.124 -  moreover hence "B' = enum_basis (to_nat [n])" by (auto simp: enum_basis_def)
   2.125 -  ultimately show "\<exists>B'\<in>range enum_basis. x \<in> B' \<and> B' \<subseteq> O'" by blast
   2.126 +  from topological_basisE[OF is_basis this] guess B' . note B' = this
   2.127 +  thus "\<exists>B'\<in>union_closed_basis. x \<in> B' \<and> B' \<subseteq> O'" unfolding union_closed_basis_def
   2.128 +    by (auto intro!: bexI[where x="[B']"])
   2.129  next
   2.130 -  fix B' assume "B' \<in> range enum_basis"
   2.131 -  with topological_basis_open[OF enumerable_basis]
   2.132 -  show "open B'" by (auto simp add: enum_basis_def intro!: open_UN)
   2.133 -qed
   2.134 -
   2.135 -lemmas open_enum_basis = topological_basis_open[OF enum_basis_basis]
   2.136 -
   2.137 -lemma empty_basisI[intro]: "{} \<in> range enum_basis"
   2.138 -proof
   2.139 -  show "{} = enum_basis (to_nat ([]::nat list))" by (simp add: enum_basis_def)
   2.140 -qed rule
   2.141 +  fix B' assume "B' \<in> union_closed_basis"
   2.142 +  thus "open B'"
   2.143 +    using topological_basis_open[OF is_basis]
   2.144 +    by (auto simp: union_closed_basis_def)
   2.145 +qed
   2.146 +
   2.147 +lemma countable_union_closed_basis: "countable union_closed_basis"
   2.148 +  unfolding union_closed_basis_def using countable_basis by simp
   2.149 +
   2.150 +lemmas open_union_closed_basis = topological_basis_open[OF basis_union_closed_basis]
   2.151 +
   2.152 +lemma union_closed_basis_ex:
   2.153 + assumes X: "X \<in> union_closed_basis"
   2.154 + shows "\<exists>B'. finite B' \<and> X = \<Union>B' \<and> B' \<subseteq> B"
   2.155 +proof -
   2.156 +  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)
   2.157 +  thus ?thesis by auto
   2.158 +qed
   2.159 +
   2.160 +lemma union_closed_basisE:
   2.161 +  assumes "X \<in> union_closed_basis"
   2.162 +  obtains B' where "finite B'" "X = \<Union>B'" "B' \<subseteq> B" using union_closed_basis_ex[OF assms] by blast
   2.163 +
   2.164 +lemma union_closed_basisI:
   2.165 +  assumes "finite B'" "X = \<Union>B'" "B' \<subseteq> B"
   2.166 +  shows "X \<in> union_closed_basis"
   2.167 +proof -
   2.168 +  from finite_list[OF `finite B'`] guess l ..
   2.169 +  thus ?thesis using assms unfolding union_closed_basis_def by (auto intro!: image_eqI[where x=l])
   2.170 +qed
   2.171 +
   2.172 +lemma empty_basisI[intro]: "{} \<in> union_closed_basis"
   2.173 +  by (rule union_closed_basisI[of "{}"]) auto
   2.174  
   2.175  lemma union_basisI[intro]:
   2.176 -  assumes "A \<in> range enum_basis" "B \<in> range enum_basis"
   2.177 -  shows "A \<union> B \<in> range enum_basis"
   2.178 -proof -
   2.179 -  from assms obtain a b where "A \<union> B = enum_basis a \<union> enum_basis b" by auto
   2.180 -  also have "\<dots> = enum_basis (to_nat (from_nat a @ from_nat b::nat list))"
   2.181 -    by (simp add: enum_basis_def)
   2.182 -  finally show ?thesis by simp
   2.183 -qed
   2.184 +  assumes "X \<in> union_closed_basis" "Y \<in> union_closed_basis"
   2.185 +  shows "X \<union> Y \<in> union_closed_basis"
   2.186 +  using assms by (auto intro: union_closed_basisI elim!:union_closed_basisE)
   2.187  
   2.188  lemma open_imp_Union_of_incseq:
   2.189    assumes "open X"
   2.190 -  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> range enum_basis"
   2.191 +  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> union_closed_basis"
   2.192  proof -
   2.193 -  interpret E: enumerates_basis enum_basis proof qed (rule enum_basis_basis)
   2.194 -  from E.open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n\<in>N. enum_basis n)" by auto
   2.195 -  hence X: "X = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
   2.196 -  def S \<equiv> "nat_rec (if 0 \<in> N then enum_basis 0 else {})
   2.197 -    (\<lambda>n S. if (Suc n) \<in> N then S \<union> enum_basis (Suc n) else S)"
   2.198 -  have S_simps[simp]:
   2.199 -    "S 0 = (if 0 \<in> N then enum_basis 0 else {})"
   2.200 -    "\<And>n. S (Suc n) = (if (Suc n) \<in> N then S n \<union> enum_basis (Suc n) else S n)"
   2.201 -    by (simp_all add: S_def)
   2.202 -  have "incseq S" by (rule incseq_SucI) auto
   2.203 -  moreover
   2.204 -  have "(\<Union>j. S j) = X" unfolding N
   2.205 -  proof safe
   2.206 -    fix x n assume "n \<in> N" "x \<in> enum_basis n"
   2.207 -    hence "x \<in> S n" by (cases n) auto
   2.208 -    thus "x \<in> (\<Union>j. S j)" by auto
   2.209 -  next
   2.210 -    fix x j
   2.211 -    assume "x \<in> S j"
   2.212 -    thus "x \<in> UNION N enum_basis" by (induct j) (auto split: split_if_asm)
   2.213 -  qed
   2.214 -  moreover have "range S \<subseteq> range enum_basis"
   2.215 -  proof safe
   2.216 -    fix j show "S j \<in> range enum_basis" by (induct j) auto
   2.217 -  qed
   2.218 -  ultimately show ?thesis by auto
   2.219 +  from open_countable_basis_ex[OF `open X`]
   2.220 +  obtain B' where B': "B'\<subseteq>B" "X = \<Union>B'" by auto
   2.221 +  from this(1) countable_basis have "countable B'" by (rule countable_subset)
   2.222 +  show ?thesis
   2.223 +  proof cases
   2.224 +    assume "B' \<noteq> {}"
   2.225 +    def S \<equiv> "\<lambda>n. \<Union>i\<in>{0..n}. from_nat_into B' i"
   2.226 +    have S:"\<And>n. S n = \<Union>{from_nat_into B' i|i. i\<in>{0..n}}" unfolding S_def by force
   2.227 +    have "incseq S" by (force simp: S_def incseq_Suc_iff)
   2.228 +    moreover
   2.229 +    have "(\<Union>j. S j) = X" unfolding B'
   2.230 +    proof safe
   2.231 +      fix x X assume "X \<in> B'" "x \<in> X"
   2.232 +      then obtain n where "X = from_nat_into B' n"
   2.233 +        by (metis `countable B'` from_nat_into_surj)
   2.234 +      also have "\<dots> \<subseteq> S n" by (auto simp: S_def)
   2.235 +      finally show "x \<in> (\<Union>j. S j)" using `x \<in> X` by auto
   2.236 +    next
   2.237 +      fix x n
   2.238 +      assume "x \<in> S n"
   2.239 +      also have "\<dots> = (\<Union>i\<in>{0..n}. from_nat_into B' i)"
   2.240 +        by (simp add: S_def)
   2.241 +      also have "\<dots> \<subseteq> (\<Union>i. from_nat_into B' i)" by auto
   2.242 +      also have "\<dots> \<subseteq> \<Union>B'" using `B' \<noteq> {}` by (auto intro: from_nat_into)
   2.243 +      finally show "x \<in> \<Union>B'" .
   2.244 +    qed
   2.245 +    moreover have "range S \<subseteq> union_closed_basis" using B'
   2.246 +      by (auto intro!: union_closed_basisI[OF _ S] simp: from_nat_into `B' \<noteq> {}`)
   2.247 +    ultimately show ?thesis by auto
   2.248 +  qed (auto simp: B')
   2.249  qed
   2.250  
   2.251  lemma open_incseqE:
   2.252    assumes "open X"
   2.253 -  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> range enum_basis"
   2.254 +  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> union_closed_basis"
   2.255    using open_imp_Union_of_incseq assms by atomize_elim
   2.256  
   2.257  end
   2.258  
   2.259 -class enumerable_basis = topological_space +
   2.260 -  assumes ex_enum_basis: "\<exists>f::nat \<Rightarrow> 'a::topological_space set. topological_basis (range f)"
   2.261 -
   2.262 -sublocale enumerable_basis < enumerates_basis "Eps (topological_basis o range)"
   2.263 -  unfolding o_def
   2.264 -  proof qed (rule someI_ex[OF ex_enum_basis])
   2.265 +class countable_basis_space = topological_space +
   2.266 +  assumes ex_countable_basis:
   2.267 +    "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
   2.268 +
   2.269 +sublocale countable_basis_space < countable_basis "SOME B. countable B \<and> topological_basis B"
   2.270 +  using someI_ex[OF ex_countable_basis] by unfold_locales safe
   2.271  
   2.272  subsection {* Polish spaces *}
   2.273  
   2.274  text {* Textbooks define Polish spaces as completely metrizable.
   2.275    We assume the topology to be complete for a given metric. *}
   2.276  
   2.277 -class polish_space = complete_space + enumerable_basis
   2.278 +class polish_space = complete_space + countable_basis_space
   2.279  
   2.280  subsection {* General notion of a topology as a value *}
   2.281  
   2.282 @@ -5444,35 +5457,36 @@
   2.283    thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
   2.284  qed
   2.285  
   2.286 -instance ordered_euclidean_space \<subseteq> enumerable_basis
   2.287 +instance ordered_euclidean_space \<subseteq> countable_basis_space
   2.288  proof
   2.289    def to_cube \<equiv> "\<lambda>(a, b). {Chi (real_of_rat \<circ> op ! a)<..<Chi (real_of_rat \<circ> op ! b)}::'a set"
   2.290 -  def enum \<equiv> "\<lambda>n. (to_cube (from_nat n)::'a set)"
   2.291 -  have "Ball (range enum) open" unfolding enum_def
   2.292 +  def B \<equiv> "(\<lambda>n. (to_cube (from_nat n)::'a set)) ` UNIV"
   2.293 +  have "countable B" unfolding B_def by simp
   2.294 +  moreover
   2.295 +  have "Ball B open" unfolding B_def
   2.296    proof safe
   2.297      fix n show "open (to_cube (from_nat n))"
   2.298        by (cases "from_nat n::rat list \<times> rat list")
   2.299           (simp add: open_interval to_cube_def)
   2.300    qed
   2.301 -  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>range enum. \<Union>B' = x))"
   2.302 +  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = x))"
   2.303    proof safe
   2.304      fix x::"'a set" assume "open x"
   2.305      def lists \<equiv> "{(a, b) |a b. to_cube (a, b) \<subseteq> x}"
   2.306      from open_UNION[OF `open x`]
   2.307      have "\<Union>(to_cube ` lists) = x" unfolding lists_def to_cube_def
   2.308       by simp
   2.309 -    moreover have "to_cube ` lists \<subseteq> range enum"
   2.310 +    moreover have "to_cube ` lists \<subseteq> B"
   2.311      proof
   2.312        fix x assume "x \<in> to_cube ` lists"
   2.313        then obtain l where "l \<in> lists" "x = to_cube l" by auto
   2.314 -      hence "x = enum (to_nat l)" by (simp add: to_cube_def enum_def)
   2.315 -      thus "x \<in> range enum" by simp
   2.316 +      thus "x \<in> B" by (auto simp add: B_def intro!: image_eqI[where x="to_nat l"])
   2.317      qed
   2.318      ultimately
   2.319 -    show "\<exists>B'\<subseteq>range enum. \<Union>B' = x" by blast
   2.320 +    show "\<exists>B'\<subseteq>B. \<Union>B' = x" by blast
   2.321    qed
   2.322    ultimately
   2.323 -  show "\<exists>f::nat\<Rightarrow>'a set. topological_basis (range f)" unfolding topological_basis_def by blast
   2.324 +  show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
   2.325  qed
   2.326  
   2.327  instance ordered_euclidean_space \<subseteq> polish_space ..
     3.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Nov 27 11:29:47 2012 +0100
     3.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Nov 27 13:48:40 2012 +0100
     3.3 @@ -462,27 +462,32 @@
     3.4    finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
     3.5  qed simp_all
     3.6  
     3.7 -lemma borel_eq_enumerated_basis:
     3.8 -  fixes f::"nat\<Rightarrow>'a::topological_space set"
     3.9 -  assumes "topological_basis (range f)"
    3.10 -  shows "borel = sigma UNIV (range f)"
    3.11 +lemma borel_eq_countable_basis:
    3.12 +  fixes B::"'a::topological_space set set"
    3.13 +  assumes "countable B"
    3.14 +  assumes "topological_basis B"
    3.15 +  shows "borel = sigma UNIV B"
    3.16    unfolding borel_def
    3.17  proof (intro sigma_eqI sigma_sets_eqI, safe)
    3.18 -  interpret enumerates_basis proof qed (rule assms)
    3.19 -  fix x::"'a set" assume "open x"
    3.20 -  from open_enumerable_basisE[OF this] guess N .
    3.21 -  hence x: "x = (\<Union>n. if n \<in> N then f n else {})" by (auto split: split_if_asm)
    3.22 -  also have "\<dots> \<in> sigma_sets UNIV (range f)" by (auto intro!: sigma_sets.Empty Union)
    3.23 -  finally show "x \<in> sigma_sets UNIV (range f)" .
    3.24 +  interpret countable_basis using assms by unfold_locales
    3.25 +  fix X::"'a set" assume "open X"
    3.26 +  from open_countable_basisE[OF this] guess B' . note B' = this
    3.27 +  show "X \<in> sigma_sets UNIV B"
    3.28 +  proof cases
    3.29 +    assume "B' \<noteq> {}"
    3.30 +    thus "X \<in> sigma_sets UNIV B" using assms B'
    3.31 +      by (metis from_nat_into Union_image_eq countable_subset range_from_nat_into
    3.32 +        in_mono sigma_sets.Basic sigma_sets.Union)
    3.33 +  qed (simp add: sigma_sets.Empty B')
    3.34  next
    3.35 -  fix n
    3.36 -  have "open (f n)" by (rule topological_basis_open[OF assms]) simp
    3.37 -  thus "f n \<in> sigma_sets UNIV (Collect open)" by auto
    3.38 +  fix b assume "b \<in> B"
    3.39 +  hence "open b" by (rule topological_basis_open[OF assms(2)])
    3.40 +  thus "b \<in> sigma_sets UNIV (Collect open)" by auto
    3.41  qed simp_all
    3.42  
    3.43 -lemma borel_eq_enum_basis:
    3.44 -  "borel = sigma UNIV (range enum_basis)"
    3.45 -  by (rule borel_eq_enumerated_basis[OF enum_basis_basis])
    3.46 +lemma borel_eq_union_closed_basis:
    3.47 +  "borel = sigma UNIV union_closed_basis"
    3.48 +  by (rule borel_eq_countable_basis[OF countable_union_closed_basis basis_union_closed_basis])
    3.49  
    3.50  lemma borel_measurable_halfspacesI:
    3.51    fixes f :: "'a \<Rightarrow> 'c\<Colon>ordered_euclidean_space"
     4.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Tue Nov 27 11:29:47 2012 +0100
     4.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Tue Nov 27 13:48:40 2012 +0100
     4.3 @@ -48,15 +48,17 @@
     4.4    thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
     4.5  qed
     4.6  
     4.7 -instance discrete :: (countable) enumerable_basis
     4.8 +instance discrete :: (countable) countable_basis_space
     4.9  proof
    4.10 -  have "topological_basis (range (\<lambda>n::nat. {from_nat n::'a discrete}))"
    4.11 +  let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
    4.12 +  have "topological_basis ?B"
    4.13    proof (intro topological_basisI)
    4.14      fix x::"'a discrete" and O' assume "open O'" "x \<in> O'"
    4.15      thus "\<exists>B'\<in>range (\<lambda>n. {from_nat n}). x \<in> B' \<and> B' \<subseteq> O'"
    4.16        by (auto intro: exI[where x="to_nat x"])
    4.17    qed (simp add: open_discrete_def)
    4.18 -  thus "\<exists>f::nat\<Rightarrow>'a discrete set. topological_basis (range f)" by blast
    4.19 +  moreover have "countable ?B" by simp
    4.20 +  ultimately show "\<exists>B::'a discrete set set. countable B \<and> topological_basis B" by blast
    4.21  qed
    4.22  
    4.23  instance discrete :: (countable) polish_space ..
     5.1 --- a/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 11:29:47 2012 +0100
     5.2 +++ b/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 13:48:40 2012 +0100
     5.3 @@ -450,40 +450,41 @@
     5.4  instantiation finmap :: (countable, polish_space) polish_space
     5.5  begin
     5.6  
     5.7 -definition enum_basis_finmap :: "nat \<Rightarrow> ('a \<Rightarrow>\<^isub>F 'b) set" where
     5.8 -  "enum_basis_finmap n =
     5.9 -  (let m = from_nat n::('a \<Rightarrow>\<^isub>F nat) in Pi' (domain m) (enum_basis o (m)\<^isub>F))"
    5.10 +definition basis_finmap::"('a \<Rightarrow>\<^isub>F 'b) set set"
    5.11 +  where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> union_closed_basis)}"
    5.12 +
    5.13 +lemma in_basis_finmapI:
    5.14 +  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
    5.15 +  shows "Pi' I S \<in> basis_finmap"
    5.16 +  using assms unfolding basis_finmap_def by auto
    5.17 +
    5.18 +lemma in_basis_finmapE:
    5.19 +  assumes "x \<in> basis_finmap"
    5.20 +  obtains I S where "x = Pi' I S" "finite I" "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
    5.21 +  using assms unfolding basis_finmap_def by auto
    5.22  
    5.23 -lemma range_enum_basis_eq:
    5.24 -  "range enum_basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> range enum_basis)}"
    5.25 -proof (auto simp: enum_basis_finmap_def[abs_def])
    5.26 -  fix S::"('a \<Rightarrow> 'b set)" and I
    5.27 -  assume "\<forall>i\<in>I. S i \<in> range enum_basis"
    5.28 -  hence "\<forall>i\<in>I. \<exists>n. S i = enum_basis n" by auto
    5.29 -  then obtain n where n: "\<forall>i\<in>I. S i = enum_basis (n i)"
    5.30 -    unfolding bchoice_iff by blast
    5.31 -  assume [simp]: "finite I"
    5.32 -  have "\<exists>fm. domain fm = I \<and> (\<forall>i\<in>I. n i = (fm i))"
    5.33 -    by (rule finmap_choice) auto
    5.34 -  then obtain m where "Pi' I S = Pi' (domain m) (enum_basis o m)"
    5.35 -    using n by (auto simp: Pi'_def)
    5.36 -  hence "Pi' I S = (let m = from_nat (to_nat m) in Pi' (domain m) (enum_basis \<circ> m))"
    5.37 -    by simp
    5.38 -  thus "Pi' I S \<in> range (\<lambda>n. let m = from_nat n in Pi' (domain m) (enum_basis \<circ> m))"
    5.39 -    by blast
    5.40 -qed (metis finite_domain o_apply rangeI)
    5.41 +lemma basis_finmap_eq:
    5.42 +  "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into union_closed_basis ((f)\<^isub>F i))) `
    5.43 +    (UNIV::('a \<Rightarrow>\<^isub>F nat) set)" (is "_ = ?f ` _")
    5.44 +  unfolding basis_finmap_def
    5.45 +proof safe
    5.46 +  fix I::"'a set" and S::"'a \<Rightarrow> 'b set"
    5.47 +  assume "finite I" "\<forall>i\<in>I. S i \<in> union_closed_basis"
    5.48 +  hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on union_closed_basis (S x)))"
    5.49 +    by (force simp: Pi'_def countable_union_closed_basis)
    5.50 +  thus "Pi' I S \<in> range ?f" by simp
    5.51 +qed (metis (mono_tags) empty_basisI equals0D finite_domain from_nat_into)
    5.52  
    5.53 -lemma in_enum_basis_finmapI:
    5.54 -  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> range enum_basis"
    5.55 -  shows "Pi' I S \<in> range enum_basis_finmap"
    5.56 -  using assms unfolding range_enum_basis_eq by auto
    5.57 +lemma countable_basis_finmap: "countable basis_finmap"
    5.58 +  unfolding basis_finmap_eq by simp
    5.59  
    5.60  lemma finmap_topological_basis:
    5.61 -  "topological_basis (range (enum_basis_finmap))"
    5.62 +  "topological_basis basis_finmap"
    5.63  proof (subst topological_basis_iff, safe)
    5.64 -  fix n::nat
    5.65 -  show "open (enum_basis_finmap n::('a \<Rightarrow>\<^isub>F 'b) set)" using enum_basis_basis
    5.66 -    by (auto intro!: open_Pi'I simp: topological_basis_def enum_basis_finmap_def Let_def)
    5.67 +  fix B' assume "B' \<in> basis_finmap"
    5.68 +  thus "open B'"
    5.69 +    by (auto intro!: open_Pi'I topological_basis_open[OF basis_union_closed_basis]
    5.70 +      simp: topological_basis_def basis_finmap_def Let_def)
    5.71  next
    5.72    fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
    5.73    assume "open O'" "x \<in> O'"
    5.74 @@ -491,19 +492,18 @@
    5.75    def e' \<equiv> "e / (card (domain x) + 1)"
    5.76  
    5.77    have "\<exists>B.
    5.78 -    (\<forall>i\<in>domain x. x i \<in> enum_basis (B i) \<and> enum_basis (B i) \<subseteq> ball (x i) e')"
    5.79 +    (\<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)"
    5.80    proof (rule bchoice, safe)
    5.81      fix i assume "i \<in> domain x"
    5.82      have "open (ball (x i) e')" "x i \<in> ball (x i) e'" using e
    5.83        by (auto simp add: e'_def intro!: divide_pos_pos)
    5.84 -    from topological_basisE[OF enum_basis_basis this] guess b' .
    5.85 -    thus "\<exists>y. x i \<in> enum_basis y \<and>
    5.86 -            enum_basis y \<subseteq> ball (x i) e'" by auto
    5.87 +    from topological_basisE[OF basis_union_closed_basis this] guess b' .
    5.88 +    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> ball (x i) e' \<and> y \<in> union_closed_basis" by auto
    5.89    qed
    5.90    then guess B .. note B = this
    5.91 -  def B' \<equiv> "Pi' (domain x) (\<lambda>i. enum_basis (B i)::'b set)"
    5.92 -  hence "B' \<in> range enum_basis_finmap" unfolding B'_def
    5.93 -    by (intro in_enum_basis_finmapI) auto
    5.94 +  def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)"
    5.95 +  hence "B' \<in> basis_finmap" unfolding B'_def using B
    5.96 +    by (intro in_basis_finmapI) auto
    5.97    moreover have "x \<in> B'" unfolding B'_def using B by auto
    5.98    moreover have "B' \<subseteq> O'"
    5.99    proof
   5.100 @@ -516,7 +516,7 @@
   5.101        also have "\<dots> \<le> (\<Sum>i \<in> domain x. e')"
   5.102        proof (rule setsum_mono)
   5.103          fix i assume "i \<in> domain x"
   5.104 -        with `y \<in> B'` B have "y i \<in> enum_basis (B i)"
   5.105 +        with `y \<in> B'` B have "y i \<in> B i"
   5.106            by (simp add: Pi'_def B'_def)
   5.107          hence "y i \<in> ball (x i) e'" using B `domain y = domain x` `i \<in> domain x`
   5.108            by force
   5.109 @@ -528,73 +528,15 @@
   5.110      qed
   5.111    qed
   5.112    ultimately
   5.113 -  show "\<exists>B'\<in>range enum_basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" by blast
   5.114 +  show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" by blast
   5.115  qed
   5.116  
   5.117  lemma range_enum_basis_finmap_imp_open:
   5.118 -  assumes "x \<in> range enum_basis_finmap"
   5.119 +  assumes "x \<in> basis_finmap"
   5.120    shows "open x"
   5.121    using finmap_topological_basis assms by (auto simp: topological_basis_def)
   5.122  
   5.123 -lemma open_imp_ex_UNION_of_enum:
   5.124 -  fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
   5.125 -  assumes "open X" assumes "X \<noteq> {}"
   5.126 -  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>
   5.127 -    (\<forall>n. \<forall>i\<in>A n. (B n) i \<in> range enum_basis) \<and> (\<forall>n. finite (A n))"
   5.128 -proof -
   5.129 -  from `open X` obtain B' where B': "B'\<subseteq>range enum_basis_finmap" "\<Union>B' = X"
   5.130 -    using finmap_topological_basis by (force simp add: topological_basis_def)
   5.131 -  then obtain B where B: "B' = enum_basis_finmap ` B" by (auto simp: subset_image_iff)
   5.132 -  show ?thesis
   5.133 -  proof cases
   5.134 -    assume "B = {}" with B have "B' = {}" by simp hence False using B' assms by simp
   5.135 -    thus ?thesis by simp
   5.136 -  next
   5.137 -    assume "B \<noteq> {}" then obtain b where b: "b \<in> B" by auto
   5.138 -    def NA \<equiv> "\<lambda>n::nat. if n \<in> B
   5.139 -      then domain ((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) n)
   5.140 -      else domain ((from_nat::_\<Rightarrow>'a\<Rightarrow>\<^isub>F nat) b)"
   5.141 -    def NB \<equiv> "\<lambda>n::nat. if n \<in> B
   5.142 -      then (\<lambda>i. (enum_basis::nat\<Rightarrow>'b set) (((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) n) i))
   5.143 -      else (\<lambda>i. (enum_basis::nat\<Rightarrow>'b set) (((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) b) i))"
   5.144 -    have "X = UNION UNIV (\<lambda>i. Pi' (NA i) (NB i))" unfolding B'(2)[symmetric] using b
   5.145 -      unfolding B
   5.146 -      by safe
   5.147 -         (auto simp add: NA_def NB_def enum_basis_finmap_def Let_def o_def split: split_if_asm)
   5.148 -    moreover
   5.149 -    have "(\<forall>n. \<forall>i\<in>NA n. (NB n) i \<in> range enum_basis)"
   5.150 -      using enumerable_basis by (auto simp: topological_basis_def NA_def NB_def)
   5.151 -    moreover have "(\<forall>n. finite (NA n))" by (simp add: NA_def)
   5.152 -    ultimately show ?thesis by auto
   5.153 -  qed
   5.154 -qed
   5.155 -
   5.156 -lemma open_imp_ex_UNION:
   5.157 -  fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
   5.158 -  assumes "open X" assumes "X \<noteq> {}"
   5.159 -  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>
   5.160 -    (\<forall>n. \<forall>i\<in>A n. open ((B n) i)) \<and> (\<forall>n. finite (A n))"
   5.161 -  using open_imp_ex_UNION_of_enum[OF assms]
   5.162 -  apply auto
   5.163 -  apply (rule_tac x = A in exI)
   5.164 -  apply (rule_tac x = B in exI)
   5.165 -  apply (auto simp: open_enum_basis)
   5.166 -  done
   5.167 -
   5.168 -lemma open_basisE:
   5.169 -  assumes "open X" assumes "X \<noteq> {}"
   5.170 -  obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
   5.171 -  "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)"
   5.172 -  using open_imp_ex_UNION[OF assms] by auto
   5.173 -
   5.174 -lemma open_basis_of_enumE:
   5.175 -  assumes "open X" assumes "X \<noteq> {}"
   5.176 -  obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
   5.177 -  "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"
   5.178 -  "\<And>n. finite (A n)"
   5.179 -  using open_imp_ex_UNION_of_enum[OF assms] by auto
   5.180 -
   5.181 -instance proof qed (blast intro: finmap_topological_basis)
   5.182 +instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap)
   5.183  
   5.184  end
   5.185  
   5.186 @@ -746,16 +688,12 @@
   5.187  proof safe
   5.188    fix y assume "y \<in> sets N"
   5.189    have "A -` y = (\<Union>{A -` y \<inter> {x. domain x = J}|J. finite J})" by auto
   5.190 -  hence "A -` y \<inter> space (PiF I M) = (\<Union>n. A -` y \<inter> space (PiF ({set (from_nat n)}\<inter>I) M))"
   5.191 -    apply (auto simp: space_PiF Pi'_def)
   5.192 -  proof -
   5.193 -    case goal1
   5.194 +  { fix x::"'a \<Rightarrow>\<^isub>F 'b"
   5.195      from finite_list[of "domain x"] obtain xs where "set xs = domain x" by auto
   5.196 -    thus ?case
   5.197 -      apply (intro exI[where x="to_nat xs"])
   5.198 -      apply auto
   5.199 -      done
   5.200 -  qed
   5.201 +    hence "\<exists>n. domain x = set (from_nat n)"
   5.202 +      by (intro exI[where x="to_nat xs"]) auto }
   5.203 +  hence "A -` y \<inter> space (PiF I M) = (\<Union>n. A -` y \<inter> space (PiF ({set (from_nat n)}\<inter>I) M))"
   5.204 +    by (auto simp: space_PiF Pi'_def)
   5.205    also have "\<dots> \<in> sets (PiF I M)"
   5.206      apply (intro sets.Int sets.countable_nat_UN subsetI, safe)
   5.207      apply (case_tac "set (from_nat i) \<in> I")
   5.208 @@ -928,16 +866,6 @@
   5.209    qed simp
   5.210  qed
   5.211  
   5.212 -lemma sets_subspaceI:
   5.213 -  assumes "A \<inter> space M \<in> sets M"
   5.214 -  assumes "B \<in> sets M"
   5.215 -  shows "A \<inter> B \<in> sets M" using assms
   5.216 -proof -
   5.217 -  have "A \<inter> B = (A \<inter> space M) \<inter> B"
   5.218 -    using assms sets.sets_into_space by auto
   5.219 -  thus ?thesis using assms by auto
   5.220 -qed
   5.221 -
   5.222  lemma space_PiF_singleton_eq_product:
   5.223    assumes "finite I"
   5.224    shows "space (PiF {I} M) = (\<Pi>' i\<in>I. space (M i))"
   5.225 @@ -1075,49 +1003,49 @@
   5.226      by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
   5.227  qed
   5.228  
   5.229 -lemma enumerable_sigma_fprod_algebra_sigma_eq:
   5.230 +lemma sets_PiF_eq_sigma_union_closed_basis_single:
   5.231    assumes "I \<noteq> {}"
   5.232    assumes [simp]: "finite I"
   5.233    shows "sets (PiF {I} (\<lambda>_. borel)) = sigma_sets (space (PiF {I} (\<lambda>_. borel)))
   5.234 -    {Pi' I F |F. (\<forall>i\<in>I. F i \<in> range enum_basis)}"
   5.235 +    {Pi' I F |F. (\<forall>i\<in>I. F i \<in> union_closed_basis)}"
   5.236  proof -
   5.237    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   5.238    show ?thesis
   5.239    proof (rule sigma_fprod_algebra_sigma_eq)
   5.240      show "finite I" by simp
   5.241      show "I \<noteq> {}" by fact
   5.242 -    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> range enum_basis"
   5.243 +    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
   5.244        using S by simp_all
   5.245 -    show "range enum_basis \<subseteq> Pow (space borel)" by simp
   5.246 -    show "sets borel = sigma_sets (space borel) (range enum_basis)"
   5.247 -      by (simp add: borel_eq_enum_basis)
   5.248 +    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
   5.249 +    show "sets borel = sigma_sets (space borel) union_closed_basis"
   5.250 +      by (simp add: borel_eq_union_closed_basis)
   5.251    qed
   5.252  qed
   5.253  
   5.254 -text {* adapted from @{thm enumerable_sigma_fprod_algebra_sigma_eq} *}
   5.255 +text {* adapted from @{thm sets_PiF_eq_sigma_union_closed_basis_single} *}
   5.256  
   5.257 -lemma enumerable_sigma_prod_algebra_sigma_eq:
   5.258 +lemma sets_PiM_eq_sigma_union_closed_basis:
   5.259    assumes "I \<noteq> {}"
   5.260    assumes [simp]: "finite I"
   5.261    shows "sets (PiM I (\<lambda>_. borel)) = sigma_sets (space (PiM I (\<lambda>_. borel)))
   5.262 -    {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> range enum_basis}"
   5.263 +    {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> union_closed_basis}"
   5.264  proof -
   5.265    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   5.266    show ?thesis
   5.267    proof (rule sigma_prod_algebra_sigma_eq)
   5.268      show "finite I" by simp note[[show_types]]
   5.269 -    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> range enum_basis"
   5.270 +    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
   5.271        using S by simp_all
   5.272 -    show "range enum_basis \<subseteq> Pow (space borel)" by simp
   5.273 -    show "sets borel = sigma_sets (space borel) (range enum_basis)"
   5.274 -      by (simp add: borel_eq_enum_basis)
   5.275 +    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
   5.276 +    show "sets borel = sigma_sets (space borel) union_closed_basis"
   5.277 +      by (simp add: borel_eq_union_closed_basis)
   5.278    qed
   5.279  qed
   5.280  
   5.281  lemma product_open_generates_sets_PiF_single:
   5.282    assumes "I \<noteq> {}"
   5.283    assumes [simp]: "finite I"
   5.284 -  shows "sets (PiF {I} (\<lambda>_. borel::'b::enumerable_basis measure)) =
   5.285 +  shows "sets (PiF {I} (\<lambda>_. borel::'b::countable_basis_space measure)) =
   5.286      sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
   5.287  proof -
   5.288    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   5.289 @@ -1126,7 +1054,7 @@
   5.290      show "finite I" by simp
   5.291      show "I \<noteq> {}" by fact
   5.292      show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
   5.293 -      using S by (auto simp: open_enum_basis)
   5.294 +      using S by (auto simp: open_union_closed_basis)
   5.295      show "Collect open \<subseteq> Pow (space borel)" by simp
   5.296      show "sets borel = sigma_sets (space borel) (Collect open)"
   5.297        by (simp add: borel_def)
   5.298 @@ -1136,7 +1064,7 @@
   5.299  lemma product_open_generates_sets_PiM:
   5.300    assumes "I \<noteq> {}"
   5.301    assumes [simp]: "finite I"
   5.302 -  shows "sets (PiM I (\<lambda>_. borel::'b::enumerable_basis measure)) =
   5.303 +  shows "sets (PiM I (\<lambda>_. borel::'b::countable_basis_space measure)) =
   5.304      sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
   5.305  proof -
   5.306    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   5.307 @@ -1144,7 +1072,7 @@
   5.308    proof (rule sigma_prod_algebra_sigma_eq)
   5.309      show "finite I" by simp note[[show_types]]
   5.310      fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
   5.311 -      using S by (auto simp: open_enum_basis)
   5.312 +      using S by (auto simp: open_union_closed_basis)
   5.313      show "Collect open \<subseteq> Pow (space borel)" by simp
   5.314      show "sets borel = sigma_sets (space borel) (Collect open)"
   5.315        by (simp add: borel_def)
   5.316 @@ -1155,88 +1083,62 @@
   5.317  
   5.318  lemma borel_eq_PiF_borel:
   5.319    shows "(borel :: ('i::countable \<Rightarrow>\<^isub>F 'a::polish_space) measure) =
   5.320 -  PiF (Collect finite) (\<lambda>_. borel :: 'a measure)"
   5.321 -proof (rule measure_eqI)
   5.322 -  have C: "Collect finite \<noteq> {}" by auto
   5.323 -  show "sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure) = sets (PiF (Collect finite) (\<lambda>_. borel))"
   5.324 -  proof
   5.325 -    show "sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure) \<subseteq> sets (PiF (Collect finite) (\<lambda>_. borel))"
   5.326 -      apply (simp add: borel_def sets_PiF)
   5.327 -    proof (rule sigma_sets_mono, safe, cases)
   5.328 -      fix X::"('i \<Rightarrow>\<^isub>F 'a) set" assume "open X" "X \<noteq> {}"
   5.329 -      from open_basisE[OF this] guess NA NB . note N = this
   5.330 -      hence "X = (\<Union>i. Pi' (NA i) (NB i))" by simp
   5.331 -      also have "\<dots> \<in>
   5.332 -        sigma_sets UNIV {Pi' J S |S J. finite J \<and> S \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
   5.333 -        using N by (intro Union sigma_sets.Basic) blast
   5.334 -      finally show "X \<in> sigma_sets UNIV
   5.335 -        {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}" .
   5.336 -    qed (auto simp: Empty)
   5.337 +    PiF (Collect finite) (\<lambda>_. borel :: 'a measure)"
   5.338 +  unfolding borel_def PiF_def
   5.339 +proof (rule measure_eqI, clarsimp, rule sigma_sets_eqI)
   5.340 +  fix a::"('i \<Rightarrow>\<^isub>F 'a) set" assume "a \<in> Collect open" hence "open a" by simp
   5.341 +  then obtain B' where B': "B'\<subseteq>basis_finmap" "a = \<Union>B'"
   5.342 +    using finmap_topological_basis by (force simp add: topological_basis_def)
   5.343 +  have "a \<in> sigma UNIV {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
   5.344 +    unfolding `a = \<Union>B'`
   5.345 +  proof (rule sets.countable_Union)
   5.346 +    from B' countable_basis_finmap show "countable B'" by (metis countable_subset)
   5.347    next
   5.348 -    show "sets (PiF (Collect finite) (\<lambda>_. borel)) \<subseteq> sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure)"
   5.349 +    show "B' \<subseteq> sets (sigma UNIV
   5.350 +      {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)})" (is "_ \<subseteq> sets ?s")
   5.351      proof
   5.352 -      fix x assume x: "x \<in> sets (PiF (Collect finite::'i set set) (\<lambda>_. borel::'a measure))"
   5.353 -      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets.sets_into_space)
   5.354 -      let ?x = "\<lambda>J. x \<inter> {x. domain x = J}"
   5.355 -      have "x = \<Union>{?x J |J. finite J}" by auto
   5.356 -      also have "\<dots> \<in> sets borel"
   5.357 -      proof (rule countable_finite_comprehension, assumption)
   5.358 -        fix J::"'i set" assume "finite J"
   5.359 -        { assume ef: "J = {}"
   5.360 -          { assume e: "?x J = {}"
   5.361 -            hence "?x J \<in> sets borel" by simp
   5.362 -          } moreover {
   5.363 -            assume "?x J \<noteq> {}"
   5.364 -            then obtain f where "f \<in> x" "domain f = {}" using ef by auto
   5.365 -            hence "?x J = {f}" using `J = {}`
   5.366 -              by (auto simp: finmap_eq_iff)
   5.367 -            also have "{f} \<in> sets borel" by simp
   5.368 -            finally have "?x J \<in> sets borel" .
   5.369 -          } ultimately have "?x J \<in> sets borel" by blast
   5.370 -        } moreover {
   5.371 -          assume "J \<noteq> ({}::'i set)"
   5.372 -          from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'a set" . note S = this
   5.373 -          have "(?x J) = x \<inter> {m. domain m \<in> {J}}" by auto
   5.374 -          also have "\<dots> \<in> sets (PiF {J} (\<lambda>_. borel))"
   5.375 -            using x by (rule restrict_sets_measurable) (auto simp: `finite J`)
   5.376 -          also have "\<dots> = sigma_sets (space (PiF {J} (\<lambda>_. borel)))
   5.377 -            {Pi' (J) F |F. (\<forall>j\<in>J. F j \<in> range enum_basis)}"
   5.378 -            (is "_ = sigma_sets _ ?P")
   5.379 -            by (rule enumerable_sigma_fprod_algebra_sigma_eq[OF `J \<noteq> {}` `finite J`])
   5.380 -          also have "\<dots> \<subseteq> sets borel"
   5.381 -          proof
   5.382 -            fix x
   5.383 -            assume "x \<in> sigma_sets (space (PiF {J} (\<lambda>_. borel))) ?P"
   5.384 -            thus "x \<in> sets borel"
   5.385 -            proof (rule sigma_sets.induct, safe)
   5.386 -              fix F::"'i \<Rightarrow> 'a set"
   5.387 -              assume "\<forall>j\<in>J. F j \<in> range enum_basis"
   5.388 -              hence "Pi' J F \<in> range enum_basis_finmap"
   5.389 -                unfolding range_enum_basis_eq
   5.390 -                by (auto simp: `finite J` intro!: exI[where x=J] exI[where x=F])
   5.391 -              hence "open (Pi' (J) F)" by (rule range_enum_basis_finmap_imp_open)
   5.392 -              thus "Pi' (J) F \<in> sets borel" by simp
   5.393 -            next
   5.394 -              fix a::"('i \<Rightarrow>\<^isub>F 'a) set"
   5.395 -              have "space (PiF {J::'i set} (\<lambda>_. borel::'a measure)) =
   5.396 -                Pi' (J) (\<lambda>_. UNIV)"
   5.397 -                by (auto simp: space_PiF product_def)
   5.398 -              moreover have "open (Pi' (J::'i set) (\<lambda>_. UNIV::'a set))"
   5.399 -                by (intro open_Pi'I) auto
   5.400 -              ultimately
   5.401 -              have "space (PiF {J::'i set} (\<lambda>_. borel::'a measure)) \<in> sets borel"
   5.402 -                by simp
   5.403 -              moreover
   5.404 -              assume "a \<in> sets borel"
   5.405 -              ultimately show "space (PiF {J} (\<lambda>_. borel)) - a \<in> sets borel" ..
   5.406 -            qed auto
   5.407 -          qed
   5.408 -          finally have "(?x J) \<in> sets borel" .
   5.409 -        } ultimately show "(?x J) \<in> sets borel" by blast
   5.410 -      qed
   5.411 -      finally show "x \<in> sets (borel)" .
   5.412 +      fix x assume "x \<in> B'" with B' have "x \<in> basis_finmap" by auto
   5.413 +      then obtain J X where "x = Pi' J X" "finite J" "X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)"
   5.414 +        by (auto simp: basis_finmap_def open_union_closed_basis)
   5.415 +      thus "x \<in> sets ?s" by auto
   5.416      qed
   5.417    qed
   5.418 +  thus "a \<in> sigma_sets UNIV {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
   5.419 +    by simp
   5.420 +next
   5.421 +  fix b::"('i \<Rightarrow>\<^isub>F 'a) set"
   5.422 +  assume "b \<in> {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
   5.423 +  hence b': "b \<in> sets (Pi\<^isub>F (Collect finite) (\<lambda>_. borel))" by (auto simp: sets_PiF borel_def)
   5.424 +  let ?b = "\<lambda>J. b \<inter> {x. domain x = J}"
   5.425 +  have "b = \<Union>((\<lambda>J. ?b J) ` Collect finite)" by auto
   5.426 +  also have "\<dots> \<in> sets borel"
   5.427 +  proof (rule sets.countable_Union, safe)
   5.428 +    fix J::"'i set" assume "finite J"
   5.429 +    { assume ef: "J = {}"
   5.430 +      have "?b J \<in> sets borel"
   5.431 +      proof cases
   5.432 +        assume "?b J \<noteq> {}"
   5.433 +        then obtain f where "f \<in> b" "domain f = {}" using ef by auto
   5.434 +        hence "?b J = {f}" using `J = {}`
   5.435 +          by (auto simp: finmap_eq_iff)
   5.436 +        also have "{f} \<in> sets borel" by simp
   5.437 +        finally show ?thesis .
   5.438 +      qed simp
   5.439 +    } moreover {
   5.440 +      assume "J \<noteq> ({}::'i set)"
   5.441 +      have "(?b J) = b \<inter> {m. domain m \<in> {J}}" by auto
   5.442 +      also have "\<dots> \<in> sets (PiF {J} (\<lambda>_. borel))"
   5.443 +        using b' by (rule restrict_sets_measurable) (auto simp: `finite J`)
   5.444 +      also have "\<dots> = sigma_sets (space (PiF {J} (\<lambda>_. borel)))
   5.445 +        {Pi' (J) F |F. (\<forall>j\<in>J. F j \<in> Collect open)}"
   5.446 +        (is "_ = sigma_sets _ ?P")
   5.447 +       by (rule product_open_generates_sets_PiF_single[OF `J \<noteq> {}` `finite J`])
   5.448 +      also have "\<dots> \<subseteq> sigma_sets UNIV (Collect open)"
   5.449 +        by (intro sigma_sets_mono'') (auto intro!: open_Pi'I simp: space_PiF)
   5.450 +      finally have "(?b J) \<in> sets borel" by (simp add: borel_def)
   5.451 +    } ultimately show "(?b J) \<in> sets borel" by blast
   5.452 +  qed (simp add: countable_Collect_finite)
   5.453 +  finally show "b \<in> sigma_sets UNIV (Collect open)" by (simp add: borel_def)
   5.454  qed (simp add: emeasure_sigma borel_def PiF_def)
   5.455  
   5.456  subsection {* Isomorphism between Functions and Finite Maps *}
     6.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 27 11:29:47 2012 +0100
     6.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 27 13:48:40 2012 +0100
     6.3 @@ -178,7 +178,7 @@
     6.4  
     6.5  lemma prod_algebra_sets_into_space:
     6.6    "prod_algebra I M \<subseteq> Pow (\<Pi>\<^isub>E i\<in>I. space (M i))"
     6.7 -  using assms by (auto simp: prod_emb_def prod_algebra_def)
     6.8 +  by (auto simp: prod_emb_def prod_algebra_def)
     6.9  
    6.10  lemma prod_algebra_eq_finite:
    6.11    assumes I: "finite I"
     7.1 --- a/src/HOL/Probability/Projective_Limit.thy	Tue Nov 27 11:29:47 2012 +0100
     7.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Tue Nov 27 13:48:40 2012 +0100
     7.3 @@ -550,7 +550,7 @@
     7.4  hide_const (open) finmap_of
     7.5  hide_const (open) proj
     7.6  hide_const (open) domain
     7.7 -hide_const (open) enum_basis_finmap
     7.8 +hide_const (open) basis_finmap
     7.9  
    7.10  sublocale polish_projective \<subseteq> P!: prob_space "(lim\<^isub>B I P)"
    7.11  proof
     8.1 --- a/src/HOL/Probability/Regularity.thy	Tue Nov 27 11:29:47 2012 +0100
     8.2 +++ b/src/HOL/Probability/Regularity.thy	Tue Nov 27 13:48:40 2012 +0100
     8.3 @@ -104,7 +104,7 @@
     8.4  qed
     8.5  
     8.6  lemma
     8.7 -  fixes M::"'a::{enumerable_basis, complete_space} measure"
     8.8 +  fixes M::"'a::{countable_basis_space, complete_space} measure"
     8.9    assumes sb: "sets M = sets borel"
    8.10    assumes "emeasure M (space M) \<noteq> \<infinity>"
    8.11    assumes "B \<in> sets borel"
    8.12 @@ -124,43 +124,48 @@
    8.13      (\<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"
    8.14      by (rule ereal_approx_INF)
    8.15         (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
    8.16 -  from countable_dense_setE guess x::"nat \<Rightarrow> 'a"  . note x = this
    8.17 +  from countable_dense_setE guess X::"'a set"  . note X = this
    8.18    {
    8.19      fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
    8.20 -    with x[OF this]
    8.21 -    have x: "space M = (\<Union>n. cball (x n) r)"
    8.22 +    with X(2)[OF this]
    8.23 +    have x: "space M = (\<Union>x\<in>X. cball x r)"
    8.24        by (auto simp add: sU) (metis dist_commute order_less_imp_le)
    8.25 -    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))"
    8.26 +    let ?U = "\<Union>k. (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)"
    8.27 +    have "(\<lambda>k. emeasure M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) ----> M ?U"
    8.28        by (rule Lim_emeasure_incseq)
    8.29          (auto intro!: borel_closed bexI simp: closed_cball incseq_def Us sb)
    8.30 -    also have "(\<Union>k. (\<Union>n\<in>{0..k}. cball (x n) r)) = space M"
    8.31 -      unfolding x by force
    8.32 -    finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (x n) r)) ----> M (space M)" .
    8.33 +    also have "?U = space M"
    8.34 +    proof safe
    8.35 +      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
    8.36 +      show "x \<in> ?U"
    8.37 +        using X(1) d by (auto intro!: exI[where x="to_nat_on X d"] simp: dist_commute Bex_def)
    8.38 +    qed (simp add: sU)
    8.39 +    finally have "(\<lambda>k. M (\<Union>n\<in>{0..k}. cball (from_nat_into X n) r)) ----> M (space M)" .
    8.40    } note M_space = this
    8.41    {
    8.42      fix e ::real and n :: nat assume "e > 0" "n > 0"
    8.43      hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
    8.44      from M_space[OF `1/n>0`]
    8.45 -    have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) ----> measure M (space M)"
    8.46 +    have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)"
    8.47        unfolding emeasure_eq_measure by simp
    8.48      from metric_LIMSEQ_D[OF this `0 < e * 2 powr -n`]
    8.49 -    obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n))) (measure M (space M)) <
    8.50 +    obtain k where "dist (measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) <
    8.51        e * 2 powr -n"
    8.52        by auto
    8.53 -    hence "measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
    8.54 +    hence "measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>
    8.55        measure M (space M) - e * 2 powr -real n"
    8.56        by (auto simp: dist_real_def)
    8.57 -    hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge>
    8.58 +    hence "\<exists>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n)) \<ge>
    8.59        measure M (space M) - e * 2 powr - real n" ..
    8.60    } note k=this
    8.61    hence "\<forall>e\<in>{0<..}. \<forall>(n::nat)\<in>{0<..}. \<exists>k.
    8.62 -    measure M (\<Union>i\<in>{0..k}. cball (x i) (1/real n)) \<ge> measure M (space M) - e * 2 powr - real n"
    8.63 +    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"
    8.64      by blast
    8.65    then obtain k where k: "\<forall>e\<in>{0<..}. \<forall>n\<in>{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
    8.66 -    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
    8.67 +    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
    8.68      apply atomize_elim unfolding bchoice_iff .
    8.69    hence k: "\<And>e n. e > 0 \<Longrightarrow> n > 0 \<Longrightarrow> measure M (space M) - e * 2 powr - n
    8.70 -    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (x i) (1 / n))"
    8.71 +    \<le> measure M (\<Union>i\<in>{0..k e n}. cball (from_nat_into X i) (1 / n))"
    8.72      unfolding Ball_def by blast
    8.73    have approx_space:
    8.74      "\<And>e. e > 0 \<Longrightarrow>
    8.75 @@ -168,7 +173,7 @@
    8.76        (is "\<And>e. _ \<Longrightarrow> ?thesis e")
    8.77    proof -
    8.78      fix e :: real assume "e > 0"
    8.79 -    def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (x i) (1 / Suc n)"
    8.80 +    def B \<equiv> "\<lambda>n. \<Union>i\<in>{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n)"
    8.81      have "\<And>n. closed (B n)" by (auto simp: B_def closed_cball)
    8.82      hence [simp]: "\<And>n. B n \<in> sets M" by (simp add: sb)
    8.83      from k[OF `e > 0` zero_less_Suc]
    8.84 @@ -202,7 +207,7 @@
    8.85        show "complete K" using `closed K` by (simp add: complete_eq_closed)
    8.86        fix e'::real assume "0 < e'"
    8.87        from nat_approx_posE[OF this] guess n . note n = this
    8.88 -      let ?k = "x ` {0..k e (Suc n)}"
    8.89 +      let ?k = "from_nat_into X ` {0..k e (Suc n)}"
    8.90        have "finite ?k" by simp
    8.91        moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
    8.92        ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
     9.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 27 11:29:47 2012 +0100
     9.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 27 13:48:40 2012 +0100
     9.3 @@ -10,7 +10,7 @@
     9.4  theory Sigma_Algebra
     9.5  imports
     9.6    Complex_Main
     9.7 -  "~~/src/HOL/Library/Countable"
     9.8 +  "~~/src/HOL/Library/Countable_Set"
     9.9    "~~/src/HOL/Library/FuncSet"
    9.10    "~~/src/HOL/Library/Indicator_Function"
    9.11    "~~/src/HOL/Library/Extended_Real"
    9.12 @@ -298,6 +298,17 @@
    9.13    show ?thesis unfolding * ** ..
    9.14  qed
    9.15  
    9.16 +lemma (in sigma_algebra) countable_Union [intro]:
    9.17 +  assumes "countable X" "X \<subseteq> M" shows "Union X \<in> M"
    9.18 +proof cases
    9.19 +  assume "X \<noteq> {}"
    9.20 +  hence "\<Union>X = (\<Union>n. from_nat_into X n)"
    9.21 +    using assms by (auto intro: from_nat_into) (metis from_nat_into_surj)
    9.22 +  also have "\<dots> \<in> M" using assms
    9.23 +    by (auto intro!: countable_nat_UN) (metis `X \<noteq> {}` from_nat_into set_mp)
    9.24 +  finally show ?thesis .
    9.25 +qed simp
    9.26 +
    9.27  lemma (in sigma_algebra) countable_UN[intro]:
    9.28    fixes A :: "'i::countable \<Rightarrow> 'a set"
    9.29    assumes "A`X \<subseteq> M"
    9.30 @@ -1100,6 +1111,30 @@
    9.31    "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
    9.32    by (auto intro!: sigma_sets_subseteq)
    9.33  
    9.34 +lemma sigma_sets_mono'':
    9.35 +  assumes "A \<in> sigma_sets C D"
    9.36 +  assumes "B \<subseteq> D"
    9.37 +  assumes "D \<subseteq> Pow C"
    9.38 +  shows "sigma_sets A B \<subseteq> sigma_sets C D"
    9.39 +proof
    9.40 +  fix x assume "x \<in> sigma_sets A B"
    9.41 +  thus "x \<in> sigma_sets C D"
    9.42 +  proof induct
    9.43 +    case (Basic a) with assms have "a \<in> D" by auto
    9.44 +    thus ?case ..
    9.45 +  next
    9.46 +    case Empty show ?case by (rule sigma_sets.Empty)
    9.47 +  next
    9.48 +    from assms have "A \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`])
    9.49 +    moreover case (Compl a) hence "a \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`])
    9.50 +    ultimately have "A - a \<in> sets (sigma C D)" ..
    9.51 +    thus ?case by (subst (asm) sets_measure_of[OF `D \<subseteq> Pow C`])
    9.52 +  next
    9.53 +    case (Union a)
    9.54 +    thus ?case by (intro sigma_sets.Union)
    9.55 +  qed
    9.56 +qed
    9.57 +
    9.58  lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
    9.59    by auto
    9.60