tune proof
authorAndreas Lochbihler
Tue Feb 10 12:10:26 2015 +0100 (2015-02-10)
changeset 59490f71732294f29
parent 59489 fd5d23cc0e97
child 59491 40f570f9a284
tune proof
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 12:05:21 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 10 12:10:26 2015 +0100
     1.3 @@ -279,6 +279,9 @@
     1.4      using measure_pmf.emeasure_space_1 by simp
     1.5  qed
     1.6  
     1.7 +lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1"
     1.8 +using measure_pmf.emeasure_space_1[of M] by simp
     1.9 +
    1.10  lemma in_null_sets_measure_pmfI:
    1.11    "A \<inter> set_pmf p = {} \<Longrightarrow> A \<in> null_sets (measure_pmf p)"
    1.12  using emeasure_eq_0_AE[where ?P="\<lambda>x. x \<in> A" and M="measure_pmf p"]
    1.13 @@ -1064,19 +1067,14 @@
    1.14          unfolding pqr_def
    1.15        proof (subst pmf_embed_pmf)
    1.16          have "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) =
    1.17 -          (\<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.18 -          by (force simp add: pmf_eq_0_set_pmf r set_map_pmf split: split_indicator
    1.19 -                    intro!: nn_integral_count_space_eq assign_eq_0_outside)
    1.20 -        also have "\<dots> = (\<integral>\<^sup>+ x. ereal ((\<lambda>((x, y), z). assign y x z) x) \<partial>(count_space (pq \<times> r)))"
    1.21 -          by (subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
    1.22 -             (auto simp: inj_on_def intro!: nn_integral_cong)
    1.23 -        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.24 -          by (subst sigma_finite_measure.nn_integral_fst)
    1.25 -             (auto simp: pair_measure_countable sigma_finite_measure_count_space_countable)
    1.26 -        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.27 -          by (intro nn_integral_cong nn_integral_count_space_eq)
    1.28 -             (force simp: r set_map_pmf pmf_eq_0_set_pmf intro!: assign_eq_0_outside)+
    1.29 -        also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space pq)"
    1.30 +              (\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space ((\<lambda>((x, y), z). (y, x, z)) ` UNIV))"
    1.31 +          by(rule nn_integral_count_space_eq)(auto simp add: image_def)
    1.32 +        also have "\<dots> = \<integral>\<^sup>+ x. ereal ((\<lambda>((x, y), z). assign y x z) x) \<partial>count_space UNIV"
    1.33 +          by(subst nn_integral_bij_count_space[OF inj_on_imp_bij_betw, symmetric])
    1.34 +            (auto simp add: inj_on_def split_beta)
    1.35 +        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 UNIV)"
    1.36 +          by(subst nn_integral_fst_count_space) simp
    1.37 +        also have "\<dots> = (\<integral>\<^sup>+ z. ?pq (snd z) (fst z) \<partial>count_space UNIV)"
    1.38            by (subst nn_integral_assign2[symmetric]) (auto intro!: nn_integral_cong)
    1.39          finally show "(\<integral>\<^sup>+ x. ereal ((\<lambda>(y, x, z). assign y x z) x) \<partial>count_space UNIV) = 1"
    1.40            by (simp add: nn_integral_pmf emeasure_pmf)