Theory GPV_Applicative

theory GPV_Applicative imports
  Generative_Probabilistic_Value
  SPMF_Applicative
begin

subsection ‹Applicative instance for @{typ "(_, 'out, 'in) gpv"}›

definition ap_gpv :: "('a ⇒ 'b, 'out, 'in) gpv ⇒ ('a, 'out, 'in) gpv ⇒ ('b, 'out, 'in) gpv"
where "ap_gpv f x = bind_gpv f (λf'. bind_gpv x (λx'. Done (f' x')))"

adhoc_overloading Applicative.ap ap_gpv

abbreviation (input) pure_gpv :: "'a ⇒ ('a, 'out, 'in) gpv"
where "pure_gpv ≡ Done"

context includes applicative_syntax begin

lemma ap_gpv_id: "pure_gpv (λx. x) ⋄ x = x"
by(simp add: ap_gpv_def)

lemma ap_gpv_comp: "pure_gpv (∘) ⋄ u ⋄ v ⋄ w = u ⋄ (v ⋄ w)"
by(simp add: ap_gpv_def bind_gpv_assoc)

lemma ap_gpv_homo: "pure_gpv f ⋄ pure_gpv x = pure_gpv (f x)"
by(simp add: ap_gpv_def)

lemma ap_gpv_interchange: "u ⋄ pure_gpv x = pure_gpv (λf. f x) ⋄ u"
by(simp add: ap_gpv_def)

applicative gpv
for
  pure: pure_gpv
  ap: ap_gpv
by(rule ap_gpv_id ap_gpv_comp[unfolded o_def[abs_def]] ap_gpv_homo ap_gpv_interchange)+

lemma map_conv_ap_gpv: "map_gpv f (λx. x) gpv = pure_gpv f ⋄ gpv"
by(simp add: ap_gpv_def map_gpv_conv_bind)

lemma exec_gpv_ap:
  "exec_gpv callee (f ⋄ x) σ = 
   exec_gpv callee f σ ⤜ (λ(f', σ'). pure_spmf (λ(x', σ''). (f' x', σ'')) ⋄ exec_gpv callee x σ')"
by(simp add: ap_gpv_def exec_gpv_bind ap_spmf_conv_bind split_def)

lemma exec_gpv_ap_pure [simp]:
  "exec_gpv callee (pure_gpv f ⋄ x) σ = pure_spmf (apfst f) ⋄ exec_gpv callee x σ"
by(simp add: exec_gpv_ap apfst_def map_prod_def)

end

end