Theory Lotteries

(* License: LGPL *)
(* Author: Julian Parsert *)

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


section ‹ Lotteries ›

definition lotteries_on 
  where
    "lotteries_on Oc = {p . (set_pmf p) ⊆ Oc}"

lemma lotteries_on_subset:
  assumes "A ⊆ B"
  shows "lotteries_on A ⊆ lotteries_on B"
  by (metis (no_types, lifting) Collect_mono assms gfp.leq_trans lotteries_on_def)

lemma support_in_outcomes:
  "∀oc. ∀p ∈ lotteries_on oc. ∀a ∈ set_pmf p. a ∈ oc"
  by (simp add: lotteries_on_def subsetD)

lemma lotteries_on_nonempty:
  assumes "outcomes ≠ {}" 
  shows "lotteries_on outcomes ≠ {}"
  by (auto simp: lotteries_on_def) (metis (full_types) assms 
      empty_subsetI ex_in_conv insert_subset set_return_pmf)

lemma finite_support_one_oc:
  assumes "card outcomes = 1"
  shows "∀l ∈ lotteries_on outcomes. finite (set_pmf l)"
  by (metis assms card.infinite finite_subset lotteries_on_def mem_Collect_eq zero_neq_one)

lemma one_outcome_card_support_1:
  assumes "card outcomes = 1"
  shows "∀l ∈ lotteries_on outcomes. card (set_pmf l) = 1"
proof 
  fix l
  assume "l ∈ lotteries_on outcomes"
  have "finite outcomes"
    using assms card.infinite by force
  then have "l ∈ lotteries_on outcomes ⟶ 1 = card (set_pmf l)"
    by (metis assms card_eq_0_iff card_mono finite_support_one_oc le_neq_implies_less 
        less_one lotteries_on_def mem_Collect_eq set_pmf_not_empty)
  then show "card (set_pmf l) = 1"
    by (simp add: ‹l ∈ lotteries_on outcomes›)
qed  

lemma finite_nempty_ex_degernate_in_lotteries:
  assumes "out ≠ {}"
  assumes "finite out"
  shows "∃e ∈ lotteries_on out. ∃x ∈ out. pmf e x = 1"
proof (rule ccontr)
  assume a: "¬ (∃e∈lotteries_on out. ∃x∈out. pmf e x = 1)"
  then have subset: "∀e ∈ lotteries_on out. set_pmf e ⊆ out"
    using lotteries_on_def by (simp add: lotteries_on_def)
  then have "∀e. e ∈ lotteries_on out ⟶ ((∑i∈set_pmf e. pmf e i) = 1)"
    using sum_pmf_eq_1 by (metis subset  assms(2) finite_subset order_refl)
  then show False
    by (metis (no_types, lifting) a assms(1) assms(2) card.empty card_gt_0_iff card_seteq 
        empty_subsetI finite.emptyI finite_insert insert_subset lotteries_on_def subsetI
        measure_measure_pmf_finite mem_Collect_eq nat_less_le pmf.rep_eq set_pmf_of_set )
qed

lemma card_support_1_probability_1:
  assumes "card (set_pmf p) = 1"
  shows "∀e ∈ set_pmf p. pmf p e = 1" 
  by(auto) (metis assms card_1_singletonE card_ge_0_finite 
      card_subset_eq ex_card le_numeral_extra(4) measure_measure_pmf_finite 
      pmf.rep_eq singletonD sum_pmf_eq_1 zero_less_one)

lemma one_outcome_card_lotteries_1:
  assumes "card outcomes = 1"
  shows "card (lotteries_on outcomes) = 1"
proof -
  obtain x :: 'a where
    x: "outcomes = {x}"
    using assms card_1_singletonE by blast
  have exl: "∃l ∈ lotteries_on outcomes. pmf l x = 1"
    by (metis x assms card.infinite empty_iff 
        finite_nempty_ex_degernate_in_lotteries insert_iff zero_neq_one)
  have pmfs: "∀l ∈ lotteries_on outcomes. set_pmf l = {x}"
    by (simp add: lotteries_on_def set_pmf_subset_singleton x)
  have "∀l ∈ lotteries_on outcomes. pmf l x = 1"
    by (simp add: lotteries_on_def set_pmf_subset_singleton x)
  then show ?thesis 
    by (metis exl empty_iff is_singletonI' is_singleton_altdef
        order_refl pmfs set_pmf_subset_singleton)
qed

lemma return_pmf_card_equals_set:
  shows "card {return_pmf x |x. x ∈ S} = card S"
proof-
  have "{return_pmf x |x. x ∈ S} = return_pmf ` S" 
    by blast
  also have "card … = card S" 
    by (intro card_image) (auto simp: inj_on_def)
  finally show "card {return_pmf x |x. x ∈ S} = card S" .
qed

lemma mix_pmf_in_lotteries:
  assumes "p ∈ lotteries_on A"
    and "q ∈ lotteries_on A"
    and "a ∈ {0<..<1}"
  shows "(mix_pmf a p q) ∈ lotteries_on A"
proof -
  have "set_pmf (mix_pmf a p q) = set_pmf p ∪ set_pmf q"
    by (meson assms(3) set_pmf_mix)
  then show ?thesis
    by (metis Un_subset_iff assms(1) assms(2) lotteries_on_def mem_Collect_eq)
qed

lemma card_degen_lotteries_equals_outcomes:
  shows "card {x ∈ lotteries_on out. card (set_pmf x) = 1} = card out"
proof -
  consider (empty) "out = {}" | (not_empty) "out ≠ {}"
    by blast
  then show ?thesis
  proof (cases)
    case not_empty
    define DG where
      DG: "DG = {x ∈ lotteries_on out. card (set_pmf x) = 1}"
    define AP where
      AP: "AP = {return_pmf x |x. x ∈ out}"
    have **: "card AP = card out"
      using AP return_pmf_card_equals_set by blast
    have *: "∀d ∈ DG. d ∈ AP"
    proof
      fix l
      assume "l ∈ DG"
      then have "l ∈ lotteries_on out ∧ 1 = card (set_pmf l)"
        using DG by force
      then obtain x where
        x: "x ∈ out" "set_pmf l = {x}"
        by (metis (no_types) card_1_singletonE singletonI support_in_outcomes)
      have "return_pmf x = l"
        using set_pmf_subset_singleton x(2) by fastforce
      then show "l ∈ AP" 
        using AP x(1) by blast
    qed
    moreover have "AP = DG"
    proof
      have "∀e ∈ AP. e ∈ lotteries_on out"
        by(auto simp: lotteries_on_def AP)
      then show "AP ⊆ DG" using DG AP by force
    qed (auto simp: *)
    ultimately show ?thesis
      using DG ** by blast
  qed (simp add: lotteries_on_def set_pmf_not_empty)
qed

end