generalise lemma
authorAndreas Lochbihler
Wed Feb 11 18:38:34 2015 +0100 (2015-02-11)
changeset 59526af02440afb4a
parent 59525 dfe6449aecd8
child 59527 edaabc1ab1ed
generalise lemma
src/HOL/Probability/Probability_Mass_Function.thy
     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"
    1.46 +    by(simp add: ereal_pmf_bind)
    1.47 +  also have "\<dots> = \<integral>\<^sup>+ x. ereal (pmf q z / measure p (S z)) * indicator (S z) x \<partial>measure_pmf p"
    1.48 +    by(rule nn_integral_cong_AE)(auto simp add: AE_measure_pmf_iff pmf_cond same pmf_q_z in_S dest!: S_eq split: split_indicator)
    1.49 +  also have "\<dots> = pmf q z" using pmf_nonneg[of q z]
    1.50 +    by (subst nn_integral_cmult)(auto simp add: measure_nonneg measure_pmf.emeasure_eq_measure same measure_pmf.prob_eq_0 AE_measure_pmf_iff pmf_eq_0_set_pmf in_S)
    1.51 +  finally show "pmf ?lhs z = pmf q z" by simp
    1.52  qed
    1.53  
    1.54  inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"