src/HOL/Probability/Probability_Mass_Function.thy
changeset 61609 77b453bd616f
parent 61424 c3658c18b7bc
child 61610 4f54d2759a0b
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Nov 03 11:20:21 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Nov 10 14:18:41 2015 +0000
     1.3 @@ -59,7 +59,7 @@
     1.4      note singleton_sets = this
     1.5      have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
     1.6        using `?M \<noteq> 0`
     1.7 -      by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg)
     1.8 +      by (simp add: `card X = Suc (Suc n)` of_nat_Suc field_simps less_le measure_nonneg)
     1.9      also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
    1.10        by (rule setsum_mono) fact
    1.11      also have "\<dots> = measure M (\<Union>x\<in>X. {x})"
    1.12 @@ -956,7 +956,7 @@
    1.13  
    1.14  lemma quotient_rel_set_disjoint:
    1.15    "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.16 -  using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] 
    1.17 +  using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C]
    1.18    by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE)
    1.19       (blast dest: equivp_symp)+
    1.20  
    1.21 @@ -973,17 +973,17 @@
    1.22  next
    1.23    fix C assume C: "C \<in> UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)"
    1.24    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.25 -  
    1.26 +
    1.27    show "measure p C = measure q C"
    1.28    proof cases
    1.29      assume "p \<inter> C = {}"
    1.30 -    moreover then have "q \<inter> C = {}"  
    1.31 +    moreover then have "q \<inter> C = {}"
    1.32        using quotient_rel_set_disjoint[OF assms C R] by simp
    1.33      ultimately show ?thesis
    1.34        unfolding measure_pmf_zero_iff[symmetric] by simp
    1.35    next
    1.36      assume "p \<inter> C \<noteq> {}"
    1.37 -    moreover then have "q \<inter> C \<noteq> {}"  
    1.38 +    moreover then have "q \<inter> C \<noteq> {}"
    1.39        using quotient_rel_set_disjoint[OF assms C R] by simp
    1.40      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.41        by auto
    1.42 @@ -1068,11 +1068,11 @@
    1.43          and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
    1.44        from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
    1.45          and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
    1.46 -  
    1.47 +
    1.48        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.49        have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
    1.50          by (force simp: q')
    1.51 -  
    1.52 +
    1.53        have "rel_pmf (R OO S) p r"
    1.54        proof (rule rel_pmf.intros)
    1.55          fix x z assume "(x, z) \<in> pr"
    1.56 @@ -1283,7 +1283,7 @@
    1.57  proof (subst rel_pmf_iff_equivp, safe)
    1.58    show "equivp (inf R R\<inverse>\<inverse>)"
    1.59      using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD)
    1.60 -  
    1.61 +
    1.62    fix C assume "C \<in> UNIV // {(x, y). inf R R\<inverse>\<inverse> x y}"
    1.63    then obtain x where C: "C = {y. R x y \<and> R y x}"
    1.64      by (auto elim: quotientE)
    1.65 @@ -1399,7 +1399,7 @@
    1.66  end
    1.67  
    1.68  lemma set_pmf_geometric: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (geometric_pmf p) = UNIV"
    1.69 -  by (auto simp: set_pmf_iff) 
    1.70 +  by (auto simp: set_pmf_iff)
    1.71  
    1.72  subsubsection \<open> Uniform Multiset Distribution \<close>
    1.73  
    1.74 @@ -1445,7 +1445,7 @@
    1.75  lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
    1.76    by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
    1.77  
    1.78 -lemma nn_integral_pmf_of_set': 
    1.79 +lemma nn_integral_pmf_of_set':
    1.80    "(\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S"
    1.81  apply(subst nn_integral_measure_pmf_finite, simp_all add: S_finite)
    1.82  apply(simp add: setsum_ereal_left_distrib[symmetric])
    1.83 @@ -1453,7 +1453,7 @@
    1.84  apply(simp add: ereal_times_divide_eq one_ereal_def[symmetric])
    1.85  done
    1.86  
    1.87 -lemma nn_integral_pmf_of_set: 
    1.88 +lemma nn_integral_pmf_of_set:
    1.89    "nn_integral (measure_pmf pmf_of_set) f = setsum (max 0 \<circ> f) S / card S"
    1.90  apply(subst nn_integral_max_0[symmetric])
    1.91  apply(subst nn_integral_pmf_of_set')
    1.92 @@ -1476,7 +1476,7 @@
    1.93  lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
    1.94  by(rule pmf_eqI)(simp add: indicator_def)
    1.95  
    1.96 -lemma map_pmf_of_set_inj: 
    1.97 +lemma map_pmf_of_set_inj:
    1.98    assumes f: "inj_on f A"
    1.99    and [simp]: "A \<noteq> {}" "finite A"
   1.100    shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs")
   1.101 @@ -1540,7 +1540,7 @@
   1.102      ereal (\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))"
   1.103      using p_le_1 p_nonneg by (subst nn_integral_count_space') auto
   1.104    also have "(\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k)) = (p + (1 - p)) ^ n"
   1.105 -    by (subst binomial_ring) (simp add: atLeast0AtMost real_of_nat_def)
   1.106 +    by (subst binomial_ring) (simp add: atLeast0AtMost)
   1.107    finally show "(\<integral>\<^sup>+ x. ereal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \<partial>count_space UNIV) = 1"
   1.108      by simp
   1.109  qed (insert p_nonneg p_le_1, simp)