add Giry monad
authorhoelzl
Tue Oct 07 10:34:24 2014 +0200 (2014-10-07)
changeset 586069c66f7c541fb
parent 58605 9d5013661ac6
child 58607 1f90ea1b4010
add Giry monad
src/HOL/Library/FuncSet.thy
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/Stream_Space.thy
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Oct 06 21:21:46 2014 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Oct 07 10:34:24 2014 +0200
     1.3 @@ -199,6 +199,9 @@
     1.4      "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
     1.5    by (simp add: fun_eq_iff Pi_def restrict_def)
     1.6  
     1.7 +lemma restrict_UNIV: "restrict f UNIV = f"
     1.8 +  by (simp add: restrict_def)
     1.9 +
    1.10  lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
    1.11    by (simp add: inj_on_def restrict_def)
    1.12  
     2.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Mon Oct 06 21:21:46 2014 +0200
     2.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Oct 07 10:34:24 2014 +0200
     2.3 @@ -34,6 +34,12 @@
     2.4    unfolding pair_measure_def using pair_measure_closed[of A B]
     2.5    by (rule sets_measure_of)
     2.6  
     2.7 +lemma sets_pair_in_sets:
     2.8 +  assumes N: "space A \<times> space B = space N"
     2.9 +  assumes "\<And>a b. a \<in> sets A \<Longrightarrow> b \<in> sets B \<Longrightarrow> a \<times> b \<in> sets N"
    2.10 +  shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N"
    2.11 +  using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N)
    2.12 +
    2.13  lemma sets_pair_measure_cong[cong]:
    2.14    "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^sub>M M2) = sets (M1' \<Otimes>\<^sub>M M2')"
    2.15    unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
    2.16 @@ -42,6 +48,9 @@
    2.17    "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (A \<Otimes>\<^sub>M B)"
    2.18    by (auto simp: sets_pair_measure)
    2.19  
    2.20 +lemma sets_Pair: "{x} \<in> sets M1 \<Longrightarrow> {y} \<in> sets M2 \<Longrightarrow> {(x, y)} \<in> sets (M1 \<Otimes>\<^sub>M M2)"
    2.21 +  using pair_measureI[of "{x}" M1 "{y}" M2] by simp
    2.22 +
    2.23  lemma measurable_pair_measureI:
    2.24    assumes 1: "f \<in> space M \<rightarrow> space M1 \<times> space M2"
    2.25    assumes 2: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> f -` (A \<times> B) \<inter> space M \<in> sets M"
    2.26 @@ -98,6 +107,25 @@
    2.27      and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^sub>M M) N"
    2.28    by simp_all
    2.29  
    2.30 +lemma sets_pair_eq_sets_fst_snd:
    2.31 +  "sets (A \<Otimes>\<^sub>M B) = sets (Sup_sigma {vimage_algebra (space A \<times> space B) fst A, vimage_algebra (space A \<times> space B) snd B})"
    2.32 +    (is "?P = sets (Sup_sigma {?fst, ?snd})")
    2.33 +proof -
    2.34 +  { fix a b assume ab: "a \<in> sets A" "b \<in> sets B"
    2.35 +    then have "a \<times> b = (fst -` a \<inter> (space A \<times> space B)) \<inter> (snd -` b \<inter> (space A \<times> space B))"
    2.36 +      by (auto dest: sets.sets_into_space)
    2.37 +    also have "\<dots> \<in> sets (Sup_sigma {?fst, ?snd})"
    2.38 +      using ab by (auto intro: in_Sup_sigma in_vimage_algebra)
    2.39 +    finally have "a \<times> b \<in> sets (Sup_sigma {?fst, ?snd})" . }
    2.40 +  moreover have "sets ?fst \<subseteq> sets (A \<Otimes>\<^sub>M B)"
    2.41 +    by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric])
    2.42 +  moreover have "sets ?snd \<subseteq> sets (A \<Otimes>\<^sub>M B)"  
    2.43 +    by (rule sets_image_in_sets) (auto simp: space_pair_measure)
    2.44 +  ultimately show ?thesis
    2.45 +    by (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets )
    2.46 +       (auto simp add: space_Sup_sigma space_pair_measure)
    2.47 +qed
    2.48 +
    2.49  lemma measurable_pair_iff:
    2.50    "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
    2.51    by (auto intro: measurable_pair[of f M M1 M2]) 
     3.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon Oct 06 21:21:46 2014 +0200
     3.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Oct 07 10:34:24 2014 +0200
     3.3 @@ -353,6 +353,25 @@
     3.4    finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
     3.5  qed
     3.6  
     3.7 +lemma sets_PiM_eq_proj:
     3.8 +  "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
     3.9 +  apply (simp add: sets_PiM_single sets_Sup_sigma)
    3.10 +  apply (subst SUP_cong[OF refl])
    3.11 +  apply (rule sets_vimage_algebra2)
    3.12 +  apply auto []
    3.13 +  apply (auto intro!: arg_cong2[where f=sigma_sets])
    3.14 +  done
    3.15 +
    3.16 +lemma sets_PiM_in_sets:
    3.17 +  assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
    3.18 +  assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N"
    3.19 +  shows "sets (\<Pi>\<^sub>M i \<in> I. M i) \<subseteq> sets N"
    3.20 +  unfolding sets_PiM_single space[symmetric]
    3.21 +  by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
    3.22 +
    3.23 +lemma sets_PiM_cong: assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
    3.24 +  using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
    3.25 +
    3.26  lemma sets_PiM_I:
    3.27    assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
    3.28    shows "prod_emb I M J (PIE j:J. E j) \<in> sets (PIM i:I. M i)"
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Tue Oct 07 10:34:24 2014 +0200
     4.3 @@ -0,0 +1,868 @@
     4.4 +(*  Title:      HOL/Probability/Giry_Monad.thy
     4.5 +    Author:     Johannes Hölzl, TU München
     4.6 +    Author:     Manuel Eberl, TU München
     4.7 +
     4.8 +Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability
     4.9 +spaces.
    4.10 +*)
    4.11 +
    4.12 +theory Giry_Monad
    4.13 +  imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax"
    4.14 +begin
    4.15 +
    4.16 +section {* Sub-probability spaces *}
    4.17 +
    4.18 +locale subprob_space = finite_measure +
    4.19 +  assumes emeasure_space_le_1: "emeasure M (space M) \<le> 1"
    4.20 +  assumes subprob_not_empty: "space M \<noteq> {}"
    4.21 +
    4.22 +lemma subprob_spaceI[Pure.intro!]:
    4.23 +  assumes *: "emeasure M (space M) \<le> 1"
    4.24 +  assumes "space M \<noteq> {}"
    4.25 +  shows "subprob_space M"
    4.26 +proof -
    4.27 +  interpret finite_measure M
    4.28 +  proof
    4.29 +    show "emeasure M (space M) \<noteq> \<infinity>" using * by auto
    4.30 +  qed
    4.31 +  show "subprob_space M" by default fact+
    4.32 +qed
    4.33 +
    4.34 +lemma prob_space_imp_subprob_space:
    4.35 +  "prob_space M \<Longrightarrow> subprob_space M"
    4.36 +  by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty)
    4.37 +
    4.38 +sublocale prob_space \<subseteq> subprob_space
    4.39 +  by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
    4.40 +
    4.41 +lemma (in subprob_space) subprob_space_distr:
    4.42 +  assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)"
    4.43 +proof (rule subprob_spaceI)
    4.44 +  have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
    4.45 +  with f show "emeasure (distr M M' f) (space (distr M M' f)) \<le> 1"
    4.46 +    by (auto simp: emeasure_distr emeasure_space_le_1)
    4.47 +  show "space (distr M M' f) \<noteq> {}" by (simp add: assms)
    4.48 +qed
    4.49 +
    4.50 +lemma (in subprob_space) subprob_measure_le_1: "emeasure M X \<le> 1"
    4.51 +  by (rule order.trans[OF emeasure_space emeasure_space_le_1])
    4.52 +
    4.53 +locale pair_subprob_space = 
    4.54 +  pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
    4.55 +
    4.56 +sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2"
    4.57 +proof
    4.58 +  have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)"
    4.59 +    by (metis comm_monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)
    4.60 +  from this[OF _ _ M1.emeasure_space_le_1 M2.emeasure_space_le_1]
    4.61 +    show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) \<le> 1"
    4.62 +    by (simp add: M2.emeasure_pair_measure_Times space_pair_measure emeasure_nonneg)
    4.63 +  from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \<Otimes>\<^sub>M M2) \<noteq> {}"
    4.64 +    by (simp add: space_pair_measure)
    4.65 +qed
    4.66 +
    4.67 +definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
    4.68 +  "subprob_algebra K =
    4.69 +    (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
    4.70 +
    4.71 +lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}"
    4.72 +  by (auto simp add: subprob_algebra_def space_Sup_sigma)
    4.73 +
    4.74 +lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N"
    4.75 +  by (simp add: subprob_algebra_def)
    4.76 +
    4.77 +lemma measurable_emeasure_subprob_algebra[measurable]: 
    4.78 +  "a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)"
    4.79 +  by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def)
    4.80 +
    4.81 +context
    4.82 +  fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
    4.83 +begin
    4.84 +
    4.85 +lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)"
    4.86 +  using measurable_space[OF K] by (simp add: space_subprob_algebra)
    4.87 +
    4.88 +lemma sets_kernel: "a \<in> space M \<Longrightarrow> sets (K a) = sets N"
    4.89 +  using measurable_space[OF K] by (simp add: space_subprob_algebra)
    4.90 +
    4.91 +lemma measurable_emeasure_kernel[measurable]: 
    4.92 +    "A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M"
    4.93 +  using measurable_compose[OF K measurable_emeasure_subprob_algebra] .
    4.94 +
    4.95 +end
    4.96 +
    4.97 +lemma measurable_subprob_algebra:
    4.98 +  "(\<And>a. a \<in> space M \<Longrightarrow> subprob_space (K a)) \<Longrightarrow>
    4.99 +  (\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow>
   4.100 +  (\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow>
   4.101 +  K \<in> measurable M (subprob_algebra N)"
   4.102 +  by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def)
   4.103 +
   4.104 +lemma space_subprob_algebra_empty_iff:
   4.105 +  "space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}"
   4.106 +proof
   4.107 +  have "\<And>x. x \<in> space N \<Longrightarrow> density N (\<lambda>_. 0) \<in> space (subprob_algebra N)"
   4.108 +    by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI)
   4.109 +  then show "space (subprob_algebra N) = {} \<Longrightarrow> space N = {}"
   4.110 +    by auto
   4.111 +next
   4.112 +  assume "space N = {}"
   4.113 +  hence "sets N = {{}}" by (simp add: space_empty_iff)
   4.114 +  moreover have "\<And>M. subprob_space M \<Longrightarrow> sets M \<noteq> {{}}"
   4.115 +    by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric])
   4.116 +  ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
   4.117 +qed
   4.118 +
   4.119 +lemma measurable_distr:
   4.120 +  assumes [measurable]: "f \<in> measurable M N"
   4.121 +  shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
   4.122 +proof (cases "space N = {}")
   4.123 +  assume not_empty: "space N \<noteq> {}"
   4.124 +  show ?thesis
   4.125 +  proof (rule measurable_subprob_algebra)
   4.126 +    fix A assume A: "A \<in> sets N"
   4.127 +    then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow>
   4.128 +      (\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"
   4.129 +      by (intro measurable_cong)
   4.130 +         (auto simp: emeasure_distr space_subprob_algebra dest: sets_eq_imp_space_eq cong: measurable_cong)
   4.131 +    also have "\<dots>"
   4.132 +      using A by (intro measurable_emeasure_subprob_algebra) simp
   4.133 +    finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .
   4.134 +  qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty)
   4.135 +qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
   4.136 +
   4.137 +section {* Properties of return *}
   4.138 +
   4.139 +definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where
   4.140 +  "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)"
   4.141 +
   4.142 +lemma space_return[simp]: "space (return M x) = space M"
   4.143 +  by (simp add: return_def)
   4.144 +
   4.145 +lemma sets_return[simp]: "sets (return M x) = sets M"
   4.146 +  by (simp add: return_def)
   4.147 +
   4.148 +lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"
   4.149 +  by (simp cong: measurable_cong_sets) 
   4.150 +
   4.151 +lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
   4.152 +  by (simp cong: measurable_cong_sets) 
   4.153 +
   4.154 +lemma emeasure_return[simp]:
   4.155 +  assumes "A \<in> sets M"
   4.156 +  shows "emeasure (return M x) A = indicator A x"
   4.157 +proof (rule emeasure_measure_of[OF return_def])
   4.158 +  show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed)
   4.159 +  show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def)
   4.160 +  from assms show "A \<in> sets (return M x)" unfolding return_def by simp
   4.161 +  show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)"
   4.162 +    by (auto intro: countably_additiveI simp: suminf_indicator)
   4.163 +qed
   4.164 +
   4.165 +lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)"
   4.166 +  by rule simp
   4.167 +
   4.168 +lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"
   4.169 +  by (intro prob_space_return prob_space_imp_subprob_space)
   4.170 +
   4.171 +lemma AE_return:
   4.172 +  assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P"
   4.173 +  shows "(AE y in return M x. P y) \<longleftrightarrow> P x"
   4.174 +proof -
   4.175 +  have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x"
   4.176 +    by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator)
   4.177 +  also have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> (AE y in return M x. P y)"
   4.178 +    by (rule AE_cong) auto
   4.179 +  finally show ?thesis .
   4.180 +qed
   4.181 +  
   4.182 +lemma nn_integral_return:
   4.183 +  assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M"
   4.184 +  shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x"
   4.185 +proof-
   4.186 +  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
   4.187 +  have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms
   4.188 +    by (intro nn_integral_cong_AE) (auto simp: AE_return)
   4.189 +  also have "... = g x"
   4.190 +    using nn_integral_const[OF `g x \<ge> 0`, of "return M x"] emeasure_space_1 by simp
   4.191 +  finally show ?thesis .
   4.192 +qed
   4.193 +
   4.194 +lemma return_measurable: "return N \<in> measurable N (subprob_algebra N)"
   4.195 +  by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)
   4.196 +
   4.197 +lemma distr_return:
   4.198 +  assumes "f \<in> measurable M N" and "x \<in> space M"
   4.199 +  shows "distr (return M x) N f = return N (f x)"
   4.200 +  using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)
   4.201 +
   4.202 +definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"
   4.203 +
   4.204 +lemma select_sets1:
   4.205 +  "sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))"
   4.206 +  unfolding select_sets_def by (rule someI)
   4.207 +
   4.208 +lemma sets_select_sets[simp]:
   4.209 +  assumes sets: "sets M = sets (subprob_algebra N)"
   4.210 +  shows "sets (select_sets M) = sets N"
   4.211 +  unfolding select_sets_def
   4.212 +proof (rule someI2)
   4.213 +  show "sets M = sets (subprob_algebra N)"
   4.214 +    by fact
   4.215 +next
   4.216 +  fix L assume "sets M = sets (subprob_algebra L)"
   4.217 +  with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)"
   4.218 +    by (intro sets_eq_imp_space_eq) simp
   4.219 +  show "sets L = sets N"
   4.220 +  proof cases
   4.221 +    assume "space (subprob_algebra N) = {}"
   4.222 +    with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L]
   4.223 +    show ?thesis
   4.224 +      by (simp add: eq space_empty_iff)
   4.225 +  next
   4.226 +    assume "space (subprob_algebra N) \<noteq> {}"
   4.227 +    with eq show ?thesis
   4.228 +      by (fastforce simp add: space_subprob_algebra)
   4.229 +  qed
   4.230 +qed
   4.231 +
   4.232 +lemma space_select_sets[simp]:
   4.233 +  "sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N"
   4.234 +  by (intro sets_eq_imp_space_eq sets_select_sets)
   4.235 +
   4.236 +section {* Join *}
   4.237 +
   4.238 +definition join :: "'a measure measure \<Rightarrow> 'a measure" where
   4.239 +  "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
   4.240 +
   4.241 +lemma
   4.242 +  shows space_join[simp]: "space (join M) = space (select_sets M)"
   4.243 +    and sets_join[simp]: "sets (join M) = sets (select_sets M)"
   4.244 +  by (simp_all add: join_def)
   4.245 +
   4.246 +lemma emeasure_join:
   4.247 +  assumes M[simp]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
   4.248 +  shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
   4.249 +proof (rule emeasure_measure_of[OF join_def])
   4.250 +  have eq: "borel_measurable M = borel_measurable (subprob_algebra N)"
   4.251 +    by auto
   4.252 +  show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
   4.253 +  proof (rule countably_additiveI)
   4.254 +    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"
   4.255 +    have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"
   4.256 +      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra eq)
   4.257 +    also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"
   4.258 +    proof (rule nn_integral_cong)
   4.259 +      fix M' assume "M' \<in> space M"
   4.260 +      then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)"
   4.261 +        using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra)
   4.262 +    qed
   4.263 +    finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" .
   4.264 +  qed
   4.265 +qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg)
   4.266 +
   4.267 +lemma nn_integral_measurable_subprob_algebra:
   4.268 +  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
   4.269 +  shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
   4.270 +  using f
   4.271 +proof induct
   4.272 +  case (cong f g)
   4.273 +  moreover have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. \<integral>\<^sup>+M''. g M'' \<partial>M') \<in> ?B"
   4.274 +    by (intro measurable_cong nn_integral_cong cong)
   4.275 +       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
   4.276 +  ultimately show ?case by simp
   4.277 +next
   4.278 +  case (set B)
   4.279 +  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
   4.280 +    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
   4.281 +  ultimately show ?case
   4.282 +    by (simp add: measurable_emeasure_subprob_algebra)
   4.283 +next
   4.284 +  case (mult f c)
   4.285 +  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
   4.286 +    by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra)
   4.287 +  ultimately show ?case
   4.288 +    by simp
   4.289 +next
   4.290 +  case (add f g)
   4.291 +  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
   4.292 +    by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra)
   4.293 +  ultimately show ?case
   4.294 +    by (simp add: ac_simps)
   4.295 +next
   4.296 +  case (seq F)
   4.297 +  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
   4.298 +    unfolding SUP_apply
   4.299 +    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra)
   4.300 +  ultimately show ?case
   4.301 +    by (simp add: ac_simps)
   4.302 +qed
   4.303 +
   4.304 +
   4.305 +lemma measurable_join:
   4.306 +  "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
   4.307 +proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra)
   4.308 +  fix A assume "A \<in> sets N"
   4.309 +  let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))"
   4.310 +  have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B"
   4.311 +  proof (rule measurable_cong)
   4.312 +    fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))"
   4.313 +    then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')"
   4.314 +      by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`)
   4.315 +  qed
   4.316 +  also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"
   4.317 +    using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`] emeasure_nonneg[of _ A]
   4.318 +    by (rule nn_integral_measurable_subprob_algebra)
   4.319 +  finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .
   4.320 +next
   4.321 +  assume [simp]: "space N \<noteq> {}"
   4.322 +  fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))"
   4.323 +  then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)"
   4.324 +    apply (intro nn_integral_mono)
   4.325 +    apply (auto simp: space_subprob_algebra 
   4.326 +                 dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1)
   4.327 +    done
   4.328 +  with M show "subprob_space (join M)"
   4.329 +    by (intro subprob_spaceI)
   4.330 +       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
   4.331 +next
   4.332 +  assume "\<not>(space N \<noteq> {})"
   4.333 +  thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
   4.334 +qed (auto simp: space_subprob_algebra)
   4.335 +
   4.336 +lemma nn_integral_join:
   4.337 +  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" and M: "sets M = sets (subprob_algebra N)"
   4.338 +  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
   4.339 +  using f
   4.340 +proof induct
   4.341 +  case (cong f g)
   4.342 +  moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g"
   4.343 +    by (intro nn_integral_cong cong) (simp add: M)
   4.344 +  moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)"
   4.345 +    by (intro nn_integral_cong cong)
   4.346 +       (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq)
   4.347 +  ultimately show ?case
   4.348 +    by simp
   4.349 +next
   4.350 +  case (set A)
   4.351 +  moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 
   4.352 +    by (intro nn_integral_cong nn_integral_indicator)
   4.353 +       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
   4.354 +  ultimately show ?case
   4.355 +    using M by (simp add: emeasure_join)
   4.356 +next
   4.357 +  case (mult f c)
   4.358 +  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. c * f x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. c * \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
   4.359 +    using mult M
   4.360 +    by (intro nn_integral_cong nn_integral_cmult)
   4.361 +       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
   4.362 +  also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
   4.363 +    using nn_integral_measurable_subprob_algebra[OF mult(3,4)]
   4.364 +    by (intro nn_integral_cmult mult) (simp add: M)
   4.365 +  also have "\<dots> = c * (integral\<^sup>N (join M) f)"
   4.366 +    by (simp add: mult)
   4.367 +  also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"
   4.368 +    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M)
   4.369 +  finally show ?case by simp
   4.370 +next
   4.371 +  case (add f g)
   4.372 +  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x + g x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (\<integral>\<^sup>+ x. f x \<partial>M') + (\<integral>\<^sup>+ x. g x \<partial>M') \<partial>M)"
   4.373 +    using add M
   4.374 +    by (intro nn_integral_cong nn_integral_add)
   4.375 +       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
   4.376 +  also have "\<dots> = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) + (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. g x \<partial>M' \<partial>M)"
   4.377 +    using nn_integral_measurable_subprob_algebra[OF add(1,2)]
   4.378 +    using nn_integral_measurable_subprob_algebra[OF add(5,6)]
   4.379 +    by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)
   4.380 +  also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
   4.381 +    by (simp add: add)
   4.382 +  also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
   4.383 +    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M)
   4.384 +  finally show ?case by (simp add: ac_simps)
   4.385 +next
   4.386 +  case (seq F)
   4.387 +  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. (SUP i. F i) x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (SUP i. \<integral>\<^sup>+ x. F i x \<partial>M') \<partial>M)"
   4.388 +    using seq M unfolding SUP_apply
   4.389 +    by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
   4.390 +       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
   4.391 +  also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"
   4.392 +    using nn_integral_measurable_subprob_algebra[OF seq(1,2)] seq
   4.393 +    by (intro nn_integral_monotone_convergence_SUP)
   4.394 +       (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
   4.395 +  also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"
   4.396 +    by (simp add: seq)
   4.397 +  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
   4.398 +    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) (simp_all add: M)
   4.399 +  finally show ?case by (simp add: ac_simps)
   4.400 +qed
   4.401 +
   4.402 +lemma join_assoc:
   4.403 +  assumes M: "sets M = sets (subprob_algebra (subprob_algebra N))"
   4.404 +  shows "join (distr M (subprob_algebra N) join) = join (join M)"
   4.405 +proof (rule measure_eqI)
   4.406 +  fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"
   4.407 +  then have A: "A \<in> sets N" by simp
   4.408 +  show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
   4.409 +    using measurable_join[of N]
   4.410 +    by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg
   4.411 +                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ _ M]
   4.412 +             intro!: nn_integral_cong emeasure_join cong: measurable_cong)
   4.413 +qed (simp add: M)
   4.414 +
   4.415 +lemma join_return: 
   4.416 +  assumes "sets M = sets N" and "subprob_space M"
   4.417 +  shows "join (return (subprob_algebra N) M) = M"
   4.418 +  by (rule measure_eqI)
   4.419 +     (simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra  
   4.420 +                    measurable_emeasure_subprob_algebra nn_integral_return assms)
   4.421 +
   4.422 +lemma join_return':
   4.423 +  assumes "sets N = sets M"
   4.424 +  shows "join (distr M (subprob_algebra N) (return N)) = M"
   4.425 +apply (rule measure_eqI)
   4.426 +apply (simp add: assms)
   4.427 +apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)")
   4.428 +apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)
   4.429 +apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable)
   4.430 +done
   4.431 +
   4.432 +lemma join_distr_distr:
   4.433 +  fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure"
   4.434 +  assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N"
   4.435 +  shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l")
   4.436 +proof (rule measure_eqI)
   4.437 +  fix A assume "A \<in> sets ?r"
   4.438 +  hence A_in_N: "A \<in> sets N" by simp
   4.439 +
   4.440 +  from assms have "f \<in> measurable (join M) N" 
   4.441 +      by (simp cong: measurable_cong_sets)
   4.442 +  moreover from assms and A_in_N have "f-`A \<inter> space R \<in> sets R" 
   4.443 +      by (intro measurable_sets) simp_all
   4.444 +  ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-`A \<inter> space R) \<partial>M"
   4.445 +      by (simp_all add: A_in_N emeasure_distr emeasure_join assms)
   4.446 +  
   4.447 +  also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N
   4.448 +  proof (intro nn_integral_cong, subst emeasure_distr)
   4.449 +    fix M' assume "M' \<in> space M"
   4.450 +    from assms have "space M = space (subprob_algebra R)"
   4.451 +        using sets_eq_imp_space_eq by blast
   4.452 +    with `M' \<in> space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast
   4.453 +    show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms)
   4.454 +    have "space M' = space R" by (rule sets_eq_imp_space_eq) simp
   4.455 +    thus "emeasure M' (f -` A \<inter> space R) = emeasure M' (f -` A \<inter> space M')" by simp
   4.456 +  qed
   4.457 +
   4.458 +  also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)"
   4.459 +      by (simp cong: measurable_cong_sets add: assms measurable_distr)
   4.460 +  hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = 
   4.461 +             emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A"
   4.462 +      by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra)
   4.463 +  finally show "emeasure ?r A = emeasure ?l A" ..
   4.464 +qed simp
   4.465 +
   4.466 +definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where
   4.467 +  "bind M f = (if space M = {} then count_space {} else
   4.468 +    join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
   4.469 +
   4.470 +adhoc_overloading Monad_Syntax.bind bind
   4.471 +
   4.472 +lemma bind_empty: 
   4.473 +  "space M = {} \<Longrightarrow> bind M f = count_space {}"
   4.474 +  by (simp add: bind_def)
   4.475 +
   4.476 +lemma bind_nonempty:
   4.477 +  "space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)"
   4.478 +  by (simp add: bind_def)
   4.479 +
   4.480 +lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}"
   4.481 +  by (auto simp: bind_def)
   4.482 +
   4.483 +lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
   4.484 +  by (simp add: bind_def)
   4.485 +
   4.486 +lemma sets_bind[simp]: 
   4.487 +  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
   4.488 +  shows "sets (bind M f) = sets N"
   4.489 +    using assms(2) by (force simp: bind_nonempty intro!: sets_kernel[OF assms(1) someI_ex])
   4.490 +
   4.491 +lemma space_bind[simp]: 
   4.492 +  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
   4.493 +  shows "space (bind M f) = space N"
   4.494 +    using assms by (intro sets_eq_imp_space_eq sets_bind)
   4.495 +
   4.496 +lemma bind_cong: 
   4.497 +  assumes "\<forall>x \<in> space M. f x = g x"
   4.498 +  shows "bind M f = bind M g"
   4.499 +proof (cases "space M = {}")
   4.500 +  assume "space M \<noteq> {}"
   4.501 +  hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast
   4.502 +  with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast
   4.503 +  with `space M \<noteq> {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong)
   4.504 +qed (simp add: bind_empty)
   4.505 +
   4.506 +lemma bind_nonempty':
   4.507 +  assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M"
   4.508 +  shows "bind M f = join (distr M (subprob_algebra N) f)"
   4.509 +  using assms
   4.510 +  apply (subst bind_nonempty, blast)
   4.511 +  apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast)
   4.512 +  apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]])
   4.513 +  done
   4.514 +
   4.515 +lemma bind_nonempty'':
   4.516 +  assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}"
   4.517 +  shows "bind M f = join (distr M (subprob_algebra N) f)"
   4.518 +  using assms by (auto intro: bind_nonempty')
   4.519 +
   4.520 +lemma emeasure_bind:
   4.521 +    "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>
   4.522 +      \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
   4.523 +  by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
   4.524 +
   4.525 +lemma bind_return: 
   4.526 +  assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M"
   4.527 +  shows "bind (return M x) f = f x"
   4.528 +  using sets_kernel[OF assms] assms
   4.529 +  by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty'
   4.530 +               cong: subprob_algebra_cong)
   4.531 +
   4.532 +lemma bind_return':
   4.533 +  shows "bind M (return M) = M"
   4.534 +  by (cases "space M = {}")
   4.535 +     (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 
   4.536 +               cong: subprob_algebra_cong)
   4.537 +
   4.538 +lemma bind_count_space_singleton:
   4.539 +  assumes "subprob_space (f x)"
   4.540 +  shows "count_space {x} \<guillemotright>= f = f x"
   4.541 +proof-
   4.542 +  have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
   4.543 +  have "count_space {x} = return (count_space {x}) x"
   4.544 +    by (intro measure_eqI) (auto dest: A)
   4.545 +  also have "... \<guillemotright>= f = f x"
   4.546 +    by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
   4.547 +  finally show ?thesis .
   4.548 +qed
   4.549 +
   4.550 +lemma emeasure_bind_const: 
   4.551 +    "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 
   4.552 +         emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
   4.553 +  by (simp add: bind_nonempty emeasure_join nn_integral_distr 
   4.554 +                space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg)
   4.555 +
   4.556 +lemma emeasure_bind_const':
   4.557 +  assumes "subprob_space M" "subprob_space N"
   4.558 +  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
   4.559 +using assms
   4.560 +proof (case_tac "X \<in> sets N")
   4.561 +  fix X assume "X \<in> sets N"
   4.562 +  thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
   4.563 +      by (subst emeasure_bind_const) 
   4.564 +         (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1)
   4.565 +next
   4.566 +  fix X assume "X \<notin> sets N"
   4.567 +  with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
   4.568 +      by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty
   4.569 +                    space_subprob_algebra emeasure_notin_sets)
   4.570 +qed
   4.571 +
   4.572 +lemma emeasure_bind_const_prob_space:
   4.573 +  assumes "prob_space M" "subprob_space N"
   4.574 +  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X"
   4.575 +  using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 
   4.576 +                            prob_space.emeasure_space_1)
   4.577 +
   4.578 +lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
   4.579 +  by (intro measure_eqI) 
   4.580 +     (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
   4.581 +
   4.582 +lemma bind_return_distr: 
   4.583 +    "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (return N \<circ> f) = distr M N f"
   4.584 +  apply (simp add: bind_nonempty)
   4.585 +  apply (subst subprob_algebra_cong)
   4.586 +  apply (rule sets_return)
   4.587 +  apply (subst distr_distr[symmetric])
   4.588 +  apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return')
   4.589 +  done
   4.590 +
   4.591 +lemma bind_assoc:
   4.592 +  fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure"
   4.593 +  assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)"
   4.594 +  shows "bind (bind M f) g = bind M (\<lambda>x. bind (f x) g)"
   4.595 +proof (cases "space M = {}")
   4.596 +  assume [simp]: "space M \<noteq> {}"
   4.597 +  from assms have [simp]: "space N \<noteq> {}" "space R \<noteq> {}"
   4.598 +      by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
   4.599 +  from assms have sets_fx[simp]: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N"
   4.600 +      by (simp add: sets_kernel)
   4.601 +  have ex_in: "\<And>A. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A" by blast
   4.602 +  note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF `space M \<noteq> {}`]]]
   4.603 +                         sets_kernel[OF M2 someI_ex[OF ex_in[OF `space N \<noteq> {}`]]]
   4.604 +  note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)]
   4.605 +
   4.606 +  have "bind M (\<lambda>x. bind (f x) g) = 
   4.607 +        join (distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f))"
   4.608 +    by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def
   4.609 +             cong: subprob_algebra_cong distr_cong)
   4.610 +  also have "distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f) =
   4.611 +             distr (distr (distr M (subprob_algebra N) f)
   4.612 +                          (subprob_algebra (subprob_algebra R))
   4.613 +                          (\<lambda>x. distr x (subprob_algebra R) g)) 
   4.614 +                   (subprob_algebra R) join"
   4.615 +      apply (subst distr_distr, 
   4.616 +             (blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+
   4.617 +      apply (simp add: o_assoc)
   4.618 +      done
   4.619 +  also have "join ... = bind (bind M f) g"
   4.620 +      by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong)
   4.621 +  finally show ?thesis ..
   4.622 +qed (simp add: bind_empty)
   4.623 +
   4.624 +lemma emeasure_space_subprob_algebra[measurable]:
   4.625 +  "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"
   4.626 +proof-
   4.627 +  have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M")
   4.628 +    by (rule measurable_emeasure_subprob_algebra) simp
   4.629 +  also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
   4.630 +    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
   4.631 +  finally show ?thesis .
   4.632 +qed
   4.633 +
   4.634 +(* TODO: Rename. This name is too general – Manuel *)
   4.635 +lemma measurable_pair_measure:
   4.636 +  assumes f: "f \<in> measurable M (subprob_algebra N)"
   4.637 +  assumes g: "g \<in> measurable M (subprob_algebra L)"
   4.638 +  shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
   4.639 +proof (rule measurable_subprob_algebra)
   4.640 +  { fix x assume "x \<in> space M"
   4.641 +    with measurable_space[OF f] measurable_space[OF g]
   4.642 +    have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"
   4.643 +      by auto
   4.644 +    interpret F: subprob_space "f x"
   4.645 +      using fx by (simp add: space_subprob_algebra)
   4.646 +    interpret G: subprob_space "g x"
   4.647 +      using gx by (simp add: space_subprob_algebra)
   4.648 +
   4.649 +    interpret pair_subprob_space "f x" "g x" ..
   4.650 +    show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales
   4.651 +    show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"
   4.652 +      using fx gx by (simp add: space_subprob_algebra)
   4.653 +
   4.654 +    have 1: "\<And>A B. A \<in> sets N \<Longrightarrow> B \<in> sets L \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (A \<times> B) = emeasure (f x) A * emeasure (g x) B"
   4.655 +      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 
   4.656 +    have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 
   4.657 +              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
   4.658 +      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
   4.659 +    hence 2: "\<And>A. A \<in> sets (N \<Otimes>\<^sub>M L) \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (space N \<times> space L - A) =
   4.660 +                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
   4.661 +      using emeasure_compl[OF _ P.emeasure_finite]
   4.662 +      unfolding sets_eq
   4.663 +      unfolding sets_eq_imp_space_eq[OF sets_eq]
   4.664 +      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
   4.665 +    note 1 2 sets_eq }
   4.666 +  note Times = this(1) and Compl = this(2) and sets_eq = this(3)
   4.667 +
   4.668 +  fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
   4.669 +  show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"
   4.670 +    using Int_stable_pair_measure_generator pair_measure_closed A
   4.671 +    unfolding sets_pair_measure
   4.672 +  proof (induct A rule: sigma_sets_induct_disjoint)
   4.673 +    case (basic A) then show ?case
   4.674 +      by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)
   4.675 +         (auto intro!: measurable_emeasure_kernel f g)
   4.676 +  next
   4.677 +    case (compl A)
   4.678 +    then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
   4.679 +      by (auto simp: sets_pair_measure)
   4.680 +    have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 
   4.681 +                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
   4.682 +      using compl(2) f g by measurable
   4.683 +    thus ?case by (simp add: Compl A cong: measurable_cong)
   4.684 +  next
   4.685 +    case (union A)
   4.686 +    then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"
   4.687 +      by (auto simp: sets_pair_measure)
   4.688 +    then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>
   4.689 +      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
   4.690 +      by (intro measurable_cong suminf_emeasure[symmetric])
   4.691 +         (auto simp: sets_eq)
   4.692 +    also have "\<dots>"
   4.693 +      using union by auto
   4.694 +    finally show ?case .
   4.695 +  qed simp
   4.696 +qed
   4.697 +
   4.698 +(* TODO: Move *)
   4.699 +lemma measurable_distr2:
   4.700 +  assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
   4.701 +  assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
   4.702 +  shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
   4.703 +proof -
   4.704 +  have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
   4.705 +    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
   4.706 +  proof (rule measurable_cong)
   4.707 +    fix x assume x: "x \<in> space L"
   4.708 +    have gx: "g x \<in> space (subprob_algebra M)"
   4.709 +      using measurable_space[OF g x] .
   4.710 +    then have [simp]: "sets (g x) = sets M"
   4.711 +      by (simp add: space_subprob_algebra)
   4.712 +    then have [simp]: "space (g x) = space M"
   4.713 +      by (rule sets_eq_imp_space_eq)
   4.714 +    let ?R = "return L x"
   4.715 +    from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"
   4.716 +      by simp
   4.717 +    interpret subprob_space "g x"
   4.718 +      using gx by (simp add: space_subprob_algebra)
   4.719 +    have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
   4.720 +      by (simp add: space_pair_measure)
   4.721 +    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
   4.722 +    proof (rule measure_eqI)
   4.723 +      show "sets ?l = sets ?r"
   4.724 +        by simp
   4.725 +    next
   4.726 +      fix A assume "A \<in> sets ?l"
   4.727 +      then have A[measurable]: "A \<in> sets N"
   4.728 +        by simp
   4.729 +      then have "emeasure ?r A = emeasure (?R \<Otimes>\<^sub>M g x) ((\<lambda>(x, y). f x y) -` A \<inter> space (?R \<Otimes>\<^sub>M g x))"
   4.730 +        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
   4.731 +      also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)"
   4.732 +        apply (subst emeasure_pair_measure_alt)
   4.733 +        apply (rule measurable_sets[OF _ A])
   4.734 +        apply (auto simp add: f_M' cong: measurable_cong_sets)
   4.735 +        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
   4.736 +        apply (auto simp: space_subprob_algebra space_pair_measure)
   4.737 +        done
   4.738 +      also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)"
   4.739 +        by (subst nn_integral_return)
   4.740 +           (auto simp: x intro!: measurable_emeasure)
   4.741 +      also have "\<dots> = emeasure ?l A"
   4.742 +        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
   4.743 +      finally show "emeasure ?l A = emeasure ?r A" ..
   4.744 +    qed
   4.745 +  qed
   4.746 +  also have "\<dots>"
   4.747 +    apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])
   4.748 +    apply (rule return_measurable)
   4.749 +    apply measurable
   4.750 +    done
   4.751 +  finally show ?thesis .
   4.752 +qed
   4.753 +
   4.754 +(* END TODO *)
   4.755 +
   4.756 +lemma measurable_bind':
   4.757 +  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
   4.758 +          M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
   4.759 +  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
   4.760 +proof (subst measurable_cong)
   4.761 +  fix x assume x_in_M: "x \<in> space M"
   4.762 +  with assms have "space (f x) \<noteq> {}" 
   4.763 +      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
   4.764 +  moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)"
   4.765 +      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
   4.766 +         (auto dest: measurable_Pair2)
   4.767 +  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 
   4.768 +      by (simp_all add: bind_nonempty'')
   4.769 +next
   4.770 +  show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)"
   4.771 +    apply (rule measurable_compose[OF _ measurable_join])
   4.772 +    apply (rule measurable_distr2[OF M2 M1])
   4.773 +    done
   4.774 +qed
   4.775 +
   4.776 +lemma measurable_bind:
   4.777 +  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
   4.778 +          M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
   4.779 +  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
   4.780 +  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)
   4.781 +
   4.782 +lemma measurable_bind2:
   4.783 +  assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)"
   4.784 +  shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)"
   4.785 +    using assms by (intro measurable_bind' measurable_const) auto
   4.786 +
   4.787 +lemma subprob_space_bind:
   4.788 +  assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
   4.789 +  shows "subprob_space (M \<guillemotright>= f)"
   4.790 +proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
   4.791 +  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
   4.792 +    by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
   4.793 +        rule measurable_compose[OF measurable_snd assms(2)])
   4.794 +  from assms(1) show "M \<in> space (subprob_algebra M)"
   4.795 +    by (simp add: space_subprob_algebra)
   4.796 +qed
   4.797 +
   4.798 +lemma double_bind_assoc:
   4.799 +  assumes Mg: "g \<in> measurable N (subprob_algebra N')"
   4.800 +  assumes Mf: "f \<in> measurable M (subprob_algebra M')"
   4.801 +  assumes Mh: "split h \<in> measurable (M \<Otimes>\<^sub>M M') N"
   4.802 +  shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g"
   4.803 +proof-
   4.804 +  have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g = 
   4.805 +            do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g}"
   4.806 +    using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg
   4.807 +                      measurable_compose[OF _ return_measurable] simp: measurable_split_conv)
   4.808 +  also from Mh have "\<And>x. x \<in> space M \<Longrightarrow> h x \<in> measurable M' N" by measurable
   4.809 +  hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g} = 
   4.810 +            do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g}"
   4.811 +    apply (intro ballI bind_cong bind_assoc)
   4.812 +    apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp)
   4.813 +    apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg)
   4.814 +    done
   4.815 +  also have "\<And>x. x \<in> space M \<Longrightarrow> space (f x) = space M'"
   4.816 +    by (intro sets_eq_imp_space_eq sets_kernel[OF Mf])
   4.817 +  with measurable_space[OF Mh] 
   4.818 +    have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}"
   4.819 +    by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure)
   4.820 +  finally show ?thesis ..
   4.821 +qed
   4.822 +
   4.823 +section {* Measures are \omega-chain complete partial orders *}
   4.824 +
   4.825 +definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where
   4.826 +  "SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)"
   4.827 +
   4.828 +lemma
   4.829 +  assumes const: "\<And>i j. sets (M i) = sets (M j)"
   4.830 +  shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp)
   4.831 +    and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st)
   4.832 +proof -
   4.833 +  have "(\<Union>i. sets (M i)) = sets (M i)"
   4.834 +    using const by auto
   4.835 +  moreover have "(\<Union>i. space (M i)) = space (M i)"
   4.836 +    using const[THEN sets_eq_imp_space_eq] by auto
   4.837 +  moreover have "\<And>i. sets (M i) \<subseteq> Pow (space (M i))"
   4.838 +    by (auto dest: sets.sets_into_space)
   4.839 +  ultimately show ?sp ?st
   4.840 +    by (simp_all add: SUP_measure_def)
   4.841 +qed
   4.842 +
   4.843 +lemma emeasure_SUP_measure:
   4.844 +  assumes const: "\<And>i j. sets (M i) = sets (M j)"
   4.845 +    and mono: "mono (\<lambda>i. emeasure (M i))"
   4.846 +  shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)"
   4.847 +proof cases
   4.848 +  assume "A \<in> sets (SUP_measure M)"
   4.849 +  show ?thesis
   4.850 +  proof (rule emeasure_measure_of[OF SUP_measure_def])
   4.851 +    show "countably_additive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"
   4.852 +    proof (rule countably_additiveI)
   4.853 +      fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (SUP_measure M)"
   4.854 +      then have "\<And>i j. A i \<in> sets (M j)"
   4.855 +        using sets_SUP_measure[of M, OF const] by simp
   4.856 +      moreover assume "disjoint_family A"
   4.857 +      ultimately show "(\<Sum>i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\<Union>i. A i))"
   4.858 +        using mono by (subst suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure)
   4.859 +    qed
   4.860 +    show "positive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"
   4.861 +      by (auto simp: positive_def intro: SUP_upper2)
   4.862 +    show "(\<Union>i. sets (M i)) \<subseteq> Pow (\<Union>i. space (M i))"
   4.863 +      using sets.sets_into_space by auto
   4.864 +  qed fact
   4.865 +next
   4.866 +  assume "A \<notin> sets (SUP_measure M)"
   4.867 +  with sets_SUP_measure[of M, OF const] show ?thesis
   4.868 +    by (simp add: emeasure_notin_sets)
   4.869 +qed
   4.870 +
   4.871 +end
     5.1 --- a/src/HOL/Probability/Measure_Space.thy	Mon Oct 06 21:21:46 2014 +0200
     5.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Oct 07 10:34:24 2014 +0200
     5.3 @@ -1643,6 +1643,10 @@
     5.4    "X \<subseteq> A \<Longrightarrow> infinite X \<Longrightarrow> emeasure (count_space A) X = \<infinity>"
     5.5    using emeasure_count_space[of X A] by simp
     5.6  
     5.7 +lemma measure_count_space: "measure (count_space A) X = (if X \<subseteq> A then card X else 0)"
     5.8 +  unfolding measure_def
     5.9 +  by (cases "finite X") (simp_all add: emeasure_notin_sets)
    5.10 +
    5.11  lemma emeasure_count_space_eq_0:
    5.12    "emeasure (count_space A) X = 0 \<longleftrightarrow> (X \<subseteq> A \<longrightarrow> X = {})"
    5.13  proof cases
    5.14 @@ -1655,6 +1659,9 @@
    5.15    qed simp
    5.16  qed (simp add: emeasure_notin_sets)
    5.17  
    5.18 +lemma space_empty: "space M = {} \<Longrightarrow> M = count_space {}"
    5.19 +  by (rule measure_eqI) (simp_all add: space_empty_iff)
    5.20 +
    5.21  lemma null_sets_count_space: "null_sets (count_space A) = { {} }"
    5.22    unfolding null_sets_def by (auto simp add: emeasure_count_space_eq_0)
    5.23  
     6.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Oct 06 21:21:46 2014 +0200
     6.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Oct 07 10:34:24 2014 +0200
     6.3 @@ -748,6 +748,9 @@
     6.4  lemma nn_integral_nonneg: "0 \<le> integral\<^sup>N M f"
     6.5    by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: nn_integral_def le_fun_def)
     6.6  
     6.7 +lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \<le> 0 \<longleftrightarrow> integral\<^sup>N M f = 0"
     6.8 +  using nn_integral_nonneg[of M f] by auto
     6.9 +
    6.10  lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \<noteq> -\<infinity>"
    6.11    using nn_integral_nonneg[of M f] by auto
    6.12  
    6.13 @@ -2187,6 +2190,10 @@
    6.14    using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)] B] A
    6.15    by (cases "emeasure M A" "emeasure M (A \<inter> B)" rule: ereal2_cases) (simp_all add: measure_def)
    6.16  
    6.17 +lemma AE_uniform_measureI:
    6.18 +  "A \<in> sets M \<Longrightarrow> (AE x in M. x \<in> A \<longrightarrow> P x) \<Longrightarrow> (AE x in uniform_measure M A. P x)"
    6.19 +  unfolding uniform_measure_def by (auto simp: AE_density)
    6.20 +
    6.21  subsubsection {* Uniform count measure *}
    6.22  
    6.23  definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
     7.1 --- a/src/HOL/Probability/Probability.thy	Mon Oct 06 21:21:46 2014 +0200
     7.2 +++ b/src/HOL/Probability/Probability.thy	Tue Oct 07 10:34:24 2014 +0200
     7.3 @@ -7,6 +7,7 @@
     7.4    Distributions
     7.5    Probability_Mass_Function
     7.6    Stream_Space
     7.7 +  Giry_Monad
     7.8  begin
     7.9  
    7.10  end
     8.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Oct 06 21:21:46 2014 +0200
     8.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 07 10:34:24 2014 +0200
     8.3 @@ -1,20 +1,10 @@
     8.4 +(*  Title:      HOL/Probability/Probability_Mass_Function.thy
     8.5 +    Author:     Johannes Hölzl, TU München *)
     8.6 +
     8.7  theory Probability_Mass_Function
     8.8    imports Probability_Measure
     8.9  begin
    8.10  
    8.11 -lemma sets_Pair: "{x} \<in> sets M1 \<Longrightarrow> {y} \<in> sets M2 \<Longrightarrow> {(x, y)} \<in> sets (M1 \<Otimes>\<^sub>M M2)"
    8.12 -  using pair_measureI[of "{x}" M1 "{y}" M2] by simp
    8.13 -
    8.14 -lemma finite_subset_card:
    8.15 -  assumes X: "infinite X" shows "\<exists>A\<subseteq>X. finite A \<and> card A = n"
    8.16 -proof (induct n)
    8.17 -  case (Suc n) then guess A .. note A = this
    8.18 -  with X obtain x where "x \<in> X" "x \<notin> A"
    8.19 -    by (metis subset_antisym subset_eq)
    8.20 -  with A show ?case  
    8.21 -    by (intro exI[of _ "insert x A"]) auto
    8.22 -qed (simp cong: conj_cong)
    8.23 -
    8.24  lemma (in prob_space) countable_support:
    8.25    "countable {x. measure M {x} \<noteq> 0}"
    8.26  proof -
    8.27 @@ -25,7 +15,7 @@
    8.28    proof (rule ccontr)
    8.29      fix n assume "infinite {x. inverse (Suc n) < ?m x}" (is "infinite ?X")
    8.30      then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
    8.31 -      by (metis finite_subset_card)
    8.32 +      by (metis infinite_arbitrarily_large)
    8.33      from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> 1 / Suc n \<le> ?m x" 
    8.34        by (auto simp: inverse_eq_divide)
    8.35      { fix x assume "x \<in> X"
    8.36 @@ -46,17 +36,10 @@
    8.37      unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
    8.38  qed
    8.39  
    8.40 -lemma measure_count_space: "measure (count_space A) X = (if X \<subseteq> A then card X else 0)"
    8.41 -  unfolding measure_def
    8.42 -  by (cases "finite X") (simp_all add: emeasure_notin_sets)
    8.43 -
    8.44  typedef 'a pmf = "{M :: 'a measure. prob_space M \<and> sets M = UNIV \<and> (AE x in M. measure M {x} \<noteq> 0)}"
    8.45    morphisms measure_pmf Abs_pmf
    8.46 -  apply (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
    8.47 -  apply (auto intro!: prob_space_uniform_measure simp: measure_count_space)
    8.48 -  apply (subst uniform_measure_def)
    8.49 -  apply (simp add: AE_density AE_count_space split: split_indicator)
    8.50 -  done
    8.51 +  by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
    8.52 +     (auto intro!: prob_space_uniform_measure AE_uniform_measureI)
    8.53  
    8.54  declare [[coercion measure_pmf]]
    8.55  
     9.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Oct 06 21:21:46 2014 +0200
     9.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Oct 07 10:34:24 2014 +0200
     9.3 @@ -1759,6 +1759,10 @@
     9.4  lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
     9.5    by auto
     9.6  
     9.7 +lemma space_empty_iff: "space N = {} \<longleftrightarrow> sets N = {{}}"
     9.8 +  by (metis Pow_empty Sup_bot_conv(1) cSup_singleton empty_iff
     9.9 +            sets.sigma_sets_eq sets.space_closed sigma_sets_top subset_singletonD)
    9.10 +
    9.11  subsubsection {* Constructing simple @{typ "'a measure"} *}
    9.12  
    9.13  lemma emeasure_measure_of:
    9.14 @@ -2154,6 +2158,10 @@
    9.15      unfolding measurable_def by auto
    9.16  qed
    9.17  
    9.18 +lemma measurable_empty_iff: 
    9.19 +  "space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}"
    9.20 +  by (auto simp add: measurable_def Pi_iff)
    9.21 +
    9.22  subsubsection {* Extend measure *}
    9.23  
    9.24  definition "extend_measure \<Omega> I G \<mu> =
    10.1 --- a/src/HOL/Probability/Stream_Space.thy	Mon Oct 06 21:21:46 2014 +0200
    10.2 +++ b/src/HOL/Probability/Stream_Space.thy	Tue Oct 07 10:34:24 2014 +0200
    10.3 @@ -1,3 +1,6 @@
    10.4 +(*  Title:      HOL/Probability/Stream_Space.thy
    10.5 +    Author:     Johannes Hölzl, TU München *)
    10.6 +
    10.7  theory Stream_Space
    10.8  imports
    10.9    Infinite_Product_Measure
   10.10 @@ -10,15 +13,6 @@
   10.11  lemma Stream_snth: "(x ## s) !! n = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> s !! n)"
   10.12    by (cases n) simp_all
   10.13  
   10.14 -lemma sets_PiM_cong: assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
   10.15 -  using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
   10.16 -
   10.17 -lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \<le> 0 \<longleftrightarrow> integral\<^sup>N M f = 0"
   10.18 -  using nn_integral_nonneg[of M f] by auto
   10.19 -
   10.20 -lemma restrict_UNIV: "restrict f UNIV = f"
   10.21 -  by (simp add: restrict_def)
   10.22 -
   10.23  definition to_stream :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream" where
   10.24    "to_stream X = smap X nats"
   10.25