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.143              by (simp add: P_closed)
   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)"
   1.237        by (simp add: borel_def)
   1.238 @@ -1174,7 +1132,7 @@
   1.239      proof
   1.240        fix x assume "x \<in> B'" with B' have "x \<in> basis_finmap" by auto
   1.241        then obtain J X where "x = Pi' J X" "finite J" "X \<in> J \<rightarrow> sigma_sets UNIV (Collect open)"
   1.242 -        by (auto simp: basis_finmap_def open_union_closed_basis)
   1.243 +        by (auto simp: basis_finmap_def topological_basis_open[OF basis_proj])
   1.244        thus "x \<in> sets ?s" by auto
   1.245      qed
   1.246    qed