src/HOL/Probability/Probability_Mass_Function.thy
 changeset 59526 af02440afb4a parent 59525 dfe6449aecd8 child 59527 edaabc1ab1ed
```     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 11 15:22:37 2015 +0100
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Feb 11 18:38:34 2015 +0100
1.3 @@ -1078,29 +1078,32 @@
1.4  qed
1.5
1.6  lemma bind_cond_pmf_cancel:
1.7 -  assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x"
1.8 +  assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x" "\<And>x. x \<in> set_pmf q \<Longrightarrow> x \<in> S x"
1.9    assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y"
1.10 -  shows "bind_pmf p (\<lambda>x. cond_pmf p (S x)) = p"
1.11 +  and same: "\<And>x. measure (measure_pmf p) (S x) = measure (measure_pmf q) (S x)"
1.12 +  shows "bind_pmf p (\<lambda>x. cond_pmf q (S x)) = q" (is "?lhs = _")
1.13  proof (rule pmf_eqI)
1.14 -  have [simp]: "\<And>x. x \<in> p \<Longrightarrow> p \<inter> (S x) \<noteq> {}"
1.15 -    using in_S by auto
1.16 +  { fix x
1.17 +    assume "x \<in> set_pmf p"
1.18 +    hence "set_pmf p \<inter> (S x) \<noteq> {}" using in_S by auto
1.19 +    hence "measure (measure_pmf p) (S x) \<noteq> 0"
1.20 +      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff)
1.21 +    with same have "measure (measure_pmf q) (S x) \<noteq> 0" by simp
1.22 +    hence "set_pmf q \<inter> S x \<noteq> {}"
1.23 +      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
1.24 +  note [simp] = this
1.25 +
1.26    fix z
1.27 -  have pmf_le: "pmf p z \<le> measure p (S z)"
1.28 -  proof cases
1.29 -    assume "z \<in> p" from in_S[OF this] show ?thesis
1.30 -      by (auto intro!: measure_pmf.finite_measure_mono simp: pmf.rep_eq)
1.31 -  qed (simp add: set_pmf_iff measure_nonneg)
1.32 +  have pmf_q_z: "z \<notin> S z \<Longrightarrow> pmf q z = 0"
1.33 +    by(erule contrapos_np)(simp add: pmf_eq_0_set_pmf in_S)
1.34
1.35 -  have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z) =
1.36 -    (\<integral>\<^sup>+ x. ereal (pmf p z / measure p (S z)) * indicator (S z) x \<partial>p)"
1.37 -    by (subst ereal_pmf_bind)
1.38 -       (auto intro!: nn_integral_cong_AE dest!: S_eq split: split_indicator
1.39 -             simp: AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf in_S)
1.40 -  also have "\<dots> = pmf p z"
1.41 -    using pmf_le pmf_nonneg[of p z]
1.42 -    by (subst nn_integral_cmult) (simp_all add: measure_nonneg measure_pmf.emeasure_eq_measure)
1.43 -  finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf p (S x))) z = pmf p z"
1.44 -    by simp
1.45 +  have "ereal (pmf ?lhs z) = \<integral>\<^sup>+ x. ereal (pmf (cond_pmf q (S x)) z) \<partial>measure_pmf p"