src/HOL/Probability/Probability_Mass_Function.thy
changeset 59665 37adca7fd48f
parent 59664 224741ede5ae
child 59667 651ea265d568
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 10:53:48 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 11:56:32 2015 +0100
     1.3 @@ -384,7 +384,7 @@
     1.4  lemma bind_pmf_const[simp]: "bind_pmf M (\<lambda>x. c) = c"
     1.5    by transfer (simp add: bind_const' prob_space_imp_subprob_space)
     1.6  
     1.7 -lemma set_bind_pmf: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
     1.8 +lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
     1.9    unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind  
    1.10    by (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff set_pmf_eq not_le less_le pmf_nonneg)
    1.11  
    1.12 @@ -424,7 +424,7 @@
    1.13       (auto intro!: prob_space_imp_subprob_space bind_return[where N="count_space UNIV"]
    1.14             simp: space_subprob_algebra)
    1.15  
    1.16 -lemma set_return_pmf: "set_pmf (return_pmf x) = {x}"
    1.17 +lemma set_return_pmf[simp]: "set_pmf (return_pmf x) = {x}"
    1.18    by transfer (auto simp add: measure_return split: split_indicator)
    1.19  
    1.20  lemma bind_return_pmf': "bind_pmf N return_pmf = N"
    1.21 @@ -477,9 +477,9 @@
    1.22    unfolding map_pmf_def by (rule bind_pmf_cong) auto
    1.23  
    1.24  lemma pmf_set_map: "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
    1.25 -  by (auto simp add: comp_def fun_eq_iff map_pmf_def set_bind_pmf set_return_pmf)
    1.26 +  by (auto simp add: comp_def fun_eq_iff map_pmf_def)
    1.27  
    1.28 -lemma set_map_pmf: "set_pmf (map_pmf f M) = f`set_pmf M"
    1.29 +lemma set_map_pmf[simp]: "set_pmf (map_pmf f M) = f`set_pmf M"
    1.30    using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff)
    1.31  
    1.32  lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
    1.33 @@ -529,6 +529,18 @@
    1.34  lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \<longleftrightarrow> x = y"
    1.35    by (metis insertI1 set_return_pmf singletonD)
    1.36  
    1.37 +lemma map_pmf_eq_return_pmf_iff:
    1.38 +  "map_pmf f p = return_pmf x \<longleftrightarrow> (\<forall>y \<in> set_pmf p. f y = x)"
    1.39 +proof
    1.40 +  assume "map_pmf f p = return_pmf x"
    1.41 +  then have "set_pmf (map_pmf f p) = set_pmf (return_pmf x)" by simp
    1.42 +  then show "\<forall>y \<in> set_pmf p. f y = x" by auto
    1.43 +next
    1.44 +  assume "\<forall>y \<in> set_pmf p. f y = x"
    1.45 +  then show "map_pmf f p = return_pmf x"
    1.46 +    unfolding map_pmf_const[symmetric, of _ p] by (intro map_pmf_cong) auto
    1.47 +qed
    1.48 +
    1.49  definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
    1.50  
    1.51  lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b"
    1.52 @@ -539,7 +551,7 @@
    1.53    apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg)
    1.54    done
    1.55  
    1.56 -lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
    1.57 +lemma set_pair_pmf[simp]: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
    1.58    unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
    1.59  
    1.60  lemma measure_pmf_in_subprob_space[measurable (raw)]:
    1.61 @@ -550,7 +562,7 @@
    1.62  proof -
    1.63    have "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+x. max 0 (f x) * indicator (A \<times> B) x \<partial>pair_pmf A B)"
    1.64      by (subst nn_integral_max_0[symmetric])
    1.65 -       (auto simp: AE_measure_pmf_iff set_pair_pmf intro!: nn_integral_cong_AE)
    1.66 +       (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE)
    1.67    also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) * indicator (A \<times> B) (a, b) \<partial>B \<partial>A)"
    1.68      by (simp add: pair_pmf_def)
    1.69    also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) \<partial>B \<partial>A)"
    1.70 @@ -581,7 +593,7 @@
    1.71    then show "emeasure ?L X = emeasure ?R X"
    1.72      apply (simp add: emeasure_bind[OF _ M' X])
    1.73      apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
    1.74 -      nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
    1.75 +                     nn_integral_measure_pmf_finite emeasure_nonneg pmf_return one_ereal_def[symmetric])
    1.76      apply (subst emeasure_bind[OF _ _ X])
    1.77      apply measurable
    1.78      apply (subst emeasure_bind[OF _ _ X])
    1.79 @@ -814,7 +826,7 @@
    1.80  lemma pmf_cond: "pmf cond_pmf x = (if x \<in> s then pmf p x / measure p s else 0)"
    1.81    by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq)
    1.82  
    1.83 -lemma set_cond_pmf: "set_pmf cond_pmf = set_pmf p \<inter> s"
    1.84 +lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \<inter> s"
    1.85    by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm)
    1.86  
    1.87  end
    1.88 @@ -824,7 +836,7 @@
    1.89    shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))"
    1.90  proof -
    1.91    have *: "set_pmf (map_pmf f p) \<inter> s \<noteq> {}"
    1.92 -    using assms by (simp add: set_map_pmf) auto
    1.93 +    using assms by auto
    1.94    { fix x
    1.95      have "ereal (pmf (map_pmf f (cond_pmf p (f -` s))) x) =
    1.96        emeasure p (f -` s \<inter> f -` {x}) / emeasure p (f -` s)"
    1.97 @@ -919,13 +931,13 @@
    1.98  
    1.99      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.100      have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
   1.101 -      by (force simp: q' set_map_pmf)
   1.102 +      by (force simp: q')
   1.103  
   1.104      have "rel_pmf (R OO S) p r"
   1.105      proof (rule rel_pmf.intros)
   1.106        fix x z assume "(x, z) \<in> pr"
   1.107        then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
   1.108 -        by (auto simp: q pr_welldefined pr_def set_bind_pmf split_beta set_return_pmf set_cond_pmf set_map_pmf)
   1.109 +        by (auto simp: q pr_welldefined pr_def split_beta)
   1.110        with pq qr show "(R OO S) x z"
   1.111          by blast
   1.112      next
   1.113 @@ -938,6 +950,15 @@
   1.114      by(auto simp add: le_fun_def)
   1.115  qed (fact natLeq_card_order natLeq_cinfinite)+
   1.116  
   1.117 +lemma rel_pmf_conj[simp]:
   1.118 +  "rel_pmf (\<lambda>x y. P \<and> Q x y) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
   1.119 +  "rel_pmf (\<lambda>x y. Q x y \<and> P) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
   1.120 +  using set_pmf_not_empty by (fastforce simp: pmf.in_rel subset_eq)+
   1.121 +
   1.122 +lemma rel_pmf_top[simp]: "rel_pmf top = top"
   1.123 +  by (auto simp: pmf.in_rel[abs_def] fun_eq_iff map_fst_pair_pmf map_snd_pair_pmf
   1.124 +           intro: exI[of _ "pair_pmf x y" for x y])
   1.125 +
   1.126  lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \<longleftrightarrow> (\<forall>a\<in>M. R x a)"
   1.127  proof safe
   1.128    fix a assume "a \<in> M" "rel_pmf R (return_pmf x) M"
   1.129 @@ -945,13 +966,13 @@
   1.130      and eq: "return_pmf x = map_pmf fst pq" "M = map_pmf snd pq"
   1.131      by (force elim: rel_pmf.cases)
   1.132    moreover have "set_pmf (return_pmf x) = {x}"
   1.133 -    by (simp add: set_return_pmf)
   1.134 +    by simp
   1.135    with `a \<in> M` have "(x, a) \<in> pq"
   1.136 -    by (force simp: eq set_map_pmf)
   1.137 +    by (force simp: eq)
   1.138    with * show "R x a"
   1.139      by auto
   1.140  qed (auto intro!: rel_pmf.intros[where pq="pair_pmf (return_pmf x) M"]
   1.141 -          simp: map_fst_pair_pmf map_snd_pair_pmf set_pair_pmf set_return_pmf)
   1.142 +          simp: map_fst_pair_pmf map_snd_pair_pmf)
   1.143  
   1.144  lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \<longleftrightarrow> (\<forall>a\<in>M. R a x)"
   1.145    by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1)
   1.146 @@ -982,7 +1003,7 @@
   1.147  
   1.148      fix a b assume "(a, b) \<in> set_pmf (map_pmf ?f pq)"
   1.149      then obtain c d where "((a, c), (b, d)) \<in> set_pmf pq"
   1.150 -      by (auto simp: set_map_pmf)
   1.151 +      by auto
   1.152      from pq[OF this] show "R a b" ..
   1.153    qed
   1.154    show "rel_pmf S A' B'"
   1.155 @@ -998,7 +1019,7 @@
   1.156  
   1.157      fix c d assume "(c, d) \<in> set_pmf (map_pmf ?f pq)"
   1.158      then obtain a b where "((a, c), (b, d)) \<in> set_pmf pq"
   1.159 -      by (auto simp: set_map_pmf)
   1.160 +      by auto
   1.161      from pq[OF this] show "S c d" ..
   1.162    qed
   1.163  next
   1.164 @@ -1017,14 +1038,15 @@
   1.165  
   1.166    show "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')"
   1.167      by (rule rel_pmf.intros[where pq="?pq"])
   1.168 -       (auto simp: map_snd_pair_pmf map_fst_pair_pmf set_pair_pmf set_map_pmf map_pmf_comp Rpq Spq
   1.169 +       (auto simp: map_snd_pair_pmf map_fst_pair_pmf map_pmf_comp Rpq Spq
   1.170                     map_pair)
   1.171  qed
   1.172  
   1.173  lemma rel_pmf_reflI: 
   1.174    assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> P x x"
   1.175    shows "rel_pmf P p p"
   1.176 -by(rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])(auto simp add: pmf.map_comp o_def set_map_pmf assms)
   1.177 +  by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
   1.178 +     (auto simp add: pmf.map_comp o_def assms)
   1.179  
   1.180  context
   1.181  begin
   1.182 @@ -1045,8 +1067,8 @@
   1.183  lemma ereal_pmf_join: "ereal (pmf (join_pmf N) i) = (\<integral>\<^sup>+M. pmf M i \<partial>measure_pmf N)"
   1.184    unfolding join_pmf_def ereal_pmf_bind ..
   1.185  
   1.186 -lemma set_pmf_join_pmf: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
   1.187 -  by (simp add: join_pmf_def set_bind_pmf)
   1.188 +lemma set_pmf_join_pmf[simp]: "set_pmf (join_pmf f) = (\<Union>p\<in>set_pmf f. set_pmf p)"
   1.189 +  by (simp add: join_pmf_def)
   1.190  
   1.191  lemma join_return_pmf: "join_pmf (return_pmf M) = M"
   1.192    by (simp add: integral_return pmf_eq_iff pmf_join return_pmf.rep_eq)
   1.193 @@ -1074,7 +1096,7 @@
   1.194      by(metis rel_pmf.simps)
   1.195  
   1.196    let ?r = "bind_pmf pq (\<lambda>(x, y). PQ x y)"
   1.197 -  have "\<And>a b. (a, b) \<in> set_pmf ?r \<Longrightarrow> P a b" by(auto simp add: set_bind_pmf intro: PQ)
   1.198 +  have "\<And>a b. (a, b) \<in> set_pmf ?r \<Longrightarrow> P a b" by (auto intro: PQ)
   1.199    moreover have "map_pmf fst ?r = join_pmf p" "map_pmf snd ?r = join_pmf q"
   1.200      by (simp_all add: p q x y join_pmf_def map_bind_pmf bind_map_pmf split_def cong: bind_pmf_cong)
   1.201    ultimately show ?thesis ..
   1.202 @@ -1150,12 +1172,12 @@
   1.203    moreover
   1.204    { assume "x \<in> set_pmf p"
   1.205      hence "measure (measure_pmf p) (?E x) \<noteq> 0"
   1.206 -      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
   1.207 +      by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
   1.208      hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
   1.209      hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}" 
   1.210 -      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
   1.211 +      by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
   1.212    ultimately show "inf R R\<inverse>\<inverse> x y"
   1.213 -    by(auto simp add: pq_def set_bind_pmf set_return_pmf set_cond_pmf)
   1.214 +    by (auto simp add: pq_def)
   1.215  qed
   1.216  
   1.217  lemma rel_pmf_antisym:
   1.218 @@ -1167,7 +1189,7 @@
   1.219  proof -
   1.220    from 1 2 refl trans have "rel_pmf (inf R R\<inverse>\<inverse>) p q" by(rule rel_pmf_inf)
   1.221    also have "inf R R\<inverse>\<inverse> = op ="
   1.222 -    using refl antisym by(auto intro!: ext simp add: reflpD dest: antisymD)
   1.223 +    using refl antisym by (auto intro!: ext simp add: reflpD dest: antisymD)
   1.224    finally show ?thesis unfolding pmf.rel_eq .
   1.225  qed
   1.226