rel_pmf OO: conversion to nat is not necessary
authorhoelzl
Fri Jan 09 10:49:35 2015 +0100 (2015-01-09)
changeset 593278a779359df67
parent 59326 46491010b83a
child 59328 b83d6c3c439a
rel_pmf OO: conversion to nat is not necessary
src/HOL/Probability/Probability_Mass_Function.thy
     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 }