Theory GPV_Bare_Bones

(*  Title:      HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy
    Author:     Andreas Lochbihler, ETH Zuerich
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
    Copyright   2016

A bare bones version of generative probabilistic values (GPVs).
*)

section ‹A Bare Bones Version of Generative Probabilistic Values (GPVs)›

theory GPV_Bare_Bones
imports "HOL-Library.BNF_Corec"
begin

datatype 'a pmf = return_pmf 'a

type_synonym 'a spmf = "'a option pmf"

abbreviation map_spmf :: "('a ⇒ 'b) ⇒ 'a spmf ⇒ 'b spmf"
where "map_spmf f ≡ map_pmf (map_option f)"

abbreviation return_spmf :: "'a ⇒ 'a spmf"
where "return_spmf x ≡ return_pmf (Some x)"

datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat =
  Pure (result: 'a)
| IO ("output": 'b) (continuation: "'c")

codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv =
  GPV (the_gpv: "('a, 'out, 'in ⇒ ('a, 'out, 'in) gpv) generat spmf")

codatatype ('a, 'call, 'ret, 'x) gpv' =
  GPV' (the_gpv': "('a, 'call, 'ret ⇒ ('a, 'call, 'ret, 'x) gpv') generat spmf")

consts bind_gpv' :: "('a, 'call, 'ret) gpv ⇒ ('a ⇒ ('b, 'call, 'ret, 'a) gpv') ⇒ ('b, 'call, 'ret, 'a) gpv'"

definition bind_spmf :: "'a spmf ⇒ ('a ⇒ 'b spmf) ⇒ 'b spmf"
where "bind_spmf x f = undefined x (λa. case a of None ⇒ return_pmf None | Some a' ⇒ f a')"

friend_of_corec bind_gpv'
where "bind_gpv' r f =
GPV' (map_spmf (map_generat id id ((∘) (case_sum id (λr. bind_gpv' r f))))
      (bind_spmf (the_gpv r)
        (case_generat (λx. map_spmf (map_generat id id ((∘) Inl)) (the_gpv' (f x)))
          (λout c. return_spmf (IO out (λinput. Inr (c input)))))))"
  sorry

end