src/HOL/Probability/Giry_Monad.thy
changeset 64320 ba194424b895
parent 64010 9c99fccce3cf
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Probability/Giry_Monad.thy	Thu Oct 20 18:41:58 2016 +0200
     1.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Thu Oct 20 18:41:59 2016 +0200
     1.3 @@ -1778,4 +1778,10 @@
     1.4    shows "space (M \<bind> f) = space B"
     1.5    using M by (intro space_bind[OF sets_kernel[OF f]]) auto
     1.6  
     1.7 +lemma bind_distr_return:
     1.8 +  "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> g \<in> N \<rightarrow>\<^sub>M L \<Longrightarrow> space M \<noteq> {} \<Longrightarrow>
     1.9 +    distr M N f \<bind> (\<lambda>x. return L (g x)) = distr M L (\<lambda>x. g (f x))"
    1.10 +  by (subst bind_distr[OF _ measurable_compose[OF _ return_measurable]])
    1.11 +     (auto intro!: bind_return_distr')
    1.12 +
    1.13  end