src/HOL/Probability/Probability_Mass_Function.thy
changeset 59670 dee043d19729
parent 59667 651ea265d568
child 59681 f24ab09e4c37
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 16:12:35 2015 +0000
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 17:50:10 2015 +0100
     1.3 @@ -793,6 +793,9 @@
     1.4  
     1.5  subsection \<open> Conditional Probabilities \<close>
     1.6  
     1.7 +lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \<longleftrightarrow> set_pmf p \<inter> s = {}"
     1.8 +  by (subst measure_pmf.prob_eq_0) (auto simp: AE_measure_pmf_iff)
     1.9 +
    1.10  context
    1.11    fixes p :: "'a pmf" and s :: "'a set"
    1.12    assumes not_empty: "set_pmf p \<inter> s \<noteq> {}"
    1.13 @@ -854,32 +857,22 @@
    1.14  qed
    1.15  
    1.16  lemma bind_cond_pmf_cancel:
    1.17 -  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.18 -  assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y"
    1.19 -  and same: "\<And>x. measure (measure_pmf p) (S x) = measure (measure_pmf q) (S x)"
    1.20 -  shows "bind_pmf p (\<lambda>x. cond_pmf q (S x)) = q" (is "?lhs = _")
    1.21 +  assumes [simp]: "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}"
    1.22 +  assumes [simp]: "\<And>y. y \<in> set_pmf q \<Longrightarrow> set_pmf p \<inter> {x. R x y} \<noteq> {}"
    1.23 +  assumes [simp]: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow> measure q {y. R x y} = measure p {x. R x y}"
    1.24 +  shows "bind_pmf p (\<lambda>x. cond_pmf q {y. R x y}) = q"
    1.25  proof (rule pmf_eqI)
    1.26 -  { fix x
    1.27 -    assume "x \<in> set_pmf p"
    1.28 -    hence "set_pmf p \<inter> (S x) \<noteq> {}" using in_S by auto
    1.29 -    hence "measure (measure_pmf p) (S x) \<noteq> 0"
    1.30 -      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff)
    1.31 -    with same have "measure (measure_pmf q) (S x) \<noteq> 0" by simp
    1.32 -    hence "set_pmf q \<inter> S x \<noteq> {}"
    1.33 -      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
    1.34 -  note [simp] = this
    1.35 -
    1.36 -  fix z
    1.37 -  have pmf_q_z: "z \<notin> S z \<Longrightarrow> pmf q z = 0"
    1.38 -    by(erule contrapos_np)(simp add: pmf_eq_0_set_pmf in_S)
    1.39 -
    1.40 -  have "ereal (pmf ?lhs z) = \<integral>\<^sup>+ x. ereal (pmf (cond_pmf q (S x)) z) \<partial>measure_pmf p"
    1.41 -    by(simp add: ereal_pmf_bind)
    1.42 -  also have "\<dots> = \<integral>\<^sup>+ x. ereal (pmf q z / measure p (S z)) * indicator (S z) x \<partial>measure_pmf p"
    1.43 -    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.44 -  also have "\<dots> = pmf q z" using pmf_nonneg[of q z]
    1.45 -    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.46 -  finally show "pmf ?lhs z = pmf q z" by simp
    1.47 +  fix i
    1.48 +  have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i) =
    1.49 +    (\<integral>\<^sup>+x. ereal (pmf q i / measure p {x. R x i}) * ereal (indicator {x. R x i} x) \<partial>p)"
    1.50 +    by (auto simp add: ereal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf intro!: nn_integral_cong_AE)
    1.51 +  also have "\<dots> = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}"
    1.52 +    by (simp add: pmf_nonneg measure_nonneg zero_ereal_def[symmetric] ereal_indicator
    1.53 +                  nn_integral_cmult measure_pmf.emeasure_eq_measure)
    1.54 +  also have "\<dots> = pmf q i"
    1.55 +    by (cases "pmf q i = 0") (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero)
    1.56 +  finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i = pmf q i"
    1.57 +    by simp
    1.58  qed
    1.59  
    1.60  subsection \<open> Relator \<close>
    1.61 @@ -928,8 +921,8 @@
    1.62      from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
    1.63        and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
    1.64  
    1.65 -    def pr \<equiv> "bind_pmf pq (\<lambda>(x, y). bind_pmf (cond_pmf qr {(y', z). y' = y}) (\<lambda>(y', z). return_pmf (x, z)))"
    1.66 -    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
    1.67 +    def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))"
    1.68 +    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
    1.69        by (force simp: q')
    1.70  
    1.71      have "rel_pmf (R OO S) p r"
    1.72 @@ -940,11 +933,11 @@
    1.73        with pq qr show "(R OO S) x z"
    1.74          by blast
    1.75      next
    1.76 -      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {(y', z). y' = y}))"
    1.77 -        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf)
    1.78 +      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
    1.79 +        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf map_pmf_comp)
    1.80        then show "map_pmf snd pr = r"
    1.81 -        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto
    1.82 -    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p) }
    1.83 +        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
    1.84 +    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p map_pmf_comp) }
    1.85    then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
    1.86      by(auto simp add: le_fun_def)
    1.87  qed (fact natLeq_card_order natLeq_cinfinite)+
    1.88 @@ -1138,10 +1131,10 @@
    1.89    and refl: "reflp R" and trans: "transp R"
    1.90    shows "rel_pmf (inf R R\<inverse>\<inverse>) p q"
    1.91  proof
    1.92 -  let ?E = "\<lambda>x. {y. R x y \<and> R y x}"
    1.93 -  let ?\<mu>E = "\<lambda>x. measure q (?E x)"
    1.94 +  let ?R = "\<lambda>x y. R x y \<and> R y x"
    1.95 +  let ?\<mu>R = "\<lambda>y. measure q {x. ?R x y}"
    1.96    { fix x
    1.97 -    have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
    1.98 +    have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
    1.99        by(auto intro!: arg_cong[where f="measure p"])
   1.100      also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
   1.101        by (rule measure_pmf.finite_measure_Diff) auto
   1.102 @@ -1152,30 +1145,30 @@
   1.103      also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} =
   1.104        measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
   1.105        by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
   1.106 -    also have "\<dots> = ?\<mu>E x"
   1.107 +    also have "\<dots> = ?\<mu>R x"
   1.108        by(auto intro!: arg_cong[where f="measure q"])
   1.109      also note calculation }
   1.110    note eq = this
   1.111  
   1.112 -  def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q (?E x)) (\<lambda>y. return_pmf (x, y)))"
   1.113 +  def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q {y. ?R y x}) (\<lambda>y. return_pmf (x, y)))"
   1.114  
   1.115    show "map_pmf fst pq = p"
   1.116      by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf')
   1.117  
   1.118 +  { fix y assume "y \<in> set_pmf p" then have "set_pmf q \<inter> {x. ?R x y} \<noteq> {}"
   1.119 +      unfolding measure_pmf_zero_iff[symmetric] eq[symmetric] by (auto simp: measure_pmf_zero_iff intro: reflpD[OF refl]) }
   1.120 +  note set_p = this
   1.121 +  moreover
   1.122 +  { fix x assume "x \<in> set_pmf q" then have "set_pmf p \<inter> {y. R x y \<and> R y x} \<noteq> {}"
   1.123 +      unfolding measure_pmf_zero_iff[symmetric] eq by (auto simp: measure_pmf_zero_iff intro: reflpD[OF refl]) }
   1.124 +  ultimately
   1.125    show "map_pmf snd pq = q"
   1.126      unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv
   1.127 -    by(subst bind_cond_pmf_cancel)(auto simp add: reflpD[OF \<open>reflp R\<close>] eq  intro: transpD[OF \<open>transp R\<close>])
   1.128 +    by (subst bind_cond_pmf_cancel)
   1.129 +       (auto simp add: eq AE_measure_pmf_iff dest: transpD[OF trans]
   1.130 +             intro!: measure_pmf.finite_measure_eq_AE)
   1.131  
   1.132 -  fix x y
   1.133 -  assume "(x, y) \<in> set_pmf pq"
   1.134 -  moreover
   1.135 -  { assume "x \<in> set_pmf p"
   1.136 -    hence "measure (measure_pmf p) (?E x) \<noteq> 0"
   1.137 -      by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
   1.138 -    hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
   1.139 -    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
   1.140 -      by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
   1.141 -  ultimately show "inf R R\<inverse>\<inverse> x y"
   1.142 +  fix x y assume "(x, y) \<in> set_pmf pq" with set_p show "inf R R\<inverse>\<inverse> x y"
   1.143      by (auto simp add: pq_def)
   1.144  qed
   1.145