Theory Lotteries

(*  
  Title:    Libraries.thy
  Author:   Manuel Eberl, TU München

  Definition of lotteries on a set. (Essentially just restricting PMFs to a carrier set)
*)

section ‹Auxiliary facts about PMFs›

theory Lotteries
  imports Complex_Main "HOL-Probability.Probability"
begin

text ‹The type of lotteries (a probability mass function)›
type_synonym 'alt lottery = "'alt pmf"

definition lotteries_on :: "'a set ⇒ 'a lottery set" where
  "lotteries_on A = {p. set_pmf p ⊆ A}"

lemma pmf_of_set_lottery:
  "A ≠ {} ⟹ finite A ⟹ A ⊆ B ⟹ pmf_of_set A ∈ lotteries_on B"
  unfolding lotteries_on_def by auto

lemma pmf_of_list_lottery: 
  "pmf_of_list_wf xs ⟹ set (map fst xs) ⊆ A ⟹ pmf_of_list xs ∈ lotteries_on A"
  using set_pmf_of_list[of xs] by (auto simp: lotteries_on_def)

lemma return_pmf_in_lotteries_on [simp,intro]: 
  "x ∈ A ⟹ return_pmf x ∈ lotteries_on A"
  by (simp add: lotteries_on_def)

end