Theory CVM_Preliminary

section ‹Preliminary Definitions and Results›

theory CVM_Preliminary
  imports "HOL-Probability.SPMF"
begin

lemma bounded_finite:
  assumes ‹finite S›
  shows ‹bounded (f ` S)›
  using assms by (intro finite_imp_bounded) auto

lemma of_bool_power:
  assumes ‹y > 0›
  shows ‹(of_bool x::real) ^ (y::nat) = of_bool x›
  by (simp add: assms)

lemma card_filter_mono:
  assumes ‹finite S›
  shows ‹card (Set.filter p S) ≤ card S›
  by (intro card_mono assms) auto

fun foldM ::
  ‹('a ⇒ ('b ⇒ 'c) ⇒ 'c) ⇒ ('b ⇒ 'c) ⇒ ('d ⇒ 'b ⇒ 'a) ⇒ 'd list ⇒ 'b ⇒ 'c› where
  ‹foldM _ return' _ [] val = return' val› |
  ‹foldM bind' return' f (x # xs) val =
    bind' (f x val) (foldM bind' return' f xs)›

abbreviation foldM_pmf ::
  ‹('a ⇒ 'b ⇒ 'b pmf) ⇒ 'a list ⇒ 'b ⇒ 'b pmf› where
  ‹foldM_pmf ≡ foldM bind_pmf return_pmf›

lemma foldM_pmf_snoc: ‹foldM_pmf f (xs@[y]) val = bind_pmf (foldM_pmf f xs val) (f y)›
  by (induction xs arbitrary:val)
    (simp_all add: bind_return_pmf bind_return_pmf' bind_assoc_pmf cong:bind_pmf_cong)

abbreviation foldM_spmf
  :: ‹('a ⇒ 'b ⇒ 'b spmf) ⇒ 'a list ⇒ 'b ⇒ 'b spmf› where
  ‹foldM_spmf ≡ foldM bind_spmf return_spmf›

lemma foldM_spmf_snoc: ‹foldM_spmf f (xs@[y]) val = bind_spmf (foldM_spmf f xs val) (f y)›
  by (induction xs arbitrary:val) (simp_all cong:bind_spmf_cong)

abbreviation ‹prob_fail ≡ (λx. pmf x None)›

abbreviation ‹fail_spmf ≡ return_pmf None›

abbreviation fails_or_satisfies :: ‹('a ⇒ bool) ⇒ 'a option ⇒ bool› where
  ‹fails_or_satisfies ≡ case_option True›

lemma prob_fail_foldM_spmf_le :
  fixes
    p :: real and
    P :: ‹'b ⇒ bool› and
    f :: ‹'a ⇒ 'b ⇒ 'b spmf›
  assumes
    ‹⋀ x y z. P y ⟹ z ∈ set_spmf (f x y) ⟹ P z›
    ‹⋀ x val. P val ⟹ prob_fail (f x val) ≤ p›
    ‹P val›
  shows ‹prob_fail (foldM_spmf f xs val) ≤ real (length xs) * p›
using assms(3) proof (induction xs arbitrary: val)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)

  have p_ge_0: ‹p ≥ 0› using Cons(2) assms(2) order_trans[OF pmf_nonneg] by metis

  let ?val' = ‹f x val›
  let ?μ' = ‹measure_spmf ?val'›

  have
    ‹prob_fail (foldM_spmf f (x # xs) val) =
      prob_fail ?val' + ∫ val'. prob_fail (foldM_spmf f xs val') ∂ ?μ'›
    by (simp add: pmf_bind_spmf_None)
  also have ‹… ≤ p + ∫ _. length xs * p ∂ ?μ'›
    using assms(1)[OF Cons(2)]
    by (intro add_mono integral_mono_AE iffD2[OF AE_measure_spmf_iff] ballI assms(2) Cons
         measure_spmf.integrable_const measure_spmf.integrable_const_bound[where B=‹1›])
     (simp_all add:pmf_le_1)
  also have ‹… ≤ p + weight_spmf (f x val)* length xs * p›
    by simp
  also have ‹… ≤ p + 1 * real (length xs) * p›
    by (intro add_mono mult_right_mono p_ge_0 weight_spmf_le_1) simp_all
  finally show ?case by (simp add: algebra_simps)
qed

lemma foldM_spmf_of_pmf_eq :
  shows ‹foldM_spmf (λx y. spmf_of_pmf (f x y)) xs = spmf_of_pmf ∘ foldM_pmf f xs›
  (is ?thesis_0)
    and ‹foldM_spmf (λx y. spmf_of_pmf (f x y)) xs val = spmf_of_pmf (foldM_pmf f xs val)›
  (is ?thesis_1)
proof -
  show ?thesis_0
    by (induction xs) (simp_all add: spmf_of_pmf_bind)

  then show ?thesis_1 by simp
qed

end