src/HOL/Probability/Giry_Monad.thy
changeset 61753 865bb718bdb9
parent 61634 48e2de1b1df5
child 61808 fc1556774cfe
equal deleted inserted replaced
61752:814bbe5d9204 61753:865bb718bdb9
   277 next
   277 next
   278   case (mult f c)
   278   case (mult f c)
   279   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"
   279   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"
   280     by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
   280     by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
   281   ultimately show ?case
   281   ultimately show ?case
   282     using [[simp_trace_new]]
       
   283     by simp
   282     by simp
   284 next
   283 next
   285   case (add f g)
   284   case (add f g)
   286   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"
   285   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"
   287     by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
   286     by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)