author hoelzl Fri Jan 09 10:49:35 2015 +0100 (2015-01-09) changeset 59327 8a779359df67 parent 59326 46491010b83a child 59328 b83d6c3c439a
rel_pmf OO: conversion to nat is not necessary
```     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 09 09:17:10 2015 +0100
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 09 10:49:35 2015 +0100
1.3 @@ -993,6 +993,11 @@
1.4       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
1.5    \<Longrightarrow> rel_pmf R p q"
1.6
1.7 +lemma nn_integral_count_space_eq:
1.8 +  "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>
1.9 +    (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
1.10 +  by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
1.11 +
1.12  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
1.13  proof -
1.14    show "map_pmf id = id" by (rule map_pmf_id)
1.15 @@ -1031,138 +1036,93 @@
1.16        and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
1.17
1.18      note pmf_nonneg[intro, simp]
1.19 -
1.20 -    def A \<equiv> "\<lambda>y. {x. (x, y) \<in> set_pmf pq}"
1.21 -    then have "\<And>y. A y \<subseteq> set_pmf p" by (auto simp add: p set_map_pmf intro: rev_image_eqI)
1.22 -    then have [simp]: "\<And>y. countable (A y)" by (rule countable_subset) simp
1.23 -    have A: "\<And>x y. (x, y) \<in> set_pmf pq \<longleftrightarrow> x \<in> A y"
1.24 -      by (simp add: A_def)
1.25 -
1.26 -    let ?P = "\<lambda>y. to_nat_on (A y)"
1.27 -    def pp \<equiv> "map_pmf (\<lambda>(x, y). (y, ?P y x)) pq"
1.28 -    let ?pp = "\<lambda>y x. pmf pp (y, x)"
1.29 -    { fix x y have "x \<in> A y \<Longrightarrow> ?pp y (?P y x) = pmf pq (x, y)"
1.30 -        unfolding pp_def
1.31 -        by (intro pmf_map_inj[of "\<lambda>(x, y). (y, ?P y x)" pq "(x, y)", simplified])
1.32 -           (auto simp: inj_on_def A) }
1.33 -    note pmf_pp = this
1.34 -    have pp_0: "\<And>y x. pmf q y = 0 \<Longrightarrow> ?pp y x = 0"
1.35 -    proof(erule contrapos_pp)
1.36 -      fix y x
1.37 -      assume "?pp y x \<noteq> 0"
1.38 -      hence "(y, x) \<in> set_pmf pp" by(simp add: set_pmf_iff)
1.39 -      hence "y \<in> set_pmf q" by(auto simp add: pp_def q set_map_pmf intro: rev_image_eqI)
1.40 -      thus "pmf q y \<noteq> 0" by(simp add: set_pmf_iff)
1.41 -    qed
1.42 +    let ?pq = "\<lambda>y x. pmf pq (x, y)"
1.43 +    let ?qr = "\<lambda>y z. pmf qr (y, z)"
1.44
1.45 -    def B \<equiv> "\<lambda>y. {z. (y, z) \<in> set_pmf qr}"
1.46 -    then have "\<And>y. B y \<subseteq> set_pmf r" by (auto simp add: r set_map_pmf intro: rev_image_eqI)
1.47 -    then have [simp]: "\<And>y. countable (B y)" by (rule countable_subset) simp
1.48 -    have B: "\<And>y z. (y, z) \<in> set_pmf qr \<longleftrightarrow> z \<in> B y"
1.49 -      by (simp add: B_def)
1.50 -
1.51 -    let ?R = "\<lambda>y. to_nat_on (B y)"
1.52 -    def rr \<equiv> "map_pmf (\<lambda>(y, z). (y, ?R y z)) qr"
1.53 -    let ?rr = "\<lambda>y z. pmf rr (y, z)"
1.54 -    { fix y z have "z \<in> B y \<Longrightarrow> ?rr y (?R y z) = pmf qr (y, z)"
1.55 -        unfolding rr_def
1.56 -        by (intro pmf_map_inj[of "\<lambda>(y, z). (y, ?R y z)" qr "(y, z)", simplified])
1.57 -           (auto simp: inj_on_def B) }
1.58 -    note pmf_rr = this
1.59 -    have rr_0: "\<And>y z. pmf q y = 0 \<Longrightarrow> ?rr y z = 0"
1.60 -    proof(erule contrapos_pp)
1.61 -      fix y z
1.62 -      assume "?rr y z \<noteq> 0"
1.63 -      hence "(y, z) \<in> set_pmf rr" by(simp add: set_pmf_iff)
1.64 -      hence "y \<in> set_pmf q" by(auto simp add: rr_def q' set_map_pmf intro: rev_image_eqI)
1.65 -      thus "pmf q y \<noteq> 0" by(simp add: set_pmf_iff)
1.66 -    qed
1.67 -
1.68 -    have nn_integral_pp2: "\<And>y. (\<integral>\<^sup>+ x. ?pp y x \<partial>count_space UNIV) = pmf q y"
1.69 -      by (simp add: nn_integral_pmf' inj_on_def pp_def q)
1.70 +    have nn_integral_pp2: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = pmf q y"
1.71 +      by (simp add: nn_integral_pmf' inj_on_def q)
1.72           (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure])
1.73 -    have nn_integral_rr1: "\<And>y. (\<integral>\<^sup>+ x. ?rr y x \<partial>count_space UNIV) = pmf q y"
1.74 -      by (simp add: nn_integral_pmf' inj_on_def rr_def q')
1.75 +    have nn_integral_rr1: "\<And>y. (\<integral>\<^sup>+ x. ?qr y x \<partial>count_space UNIV) = pmf q y"
1.76 +      by (simp add: nn_integral_pmf' inj_on_def q')
1.77           (auto simp add: ereal_pmf_map intro!: arg_cong2[where f=emeasure])
1.78 -    have eq: "\<And>y. (\<integral>\<^sup>+ x. ?pp y x \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?rr y z \<partial>count_space UNIV)"
1.79 +    have eq: "\<And>y. (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV)"
1.80        by(simp add: nn_integral_pp2 nn_integral_rr1)
1.81
1.82 -    def assign \<equiv> "\<lambda>y x z. ?pp y x * ?rr y z / pmf q y"
1.83 +    def assign \<equiv> "\<lambda>y x z. ?pq y x * ?qr y z / pmf q y"
1.84      have assign_nonneg [simp]: "\<And>y x z. 0 \<le> assign y x z" by(simp add: assign_def)
1.85 -    have assign_eq_0_outside: "\<And>y x z. \<lbrakk> ?pp y x = 0 \<or> ?rr y z = 0 \<rbrakk> \<Longrightarrow> assign y x z = 0"
1.86 +    have assign_eq_0_outside: "\<And>y x z. \<lbrakk> ?pq y x = 0 \<or> ?qr y z = 0 \<rbrakk> \<Longrightarrow> assign y x z = 0"
1.87        by(auto simp add: assign_def)
1.88 -    have nn_integral_assign1: "\<And>y z. (\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = ?rr y z"
1.89 +    have nn_integral_assign1: "\<And>y z. (\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) = ?qr y z"
1.90      proof -
1.91        fix y z
1.92        have "(\<integral>\<^sup>+ x. assign y x z \<partial>count_space UNIV) =
1.93 -            (\<integral>\<^sup>+ x. ?pp y x \<partial>count_space UNIV) * (?rr y z / pmf q y)"
1.94 +            (\<integral>\<^sup>+ x. ?pq y x \<partial>count_space UNIV) * (?qr y z / pmf q y)"
1.95          by(simp add: assign_def nn_integral_multc times_ereal.simps(1)[symmetric] divide_real_def mult.assoc del: times_ereal.simps(1))
1.96 -      also have "\<dots> = ?rr y z" by(simp add: rr_0 nn_integral_pp2)
1.97 +      also have "\<dots> = ?qr y z" by(auto simp add: image_iff q' pmf_eq_0_set_pmf set_map_pmf nn_integral_pp2)
1.98        finally show "?thesis y z" .
1.99      qed
1.100 -    have nn_integral_assign2: "\<And>y x. (\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = ?pp y x"
1.101 +    have nn_integral_assign2: "\<And>y x. (\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = ?pq y x"
1.102      proof -
1.103        fix x y
1.104 -      have "(\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?rr y z \<partial>count_space UNIV) * (?pp y x / pmf q y)"
1.105 -        by(simp add: assign_def divide_real_def mult.commute[where a="?pp y x"] mult.assoc nn_integral_multc times_ereal.simps(1)[symmetric] del: times_ereal.simps(1))
1.106 -      also have "\<dots> = ?pp y x" by(simp add: nn_integral_rr1 pp_0)
1.107 +      have "(\<integral>\<^sup>+ z. assign y x z \<partial>count_space UNIV) = (\<integral>\<^sup>+ z. ?qr y z \<partial>count_space UNIV) * (?pq y x / pmf q y)"
1.108 +        by(simp add: assign_def divide_real_def mult.commute[where a="?pq y x"] mult.assoc nn_integral_multc times_ereal.simps(1)[symmetric] del: times_ereal.simps(1))
1.109 +      also have "\<dots> = ?pq y x" by(auto simp add: image_iff pmf_eq_0_set_pmf set_map_pmf q nn_integral_rr1)
1.110        finally show "?thesis y x" .
1.111      qed
1.112
1.113 -    def a \<equiv> "embed_pmf (\<lambda>(y, x, z). assign y x z)"
1.114 +    def pqr \<equiv> "embed_pmf (\<lambda>(y, x, z). assign y x z)"
1.115      { fix y x z
1.116 -      have "assign y x z = pmf a (y, x, z)"
1.117 -        unfolding a_def
1.118 +      have "assign y x z = pmf pqr (y, x, z)"
1.119 +        unfolding pqr_def
1.120        proof (subst pmf_embed_pmf)
1.121          have "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) =
1.122 -          (\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>(count_space ((\<lambda>((y, x), z). (y, x, z)) ` (pp \<times> UNIV))))"
1.123 -          by (force simp add: nn_integral_count_space_indicator pmf_eq_0_set_pmf split: split_indicator
1.124 -                    intro!: nn_integral_cong assign_eq_0_outside)
1.125 -        also have "\<dots> = (\<integral>\<^sup>+ x. ereal ((\<lambda>((y, x), z). assign y x z) x) \<partial>(count_space (pp \<times> UNIV)))"
1.126 +          (\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>(count_space ((\<lambda>((x, y), z). (y, x, z)) ` (pq \<times> r))))"
1.127 +          by (force simp add: pmf_eq_0_set_pmf r set_map_pmf split: split_indicator
1.128 +                    intro!: nn_integral_count_space_eq assign_eq_0_outside)
1.129 +        also have "\<dots> = (\<integral>\<^sup>+ x. ereal ((\<lambda>((x, y), z). assign y x z) x) \<partial>(count_space (pq \<times> r)))"
1.130            by (subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
1.131               (auto simp: inj_on_def intro!: nn_integral_cong)
1.132 -        also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+z. ereal ((\<lambda>((y, x), z). assign y x z) (y, z)) \<partial>count_space UNIV \<partial>count_space pp)"
1.133 +        also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space r \<partial>count_space pq)"
1.134            by (subst sigma_finite_measure.nn_integral_fst)
1.135               (auto simp: pair_measure_countable sigma_finite_measure_count_space_countable)
1.136 -        also have "\<dots> = (\<integral>\<^sup>+ z. ?pp (fst z) (snd z) \<partial>count_space pp)"
1.137 +        also have "\<dots> = (\<integral>\<^sup>+ xy. \<integral>\<^sup>+z. ereal ((\<lambda>((x, y), z). assign y x z) (xy, z)) \<partial>count_space UNIV \<partial>count_space pq)"
1.138 +          by (intro nn_integral_cong nn_integral_count_space_eq)
1.139 +             (force simp: r set_map_pmf pmf_eq_0_set_pmf intro!: assign_eq_0_outside)+
1.140 +        also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space pq)"
1.141            by (subst nn_integral_assign2[symmetric]) (auto intro!: nn_integral_cong)
1.142          finally show "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) = 1"
1.143            by (simp add: nn_integral_pmf emeasure_pmf)
1.144        qed auto }
1.145      note a = this
1.146
1.147 -    def pr \<equiv> "map_pmf (\<lambda>(y, x, z). (from_nat_into (A y) x, from_nat_into (B y) z)) a"
1.148 +    def pr \<equiv> "map_pmf (\<lambda>(y, x, z). (x, z)) pqr"
1.149
1.150      have "rel_pmf (R OO S) p r"
1.151      proof
1.152 -      have pp_eq: "pp = map_pmf (\<lambda>(y, x, z). (y, x)) a"
1.153 +      have pq_eq: "pq = map_pmf (\<lambda>(y, x, z). (x, y)) pqr"
1.154        proof (rule pmf_eqI)
1.155          fix i
1.156 -        show "pmf pp i = pmf (map_pmf (\<lambda>(y, x, z). (y, x)) a) i"
1.157 -          using nn_integral_assign2[of "fst i" "snd i", symmetric]
1.158 +        show "pmf pq i = pmf (map_pmf (\<lambda>(y, x, z). (x, y)) pqr) i"
1.159 +          using nn_integral_assign2[of "snd i" "fst i", symmetric]
1.160            by (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map
1.161                     simp del: ereal.inject intro!: arg_cong2[where f=emeasure])
1.162        qed
1.163 -      moreover have pq_eq: "pq = map_pmf (\<lambda>(y, x). (from_nat_into (A y) x, y)) pp"
1.164 -        by (simp add: pp_def map_pmf_comp split_beta A[symmetric] cong: map_pmf_cong)
1.165 -      ultimately show "map_pmf fst pr = p"
1.166 +      then show "map_pmf fst pr = p"
1.167          unfolding p pr_def by (simp add: map_pmf_comp split_beta)
1.168
1.169 -      have rr_eq: "rr = map_pmf (\<lambda>(y, x, z). (y, z)) a"
1.170 +      have qr_eq: "qr = map_pmf (\<lambda>(y, x, z). (y, z)) pqr"
1.171        proof (rule pmf_eqI)
1.172 -        fix i show "pmf rr i = pmf (map_pmf (\<lambda>(y, x, z). (y, z)) a) i"
1.173 +        fix i show "pmf qr i = pmf (map_pmf (\<lambda>(y, x, z). (y, z)) pqr) i"
1.174            using nn_integral_assign1[of "fst i" "snd i", symmetric]
1.175            by (auto simp add: a nn_integral_pmf' inj_on_def ereal.inject[symmetric] ereal_pmf_map
1.176                     simp del: ereal.inject intro!: arg_cong2[where f=emeasure])
1.177        qed
1.178 -      moreover have qr_eq: "qr = map_pmf (\<lambda>(y, z). (y, from_nat_into (B y) z)) rr"
1.179 -        by (simp add: rr_def map_pmf_comp split_beta B[symmetric] cong: map_pmf_cong)
1.180 -      ultimately show "map_pmf snd pr = r"
1.181 +      then show "map_pmf snd pr = r"
1.182          unfolding r pr_def by (simp add: map_pmf_comp split_beta)
1.183
1.184        fix x z assume "(x, z) \<in> set_pmf pr"
1.185        then have "\<exists>y. (x, y) \<in> set_pmf pq \<and> (y, z) \<in> set_pmf qr"
1.186 -        by (force simp add: pp_eq pq_eq rr_eq qr_eq set_map_pmf pr_def image_image)
1.187 +        unfolding pr_def pq_eq qr_eq by (force simp: set_map_pmf)
1.188        with pq qr show "(R OO S) x z"
1.189          by blast
1.190      qed }
```