diff -r 054f9c9d73ea -r 03944a830c4a src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 12:15:05 2015 +0100 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 10 13:50:30 2015 +0100 @@ -1058,6 +1058,32 @@ by (intro pmf_eqI) simp qed +lemma bind_cond_pmf_cancel: + assumes in_S: "\x. x \ set_pmf p \ x \ S x" + assumes S_eq: "\x y. x \ S y \ S x = S y" + shows "bind_pmf p (\x. cond_pmf p (S x)) = p" +proof (rule pmf_eqI) + have [simp]: "\x. x \ p \ p \ (S x) \ {}" + using in_S by auto + fix z + have pmf_le: "pmf p z \ measure p (S z)" + proof cases + assume "z \ p" from in_S[OF this] show ?thesis + by (auto intro!: measure_pmf.finite_measure_mono simp: pmf.rep_eq) + qed (simp add: set_pmf_iff measure_nonneg) + + have "ereal (pmf (bind_pmf p (\x. cond_pmf p (S x))) z) = + (\\<^sup>+ x. ereal (pmf p z / measure p (S z)) * indicator (S z) x \p)" + by (subst ereal_pmf_bind) + (auto intro!: nn_integral_cong_AE dest!: S_eq split: split_indicator + simp: AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf in_S) + also have "\ = pmf p z" + using pmf_le pmf_nonneg[of p z] + by (subst nn_integral_cmult) (simp_all add: measure_nonneg measure_pmf.emeasure_eq_measure) + finally show "pmf (bind_pmf p (\x. cond_pmf p (S x))) z = pmf p z" + by simp +qed + inductive rel_pmf :: "('a \ 'b \ bool) \ 'a pmf \ 'b pmf \ bool" for R p q where @@ -1114,28 +1140,10 @@ with pq qr show "(R OO S) x z" by blast next - { fix z - have "ereal (pmf (map_pmf snd pr) z) = - (\\<^sup>+y. \\<^sup>+x. indicator (snd -` {z}) x \cond_pmf qr {(y', z). y' = y} \q)" - by (simp add: q pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' bind_map_pmf - ereal_pmf_bind ereal_pmf_map) - also have "\ = (\\<^sup>+y. \\<^sup>+x. indicator (snd -` {z}) x \uniform_measure qr {(y', z). y' = y} \q)" - by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff cond_pmf.rep_eq pr_welldefined - simp del: emeasure_uniform_measure) - also have "\ = (\\<^sup>+y. (\\<^sup>+x. indicator {(y, z)} x \qr) / emeasure q {y} \q)" - by (auto simp: nn_integral_uniform_measure q' simp del: nn_integral_indicator split: split_indicator - intro!: nn_integral_cong arg_cong2[where f="op /"] arg_cong2[where f=emeasure]) - also have "\ = (\\<^sup>+y. pmf qr (y, z) \count_space UNIV)" - by (subst measure_pmf_eq_density) - (force simp: q' emeasure_pmf_single nn_integral_density pmf_nonneg pmf_eq_0_set_pmf set_map_pmf - intro!: nn_integral_cong split: split_indicator) - also have "\ = ereal (pmf r z)" - by (subst nn_integral_pmf') - (auto simp add: inj_on_def r ereal_pmf_map intro!: arg_cong2[where f=emeasure]) - finally have "pmf (map_pmf snd pr) z = pmf r z" - by simp } + have "map_pmf snd pr = map_pmf snd (bind_pmf q (\y. cond_pmf qr {(y', z). y' = y}))" + by (simp add: pr_def q split_beta bind_map_pmf bind_return_pmf'' map_bind_pmf map_return_pmf) then show "map_pmf snd pr = r" - by (rule pmf_eqI) + unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf bind_return_pmf'' p) } then show "rel_pmf R OO rel_pmf S \ rel_pmf (R OO S)" by(auto simp add: le_fun_def)