1(*  Title:      HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy
2    Author:     Andreas Lochbihler, ETH Zuerich
3    Author:     Jasmin Blanchette, Inria, LORIA, MPII
4    Copyright   2016
5
6A bare bones version of generative probabilistic values (GPVs).
7*)
8
9section \<open>A Bare Bones Version of Generative Probabilistic Values (GPVs)\<close>
10
11theory GPV_Bare_Bones
12imports "HOL-Library.BNF_Corec"
13begin
14
15datatype 'a pmf = return_pmf 'a
16
17type_synonym 'a spmf = "'a option pmf"
18
19abbreviation map_spmf :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a spmf \<Rightarrow> 'b spmf"
20where "map_spmf f \<equiv> map_pmf (map_option f)"
21
22abbreviation return_spmf :: "'a \<Rightarrow> 'a spmf"
23where "return_spmf x \<equiv> return_pmf (Some x)"
24
25datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat =
26  Pure (result: 'a)
27| IO ("output": 'b) (continuation: "'c")
28
29codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv =
30  GPV (the_gpv: "('a, 'out, 'in \<Rightarrow> ('a, 'out, 'in) gpv) generat spmf")
31
32codatatype ('a, 'call, 'ret, 'x) gpv' =
33  GPV' (the_gpv': "('a, 'call, 'ret \<Rightarrow> ('a, 'call, 'ret, 'x) gpv') generat spmf")
34
35consts bind_gpv' :: "('a, 'call, 'ret) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'call, 'ret, 'a) gpv') \<Rightarrow> ('b, 'call, 'ret, 'a) gpv'"
36
37definition bind_spmf :: "'a spmf \<Rightarrow> ('a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf"
38where "bind_spmf x f = undefined x (\<lambda>a. case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> f a')"
39
40friend_of_corec bind_gpv'
41where "bind_gpv' r f =
42GPV' (map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. bind_gpv' r f))))
43      (bind_spmf (the_gpv r)
44        (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv' (f x)))
45          (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
46  sorry
47
48end
49