src/HOL/Probability/Fin_Map.thy
changeset 50245 dea9363887a6
parent 50244 de72bbe42190
child 50251 227477f17c26
     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 11:29:47 2012 +0100
     1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Tue Nov 27 13:48:40 2012 +0100
     1.3 @@ -450,40 +450,41 @@
     1.4  instantiation finmap :: (countable, polish_space) polish_space
     1.5  begin
     1.6  
     1.7 -definition enum_basis_finmap :: "nat \<Rightarrow> ('a \<Rightarrow>\<^isub>F 'b) set" where
     1.8 -  "enum_basis_finmap n =
     1.9 -  (let m = from_nat n::('a \<Rightarrow>\<^isub>F nat) in Pi' (domain m) (enum_basis o (m)\<^isub>F))"
    1.10 +definition basis_finmap::"('a \<Rightarrow>\<^isub>F 'b) set set"
    1.11 +  where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> union_closed_basis)}"
    1.12 +
    1.13 +lemma in_basis_finmapI:
    1.14 +  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
    1.15 +  shows "Pi' I S \<in> basis_finmap"
    1.16 +  using assms unfolding basis_finmap_def by auto
    1.17 +
    1.18 +lemma in_basis_finmapE:
    1.19 +  assumes "x \<in> basis_finmap"
    1.20 +  obtains I S where "x = Pi' I S" "finite I" "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
    1.21 +  using assms unfolding basis_finmap_def by auto
    1.22  
    1.23 -lemma range_enum_basis_eq:
    1.24 -  "range enum_basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> range enum_basis)}"
    1.25 -proof (auto simp: enum_basis_finmap_def[abs_def])
    1.26 -  fix S::"('a \<Rightarrow> 'b set)" and I
    1.27 -  assume "\<forall>i\<in>I. S i \<in> range enum_basis"
    1.28 -  hence "\<forall>i\<in>I. \<exists>n. S i = enum_basis n" by auto
    1.29 -  then obtain n where n: "\<forall>i\<in>I. S i = enum_basis (n i)"
    1.30 -    unfolding bchoice_iff by blast
    1.31 -  assume [simp]: "finite I"
    1.32 -  have "\<exists>fm. domain fm = I \<and> (\<forall>i\<in>I. n i = (fm i))"
    1.33 -    by (rule finmap_choice) auto
    1.34 -  then obtain m where "Pi' I S = Pi' (domain m) (enum_basis o m)"
    1.35 -    using n by (auto simp: Pi'_def)
    1.36 -  hence "Pi' I S = (let m = from_nat (to_nat m) in Pi' (domain m) (enum_basis \<circ> m))"
    1.37 -    by simp
    1.38 -  thus "Pi' I S \<in> range (\<lambda>n. let m = from_nat n in Pi' (domain m) (enum_basis \<circ> m))"
    1.39 -    by blast
    1.40 -qed (metis finite_domain o_apply rangeI)
    1.41 +lemma basis_finmap_eq:
    1.42 +  "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into union_closed_basis ((f)\<^isub>F i))) `
    1.43 +    (UNIV::('a \<Rightarrow>\<^isub>F nat) set)" (is "_ = ?f ` _")
    1.44 +  unfolding basis_finmap_def
    1.45 +proof safe
    1.46 +  fix I::"'a set" and S::"'a \<Rightarrow> 'b set"
    1.47 +  assume "finite I" "\<forall>i\<in>I. S i \<in> union_closed_basis"
    1.48 +  hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on union_closed_basis (S x)))"
    1.49 +    by (force simp: Pi'_def countable_union_closed_basis)
    1.50 +  thus "Pi' I S \<in> range ?f" by simp
    1.51 +qed (metis (mono_tags) empty_basisI equals0D finite_domain from_nat_into)
    1.52  
    1.53 -lemma in_enum_basis_finmapI:
    1.54 -  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> range enum_basis"
    1.55 -  shows "Pi' I S \<in> range enum_basis_finmap"
    1.56 -  using assms unfolding range_enum_basis_eq by auto
    1.57 +lemma countable_basis_finmap: "countable basis_finmap"
    1.58 +  unfolding basis_finmap_eq by simp
    1.59  
    1.60  lemma finmap_topological_basis:
    1.61 -  "topological_basis (range (enum_basis_finmap))"
    1.62 +  "topological_basis basis_finmap"
    1.63  proof (subst topological_basis_iff, safe)
    1.64 -  fix n::nat
    1.65 -  show "open (enum_basis_finmap n::('a \<Rightarrow>\<^isub>F 'b) set)" using enum_basis_basis
    1.66 -    by (auto intro!: open_Pi'I simp: topological_basis_def enum_basis_finmap_def Let_def)
    1.67 +  fix B' assume "B' \<in> basis_finmap"
    1.68 +  thus "open B'"
    1.69 +    by (auto intro!: open_Pi'I topological_basis_open[OF basis_union_closed_basis]
    1.70 +      simp: topological_basis_def basis_finmap_def Let_def)
    1.71  next
    1.72    fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
    1.73    assume "open O'" "x \<in> O'"
    1.74 @@ -491,19 +492,18 @@
    1.75    def e' \<equiv> "e / (card (domain x) + 1)"
    1.76  
    1.77    have "\<exists>B.
    1.78 -    (\<forall>i\<in>domain x. x i \<in> enum_basis (B i) \<and> enum_basis (B i) \<subseteq> ball (x i) e')"
    1.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)"
    1.80    proof (rule bchoice, safe)
    1.81      fix i assume "i \<in> domain x"
    1.82      have "open (ball (x i) e')" "x i \<in> ball (x i) e'" using e
    1.83        by (auto simp add: e'_def intro!: divide_pos_pos)
    1.84 -    from topological_basisE[OF enum_basis_basis this] guess b' .
    1.85 -    thus "\<exists>y. x i \<in> enum_basis y \<and>
    1.86 -            enum_basis y \<subseteq> ball (x i) e'" by auto
    1.87 +    from topological_basisE[OF basis_union_closed_basis this] guess b' .
    1.88 +    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> ball (x i) e' \<and> y \<in> union_closed_basis" by auto
    1.89    qed
    1.90    then guess B .. note B = this
    1.91 -  def B' \<equiv> "Pi' (domain x) (\<lambda>i. enum_basis (B i)::'b set)"
    1.92 -  hence "B' \<in> range enum_basis_finmap" unfolding B'_def
    1.93 -    by (intro in_enum_basis_finmapI) auto
    1.94 +  def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)"
    1.95 +  hence "B' \<in> basis_finmap" unfolding B'_def using B
    1.96 +    by (intro in_basis_finmapI) auto
    1.97    moreover have "x \<in> B'" unfolding B'_def using B by auto
    1.98    moreover have "B' \<subseteq> O'"
    1.99    proof
   1.100 @@ -516,7 +516,7 @@
   1.101        also have "\<dots> \<le> (\<Sum>i \<in> domain x. e')"
   1.102        proof (rule setsum_mono)
   1.103          fix i assume "i \<in> domain x"
   1.104 -        with `y \<in> B'` B have "y i \<in> enum_basis (B i)"
   1.105 +        with `y \<in> B'` B have "y i \<in> B i"
   1.106            by (simp add: Pi'_def B'_def)
   1.107          hence "y i \<in> ball (x i) e'" using B `domain y = domain x` `i \<in> domain x`
   1.108            by force
   1.109 @@ -528,73 +528,15 @@
   1.110      qed
   1.111    qed
   1.112    ultimately
   1.113 -  show "\<exists>B'\<in>range enum_basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" by blast
   1.114 +  show "\<exists>B'\<in>basis_finmap. x \<in> B' \<and> B' \<subseteq> O'" by blast
   1.115  qed
   1.116  
   1.117  lemma range_enum_basis_finmap_imp_open:
   1.118 -  assumes "x \<in> range enum_basis_finmap"
   1.119 +  assumes "x \<in> basis_finmap"
   1.120    shows "open x"
   1.121    using finmap_topological_basis assms by (auto simp: topological_basis_def)
   1.122  
   1.123 -lemma open_imp_ex_UNION_of_enum:
   1.124 -  fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
   1.125 -  assumes "open X" assumes "X \<noteq> {}"
   1.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>
   1.127 -    (\<forall>n. \<forall>i\<in>A n. (B n) i \<in> range enum_basis) \<and> (\<forall>n. finite (A n))"
   1.128 -proof -
   1.129 -  from `open X` obtain B' where B': "B'\<subseteq>range enum_basis_finmap" "\<Union>B' = X"
   1.130 -    using finmap_topological_basis by (force simp add: topological_basis_def)
   1.131 -  then obtain B where B: "B' = enum_basis_finmap ` B" by (auto simp: subset_image_iff)
   1.132 -  show ?thesis
   1.133 -  proof cases
   1.134 -    assume "B = {}" with B have "B' = {}" by simp hence False using B' assms by simp
   1.135 -    thus ?thesis by simp
   1.136 -  next
   1.137 -    assume "B \<noteq> {}" then obtain b where b: "b \<in> B" by auto
   1.138 -    def NA \<equiv> "\<lambda>n::nat. if n \<in> B
   1.139 -      then domain ((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) n)
   1.140 -      else domain ((from_nat::_\<Rightarrow>'a\<Rightarrow>\<^isub>F nat) b)"
   1.141 -    def NB \<equiv> "\<lambda>n::nat. if n \<in> B
   1.142 -      then (\<lambda>i. (enum_basis::nat\<Rightarrow>'b set) (((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) n) i))
   1.143 -      else (\<lambda>i. (enum_basis::nat\<Rightarrow>'b set) (((from_nat::_\<Rightarrow>'a \<Rightarrow>\<^isub>F nat) b) i))"
   1.144 -    have "X = UNION UNIV (\<lambda>i. Pi' (NA i) (NB i))" unfolding B'(2)[symmetric] using b
   1.145 -      unfolding B
   1.146 -      by safe
   1.147 -         (auto simp add: NA_def NB_def enum_basis_finmap_def Let_def o_def split: split_if_asm)
   1.148 -    moreover
   1.149 -    have "(\<forall>n. \<forall>i\<in>NA n. (NB n) i \<in> range enum_basis)"
   1.150 -      using enumerable_basis by (auto simp: topological_basis_def NA_def NB_def)
   1.151 -    moreover have "(\<forall>n. finite (NA n))" by (simp add: NA_def)
   1.152 -    ultimately show ?thesis by auto
   1.153 -  qed
   1.154 -qed
   1.155 -
   1.156 -lemma open_imp_ex_UNION:
   1.157 -  fixes X::"('a \<Rightarrow>\<^isub>F 'b) set"
   1.158 -  assumes "open X" assumes "X \<noteq> {}"
   1.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>
   1.160 -    (\<forall>n. \<forall>i\<in>A n. open ((B n) i)) \<and> (\<forall>n. finite (A n))"
   1.161 -  using open_imp_ex_UNION_of_enum[OF assms]
   1.162 -  apply auto
   1.163 -  apply (rule_tac x = A in exI)
   1.164 -  apply (rule_tac x = B in exI)
   1.165 -  apply (auto simp: open_enum_basis)
   1.166 -  done
   1.167 -
   1.168 -lemma open_basisE:
   1.169 -  assumes "open X" assumes "X \<noteq> {}"
   1.170 -  obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
   1.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)"
   1.172 -  using open_imp_ex_UNION[OF assms] by auto
   1.173 -
   1.174 -lemma open_basis_of_enumE:
   1.175 -  assumes "open X" assumes "X \<noteq> {}"
   1.176 -  obtains A::"nat\<Rightarrow>'a set" and B::"nat\<Rightarrow>('a \<Rightarrow> 'b set)" where
   1.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"
   1.178 -  "\<And>n. finite (A n)"
   1.179 -  using open_imp_ex_UNION_of_enum[OF assms] by auto
   1.180 -
   1.181 -instance proof qed (blast intro: finmap_topological_basis)
   1.182 +instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap)
   1.183  
   1.184  end
   1.185  
   1.186 @@ -746,16 +688,12 @@
   1.187  proof safe
   1.188    fix y assume "y \<in> sets N"
   1.189    have "A -` y = (\<Union>{A -` y \<inter> {x. domain x = J}|J. finite J})" by auto
   1.190 -  hence "A -` y \<inter> space (PiF I M) = (\<Union>n. A -` y \<inter> space (PiF ({set (from_nat n)}\<inter>I) M))"
   1.191 -    apply (auto simp: space_PiF Pi'_def)
   1.192 -  proof -
   1.193 -    case goal1
   1.194 +  { fix x::"'a \<Rightarrow>\<^isub>F 'b"
   1.195      from finite_list[of "domain x"] obtain xs where "set xs = domain x" by auto
   1.196 -    thus ?case
   1.197 -      apply (intro exI[where x="to_nat xs"])
   1.198 -      apply auto
   1.199 -      done
   1.200 -  qed
   1.201 +    hence "\<exists>n. domain x = set (from_nat n)"
   1.202 +      by (intro exI[where x="to_nat xs"]) auto }
   1.203 +  hence "A -` y \<inter> space (PiF I M) = (\<Union>n. A -` y \<inter> space (PiF ({set (from_nat n)}\<inter>I) M))"
   1.204 +    by (auto simp: space_PiF Pi'_def)
   1.205    also have "\<dots> \<in> sets (PiF I M)"
   1.206      apply (intro sets.Int sets.countable_nat_UN subsetI, safe)
   1.207      apply (case_tac "set (from_nat i) \<in> I")
   1.208 @@ -928,16 +866,6 @@
   1.209    qed simp
   1.210  qed
   1.211  
   1.212 -lemma sets_subspaceI:
   1.213 -  assumes "A \<inter> space M \<in> sets M"
   1.214 -  assumes "B \<in> sets M"
   1.215 -  shows "A \<inter> B \<in> sets M" using assms
   1.216 -proof -
   1.217 -  have "A \<inter> B = (A \<inter> space M) \<inter> B"
   1.218 -    using assms sets.sets_into_space by auto
   1.219 -  thus ?thesis using assms by auto
   1.220 -qed
   1.221 -
   1.222  lemma space_PiF_singleton_eq_product:
   1.223    assumes "finite I"
   1.224    shows "space (PiF {I} M) = (\<Pi>' i\<in>I. space (M i))"
   1.225 @@ -1075,49 +1003,49 @@
   1.226      by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
   1.227  qed
   1.228  
   1.229 -lemma enumerable_sigma_fprod_algebra_sigma_eq:
   1.230 +lemma sets_PiF_eq_sigma_union_closed_basis_single:
   1.231    assumes "I \<noteq> {}"
   1.232    assumes [simp]: "finite I"
   1.233    shows "sets (PiF {I} (\<lambda>_. borel)) = sigma_sets (space (PiF {I} (\<lambda>_. borel)))
   1.234 -    {Pi' I F |F. (\<forall>i\<in>I. F i \<in> range enum_basis)}"
   1.235 +    {Pi' I F |F. (\<forall>i\<in>I. F i \<in> union_closed_basis)}"
   1.236  proof -
   1.237    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   1.238    show ?thesis
   1.239    proof (rule sigma_fprod_algebra_sigma_eq)
   1.240      show "finite I" by simp
   1.241      show "I \<noteq> {}" by fact
   1.242 -    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> range enum_basis"
   1.243 +    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
   1.244        using S by simp_all
   1.245 -    show "range enum_basis \<subseteq> Pow (space borel)" by simp
   1.246 -    show "sets borel = sigma_sets (space borel) (range enum_basis)"
   1.247 -      by (simp add: borel_eq_enum_basis)
   1.248 +    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
   1.249 +    show "sets borel = sigma_sets (space borel) union_closed_basis"
   1.250 +      by (simp add: borel_eq_union_closed_basis)
   1.251    qed
   1.252  qed
   1.253  
   1.254 -text {* adapted from @{thm enumerable_sigma_fprod_algebra_sigma_eq} *}
   1.255 +text {* adapted from @{thm sets_PiF_eq_sigma_union_closed_basis_single} *}
   1.256  
   1.257 -lemma enumerable_sigma_prod_algebra_sigma_eq:
   1.258 +lemma sets_PiM_eq_sigma_union_closed_basis:
   1.259    assumes "I \<noteq> {}"
   1.260    assumes [simp]: "finite I"
   1.261    shows "sets (PiM I (\<lambda>_. borel)) = sigma_sets (space (PiM I (\<lambda>_. borel)))
   1.262 -    {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> range enum_basis}"
   1.263 +    {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> union_closed_basis}"
   1.264  proof -
   1.265    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   1.266    show ?thesis
   1.267    proof (rule sigma_prod_algebra_sigma_eq)
   1.268      show "finite I" by simp note[[show_types]]
   1.269 -    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> range enum_basis"
   1.270 +    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
   1.271        using S by simp_all
   1.272 -    show "range enum_basis \<subseteq> Pow (space borel)" by simp
   1.273 -    show "sets borel = sigma_sets (space borel) (range enum_basis)"
   1.274 -      by (simp add: borel_eq_enum_basis)
   1.275 +    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
   1.276 +    show "sets borel = sigma_sets (space borel) union_closed_basis"
   1.277 +      by (simp add: borel_eq_union_closed_basis)
   1.278    qed
   1.279  qed
   1.280  
   1.281  lemma product_open_generates_sets_PiF_single:
   1.282    assumes "I \<noteq> {}"
   1.283    assumes [simp]: "finite I"
   1.284 -  shows "sets (PiF {I} (\<lambda>_. borel::'b::enumerable_basis measure)) =
   1.285 +  shows "sets (PiF {I} (\<lambda>_. borel::'b::countable_basis_space measure)) =
   1.286      sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
   1.287  proof -
   1.288    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   1.289 @@ -1126,7 +1054,7 @@
   1.290      show "finite I" by simp
   1.291      show "I \<noteq> {}" by fact
   1.292      show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
   1.293 -      using S by (auto simp: open_enum_basis)
   1.294 +      using S by (auto simp: open_union_closed_basis)
   1.295      show "Collect open \<subseteq> Pow (space borel)" by simp
   1.296      show "sets borel = sigma_sets (space borel) (Collect open)"
   1.297        by (simp add: borel_def)
   1.298 @@ -1136,7 +1064,7 @@
   1.299  lemma product_open_generates_sets_PiM:
   1.300    assumes "I \<noteq> {}"
   1.301    assumes [simp]: "finite I"
   1.302 -  shows "sets (PiM I (\<lambda>_. borel::'b::enumerable_basis measure)) =
   1.303 +  shows "sets (PiM I (\<lambda>_. borel::'b::countable_basis_space measure)) =
   1.304      sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
   1.305  proof -
   1.306    from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
   1.307 @@ -1144,7 +1072,7 @@
   1.308    proof (rule sigma_prod_algebra_sigma_eq)
   1.309      show "finite I" by simp note[[show_types]]
   1.310      fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
   1.311 -      using S by (auto simp: open_enum_basis)
   1.312 +      using S by (auto simp: open_union_closed_basis)
   1.313      show "Collect open \<subseteq> Pow (space borel)" by simp
   1.314      show "sets borel = sigma_sets (space borel) (Collect open)"
   1.315        by (simp add: borel_def)
   1.316 @@ -1155,88 +1083,62 @@
   1.317  
   1.318  lemma borel_eq_PiF_borel:
   1.319    shows "(borel :: ('i::countable \<Rightarrow>\<^isub>F 'a::polish_space) measure) =
   1.320 -  PiF (Collect finite) (\<lambda>_. borel :: 'a measure)"
   1.321 -proof (rule measure_eqI)
   1.322 -  have C: "Collect finite \<noteq> {}" by auto
   1.323 -  show "sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure) = sets (PiF (Collect finite) (\<lambda>_. borel))"
   1.324 -  proof
   1.325 -    show "sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure) \<subseteq> sets (PiF (Collect finite) (\<lambda>_. borel))"
   1.326 -      apply (simp add: borel_def sets_PiF)
   1.327 -    proof (rule sigma_sets_mono, safe, cases)
   1.328 -      fix X::"('i \<Rightarrow>\<^isub>F 'a) set" assume "open X" "X \<noteq> {}"
   1.329 -      from open_basisE[OF this] guess NA NB . note N = this
   1.330 -      hence "X = (\<Union>i. Pi' (NA i) (NB i))" by simp
   1.331 -      also have "\<dots> \<in>
   1.332 -        sigma_sets UNIV {Pi' J S |S J. finite J \<and> S \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
   1.333 -        using N by (intro Union sigma_sets.Basic) blast
   1.334 -      finally show "X \<in> sigma_sets UNIV
   1.335 -        {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}" .
   1.336 -    qed (auto simp: Empty)
   1.337 +    PiF (Collect finite) (\<lambda>_. borel :: 'a measure)"
   1.338 +  unfolding borel_def PiF_def
   1.339 +proof (rule measure_eqI, clarsimp, rule sigma_sets_eqI)
   1.340 +  fix a::"('i \<Rightarrow>\<^isub>F 'a) set" assume "a \<in> Collect open" hence "open a" by simp
   1.341 +  then obtain B' where B': "B'\<subseteq>basis_finmap" "a = \<Union>B'"
   1.342 +    using finmap_topological_basis by (force simp add: topological_basis_def)
   1.343 +  have "a \<in> sigma UNIV {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
   1.344 +    unfolding `a = \<Union>B'`
   1.345 +  proof (rule sets.countable_Union)
   1.346 +    from B' countable_basis_finmap show "countable B'" by (metis countable_subset)
   1.347    next
   1.348 -    show "sets (PiF (Collect finite) (\<lambda>_. borel)) \<subseteq> sets (borel::('i \<Rightarrow>\<^isub>F 'a) measure)"
   1.349 +    show "B' \<subseteq> sets (sigma UNIV
   1.350 +      {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)})" (is "_ \<subseteq> sets ?s")
   1.351      proof
   1.352 -      fix x assume x: "x \<in> sets (PiF (Collect finite::'i set set) (\<lambda>_. borel::'a measure))"
   1.353 -      hence x_sp: "x \<subseteq> space (PiF (Collect finite) (\<lambda>_. borel))" by (rule sets.sets_into_space)
   1.354 -      let ?x = "\<lambda>J. x \<inter> {x. domain x = J}"
   1.355 -      have "x = \<Union>{?x J |J. finite J}" by auto
   1.356 -      also have "\<dots> \<in> sets borel"
   1.357 -      proof (rule countable_finite_comprehension, assumption)
   1.358 -        fix J::"'i set" assume "finite J"
   1.359 -        { assume ef: "J = {}"
   1.360 -          { assume e: "?x J = {}"
   1.361 -            hence "?x J \<in> sets borel" by simp
   1.362 -          } moreover {
   1.363 -            assume "?x J \<noteq> {}"
   1.364 -            then obtain f where "f \<in> x" "domain f = {}" using ef by auto
   1.365 -            hence "?x J = {f}" using `J = {}`
   1.366 -              by (auto simp: finmap_eq_iff)
   1.367 -            also have "{f} \<in> sets borel" by simp
   1.368 -            finally have "?x J \<in> sets borel" .
   1.369 -          } ultimately have "?x J \<in> sets borel" by blast
   1.370 -        } moreover {
   1.371 -          assume "J \<noteq> ({}::'i set)"
   1.372 -          from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'a set" . note S = this
   1.373 -          have "(?x J) = x \<inter> {m. domain m \<in> {J}}" by auto
   1.374 -          also have "\<dots> \<in> sets (PiF {J} (\<lambda>_. borel))"
   1.375 -            using x by (rule restrict_sets_measurable) (auto simp: `finite J`)
   1.376 -          also have "\<dots> = sigma_sets (space (PiF {J} (\<lambda>_. borel)))
   1.377 -            {Pi' (J) F |F. (\<forall>j\<in>J. F j \<in> range enum_basis)}"
   1.378 -            (is "_ = sigma_sets _ ?P")
   1.379 -            by (rule enumerable_sigma_fprod_algebra_sigma_eq[OF `J \<noteq> {}` `finite J`])
   1.380 -          also have "\<dots> \<subseteq> sets borel"
   1.381 -          proof
   1.382 -            fix x
   1.383 -            assume "x \<in> sigma_sets (space (PiF {J} (\<lambda>_. borel))) ?P"
   1.384 -            thus "x \<in> sets borel"
   1.385 -            proof (rule sigma_sets.induct, safe)
   1.386 -              fix F::"'i \<Rightarrow> 'a set"
   1.387 -              assume "\<forall>j\<in>J. F j \<in> range enum_basis"
   1.388 -              hence "Pi' J F \<in> range enum_basis_finmap"
   1.389 -                unfolding range_enum_basis_eq
   1.390 -                by (auto simp: `finite J` intro!: exI[where x=J] exI[where x=F])
   1.391 -              hence "open (Pi' (J) F)" by (rule range_enum_basis_finmap_imp_open)
   1.392 -              thus "Pi' (J) F \<in> sets borel" by simp
   1.393 -            next
   1.394 -              fix a::"('i \<Rightarrow>\<^isub>F 'a) set"
   1.395 -              have "space (PiF {J::'i set} (\<lambda>_. borel::'a measure)) =
   1.396 -                Pi' (J) (\<lambda>_. UNIV)"
   1.397 -                by (auto simp: space_PiF product_def)
   1.398 -              moreover have "open (Pi' (J::'i set) (\<lambda>_. UNIV::'a set))"
   1.399 -                by (intro open_Pi'I) auto
   1.400 -              ultimately
   1.401 -              have "space (PiF {J::'i set} (\<lambda>_. borel::'a measure)) \<in> sets borel"
   1.402 -                by simp
   1.403 -              moreover
   1.404 -              assume "a \<in> sets borel"
   1.405 -              ultimately show "space (PiF {J} (\<lambda>_. borel)) - a \<in> sets borel" ..
   1.406 -            qed auto
   1.407 -          qed
   1.408 -          finally have "(?x J) \<in> sets borel" .
   1.409 -        } ultimately show "(?x J) \<in> sets borel" by blast
   1.410 -      qed
   1.411 -      finally show "x \<in> sets (borel)" .
   1.412 +      fix x assume "x \<in> B'" with B' have "x \<in> basis_finmap" by auto
   1.413 +      then obtain J X where "x = Pi' J X" "finite J" "X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)"
   1.414 +        by (auto simp: basis_finmap_def open_union_closed_basis)
   1.415 +      thus "x \<in> sets ?s" by auto
   1.416      qed
   1.417    qed
   1.418 +  thus "a \<in> sigma_sets UNIV {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
   1.419 +    by simp
   1.420 +next
   1.421 +  fix b::"('i \<Rightarrow>\<^isub>F 'a) set"
   1.422 +  assume "b \<in> {Pi' J X |X J. finite J \<and> X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)}"
   1.423 +  hence b': "b \<in> sets (Pi\<^isub>F (Collect finite) (\<lambda>_. borel))" by (auto simp: sets_PiF borel_def)
   1.424 +  let ?b = "\<lambda>J. b \<inter> {x. domain x = J}"
   1.425 +  have "b = \<Union>((\<lambda>J. ?b J) ` Collect finite)" by auto
   1.426 +  also have "\<dots> \<in> sets borel"
   1.427 +  proof (rule sets.countable_Union, safe)
   1.428 +    fix J::"'i set" assume "finite J"
   1.429 +    { assume ef: "J = {}"
   1.430 +      have "?b J \<in> sets borel"
   1.431 +      proof cases
   1.432 +        assume "?b J \<noteq> {}"
   1.433 +        then obtain f where "f \<in> b" "domain f = {}" using ef by auto
   1.434 +        hence "?b J = {f}" using `J = {}`
   1.435 +          by (auto simp: finmap_eq_iff)
   1.436 +        also have "{f} \<in> sets borel" by simp
   1.437 +        finally show ?thesis .
   1.438 +      qed simp
   1.439 +    } moreover {
   1.440 +      assume "J \<noteq> ({}::'i set)"
   1.441 +      have "(?b J) = b \<inter> {m. domain m \<in> {J}}" by auto
   1.442 +      also have "\<dots> \<in> sets (PiF {J} (\<lambda>_. borel))"
   1.443 +        using b' by (rule restrict_sets_measurable) (auto simp: `finite J`)
   1.444 +      also have "\<dots> = sigma_sets (space (PiF {J} (\<lambda>_. borel)))
   1.445 +        {Pi' (J) F |F. (\<forall>j\<in>J. F j \<in> Collect open)}"
   1.446 +        (is "_ = sigma_sets _ ?P")
   1.447 +       by (rule product_open_generates_sets_PiF_single[OF `J \<noteq> {}` `finite J`])
   1.448 +      also have "\<dots> \<subseteq> sigma_sets UNIV (Collect open)"
   1.449 +        by (intro sigma_sets_mono'') (auto intro!: open_Pi'I simp: space_PiF)
   1.450 +      finally have "(?b J) \<in> sets borel" by (simp add: borel_def)
   1.451 +    } ultimately show "(?b J) \<in> sets borel" by blast
   1.452 +  qed (simp add: countable_Collect_finite)
   1.453 +  finally show "b \<in> sigma_sets UNIV (Collect open)" by (simp add: borel_def)
   1.454  qed (simp add: emeasure_sigma borel_def PiF_def)
   1.455  
   1.456  subsection {* Isomorphism between Functions and Finite Maps *}