src/HOL/Probability/Fin_Map.thy
 changeset 51106 5746e671ea70 parent 51105 a27fcd14c384 child 51343 b61b32f62c78
```     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Wed Feb 13 16:35:07 2013 +0100
1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Wed Feb 13 16:35:07 2013 +0100
1.3 @@ -93,17 +93,6 @@
1.4    show "x = y" using assms by (simp add: extensional_restrict)
1.5  qed
1.6
1.7 -lemma finmap_choice:
1.8 -  assumes *: "\<And>i. i \<in> I \<Longrightarrow> \<exists>x. P i x" and I: "finite I"
1.9 -  shows "\<exists>fm. domain fm = I \<and> (\<forall>i\<in>I. P i (fm i))"
1.10 -proof -
1.11 -  have "\<exists>f. \<forall>i\<in>I. P i (f i)"
1.12 -    unfolding bchoice_iff[symmetric] using * by auto
1.13 -  then guess f ..
1.14 -  with I show ?thesis
1.15 -    by (intro exI[of _ "finmap_of I f"]) auto
1.16 -qed
1.17 -
1.18  subsection {* Product set of Finite Maps *}
1.19
1.20  text {* This is @{term Pi} for Finite Maps, most of this is copied *}
1.21 @@ -532,40 +521,50 @@
1.22  instantiation finmap :: (countable, second_countable_topology) second_countable_topology
1.23  begin
1.24
1.25 +definition basis_proj::"'b set set"
1.26 +  where "basis_proj = (SOME B. countable B \<and> topological_basis B)"
1.27 +
1.28 +lemma countable_basis_proj: "countable basis_proj" and basis_proj: "topological_basis basis_proj"
1.29 +  unfolding basis_proj_def by (intro is_basis countable_basis)+
1.30 +
1.31  definition basis_finmap::"('a \<Rightarrow>\<^isub>F 'b) set set"
1.32 -  where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> union_closed_basis)}"
1.33 +  where "basis_finmap = {Pi' I S|I S. finite I \<and> (\<forall>i \<in> I. S i \<in> basis_proj)}"
1.34
1.35  lemma in_basis_finmapI:
1.36 -  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
1.37 +  assumes "finite I" assumes "\<And>i. i \<in> I \<Longrightarrow> S i \<in> basis_proj"
1.38    shows "Pi' I S \<in> basis_finmap"
1.39    using assms unfolding basis_finmap_def by auto
1.40
1.41 -lemma in_basis_finmapE:
1.42 -  assumes "x \<in> basis_finmap"
1.43 -  obtains I S where "x = Pi' I S" "finite I" "\<And>i. i \<in> I \<Longrightarrow> S i \<in> union_closed_basis"
1.44 -  using assms unfolding basis_finmap_def by auto
1.45 -
1.46  lemma basis_finmap_eq:
1.47 -  "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into union_closed_basis ((f)\<^isub>F i))) `
1.48 +  assumes "basis_proj \<noteq> {}"
1.49 +  shows "basis_finmap = (\<lambda>f. Pi' (domain f) (\<lambda>i. from_nat_into basis_proj ((f)\<^isub>F i))) `
1.50      (UNIV::('a \<Rightarrow>\<^isub>F nat) set)" (is "_ = ?f ` _")
1.51    unfolding basis_finmap_def
1.52  proof safe
1.53    fix I::"'a set" and S::"'a \<Rightarrow> 'b set"
1.54 -  assume "finite I" "\<forall>i\<in>I. S i \<in> union_closed_basis"
1.55 -  hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on union_closed_basis (S x)))"
1.56 -    by (force simp: Pi'_def countable_union_closed_basis)
1.57 +  assume "finite I" "\<forall>i\<in>I. S i \<in> basis_proj"
1.58 +  hence "Pi' I S = ?f (finmap_of I (\<lambda>x. to_nat_on basis_proj (S x)))"
1.59 +    by (force simp: Pi'_def countable_basis_proj)
1.60    thus "Pi' I S \<in> range ?f" by simp
1.61 -qed (metis (mono_tags) empty_basisI equals0D finite_domain from_nat_into)
1.62 +next
1.63 +  fix x and f::"'a \<Rightarrow>\<^isub>F nat"
1.64 +  show "\<exists>I S. (\<Pi>' i\<in>domain f. from_nat_into local.basis_proj ((f)\<^isub>F i)) = Pi' I S \<and>
1.65 +    finite I \<and> (\<forall>i\<in>I. S i \<in> local.basis_proj)"
1.66 +    using assms by (auto intro: from_nat_into)
1.67 +qed
1.68 +
1.69 +lemma basis_finmap_eq_empty: "basis_proj = {} \<Longrightarrow> basis_finmap = {Pi' {} undefined}"
1.70 +  by (auto simp: Pi'_iff basis_finmap_def)
1.71
1.72  lemma countable_basis_finmap: "countable basis_finmap"
1.73 -  unfolding basis_finmap_eq by simp
1.74 +  by (cases "basis_proj = {}") (auto simp: basis_finmap_eq basis_finmap_eq_empty)
1.75
1.76  lemma finmap_topological_basis:
1.77    "topological_basis basis_finmap"
1.78  proof (subst topological_basis_iff, safe)
1.79    fix B' assume "B' \<in> basis_finmap"
1.80    thus "open B'"
1.81 -    by (auto intro!: open_Pi'I topological_basis_open[OF basis_union_closed_basis]
1.82 +    by (auto intro!: open_Pi'I topological_basis_open[OF basis_proj]
1.83        simp: topological_basis_def basis_finmap_def Let_def)
1.84  next
1.85    fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
1.86 @@ -586,12 +585,12 @@
1.87      thus ?case by blast
1.88    qed (auto simp: Pi'_def)
1.89    have "\<exists>B.
1.90 -    (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> a i \<and> B i \<in> union_closed_basis)"
1.91 +    (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> a i \<and> B i \<in> basis_proj)"
1.92    proof (rule bchoice, safe)
1.93      fix i assume "i \<in> domain x"
1.94      hence "open (a i)" "x i \<in> a i" using a by auto
1.95 -    from topological_basisE[OF basis_union_closed_basis this] guess b' .
1.96 -    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> a i \<and> y \<in> union_closed_basis" by auto
1.97 +    from topological_basisE[OF basis_proj this] guess b' .
1.98 +    thus "\<exists>y. x i \<in> y \<and> y \<subseteq> a i \<and> y \<in> basis_proj" by auto
1.99    qed
1.100    then guess B .. note B = this
1.101    def B' \<equiv> "Pi' (domain x) (\<lambda>i. (B i)::'b set)"
1.102 @@ -1017,9 +1016,8 @@
1.103  text {* adapted from @{thm sigma_prod_algebra_sigma_eq} *}
1.104
1.105  lemma sigma_fprod_algebra_sigma_eq:
1.106 -  fixes E :: "'i \<Rightarrow> 'a set set"
1.107 +  fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
1.108    assumes [simp]: "finite I" "I \<noteq> {}"
1.109 -  assumes S_mono: "\<And>i. i \<in> I \<Longrightarrow> incseq (S i)"
1.110      and S_union: "\<And>i. i \<in> I \<Longrightarrow> (\<Union>j. S i j) = space (M i)"
1.111      and S_in_E: "\<And>i. i \<in> I \<Longrightarrow> range (S i) \<subseteq> E i"
1.112    assumes E_closed: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (space (M i))"
1.113 @@ -1028,6 +1026,9 @@
1.114    shows "sets (PiF {I} M) = sigma_sets (space (PiF {I} M)) P"
1.115  proof
1.116    let ?P = "sigma (space (Pi\<^isub>F {I} M)) P"
1.117 +  from `finite I`[THEN ex_bij_betw_finite_nat] guess T ..
1.118 +  then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
1.119 +    by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f simp del: `finite I`)
1.120    have P_closed: "P \<subseteq> Pow (space (Pi\<^isub>F {I} M))"
1.121      using E_closed by (auto simp: space_PiF P_def Pi'_iff subset_eq)
1.122    then have space_P: "space ?P = (\<Pi>' i\<in>I. space (M i))"
1.123 @@ -1050,15 +1051,20 @@
1.124            using E_closed `i \<in> I` by (auto simp: space_P Pi_iff subset_eq split: split_if_asm)
1.125          also have "\<dots> = (\<Pi>' j\<in>I. \<Union>n. if i = j then A else S j n)"
1.126            by (intro Pi'_cong) (simp_all add: S_union)
1.127 -        also have "\<dots> = (\<Union>n. \<Pi>' j\<in>I. if i = j then A else S j n)"
1.128 -          using S_mono
1.129 -          by (subst Pi'_UN[symmetric, OF `finite I`]) (auto simp: incseq_def)
1.130 +        also have "\<dots> = (\<Union>xs\<in>{xs. length xs = card I}. \<Pi>' j\<in>I. if i = j then A else S j (xs ! T j))"
1.131 +          using T
1.132 +          apply auto
1.133 +          apply (simp_all add: Pi'_iff bchoice_iff)
1.134 +          apply (erule conjE exE)+
1.135 +          apply (rule_tac x="map (\<lambda>n. f (the_inv_into I T n)) [0..<card I]" in exI)
1.136 +          apply (auto simp: bij_betw_def)
1.137 +          done
1.138          also have "\<dots> \<in> sets ?P"
1.139          proof (safe intro!: sets.countable_UN)
1.140 -          fix n show "(\<Pi>' j\<in>I. if i = j then A else S j n) \<in> sets ?P"
1.141 +          fix xs show "(\<Pi>' j\<in>I. if i = j then A else S j (xs ! T j)) \<in> sets ?P"
1.142              using A S_in_E
1.144 -               (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j n"])
1.145 +               (auto simp: P_def subset_eq intro!: exI[of _ "\<lambda>j. if i = j then A else S j (xs ! T j)"])
1.146          qed
1.147          finally show "(\<lambda>x. (x)\<^isub>F i) -` A \<inter> space ?P \<in> sets ?P"
1.148            using P_closed by simp
1.149 @@ -1078,76 +1084,28 @@
1.150      by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def)
1.151  qed
1.152
1.153 -lemma sets_PiF_eq_sigma_union_closed_basis_single:
1.154 -  assumes "I \<noteq> {}"
1.155 -  assumes [simp]: "finite I"
1.156 -  shows "sets (PiF {I} (\<lambda>_. borel)) = sigma_sets (space (PiF {I} (\<lambda>_. borel)))
1.157 -    {Pi' I F |F. (\<forall>i\<in>I. F i \<in> union_closed_basis)}"
1.158 -proof -
1.159 -  from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
1.160 -  show ?thesis
1.161 -  proof (rule sigma_fprod_algebra_sigma_eq)
1.162 -    show "finite I" by simp
1.163 -    show "I \<noteq> {}" by fact
1.164 -    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
1.165 -      using S by simp_all
1.166 -    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
1.167 -    show "sets borel = sigma_sets (space borel) union_closed_basis"
1.168 -      by (simp add: borel_eq_union_closed_basis)
1.169 -  qed
1.170 -qed
1.171 -
1.172 -text {* adapted from @{thm sets_PiF_eq_sigma_union_closed_basis_single} *}
1.173 -
1.174 -lemma sets_PiM_eq_sigma_union_closed_basis:
1.175 -  assumes "I \<noteq> {}"
1.176 -  assumes [simp]: "finite I"
1.177 -  shows "sets (PiM I (\<lambda>_. borel)) = sigma_sets (space (PiM I (\<lambda>_. borel)))
1.178 -    {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> union_closed_basis}"
1.179 -proof -
1.180 -  from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
1.181 -  show ?thesis
1.182 -  proof (rule sigma_prod_algebra_sigma_eq)
1.183 -    show "finite I" by simp note[[show_types]]
1.184 -    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> union_closed_basis"
1.185 -      using S by simp_all
1.186 -    show "union_closed_basis \<subseteq> Pow (space borel)" by simp
1.187 -    show "sets borel = sigma_sets (space borel) union_closed_basis"
1.188 -      by (simp add: borel_eq_union_closed_basis)
1.189 -  qed
1.190 -qed
1.191 -
1.192  lemma product_open_generates_sets_PiF_single:
1.193    assumes "I \<noteq> {}"
1.194    assumes [simp]: "finite I"
1.195    shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
1.196      sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
1.197  proof -
1.198 -  from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
1.199 +  from open_countable_basisE[OF open_UNIV] guess S::"'b set set" . note S = this
1.200    show ?thesis
1.201    proof (rule sigma_fprod_algebra_sigma_eq)
1.202      show "finite I" by simp
1.203      show "I \<noteq> {}" by fact
1.204 -    show "incseq S" "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
1.205 -      using S by (auto simp: open_union_closed_basis)
1.206 -    show "Collect open \<subseteq> Pow (space borel)" by simp
1.207 -    show "sets borel = sigma_sets (space borel) (Collect open)"
1.208 -      by (simp add: borel_def)
1.209 -  qed
1.210 -qed
1.211 -
1.212 -lemma product_open_generates_sets_PiM:
1.213 -  assumes "I \<noteq> {}"
1.214 -  assumes [simp]: "finite I"
1.215 -  shows "sets (PiM I (\<lambda>_. borel::'b::second_countable_topology measure)) =
1.216 -    sigma_sets (space (PiM I (\<lambda>_. borel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> Collect open}"
1.217 -proof -
1.218 -  from open_incseqE[OF open_UNIV] guess S::"nat \<Rightarrow> 'b set" . note S = this
1.219 -  show ?thesis
1.220 -  proof (rule sigma_prod_algebra_sigma_eq)
1.221 -    show "finite I" by simp note[[show_types]]
1.222 -    fix i show "(\<Union>j. S j) = space borel" "range S \<subseteq> Collect open"
1.223 -      using S by (auto simp: open_union_closed_basis)
1.224 +    def S'\<equiv>"from_nat_into S"
1.225 +    show "(\<Union>j. S' j) = space borel"
1.226 +      using S
1.227 +      apply (auto simp add: from_nat_into countable_basis_proj S'_def basis_proj_def)
1.228 +      apply (metis (lifting, mono_tags) UNIV_I UnionE basis_proj_def countable_basis_proj countable_subset from_nat_into_surj)
1.229 +      done
1.230 +    show "range S' \<subseteq> Collect open"
1.231 +      using S
1.232 +      apply (auto simp add: from_nat_into countable_basis_proj S'_def)
1.233 +      apply (metis UNIV_not_empty Union_empty from_nat_into set_mp topological_basis_open[OF basis_proj] basis_proj_def)
1.234 +      done
1.235      show "Collect open \<subseteq> Pow (space borel)" by simp
1.236      show "sets borel = sigma_sets (space borel) (Collect open)"