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.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 @@ -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.232      by(auto simp add: le_fun_def)
   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: