src/HOL/Probability/Probability_Mass_Function.thy
 changeset 59731 7fccaeec22f0 parent 59730 b7c394c7a619 parent 59681 f24ab09e4c37 child 60068 ef2123db900c
```     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Mar 16 15:30:00 2015 +0000
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 17 12:23:56 2015 +0000
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.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 @@ -891,6 +884,136 @@
1.62       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
1.63    \<Longrightarrow> rel_pmf R p q"
1.64
1.65 +lemma rel_pmfI:
1.66 +  assumes R: "rel_set R (set_pmf p) (set_pmf q)"
1.67 +  assumes eq: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow>
1.68 +    measure p {x. R x y} = measure q {y. R x y}"
1.69 +  shows "rel_pmf R p q"
1.70 +proof
1.71 +  let ?pq = "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q {y. R x y}) (\<lambda>y. return_pmf (x, y)))"
1.72 +  have "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}"
1.73 +    using R by (auto simp: rel_set_def)
1.74 +  then show "\<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y"
1.75 +    by auto
1.76 +  show "map_pmf fst ?pq = p"
1.77 +    by (simp add: map_bind_pmf map_return_pmf bind_return_pmf')
1.78 +
1.79 +  show "map_pmf snd ?pq = q"
1.80 +    using R eq
1.81 +    apply (simp add: bind_cond_pmf_cancel map_bind_pmf map_return_pmf bind_return_pmf')
1.82 +    apply (rule bind_cond_pmf_cancel)
1.83 +    apply (auto simp: rel_set_def)
1.84 +    done
1.85 +qed
1.86 +
1.87 +lemma rel_pmf_imp_rel_set: "rel_pmf R p q \<Longrightarrow> rel_set R (set_pmf p) (set_pmf q)"
1.88 +  by (force simp add: rel_pmf.simps rel_set_def)
1.89 +
1.90 +lemma rel_pmfD_measure:
1.91 +  assumes rel_R: "rel_pmf R p q" and R: "\<And>a b. R a b \<Longrightarrow> R a y \<longleftrightarrow> R x b"
1.92 +  assumes "x \<in> set_pmf p" "y \<in> set_pmf q"
1.93 +  shows "measure p {x. R x y} = measure q {y. R x y}"
1.94 +proof -
1.95 +  from rel_R obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
1.96 +    and eq: "p = map_pmf fst pq" "q = map_pmf snd pq"
1.97 +    by (auto elim: rel_pmf.cases)
1.98 +  have "measure p {x. R x y} = measure pq {x. R (fst x) y}"
1.99 +    by (simp add: eq map_pmf_rep_eq measure_distr)
1.100 +  also have "\<dots> = measure pq {y. R x (snd y)}"
1.101 +    by (intro measure_pmf.finite_measure_eq_AE)
1.102 +       (auto simp: AE_measure_pmf_iff R dest!: pq)
1.103 +  also have "\<dots> = measure q {y. R x y}"
1.104 +    by (simp add: eq map_pmf_rep_eq measure_distr)
1.105 +  finally show "measure p {x. R x y} = measure q {y. R x y}" .
1.106 +qed
1.107 +
1.108 +lemma rel_pmf_iff_measure:
1.109 +  assumes "symp R" "transp R"
1.110 +  shows "rel_pmf R p q \<longleftrightarrow>
1.111 +    rel_set R (set_pmf p) (set_pmf q) \<and>
1.112 +    (\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y})"
1.113 +  by (safe intro!: rel_pmf_imp_rel_set rel_pmfI)
1.114 +     (auto intro!: rel_pmfD_measure dest: sympD[OF \<open>symp R\<close>] transpD[OF \<open>transp R\<close>])
1.115 +
1.116 +lemma quotient_rel_set_disjoint:
1.117 +  "equivp R \<Longrightarrow> C \<in> UNIV // {(x, y). R x y} \<Longrightarrow> rel_set R A B \<Longrightarrow> A \<inter> C = {} \<longleftrightarrow> B \<inter> C = {}"
1.118 +  using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C]
1.119 +  by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE)
1.120 +     (blast dest: equivp_symp)+
1.121 +
1.122 +lemma quotientD: "equiv X R \<Longrightarrow> A \<in> X // R \<Longrightarrow> x \<in> A \<Longrightarrow> A = R `` {x}"
1.123 +  by (metis Image_singleton_iff equiv_class_eq_iff quotientE)
1.124 +
1.125 +lemma rel_pmf_iff_equivp:
1.126 +  assumes "equivp R"
1.127 +  shows "rel_pmf R p q \<longleftrightarrow> (\<forall>C\<in>UNIV // {(x, y). R x y}. measure p C = measure q C)"
1.128 +    (is "_ \<longleftrightarrow>   (\<forall>C\<in>_//?R. _)")
1.129 +proof (subst rel_pmf_iff_measure, safe)
1.130 +  show "symp R" "transp R"
1.131 +    using assms by (auto simp: equivp_reflp_symp_transp)
1.132 +next
1.133 +  fix C assume C: "C \<in> UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)"
1.134 +  assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}"
1.135 +
1.136 +  show "measure p C = measure q C"
1.137 +  proof cases
1.138 +    assume "p \<inter> C = {}"
1.139 +    moreover then have "q \<inter> C = {}"
1.140 +      using quotient_rel_set_disjoint[OF assms C R] by simp
1.141 +    ultimately show ?thesis
1.142 +      unfolding measure_pmf_zero_iff[symmetric] by simp
1.143 +  next
1.144 +    assume "p \<inter> C \<noteq> {}"
1.145 +    moreover then have "q \<inter> C \<noteq> {}"
1.146 +      using quotient_rel_set_disjoint[OF assms C R] by simp
1.147 +    ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C"
1.148 +      by auto
1.149 +    then have "R x y"
1.150 +      using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms
1.151 +      by (simp add: equivp_equiv)
1.152 +    with in_set eq have "measure p {x. R x y} = measure q {y. R x y}"
1.153 +      by auto
1.154 +    moreover have "{y. R x y} = C"
1.155 +      using assms `x \<in> C` C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv)
1.156 +    moreover have "{x. R x y} = C"
1.157 +      using assms `y \<in> C` C quotientD[of UNIV "?R" C y] sympD[of R]
1.158 +      by (auto simp add: equivp_equiv elim: equivpE)
1.159 +    ultimately show ?thesis
1.160 +      by auto
1.161 +  qed
1.162 +next
1.163 +  assume eq: "\<forall>C\<in>UNIV // ?R. measure p C = measure q C"
1.164 +  show "rel_set R (set_pmf p) (set_pmf q)"
1.165 +    unfolding rel_set_def
1.166 +  proof safe
1.167 +    fix x assume x: "x \<in> set_pmf p"
1.168 +    have "{y. R x y} \<in> UNIV // ?R"
1.169 +      by (auto simp: quotient_def)
1.170 +    with eq have *: "measure q {y. R x y} = measure p {y. R x y}"
1.171 +      by auto
1.172 +    have "measure q {y. R x y} \<noteq> 0"
1.173 +      using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
1.174 +    then show "\<exists>y\<in>set_pmf q. R x y"
1.175 +      unfolding measure_pmf_zero_iff by auto
1.176 +  next
1.177 +    fix y assume y: "y \<in> set_pmf q"
1.178 +    have "{x. R x y} \<in> UNIV // ?R"
1.179 +      using assms by (auto simp: quotient_def dest: equivp_symp)
1.180 +    with eq have *: "measure p {x. R x y} = measure q {x. R x y}"
1.181 +      by auto
1.182 +    have "measure p {x. R x y} \<noteq> 0"
1.183 +      using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
1.184 +    then show "\<exists>x\<in>set_pmf p. R x y"
1.185 +      unfolding measure_pmf_zero_iff by auto
1.186 +  qed
1.187 +
1.188 +  fix x y assume "x \<in> set_pmf p" "y \<in> set_pmf q" "R x y"
1.189 +  have "{y. R x y} \<in> UNIV // ?R" "{x. R x y} = {y. R x y}"
1.190 +    using assms `R x y` by (auto simp: quotient_def dest: equivp_symp equivp_transp)
1.191 +  with eq show "measure p {x. R x y} = measure q {y. R x y}"
1.192 +    by auto
1.193 +qed
1.194 +
1.195  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
1.196  proof -
1.197    show "map_pmf id = id" by (rule map_pmf_id)
1.198 @@ -919,7 +1042,7 @@
1.199        and x: "x \<in> set_pmf p"
1.200      thus "f x = g x" by simp }
1.201
1.202 -  fix R :: "'a => 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
1.203 +  fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
1.204    { fix p q r
1.205      assume pq: "rel_pmf R p q"
1.206        and qr:"rel_pmf S q r"
1.207 @@ -928,8 +1051,8 @@
1.208      from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
1.209        and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
1.210
1.211 -    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.212 -    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
1.213 +    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.214 +    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
1.215        by (force simp: q')
1.216
1.217      have "rel_pmf (R OO S) p r"
1.218 @@ -940,11 +1063,11 @@
1.219        with pq qr show "(R OO S) x z"
1.220          by blast
1.221      next
1.222 -      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {(y', z). y' = y}))"
1.223 -        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf)
1.224 +      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
1.225 +        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.226        then show "map_pmf snd pr = r"
1.227 -        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto
1.228 -    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p) }
1.229 +        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
1.230 +    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p map_pmf_comp) }
1.231    then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
1.233  qed (fact natLeq_card_order natLeq_cinfinite)+
1.234 @@ -1137,46 +1260,31 @@
1.235    assumes 2: "rel_pmf R q p"
1.236    and refl: "reflp R" and trans: "transp R"
1.237    shows "rel_pmf (inf R R\<inverse>\<inverse>) p q"
1.238 -proof
1.239 -  let ?E = "\<lambda>x. {y. R x y \<and> R y x}"
1.240 -  let ?\<mu>E = "\<lambda>x. measure q (?E x)"
1.241 -  { fix x
1.242 -    have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
1.243 -      by(auto intro!: arg_cong[where f="measure p"])
1.244 -    also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
1.245 -      by (rule measure_pmf.finite_measure_Diff) auto
1.246 -    also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
1.247 -      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
1.248 -    also have "measure p {y. R x y} = measure q {y. R x y}"
1.249 -      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
1.250 -    also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} =
1.251 -      measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
1.252 -      by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
1.253 -    also have "\<dots> = ?\<mu>E x"
1.254 -      by(auto intro!: arg_cong[where f="measure q"])
1.255 -    also note calculation }
1.256 -  note eq = this
1.257 +proof (subst rel_pmf_iff_equivp, safe)
1.258 +  show "equivp (inf R R\<inverse>\<inverse>)"
1.259 +    using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD)
1.260 +
1.261 +  fix C assume "C \<in> UNIV // {(x, y). inf R R\<inverse>\<inverse> x y}"
1.262 +  then obtain x where C: "C = {y. R x y \<and> R y x}"
1.263 +    by (auto elim: quotientE)
1.264
1.265 -  def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q (?E x)) (\<lambda>y. return_pmf (x, y)))"
1.266 -
1.267 -  show "map_pmf fst pq = p"
1.268 -    by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf')
1.269 -
1.270 -  show "map_pmf snd pq = q"
1.271 -    unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv
1.272 -    by(subst bind_cond_pmf_cancel)(auto simp add: reflpD[OF \<open>reflp R\<close>] eq  intro: transpD[OF \<open>transp R\<close>])
1.273 -
1.274 -  fix x y
1.275 -  assume "(x, y) \<in> set_pmf pq"
1.276 -  moreover
1.277 -  { assume "x \<in> set_pmf p"
1.278 -    hence "measure (measure_pmf p) (?E x) \<noteq> 0"
1.279 -      by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
1.280 -    hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
1.281 -    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
1.282 -      by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
1.283 -  ultimately show "inf R R\<inverse>\<inverse> x y"
1.284 -    by (auto simp add: pq_def)
1.285 +  let ?R = "\<lambda>x y. R x y \<and> R y x"
1.286 +  let ?\<mu>R = "\<lambda>y. measure q {x. ?R x y}"
1.287 +  have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
1.288 +    by(auto intro!: arg_cong[where f="measure p"])
1.289 +  also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
1.290 +    by (rule measure_pmf.finite_measure_Diff) auto
1.291 +  also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
1.292 +    using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
1.293 +  also have "measure p {y. R x y} = measure q {y. R x y}"
1.294 +    using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
1.295 +  also have "measure q {y. R x y} - measure q {y. R x y \<and> \<not> R y x} =
1.296 +    measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
1.297 +    by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
1.298 +  also have "\<dots> = ?\<mu>R x"
1.299 +    by(auto intro!: arg_cong[where f="measure q"])
1.300 +  finally show "measure p C = measure q C"
1.301 +    by (simp add: C conj_commute)
1.302  qed
1.303
1.304  lemma rel_pmf_antisym:
```