src/HOL/Probability/Giry_Monad.thy

   with f show "emeasure (distr M M' f) (space (distr M M' f)) \<le> 1"
     by (auto simp: emeasure_distr emeasure_space_le_1)
   show "space (distr M M' f) \<noteq> {}" by (simp add: assms)
 qed
 
-lemma (in subprob_space) subprob_measure_le_1: "emeasure M X \<le> 1"
+lemma (in subprob_space) subprob_emeasure_le_1: "emeasure M X \<le> 1"
   by (rule order.trans[OF emeasure_space emeasure_space_le_1])
+
+lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1"
+  using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure)
 
 locale pair_subprob_space = 
   pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
 
 sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2"

 
 lemma measurable_emeasure_subprob_algebra[measurable]: 
   "a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)"
   by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def)
 
+lemma subprob_measurableD:
+  assumes N: "N \<in> measurable M (subprob_algebra S)" and x: "x \<in> space M"
+  shows "space (N x) = space S"
+    and "sets (N x) = sets S"
+    and "measurable (N x) K = measurable S K"
+    and "measurable K (N x) = measurable K S"
+  using measurable_space[OF N x]
+  by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)
+
 context
   fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
 begin
 
 lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)"

   assume "space N = {}"
   hence "sets N = {{}}" by (simp add: space_empty_iff)
   moreover have "\<And>M. subprob_space M \<Longrightarrow> sets M \<noteq> {{}}"
     by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric])
   ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
+qed
+
+lemma nn_integral_measurable_subprob_algebra:
+  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
+  shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
+  using f
+proof induct
+  case (cong f g)
+  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"
+    by (intro measurable_cong nn_integral_cong cong)
+       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
+  ultimately show ?case by simp
+next
+  case (set B)
+  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
+    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: measurable_emeasure_subprob_algebra)
+next
+  case (mult f c)
+  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"
+    by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra)
+  ultimately show ?case
+    by simp
+next
+  case (add f g)
+  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"
+    by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: ac_simps)
+next
+  case (seq F)
+  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"
+    unfolding SUP_apply
+    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra)
+  ultimately show ?case
+    by (simp add: ac_simps)
 qed
 
 lemma measurable_distr:
   assumes [measurable]: "f \<in> measurable M N"
   shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"

     also have "\<dots>"
       using A by (intro measurable_emeasure_subprob_algebra) simp
     finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .
   qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty)
 qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
