diff -r fc571ebb04e1 -r 6eb0725503fc src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -44,9 +44,12 @@
   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
 
@@ -75,6 +78,15 @@
   "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
@@ -113,6 +125,43 @@
   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)"
@@ -131,6 +180,118 @@
   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)
 
+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")
+    by (rule measurable_emeasure_subprob_algebra) simp
+  also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
+    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
+  finally show ?thesis .
+qed
+
+(* TODO: Rename. This name is too general – Manuel *)
+lemma measurable_pair_measure:
+  assumes f: "f \<in> measurable M (subprob_algebra N)"
+  assumes g: "g \<in> measurable M (subprob_algebra L)"
+  shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
+proof (rule measurable_subprob_algebra)
+  { fix x assume "x \<in> space M"
+    with measurable_space[OF f] measurable_space[OF g]
+    have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"
+      by auto
+    interpret F: subprob_space "f x"
+      using fx by (simp add: space_subprob_algebra)
+    interpret G: subprob_space "g x"
+      using gx by (simp add: space_subprob_algebra)
+
+    interpret pair_subprob_space "f x" "g x" ..
+    show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales
+    show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"
+      using fx gx by (simp add: space_subprob_algebra)
+
+    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"
+      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 
+    have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 
+              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
+      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
+    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) =
+                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
+      using emeasure_compl[OF _ P.emeasure_finite]
+      unfolding sets_eq
+      unfolding sets_eq_imp_space_eq[OF sets_eq]
+      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
+    note 1 2 sets_eq }
+  note Times = this(1) and Compl = this(2) and sets_eq = this(3)
+
+  fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
+  show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"
+    using Int_stable_pair_measure_generator pair_measure_closed A
+    unfolding sets_pair_measure
+  proof (induct A rule: sigma_sets_induct_disjoint)
+    case (basic A) then show ?case
+      by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)
+         (auto intro!: measurable_emeasure_kernel f g)
+  next
+    case (compl A)
+    then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
+      by (auto simp: sets_pair_measure)
+    have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 
+                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
+      using compl(2) f g by measurable
+    thus ?case by (simp add: Compl A cong: measurable_cong)
+  next
+    case (union A)
+    then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"
+      by (auto simp: sets_pair_measure)
+    then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>
+      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
+      by (intro measurable_cong suminf_emeasure[symmetric])
+         (auto simp: sets_eq)
+    also have "\<dots>"
+      using union by auto
+    finally show ?case .
+  qed simp
+qed
+
+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
@@ -148,6 +309,12 @@
 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"
@@ -165,6 +332,16 @@
 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"
@@ -188,7 +365,19 @@
   finally show ?thesis .
 qed
 
-lemma return_measurable: "return N \<in> measurable N (subprob_algebra N)"
+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:
@@ -196,6 +385,121 @@
   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 -
+  have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
+    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
+  proof (rule measurable_cong)
+    fix x assume x: "x \<in> space L"
+    have gx: "g x \<in> space (subprob_algebra M)"
+      using measurable_space[OF g x] .
+    then have [simp]: "sets (g x) = sets M"
+      by (simp add: space_subprob_algebra)
+    then have [simp]: "space (g x) = space M"
+      by (rule sets_eq_imp_space_eq)
+    let ?R = "return L x"
+    from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"
+      by simp
+    interpret subprob_space "g x"
+      using gx by (simp add: space_subprob_algebra)
+    have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
+      by (simp add: space_pair_measure)
+    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
+    proof (rule measure_eqI)
+      show "sets ?l = sets ?r"
+        by simp
+    next
+      fix A assume "A \<in> sets ?l"
+      then have A[measurable]: "A \<in> sets N"
+        by simp
+      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))"
+        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
+      also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)"
+        apply (subst emeasure_pair_measure_alt)
+        apply (rule measurable_sets[OF _ A])
+        apply (auto simp add: f_M' cong: measurable_cong_sets)
+        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
+        apply (auto simp: space_subprob_algebra space_pair_measure)
+        done
+      also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)"
+        by (subst nn_integral_return)
+           (auto simp: x intro!: measurable_emeasure)
+      also have "\<dots> = emeasure ?l A"
+        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
+      finally show "emeasure ?l A = emeasure ?r A" ..
+    qed
+  qed
+  also have "\<dots>"
+    apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])
+    apply (rule return_measurable)
+    apply measurable
+    done
+  finally show ?thesis .
+qed
+
+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:
@@ -261,44 +565,6 @@
   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)
@@ -519,29 +785,129 @@
       \<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 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)"
+proof (subst measurable_cong)
+  fix x assume x_in_M: "x \<in> space M"
+  with assms have "space (f x) \<noteq> {}" 
+      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
+  moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)"
+      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
+         (auto dest: measurable_Pair2)
+  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 
+      by (simp_all add: bind_nonempty'')
+next
+  show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)"
+    apply (rule measurable_compose[OF _ measurable_join])
+    apply (rule measurable_distr2[OF M2 M1])
+    done
+qed
 
