src/HOL/Probability/Probability_Mass_Function.thy
changeset 63194 0b7bdb75f451
parent 63101 65f1d7829463
child 63343 fb5d8a50c641
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue May 31 12:24:43 2016 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue May 31 13:02:44 2016 +0200
     1.3 @@ -1787,6 +1787,58 @@
     1.4  end
     1.5  
     1.6  
     1.7 +primrec replicate_pmf :: "nat \<Rightarrow> 'a pmf \<Rightarrow> 'a list pmf" where
     1.8 +  "replicate_pmf 0 _ = return_pmf []"
     1.9 +| "replicate_pmf (Suc n) p = do {x \<leftarrow> p; xs \<leftarrow> replicate_pmf n p; return_pmf (x#xs)}"
    1.10 +
    1.11 +lemma replicate_pmf_1: "replicate_pmf 1 p = map_pmf (\<lambda>x. [x]) p"
    1.12 +  by (simp add: map_pmf_def bind_return_pmf)
    1.13 +  
    1.14 +lemma set_replicate_pmf: 
    1.15 +  "set_pmf (replicate_pmf n p) = {xs\<in>lists (set_pmf p). length xs = n}"
    1.16 +  by (induction n) (auto simp: length_Suc_conv)
    1.17 +
    1.18 +lemma replicate_pmf_distrib:
    1.19 +  "replicate_pmf (m + n) p = 
    1.20 +     do {xs \<leftarrow> replicate_pmf m p; ys \<leftarrow> replicate_pmf n p; return_pmf (xs @ ys)}"
    1.21 +  by (induction m) (simp_all add: bind_return_pmf bind_return_pmf' bind_assoc_pmf)
    1.22 +
    1.23 +lemma power_diff': 
    1.24 +  assumes "b \<le> a"
    1.25 +  shows   "x ^ (a - b) = (if x = 0 \<and> a = b then 1 else x ^ a / (x::'a::field) ^ b)"
    1.26 +proof (cases "x = 0")
    1.27 +  case True
    1.28 +  with assms show ?thesis by (cases "a - b") simp_all
    1.29 +qed (insert assms, simp_all add: power_diff)
    1.30 +
    1.31 +  
    1.32 +lemma binomial_pmf_Suc:
    1.33 +  assumes "p \<in> {0..1}"
    1.34 +  shows   "binomial_pmf (Suc n) p = 
    1.35 +             do {b \<leftarrow> bernoulli_pmf p; 
    1.36 +                 k \<leftarrow> binomial_pmf n p; 
    1.37 +                 return_pmf ((if b then 1 else 0) + k)}" (is "_ = ?rhs")
    1.38 +proof (intro pmf_eqI)
    1.39 +  fix k
    1.40 +  have A: "indicator {Suc a} (Suc b) = indicator {a} b" for a b
    1.41 +    by (simp add: indicator_def)
    1.42 +  show "pmf (binomial_pmf (Suc n) p) k = pmf ?rhs k"
    1.43 +    by (cases k; cases "k > n")
    1.44 +       (insert assms, auto simp: pmf_bind measure_pmf_single A divide_simps algebra_simps
    1.45 +          not_less less_eq_Suc_le [symmetric] power_diff')
    1.46 +qed
    1.47 +
    1.48 +lemma binomial_pmf_0: "p \<in> {0..1} \<Longrightarrow> binomial_pmf 0 p = return_pmf 0"
    1.49 +  by (rule pmf_eqI) (simp_all add: indicator_def)
    1.50 +
    1.51 +lemma binomial_pmf_altdef:
    1.52 +  assumes "p \<in> {0..1}"
    1.53 +  shows   "binomial_pmf n p = map_pmf (length \<circ> filter id) (replicate_pmf n (bernoulli_pmf p))"
    1.54 +  by (induction n) 
    1.55 +     (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf 
    1.56 +        bind_return_pmf' binomial_pmf_0 intro!: bind_pmf_cong)
    1.57 +
    1.58 +
    1.59  subsection \<open>PMFs from assiciation lists\<close>
    1.60  
    1.61  definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where 
    1.62 @@ -1921,4 +1973,52 @@
    1.63    using assms unfolding pmf_of_list_wf_def Sigma_Algebra.measure_def
    1.64    by (subst emeasure_pmf_of_list [OF assms], subst enn2real_ennreal) (auto intro!: listsum_nonneg)
    1.65  
    1.66 +(* TODO Move? *)
    1.67 +lemma listsum_nonneg_eq_zero_iff:
    1.68 +  fixes xs :: "'a :: linordered_ab_group_add list"
    1.69 +  shows "(\<And>x. x \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> listsum xs = 0 \<longleftrightarrow> set xs \<subseteq> {0}"
    1.70 +proof (induction xs)
    1.71 +  case (Cons x xs)
    1.72 +  from Cons.prems have "listsum (x#xs) = 0 \<longleftrightarrow> x = 0 \<and> listsum xs = 0"
    1.73 +    unfolding listsum_simps by (subst add_nonneg_eq_0_iff) (auto intro: listsum_nonneg)
    1.74 +  with Cons.IH Cons.prems show ?case by simp
    1.75 +qed simp_all
    1.76 +
    1.77 +lemma listsum_filter_nonzero:
    1.78 +  "listsum (filter (\<lambda>x. x \<noteq> 0) xs) = listsum xs"
    1.79 +  by (induction xs) simp_all
    1.80 +(* END MOVE *)
    1.81 +  
    1.82 +lemma set_pmf_of_list_eq:
    1.83 +  assumes "pmf_of_list_wf xs" "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0"
    1.84 +  shows   "set_pmf (pmf_of_list xs) = fst ` set xs"
    1.85 +proof
    1.86 +  {
    1.87 +    fix x assume A: "x \<in> fst ` set xs" and B: "x \<notin> set_pmf (pmf_of_list xs)"
    1.88 +    then obtain y where y: "(x, y) \<in> set xs" by auto
    1.89 +    from B have "listsum (map snd [z\<leftarrow>xs. fst z = x]) = 0"
    1.90 +      by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
    1.91 +    moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
    1.92 +    ultimately have "y = 0" using assms(1) 
    1.93 +      by (subst (asm) listsum_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
    1.94 +    with assms(2) y have False by force
    1.95 +  }
    1.96 +  thus "fst ` set xs \<subseteq> set_pmf (pmf_of_list xs)" by blast
    1.97 +qed (insert set_pmf_of_list[OF assms(1)], simp_all)
    1.98 +  
    1.99 +lemma pmf_of_list_remove_zeros:
   1.100 +  assumes "pmf_of_list_wf xs"
   1.101 +  defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
   1.102 +  shows   "pmf_of_list_wf xs'" "pmf_of_list xs' = pmf_of_list xs"
   1.103 +proof -
   1.104 +  have "map snd [z\<leftarrow>xs . snd z \<noteq> 0] = filter (\<lambda>x. x \<noteq> 0) (map snd xs)"
   1.105 +    by (induction xs) simp_all
   1.106 +  with assms(1) show wf: "pmf_of_list_wf xs'"
   1.107 +    by (auto simp: pmf_of_list_wf_def xs'_def listsum_filter_nonzero)
   1.108 +  have "listsum (map snd [z\<leftarrow>xs' . fst z = i]) = listsum (map snd [z\<leftarrow>xs . fst z = i])" for i
   1.109 +    unfolding xs'_def by (induction xs) simp_all
   1.110 +  with assms(1) wf show "pmf_of_list xs' = pmf_of_list xs"
   1.111 +    by (intro pmf_eqI) (simp_all add: pmf_pmf_of_list)
   1.112 +qed
   1.113 +
   1.114  end