-
-section {* Properties of return *}
-
-definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where
-  "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)"
-
-lemma space_return[simp]: "space (return M x) = space M"
-  by (simp add: return_def)
-
-lemma sets_return[simp]: "sets (return M x) = sets M"
-  by (simp add: return_def)
-
-lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"
-  by (simp cong: measurable_cong_sets) 
-
-lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
-  by (simp cong: measurable_cong_sets) 
-
-lemma emeasure_return[simp]:
-  assumes "A \<in> sets M"
-  shows "emeasure (return M x) A = indicator A x"
-proof (rule emeasure_measure_of[OF return_def])
-  show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed)
-  show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def)
-  from assms show "A \<in> sets (return M x)" unfolding return_def by simp
-  show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)"
-    by (auto intro: countably_additiveI simp: suminf_indicator)
-qed
-
-lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)"
-  by rule simp
-
-lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"
-  by (intro prob_space_return prob_space_imp_subprob_space)
-
-lemma AE_return:
-  assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P"
-  shows "(AE y in return M x. P y) \<longleftrightarrow> P x"
-proof -
-  have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x"
-    by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator)
-  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)"
-    by (rule AE_cong) auto
-  finally show ?thesis .
-qed
-  
-lemma nn_integral_return:
-  assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M"
-  shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x"
-proof-
-  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
-  have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms
-    by (intro nn_integral_cong_AE) (auto simp: AE_return)
-  also have "... = g x"
-    using nn_integral_const[OF `g x \<ge> 0`, of "return M x"] emeasure_space_1 by simp
-  finally show ?thesis .
-qed
-
-lemma return_measurable: "return N \<in> measurable N (subprob_algebra N)"
-  by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)
-
-lemma distr_return:
-  assumes "f \<in> measurable M N" and "x \<in> space M"
-  shows "distr (return M x) N f = return N (f x)"
-  using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)
-
-definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"
-
-lemma select_sets1:
-  "sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))"
-  unfolding select_sets_def by (rule someI)
-
-lemma sets_select_sets[simp]:
-  assumes sets: "sets M = sets (subprob_algebra N)"
-  shows "sets (select_sets M) = sets N"
-  unfolding select_sets_def
-proof (rule someI2)
-  show "sets M = sets (subprob_algebra N)"
-    by fact
-next
-  fix L assume "sets M = sets (subprob_algebra L)"
-  with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)"
-    by (intro sets_eq_imp_space_eq) simp
-  show "sets L = sets N"
-  proof cases
-    assume "space (subprob_algebra N) = {}"
-    with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L]
-    show ?thesis
-      by (simp add: eq space_empty_iff)
-  next
-    assume "space (subprob_algebra N) \<noteq> {}"
-    with eq show ?thesis
-      by (fastforce simp add: space_subprob_algebra)
-  qed
-qed
-
-lemma space_select_sets[simp]:
-  "sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N"
-  by (intro sets_eq_imp_space_eq sets_select_sets)
-
-section {* Join *}
-
-definition join :: "'a measure measure \<Rightarrow> 'a measure" where
-  "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
-
-lemma
-  shows space_join[simp]: "space (join M) = space (select_sets M)"
-    and sets_join[simp]: "sets (join M) = sets (select_sets M)"
-  by (simp_all add: join_def)
-
-lemma emeasure_join:
-  assumes M[simp]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
-  shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
-proof (rule emeasure_measure_of[OF join_def])
-  have eq: "borel_measurable M = borel_measurable (subprob_algebra N)"
-    by auto
-  show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
-  proof (rule countably_additiveI)
-    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"
-    have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"
-      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra eq)
-    also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"
-    proof (rule nn_integral_cong)
-      fix M' assume "M' \<in> space M"
-      then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)"
-        using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra)
-    qed
-    finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" .
-  qed
-qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg)
-
-lemma nn_integral_measurable_subprob_algebra:
-  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
-  shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
-  using f
-proof induct
-  case (cong f g)
-  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"
-    by (intro measurable_cong nn_integral_cong cong)
-       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
-  ultimately show ?case by simp
-next
-  case (set B)
-  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
-    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
-  ultimately show ?case
-    by (simp add: measurable_emeasure_subprob_algebra)
-next
-  case (mult f c)
-  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"
-    by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra)
-  ultimately show ?case
-    by simp
-next
-  case (add f g)
-  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"
-    by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra)
-  ultimately show ?case
-    by (simp add: ac_simps)
-next
-  case (seq F)
-  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"
-    unfolding SUP_apply
-    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra)
-  ultimately show ?case
-    by (simp add: ac_simps)
-qed
-
-
-lemma measurable_join:
-  "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
-proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra)
-  fix A assume "A \<in> sets N"
-  let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))"
-  have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B"
-  proof (rule measurable_cong)
-    fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))"
-    then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')"
-      by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`)
-  qed
-  also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"
-    using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`] emeasure_nonneg[of _ A]
-    by (rule nn_integral_measurable_subprob_algebra)
-  finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .
-next
-  assume [simp]: "space N \<noteq> {}"
-  fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))"
-  then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)"
-    apply (intro nn_integral_mono)
-    apply (auto simp: space_subprob_algebra 
-                 dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1)
-    done
-  with M show "subprob_space (join M)"
-    by (intro subprob_spaceI)
-       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
-next
-  assume "\<not>(space N \<noteq> {})"
-  thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
-qed (auto simp: space_subprob_algebra)
-
-lemma nn_integral_join:
-  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" and M: "sets M = sets (subprob_algebra N)"
-  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
-  using f
-proof induct
-  case (cong f g)
-  moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g"
-    by (intro nn_integral_cong cong) (simp add: M)
-  moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)"
-    by (intro nn_integral_cong cong)
-       (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq)
-  ultimately show ?case
-    by simp
-next
-  case (set A)
-  moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 
-    by (intro nn_integral_cong nn_integral_indicator)
-       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
-  ultimately show ?case
-    using M by (simp add: emeasure_join)
-next
-  case (mult f c)
-  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)"
-    using mult M
-    by (intro nn_integral_cong nn_integral_cmult)
-       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
-  also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
-    using nn_integral_measurable_subprob_algebra[OF mult(3,4)]
-    by (intro nn_integral_cmult mult) (simp add: M)
-  also have "\<dots> = c * (integral\<^sup>N (join M) f)"
-    by (simp add: mult)
-  also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"
-    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M)
-  finally show ?case by simp
-next
-  case (add f g)
-  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)"
-    using add M
-    by (intro nn_integral_cong nn_integral_add)
-       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
-  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)"
-    using nn_integral_measurable_subprob_algebra[OF add(1,2)]
-    using nn_integral_measurable_subprob_algebra[OF add(5,6)]
-    by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)
-  also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
-    by (simp add: add)
-  also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
-    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M)
-  finally show ?case by (simp add: ac_simps)
-next
-  case (seq F)
-  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)"
-    using seq M unfolding SUP_apply
-    by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
-       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
-  also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"
-    using nn_integral_measurable_subprob_algebra[OF seq(1,2)] seq
-    by (intro nn_integral_monotone_convergence_SUP)
-       (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
-  also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"
-    by (simp add: seq)
-  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
-    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) (simp_all add: M)
-  finally show ?case by (simp add: ac_simps)
-qed
-
-lemma join_assoc:
-  assumes M: "sets M = sets (subprob_algebra (subprob_algebra N))"
-  shows "join (distr M (subprob_algebra N) join) = join (join M)"
-proof (rule measure_eqI)
-  fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"
-  then have A: "A \<in> sets N" by simp
-  show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
-    using measurable_join[of N]
-    by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg
-                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ _ M]
-             intro!: nn_integral_cong emeasure_join cong: measurable_cong)
-qed (simp add: M)
-
-lemma join_return: 
-  assumes "sets M = sets N" and "subprob_space M"
-  shows "join (return (subprob_algebra N) M) = M"
-  by (rule measure_eqI)
-     (simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra  
-                    measurable_emeasure_subprob_algebra nn_integral_return assms)
-
-lemma join_return':
-  assumes "sets N = sets M"
-  shows "join (distr M (subprob_algebra N) (return N)) = M"
-apply (rule measure_eqI)
-apply (simp add: assms)
-apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)")
-apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)
-apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable)
-done
-
-lemma join_distr_distr:
-  fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure"
-  assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N"
-  shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l")
-proof (rule measure_eqI)
-  fix A assume "A \<in> sets ?r"
-  hence A_in_N: "A \<in> sets N" by simp
-
-  from assms have "f \<in> measurable (join M) N" 
-      by (simp cong: measurable_cong_sets)
-  moreover from assms and A_in_N have "f-`A \<inter> space R \<in> sets R" 
-      by (intro measurable_sets) simp_all
-  ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-`A \<inter> space R) \<partial>M"
-      by (simp_all add: A_in_N emeasure_distr emeasure_join assms)
-  
-  also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N
-  proof (intro nn_integral_cong, subst emeasure_distr)
-    fix M' assume "M' \<in> space M"
-    from assms have "space M = space (subprob_algebra R)"
-        using sets_eq_imp_space_eq by blast
-    with `M' \<in> space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast
-    show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms)
-    have "space M' = space R" by (rule sets_eq_imp_space_eq) simp
-    thus "emeasure M' (f -` A \<inter> space R) = emeasure M' (f -` A \<inter> space M')" by simp
-  qed
-
-  also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)"
-      by (simp cong: measurable_cong_sets add: assms measurable_distr)
-  hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = 
-             emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A"
-      by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra)
-  finally show "emeasure ?r A = emeasure ?l A" ..
-qed simp
-
-definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where
-  "bind M f = (if space M = {} then count_space {} else
-    join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
-
-adhoc_overloading Monad_Syntax.bind bind
-
-lemma bind_empty: 
-  "space M = {} \<Longrightarrow> bind M f = count_space {}"
-  by (simp add: bind_def)
-
-lemma bind_nonempty:
-  "space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)"
-  by (simp add: bind_def)
-
-lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}"
-  by (auto simp: bind_def)
-
-lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
-  by (simp add: bind_def)
-
-lemma sets_bind[simp]: 
-  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
-  shows "sets (bind M f) = sets N"
-    using assms(2) by (force simp: bind_nonempty intro!: sets_kernel[OF assms(1) someI_ex])
-
-lemma space_bind[simp]: 
-  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
-  shows "space (bind M f) = space N"
-    using assms by (intro sets_eq_imp_space_eq sets_bind)
-
-lemma bind_cong: 
-  assumes "\<forall>x \<in> space M. f x = g x"
-  shows "bind M f = bind M g"
-proof (cases "space M = {}")
-  assume "space M \<noteq> {}"
-  hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast
-  with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast
-  with `space M \<noteq> {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong)
-qed (simp add: bind_empty)
-
-lemma bind_nonempty':
-  assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M"
-  shows "bind M f = join (distr M (subprob_algebra N) f)"
-  using assms
-  apply (subst bind_nonempty, blast)
-  apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast)
-  apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]])
-  done
-
-lemma bind_nonempty'':
-  assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}"
-  shows "bind M f = join (distr M (subprob_algebra N) f)"
-  using assms by (auto intro: bind_nonempty')
-
-lemma emeasure_bind:
-    "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>
-      \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
-  by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
-
-lemma bind_return: 
-  assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M"
-  shows "bind (return M x) f = f x"
-  using sets_kernel[OF assms] assms
-  by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty'
-               cong: subprob_algebra_cong)
-
-lemma bind_return':
-  shows "bind M (return M) = M"
-  by (cases "space M = {}")
-     (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 
-               cong: subprob_algebra_cong)
-
-lemma bind_count_space_singleton:
-  assumes "subprob_space (f x)"
-  shows "count_space {x} \<guillemotright>= f = f x"
-proof-
-  have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
-  have "count_space {x} = return (count_space {x}) x"
-    by (intro measure_eqI) (auto dest: A)
-  also have "... \<guillemotright>= f = f x"
-    by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
-  finally show ?thesis .
-qed
-
-lemma emeasure_bind_const: 
-    "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 
-         emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
-  by (simp add: bind_nonempty emeasure_join nn_integral_distr 
-                space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg)
-
-lemma emeasure_bind_const':
-  assumes "subprob_space M" "subprob_space N"
-  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
-using assms
-proof (case_tac "X \<in> sets N")
-  fix X assume "X \<in> sets N"
-  thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
-      by (subst emeasure_bind_const) 
-         (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1)
-next
-  fix X assume "X \<notin> sets N"
-  with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
-      by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty
-                    space_subprob_algebra emeasure_notin_sets)
-qed
-
-lemma emeasure_bind_const_prob_space:
-  assumes "prob_space M" "subprob_space N"
-  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X"
-  using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 
-                            prob_space.emeasure_space_1)
-
-lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
-  by (intro measure_eqI) 
-     (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
-
-lemma bind_return_distr: 
-    "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (return N \<circ> f) = distr M N f"
-  apply (simp add: bind_nonempty)
-  apply (subst subprob_algebra_cong)
-  apply (rule sets_return)
-  apply (subst distr_distr[symmetric])
-  apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return')
-  done
-
-lemma bind_assoc:
-  fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure"
-  assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)"
-  shows "bind (bind M f) g = bind M (\<lambda>x. bind (f x) g)"
-proof (cases "space M = {}")
-  assume [simp]: "space M \<noteq> {}"
-  from assms have [simp]: "space N \<noteq> {}" "space R \<noteq> {}"
-      by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
-  from assms have sets_fx[simp]: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N"
-      by (simp add: sets_kernel)
-  have ex_in: "\<And>A. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A" by blast
-  note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF `space M \<noteq> {}`]]]
-                         sets_kernel[OF M2 someI_ex[OF ex_in[OF `space N \<noteq> {}`]]]
-  note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)]
-
-  have "bind M (\<lambda>x. bind (f x) g) = 
-        join (distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f))"
-    by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def
-             cong: subprob_algebra_cong distr_cong)
-  also have "distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f) =
-             distr (distr (distr M (subprob_algebra N) f)
-                          (subprob_algebra (subprob_algebra R))
-                          (\<lambda>x. distr x (subprob_algebra R) g)) 
-                   (subprob_algebra R) join"
-      apply (subst distr_distr, 
-             (blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+
-      apply (simp add: o_assoc)
-      done
-  also have "join ... = bind (bind M f) g"
-      by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong)
-  finally show ?thesis ..
-qed (simp add: bind_empty)
 
 lemma emeasure_space_subprob_algebra[measurable]:
   "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"
 proof-
   have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M")

       using union by auto
     finally show ?case .
   qed simp
 qed
 
-(* TODO: Move *)
+lemma restrict_space_measurable:
+  assumes X: "X \<noteq> {}" "X \<in> sets K"
+  assumes N: "N \<in> measurable M (subprob_algebra K)"
+  shows "(\<lambda>x. restrict_space (N x) X) \<in> measurable M (subprob_algebra (restrict_space K X))"
+proof (rule measurable_subprob_algebra)
+  fix a assume a: "a \<in> space M"
+  from N[THEN measurable_space, OF this]
+  have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K"
+    by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
+  then interpret subprob_space "N a"
+    by simp
+  show "subprob_space (restrict_space (N a) X)"
+  proof
+    show "space (restrict_space (N a) X) \<noteq> {}"
+      using X by (auto simp add: space_restrict_space)
+    show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \<le> 1"
+      using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1)
+  qed
+  show "sets (restrict_space (N a) X) = sets (restrict_space K X)"
+    by (intro sets_restrict_space_cong) fact
+next
+  fix A assume A: "A \<in> sets (restrict_space K X)"
+  show "(\<lambda>a. emeasure (restrict_space (N a) X) A) \<in> borel_measurable M"
+  proof (subst measurable_cong)
+    fix a assume "a \<in> space M"
+    from N[THEN measurable_space, OF this]
+    have [simp]: "sets (N a) = sets K" "space (N a) = space K"
+      by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
+    show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \<inter> X)"
+      using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps)
+  next
+    show "(\<lambda>w. emeasure (N w) (A \<inter> X)) \<in> borel_measurable M"
+      using A X
+      by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra])
+         (auto simp: sets_restrict_space)
+  qed
+qed
+
+section {* Properties of return *}
+
+definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where
+  "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)"
+
+lemma space_return[simp]: "space (return M x) = space M"
+  by (simp add: return_def)
+
+lemma sets_return[simp]: "sets (return M x) = sets M"
+  by (simp add: return_def)
+
+lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"
+  by (simp cong: measurable_cong_sets) 
+
+lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
+  by (simp cong: measurable_cong_sets) 
+
+lemma return_sets_cong: "sets M = sets N \<Longrightarrow> return M = return N"
+  by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def)
+
+lemma return_cong: "sets A = sets B \<Longrightarrow> return A x = return B x"
+  by (auto simp add: return_def dest: sets_eq_imp_space_eq)
+
+lemma emeasure_return[simp]:
+  assumes "A \<in> sets M"
+  shows "emeasure (return M x) A = indicator A x"
+proof (rule emeasure_measure_of[OF return_def])
+  show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed)
+  show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def)
+  from assms show "A \<in> sets (return M x)" unfolding return_def by simp
+  show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)"
+    by (auto intro: countably_additiveI simp: suminf_indicator)
+qed
+
+lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)"
+  by rule simp
+
+lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"
+  by (intro prob_space_return prob_space_imp_subprob_space)
+
+lemma subprob_space_return_ne: 
+  assumes "space M \<noteq> {}" shows "subprob_space (return M x)"
+proof
+  show "emeasure (return M x) (space (return M x)) \<le> 1"
+    by (subst emeasure_return) (auto split: split_indicator)
+qed (simp, fact)
+
+lemma measure_return: assumes X: "X \<in> sets M" shows "measure (return M x) X = indicator X x"
+  unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator)
+
+lemma AE_return:
+  assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P"
+  shows "(AE y in return M x. P y) \<longleftrightarrow> P x"
+proof -
+  have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x"
+    by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator)
+  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)"
+    by (rule AE_cong) auto
+  finally show ?thesis .
+qed
+  
+lemma nn_integral_return:
+  assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M"
+  shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x"
+proof-
+  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
+  have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms
+    by (intro nn_integral_cong_AE) (auto simp: AE_return)
+  also have "... = g x"
+    using nn_integral_const[OF `g x \<ge> 0`, of "return M x"] emeasure_space_1 by simp
+  finally show ?thesis .
+qed
+
+lemma integral_return:
+  fixes g :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes "x \<in> space M" "g \<in> borel_measurable M"
+  shows "(\<integral>a. g a \<partial>return M x) = g x"
+proof-
+  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
+  have "(\<integral>a. g a \<partial>return M x) = (\<integral>a. g x \<partial>return M x)" using assms
+    by (intro integral_cong_AE) (auto simp: AE_return)
+  then show ?thesis
+    using prob_space by simp
+qed
+
+lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)"
+  by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)
+
+lemma distr_return:
+  assumes "f \<in> measurable M N" and "x \<in> space M"
+  shows "distr (return M x) N f = return N (f x)"
+  using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)
+
+lemma return_restrict_space:
+  "\<Omega> \<in> sets M \<Longrightarrow> return (restrict_space M \<Omega>) x = restrict_space (return M x) \<Omega>"
+  by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)
+
 lemma measurable_distr2:
   assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
   assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
   shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
 proof -

     apply measurable
     done
   finally show ?thesis .
 qed
 
-(* END TODO *)
+lemma nn_integral_measurable_subprob_algebra2:
+  assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" and [simp]: "\<And>x y. 0 \<le> f x y"
+  assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)"
+  shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
+proof -
+  have "(\<lambda>x. integral\<^sup>N (distr (L x) (M \<Otimes>\<^sub>M N) (\<lambda>y. (x, y))) (\<lambda>(x, y). f x y)) \<in> borel_measurable M"
+    apply (rule measurable_compose[OF _ nn_integral_measurable_subprob_algebra])
+    apply (rule measurable_distr2)
+    apply measurable
+    apply (simp split: prod.split)
+    done
+  then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
+    apply (rule measurable_cong[THEN iffD1, rotated])
+    apply (subst nn_integral_distr)
+    apply measurable
+    apply (rule subprob_measurableD(2)[OF N], assumption)
+    apply measurable
+    done
+qed
+
+lemma emeasure_measurable_subprob_algebra2:
+  assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"
+  assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"
+  shows "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"
+proof -
+  { fix x assume "x \<in> space M"
+    then have "Pair x -` Sigma (space M) A = A x"
+      by auto
+    with sets_Pair1[OF A, of x] have "A x \<in> sets N"
+      by auto }
+  note ** = this
+
+  have *: "\<And>x. fst x \<in> space M \<Longrightarrow> snd x \<in> A (fst x) \<longleftrightarrow> x \<in> (SIGMA x:space M. A x)"
+    by (auto simp: fun_eq_iff)
+  have "(\<lambda>(x, y). indicator (A x) y::ereal) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"
+    apply measurable
+    apply (subst measurable_cong)
+    apply (rule *)
+    apply (auto simp: space_pair_measure)
+    done
+  then have "(\<lambda>x. integral\<^sup>N (L x) (indicator (A x))) \<in> borel_measurable M"
+    by (intro nn_integral_measurable_subprob_algebra2[where N=N] ereal_indicator_nonneg L)
+  then show "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"
+    apply (rule measurable_cong[THEN iffD1, rotated])
+    apply (rule nn_integral_indicator)
+    apply (simp add: subprob_measurableD[OF L] **)
+    done
+qed
+
+lemma measure_measurable_subprob_algebra2:
+  assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"
+  assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"
+  shows "(\<lambda>x. measure (L x) (A x)) \<in> borel_measurable M"
+  unfolding measure_def
+  by (intro borel_measurable_real_of_ereal emeasure_measurable_subprob_algebra2[OF assms])
+
+definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"
+
+lemma select_sets1:
+  "sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))"
+  unfolding select_sets_def by (rule someI)
+
+lemma sets_select_sets[simp]:
+  assumes sets: "sets M = sets (subprob_algebra N)"
+  shows "sets (select_sets M) = sets N"
+  unfolding select_sets_def
+proof (rule someI2)
+  show "sets M = sets (subprob_algebra N)"
+    by fact
+next
+  fix L assume "sets M = sets (subprob_algebra L)"
+  with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)"
+    by (intro sets_eq_imp_space_eq) simp
+  show "sets L = sets N"
+  proof cases
+    assume "space (subprob_algebra N) = {}"
+    with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L]
+    show ?thesis
+      by (simp add: eq space_empty_iff)
+  next
+    assume "space (subprob_algebra N) \<noteq> {}"
+    with eq show ?thesis
+      by (fastforce simp add: space_subprob_algebra)
+  qed
+qed
+
+lemma space_select_sets[simp]:
+  "sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N"
+  by (intro sets_eq_imp_space_eq sets_select_sets)
+
+section {* Join *}
+
+definition join :: "'a measure measure \<Rightarrow> 'a measure" where
+  "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
+
+lemma
+  shows space_join[simp]: "space (join M) = space (select_sets M)"
+    and sets_join[simp]: "sets (join M) = sets (select_sets M)"
+  by (simp_all add: join_def)
+
+lemma emeasure_join:
+  assumes M[simp]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
+  shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
+proof (rule emeasure_measure_of[OF join_def])
+  have eq: "borel_measurable M = borel_measurable (subprob_algebra N)"
+    by auto
+  show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
+  proof (rule countably_additiveI)
+    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"
+    have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"
+      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra eq)
+    also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"
+    proof (rule nn_integral_cong)
+      fix M' assume "M' \<in> space M"
+      then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)"
+        using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra)
+    qed
+    finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" .
+  qed
+qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg)
+
+lemma measurable_join:
+  "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
+proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra)
+  fix A assume "A \<in> sets N"
+  let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))"
+  have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B"
+  proof (rule measurable_cong)
+    fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))"
+    then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')"
+      by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`)
+  qed
+  also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"
+    using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`] emeasure_nonneg[of _ A]
+    by (rule nn_integral_measurable_subprob_algebra)
+  finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .
+next
+  assume [simp]: "space N \<noteq> {}"
+  fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))"
+  then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)"
+    apply (intro nn_integral_mono)
+    apply (auto simp: space_subprob_algebra 
+                 dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1)
+    done
+  with M show "subprob_space (join M)"
+    by (intro subprob_spaceI)
+       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
+next
+  assume "\<not>(space N \<noteq> {})"
+  thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
+qed (auto simp: space_subprob_algebra)
+
+lemma nn_integral_join:
+  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" and M: "sets M = sets (subprob_algebra N)"
+  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
+  using f
+proof induct
+  case (cong f g)
+  moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g"
+    by (intro nn_integral_cong cong) (simp add: M)
+  moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)"
+    by (intro nn_integral_cong cong)
+       (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq)
+  ultimately show ?case
+    by simp
+next
+  case (set A)
+  moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 
+    by (intro nn_integral_cong nn_integral_indicator)
+       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
+  ultimately show ?case
+    using M by (simp add: emeasure_join)
+next
+  case (mult f c)
+  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)"
+    using mult M
+    by (intro nn_integral_cong nn_integral_cmult)
+       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+  also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
+    using nn_integral_measurable_subprob_algebra[OF mult(3,4)]
+    by (intro nn_integral_cmult mult) (simp add: M)
+  also have "\<dots> = c * (integral\<^sup>N (join M) f)"
+    by (simp add: mult)
+  also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"
+    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M)
+  finally show ?case by simp
+next
+  case (add f g)
+  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)"
+    using add M
+    by (intro nn_integral_cong nn_integral_add)
+       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+  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)"
+    using nn_integral_measurable_subprob_algebra[OF add(1,2)]
+    using nn_integral_measurable_subprob_algebra[OF add(5,6)]
+    by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)
+  also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
+    by (simp add: add)
+  also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
+    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M)
+  finally show ?case by (simp add: ac_simps)
+next
+  case (seq F)
+  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)"
+    using seq M unfolding SUP_apply
+    by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
+       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+  also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"
+    using nn_integral_measurable_subprob_algebra[OF seq(1,2)] seq
+    by (intro nn_integral_monotone_convergence_SUP)
+       (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
+  also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"
+    by (simp add: seq)
+  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
+    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) (simp_all add: M)
+  finally show ?case by (simp add: ac_simps)
+qed
+
+lemma join_assoc:
+  assumes M: "sets M = sets (subprob_algebra (subprob_algebra N))"
+  shows "join (distr M (subprob_algebra N) join) = join (join M)"
+proof (rule measure_eqI)
+  fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"
+  then have A: "A \<in> sets N" by simp
+  show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
+    using measurable_join[of N]
+    by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg
+                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ _ M]
+             intro!: nn_integral_cong emeasure_join cong: measurable_cong)
+qed (simp add: M)
+
+lemma join_return: 
+  assumes "sets M = sets N" and "subprob_space M"
+  shows "join (return (subprob_algebra N) M) = M"
+  by (rule measure_eqI)
+     (simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra  
+                    measurable_emeasure_subprob_algebra nn_integral_return assms)
+
+lemma join_return':
+  assumes "sets N = sets M"
+  shows "join (distr M (subprob_algebra N) (return N)) = M"
+apply (rule measure_eqI)
+apply (simp add: assms)
+apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)")
+apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)
+apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable)
+done
+
+lemma join_distr_distr:
+  fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure"
+  assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N"
+  shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l")
+proof (rule measure_eqI)
+  fix A assume "A \<in> sets ?r"
+  hence A_in_N: "A \<in> sets N" by simp
+
+  from assms have "f \<in> measurable (join M) N" 
+      by (simp cong: measurable_cong_sets)
+  moreover from assms and A_in_N have "f-`A \<inter> space R \<in> sets R" 
+      by (intro measurable_sets) simp_all
+  ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-`A \<inter> space R) \<partial>M"
+      by (simp_all add: A_in_N emeasure_distr emeasure_join assms)
+  
+  also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N
+  proof (intro nn_integral_cong, subst emeasure_distr)
+    fix M' assume "M' \<in> space M"
+    from assms have "space M = space (subprob_algebra R)"
+        using sets_eq_imp_space_eq by blast
+    with `M' \<in> space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast
+    show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms)
+    have "space M' = space R" by (rule sets_eq_imp_space_eq) simp
+    thus "emeasure M' (f -` A \<inter> space R) = emeasure M' (f -` A \<inter> space M')" by simp
+  qed
+
+  also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)"
+      by (simp cong: measurable_cong_sets add: assms measurable_distr)
+  hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = 
+             emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A"
+      by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra)
+  finally show "emeasure ?r A = emeasure ?l A" ..
+qed simp
+
+definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where
+  "bind M f = (if space M = {} then count_space {} else
+    join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
+
+adhoc_overloading Monad_Syntax.bind bind
+
+lemma bind_empty: 
+  "space M = {} \<Longrightarrow> bind M f = count_space {}"
+  by (simp add: bind_def)
+
+lemma bind_nonempty:
+  "space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)"
+  by (simp add: bind_def)
+
+lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}"
+  by (auto simp: bind_def)
+
+lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
+  by (simp add: bind_def)
+
+lemma sets_bind[simp]: 
+  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
+  shows "sets (bind M f) = sets N"
+    using assms(2) by (force simp: bind_nonempty intro!: sets_kernel[OF assms(1) someI_ex])
+
+lemma space_bind[simp]: 
+  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
+  shows "space (bind M f) = space N"
+    using assms by (intro sets_eq_imp_space_eq sets_bind)
+
+lemma bind_cong: 
+  assumes "\<forall>x \<in> space M. f x = g x"
+  shows "bind M f = bind M g"
+proof (cases "space M = {}")
+  assume "space M \<noteq> {}"
+  hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast
+  with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast
+  with `space M \<noteq> {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong)
+qed (simp add: bind_empty)
+
+lemma bind_nonempty':
+  assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M"
+  shows "bind M f = join (distr M (subprob_algebra N) f)"
+  using assms
+  apply (subst bind_nonempty, blast)
+  apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast)
+  apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]])
+  done
+
+lemma bind_nonempty'':
+  assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}"
+  shows "bind M f = join (distr M (subprob_algebra N) f)"
+  using assms by (auto intro: bind_nonempty')
+
+lemma emeasure_bind:
+    "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>
+      \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
+  by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
+
+lemma nn_integral_bind:
+  assumes f: "f \<in> borel_measurable B" "\<And>x. 0 \<le> f x"
+  assumes N: "N \<in> measurable M (subprob_algebra B)"
+  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
+proof cases
+  assume M: "space M \<noteq> {}" show ?thesis
+    unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr]
+    by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])
+qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
+
+lemma AE_bind:
+  assumes P[measurable]: "Measurable.pred B P"
+  assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
+  shows "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)"
+proof cases
+  assume M: "space M = {}" show ?thesis
+    unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
+next
+  assume M: "space M \<noteq> {}"
+  have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<guillemotright>= N))"
+    by (intro nn_integral_cong) (simp add: space_bind[OF N M] split: split_indicator)
+
+  have "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0"
+    by (simp add: AE_iff_nn_integral sets_bind[OF N M] space_bind[OF N M] * nn_integral_bind[where B=B]
+             del: nn_integral_indicator)
+  also have "\<dots> = (AE x in M. AE y in N x. P y)"
+    apply (subst nn_integral_0_iff_AE)
+    apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra])
+    apply measurable
+    apply (intro eventually_subst AE_I2)
+    apply simp
+    apply (subst nn_integral_0_iff_AE)
+    apply (simp add: subprob_measurableD(3)[OF N])
+    apply (auto simp add: ereal_indicator_le_0 subprob_measurableD(1)[OF N] intro!: eventually_subst)
+    done
+  finally show ?thesis .
+qed
 
 lemma measurable_bind':
   assumes M1: "f \<in> measurable M (subprob_algebra N)" and
           M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
   shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"

     by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
         rule measurable_compose[OF measurable_snd assms(2)])
   from assms(1) show "M \<in> space (subprob_algebra M)"
     by (simp add: space_subprob_algebra)
 qed
+
+lemma (in prob_space) prob_space_bind: 
+  assumes ae: "AE x in M. prob_space (N x)"
+    and N[measurable]: "N \<in> measurable M (subprob_algebra S)"
+  shows "prob_space (M \<guillemotright>= N)"
+proof
+  have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
+    by (subst emeasure_bind[where N=S])
+       (auto simp: not_empty space_bind[OF N] subprob_measurableD[OF N] intro!: nn_integral_cong)
+  also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)"
+    using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1)
+  finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1"
+    by (simp add: emeasure_space_1)
+qed
+
+lemma (in subprob_space) bind_in_space:
+  "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)"
+  by (auto simp add: space_subprob_algebra subprob_not_empty intro!: subprob_space_bind)
+     unfold_locales
+
+lemma (in subprob_space) measure_bind:
+  assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N"
+  shows "measure (M \<guillemotright>= f) X = \<integral>x. measure (f x) X \<partial>M"
+proof -
+  interpret Mf: subprob_space "M \<guillemotright>= f"
+    by (rule subprob_space_bind[OF _ f]) unfold_locales
+
+  { fix x assume "x \<in> space M"
+    from f[THEN measurable_space, OF this] interpret subprob_space "f x"
+      by (simp add: space_subprob_algebra)
+    have "emeasure (f x) X = ereal (measure (f x) X)" "measure (f x) X \<le> 1"
+      by (auto simp: emeasure_eq_measure subprob_measure_le_1) }
+  note this[simp]
+
+  have "emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
+    using subprob_not_empty f X by (rule emeasure_bind)
+  also have "\<dots> = \<integral>\<^sup>+x. ereal (measure (f x) X) \<partial>M"
+    by (intro nn_integral_cong) simp
+  also have "\<dots> = \<integral>x. measure (f x) X \<partial>M"
+    by (intro nn_integral_eq_integral integrable_const_bound[where B=1]
+              measure_measurable_subprob_algebra2[OF _ f] pair_measureI X)
+       (auto simp: measure_nonneg)
+  finally show ?thesis
+    by (simp add: Mf.emeasure_eq_measure)
+qed
+
+lemma emeasure_bind_const: 
+    "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 
+         emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+  by (simp add: bind_nonempty emeasure_join nn_integral_distr 
+                space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg)
+
+lemma emeasure_bind_const':
+  assumes "subprob_space M" "subprob_space N"
+  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+using assms
+proof (case_tac "X \<in> sets N")
+  fix X assume "X \<in> sets N"
+  thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
+      by (subst emeasure_bind_const) 
+         (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1)
+next
+  fix X assume "X \<notin> sets N"
+  with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
+      by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty
+                    space_subprob_algebra emeasure_notin_sets)
+qed
+
+lemma emeasure_bind_const_prob_space:
+  assumes "prob_space M" "subprob_space N"
+  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X"
+  using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 
+                            prob_space.emeasure_space_1)
+
+lemma bind_return: 
+  assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M"
+  shows "bind (return M x) f = f x"
+  using sets_kernel[OF assms] assms
+  by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty'
+               cong: subprob_algebra_cong)
+
+lemma bind_return':
+  shows "bind M (return M) = M"
+  by (cases "space M = {}")
+     (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 
+               cong: subprob_algebra_cong)
+
+lemma distr_bind:
+  assumes N: "N \<in> measurable M (subprob_algebra K)" "space M \<noteq> {}"
+  assumes f: "f \<in> measurable K R"
+  shows "distr (M \<guillemotright>= N) R f = (M \<guillemotright>= (\<lambda>x. distr (N x) R f))"
+  unfolding bind_nonempty''[OF N]
+  apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)])
+  apply (rule f)
+  apply (simp add: join_distr_distr[OF _ f, symmetric])
+  apply (subst distr_distr[OF measurable_distr, OF f N(1)])
+  apply (simp add: comp_def)
+  done
+
+lemma bind_distr:
+  assumes f[measurable]: "f \<in> measurable M X"
+  assumes N[measurable]: "N \<in> measurable X (subprob_algebra K)" and "space M \<noteq> {}"
+  shows "(distr M X f \<guillemotright>= N) = (M \<guillemotright>= (\<lambda>x. N (f x)))"
+proof -
+  have "space X \<noteq> {}" "space M \<noteq> {}"
+    using `space M \<noteq> {}` f[THEN measurable_space] by auto
+  then show ?thesis
+    by (simp add: bind_nonempty''[where N=K] distr_distr comp_def)
+qed
+
+lemma bind_count_space_singleton:
+  assumes "subprob_space (f x)"
+  shows "count_space {x} \<guillemotright>= f = f x"
+proof-
+  have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
+  have "count_space {x} = return (count_space {x}) x"
+    by (intro measure_eqI) (auto dest: A)
+  also have "... \<guillemotright>= f = f x"
+    by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
+  finally show ?thesis .
+qed
+
+lemma restrict_space_bind:
+  assumes N: "N \<in> measurable M (subprob_algebra K)"
+  assumes "space M \<noteq> {}"
+  assumes X[simp]: "X \<in> sets K" "X \<noteq> {}"
+  shows "restrict_space (bind M N) X = bind M (\<lambda>x. restrict_space (N x) X)"
+proof (rule measure_eqI)
+  fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)"
+  with X have "A \<in> sets K" "A \<subseteq> X"
+    by (auto simp: sets_restrict_space sets_bind[OF assms(1,2)])
+  then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A"
+    using assms
+    apply (subst emeasure_restrict_space)
+    apply (simp_all add: space_bind[OF assms(1,2)] sets_bind[OF assms(1,2)] emeasure_bind[OF assms(2,1)])
+    apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]])
+    apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra
+                intro!: nn_integral_cong dest!: measurable_space)
+    done
+qed (simp add: sets_restrict_space sets_bind[OF assms(1,2)] sets_bind[OF restrict_space_measurable[OF assms(4,3,1)] assms(2)])
+
+lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
+  by (intro measure_eqI) 
+     (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
+
+lemma bind_return_distr: 
+    "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (return N \<circ> f) = distr M N f"
+  apply (simp add: bind_nonempty)
+  apply (subst subprob_algebra_cong)
+  apply (rule sets_return)
+  apply (subst distr_distr[symmetric])
+  apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return')
+  done
+
+lemma bind_assoc:
+  fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure"
+  assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)"
+  shows "bind (bind M f) g = bind M (\<lambda>x. bind (f x) g)"
+proof (cases "space M = {}")
+  assume [simp]: "space M \<noteq> {}"
+  from assms have [simp]: "space N \<noteq> {}" "space R \<noteq> {}"
+      by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
+  from assms have sets_fx[simp]: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N"
+      by (simp add: sets_kernel)
+  have ex_in: "\<And>A. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A" by blast
+  note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF `space M \<noteq> {}`]]]
+                         sets_kernel[OF M2 someI_ex[OF ex_in[OF `space N \<noteq> {}`]]]
+  note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)]
+
+  have "bind M (\<lambda>x. bind (f x) g) = 
+        join (distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f))"
+    by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def
+             cong: subprob_algebra_cong distr_cong)
+  also have "distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f) =
+             distr (distr (distr M (subprob_algebra N) f)
+                          (subprob_algebra (subprob_algebra R))
+                          (\<lambda>x. distr x (subprob_algebra R) g)) 
+                   (subprob_algebra R) join"
+      apply (subst distr_distr, 
+             (blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+
+      apply (simp add: o_assoc)
+      done
+  also have "join ... = bind (bind M f) g"
+      by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong)
+  finally show ?thesis ..
+qed (simp add: bind_empty)
 
 lemma double_bind_assoc:
   assumes Mg: "g \<in> measurable N (subprob_algebra N')"
   assumes Mf: "f \<in> measurable M (subprob_algebra M')"
   assumes Mh: "split h \<in> measurable (M \<Otimes>\<^sub>M M') N"

     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)}"
     by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure)
   finally show ?thesis ..
 qed
 
+lemma (in pair_prob_space) pair_measure_eq_bind:
+  "(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
+proof (rule measure_eqI)
+  have ps_M2: "prob_space M2" by unfold_locales
+  note return_measurable[measurable]
+  have 1: "(\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))) \<in> measurable M1 (subprob_algebra (M1 \<Otimes>\<^sub>M M2))"
+    by (auto simp add: space_subprob_algebra ps_M2
+             intro!: measurable_bind[where N=M2] measurable_const prob_space_imp_subprob_space)
+  show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
+    by (simp add: M1.not_empty sets_bind[OF 1])
+  fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)"
+  show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A"
+    by (auto simp: M2.emeasure_pair_measure emeasure_bind[OF _ 1] M1.not_empty
+                          emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"] M2.not_empty
+             intro!: nn_integral_cong)
+qed
+
+lemma (in pair_prob_space) bind_rotate:
+  assumes C[measurable]: "(\<lambda>(x, y). C x y) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (subprob_algebra N)"
+  shows "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
+proof - 
+  interpret swap: pair_prob_space M2 M1 by unfold_locales
+  note measurable_bind[where N="M2", measurable]
+  note measurable_bind[where N="M1", measurable]
+  have [simp]: "M1 \<in> space (subprob_algebra M1)" "M2 \<in> space (subprob_algebra M2)"
+    by (auto simp: space_subprob_algebra) unfold_locales
+  have "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = 
+    (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<guillemotright>= (\<lambda>(x, y). C x y)"
+    by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M1 \<Otimes>\<^sub>M M2" and R=N])
+  also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<guillemotright>= (\<lambda>(x, y). C x y)"
+    unfolding pair_measure_eq_bind[symmetric] distr_pair_swap[symmetric] ..
+  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>x. M1 \<guillemotright>= (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<guillemotright>= (\<lambda>(y, x). C x y)"
+    unfolding swap.pair_measure_eq_bind[symmetric]
+    by (auto simp add: space_pair_measure M1.not_empty M2.not_empty bind_distr[OF _ C] intro!: bind_cong)
+  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
+    by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M2 \<Otimes>\<^sub>M M1" and R=N])
+  finally show ?thesis .
+qed
+
 section {* Measures form a $\omega$-chain complete partial order *}
 
 definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where
   "SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)"