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)