--- a/src/HOL/Probability/Giry_Monad.thy Wed Oct 07 15:31:59 2015 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Wed Oct 07 17:11:16 2015 +0200
@@ -1405,6 +1405,10 @@
apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return')
done
+lemma bind_return_distr':
+ "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (\<lambda>x. return N (f x)) = distr M N f"
+ using bind_return_distr[of M f N] by (simp add: comp_def)
+
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)"