src/HOL/Probability/Giry_Monad.thy
changeset 63886 685fb01256af
parent 63626 44ce6b524ff3
child 64008 17a20ca86d62
     1.1 --- a/src/HOL/Probability/Giry_Monad.thy	Thu Sep 15 22:41:05 2016 +0200
     1.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Sep 16 13:56:51 2016 +0200
     1.3 @@ -862,15 +862,15 @@
     1.4    show ?integrable
     1.5      using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
     1.6    have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
     1.7 -  proof(rule integral_cong)
     1.8 +  proof(rule Bochner_Integration.integral_cong)
     1.9      fix M'
    1.10      assume "M' \<in> space M"
    1.11      with sets_eq_imp_space_eq[OF M] have "space M' = space N"
    1.12        by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
    1.13 -    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
    1.14 +    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: Bochner_Integration.integral_empty)
    1.15    qed simp
    1.16    then show ?integral
    1.17 -    using M * by(simp add: integral_empty)
    1.18 +    using M * by(simp add: Bochner_Integration.integral_empty)
    1.19  next
    1.20    assume *: "space N \<noteq> {}"
    1.21  
    1.22 @@ -1213,7 +1213,7 @@
    1.23    also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
    1.24      by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _])
    1.25    finally show ?integral by(simp add: bind_nonempty''[where N=K])
    1.26 -qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
    1.27 +qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite Bochner_Integration.integral_empty)
    1.28  
    1.29  lemma (in prob_space) prob_space_bind:
    1.30    assumes ae: "AE x in M. prob_space (N x)"