-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 measurable_bind:
+  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
+          M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
+  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
+  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)
+
+lemma measurable_bind2:
+  assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)"
+  shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)"
+    using assms by (intro measurable_bind' measurable_const) auto
+
+lemma subprob_space_bind:
+  assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
+  shows "subprob_space (M \<guillemotright>= f)"
+proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
+  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
+    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 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 .
+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: 
@@ -572,6 +938,73 @@
   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)
@@ -618,180 +1051,6 @@
   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")
-    by (rule measurable_emeasure_subprob_algebra) simp
-  also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
-    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
-  finally show ?thesis .
-qed
-
-(* TODO: Rename. This name is too general – Manuel *)
-lemma measurable_pair_measure:
-  assumes f: "f \<in> measurable M (subprob_algebra N)"
-  assumes g: "g \<in> measurable M (subprob_algebra L)"
-  shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
-proof (rule measurable_subprob_algebra)
-  { fix x assume "x \<in> space M"
-    with measurable_space[OF f] measurable_space[OF g]
-    have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"
-      by auto
-    interpret F: subprob_space "f x"
-      using fx by (simp add: space_subprob_algebra)
-    interpret G: subprob_space "g x"
-      using gx by (simp add: space_subprob_algebra)
-
-    interpret pair_subprob_space "f x" "g x" ..
-    show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales
-    show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"
-      using fx gx by (simp add: space_subprob_algebra)
-
-    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"
-      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 
-    have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 
-              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
-      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
-    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) =
-                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
-      using emeasure_compl[OF _ P.emeasure_finite]
-      unfolding sets_eq
-      unfolding sets_eq_imp_space_eq[OF sets_eq]
-      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
-    note 1 2 sets_eq }
-  note Times = this(1) and Compl = this(2) and sets_eq = this(3)
-
-  fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
-  show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"
-    using Int_stable_pair_measure_generator pair_measure_closed A
-    unfolding sets_pair_measure
-  proof (induct A rule: sigma_sets_induct_disjoint)
-    case (basic A) then show ?case
-      by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)
-         (auto intro!: measurable_emeasure_kernel f g)
-  next
-    case (compl A)
-    then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
-      by (auto simp: sets_pair_measure)
-    have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 
-                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
-      using compl(2) f g by measurable
-    thus ?case by (simp add: Compl A cong: measurable_cong)
-  next
-    case (union A)
-    then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"
-      by (auto simp: sets_pair_measure)
-    then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>
-      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
-      by (intro measurable_cong suminf_emeasure[symmetric])
-         (auto simp: sets_eq)
-    also have "\<dots>"
-      using union by auto
-    finally show ?case .
-  qed simp
-qed
-
-(* TODO: Move *)
-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 -
-  have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
-    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
-  proof (rule measurable_cong)
-    fix x assume x: "x \<in> space L"
-    have gx: "g x \<in> space (subprob_algebra M)"
-      using measurable_space[OF g x] .
-    then have [simp]: "sets (g x) = sets M"
-      by (simp add: space_subprob_algebra)
-    then have [simp]: "space (g x) = space M"
-      by (rule sets_eq_imp_space_eq)
-    let ?R = "return L x"
-    from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"
-      by simp
-    interpret subprob_space "g x"
-      using gx by (simp add: space_subprob_algebra)
-    have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
-      by (simp add: space_pair_measure)
-    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
-    proof (rule measure_eqI)
-      show "sets ?l = sets ?r"
-        by simp
-    next
-      fix A assume "A \<in> sets ?l"
-      then have A[measurable]: "A \<in> sets N"
-        by simp
-      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))"
-        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
-      also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)"
-        apply (subst emeasure_pair_measure_alt)
-        apply (rule measurable_sets[OF _ A])
-        apply (auto simp add: f_M' cong: measurable_cong_sets)
-        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
-        apply (auto simp: space_subprob_algebra space_pair_measure)
-        done
-      also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)"
-        by (subst nn_integral_return)
-           (auto simp: x intro!: measurable_emeasure)
-      also have "\<dots> = emeasure ?l A"
-        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
-      finally show "emeasure ?l A = emeasure ?r A" ..
-    qed
-  qed
-  also have "\<dots>"
-    apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])
-    apply (rule return_measurable)
-    apply measurable
-    done
-  finally show ?thesis .
-qed
-
-(* END TODO *)
-
-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)"
-proof (subst measurable_cong)
-  fix x assume x_in_M: "x \<in> space M"
-  with assms have "space (f x) \<noteq> {}" 
-      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
-  moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)"
-      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
-         (auto dest: measurable_Pair2)
-  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 
-      by (simp_all add: bind_nonempty'')
-next
-  show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)"
-    apply (rule measurable_compose[OF _ measurable_join])
-    apply (rule measurable_distr2[OF M2 M1])
-    done
-qed
-
-lemma measurable_bind:
-  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
-          M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
-  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
-  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)
-
-lemma measurable_bind2:
-  assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)"
-  shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)"
-    using assms by (intro measurable_bind' measurable_const) auto
-
-lemma subprob_space_bind:
-  assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
-  shows "subprob_space (M \<guillemotright>= f)"
-proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
-  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
-    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 double_bind_assoc:
   assumes Mg: "g \<in> measurable N (subprob_algebra N')"
   assumes Mf: "f \<in> measurable M (subprob_algebra M')"
@@ -817,6 +1076,45 @@
   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