author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 62858 | d72a6f9ee690 |
child 67399 | eab6ce8368fa |
permissions | -rw-r--r-- |
62858 | 1 |
(* Title: HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy |
62696 | 2 |
Author: Andreas Lochbihler, ETH Zuerich |
3 |
Author: Jasmin Blanchette, Inria, LORIA, MPII |
|
4 |
Copyright 2016 |
|
5 |
||
6 |
A bare bones version of generative probabilistic values (GPVs). |
|
7 |
*) |
|
8 |
||
62726 | 9 |
section \<open>A Bare Bones Version of Generative Probabilistic Values (GPVs)\<close> |
62696 | 10 |
|
11 |
theory GPV_Bare_Bones |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
62858
diff
changeset
|
12 |
imports "HOL-Library.BNF_Corec" |
62696 | 13 |
begin |
14 |
||
15 |
datatype 'a pmf = return_pmf 'a |
|
16 |
||
17 |
type_synonym 'a spmf = "'a option pmf" |
|
18 |
||
19 |
abbreviation map_spmf :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a spmf \<Rightarrow> 'b spmf" |
|
20 |
where "map_spmf f \<equiv> map_pmf (map_option f)" |
|
21 |
||
22 |
abbreviation return_spmf :: "'a \<Rightarrow> 'a spmf" |
|
23 |
where "return_spmf x \<equiv> return_pmf (Some x)" |
|
24 |
||
25 |
datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat = |
|
26 |
Pure (result: 'a) |
|
27 |
| IO ("output": 'b) (continuation: "'c") |
|
28 |
||
29 |
codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv = |
|
30 |
GPV (the_gpv: "('a, 'out, 'in \<Rightarrow> ('a, 'out, 'in) gpv) generat spmf") |
|
31 |
||
32 |
codatatype ('a, 'call, 'ret, 'x) gpv' = |
|
33 |
GPV' (the_gpv': "('a, 'call, 'ret \<Rightarrow> ('a, 'call, 'ret, 'x) gpv') generat spmf") |
|
34 |
||
35 |
consts bind_gpv' :: "('a, 'call, 'ret) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'call, 'ret, 'a) gpv') \<Rightarrow> ('b, 'call, 'ret, 'a) gpv'" |
|
36 |
||
37 |
definition bind_spmf :: "'a spmf \<Rightarrow> ('a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf" |
|
38 |
where "bind_spmf x f = undefined x (\<lambda>a. case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> f a')" |
|
39 |
||
40 |
friend_of_corec bind_gpv' |
|
41 |
where "bind_gpv' r f = |
|
42 |
GPV' (map_spmf (map_generat id id (op \<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 (op \<circ> Inl)) (the_gpv' (f x))) |
|
45 |
(\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))" |
|
46 |
sorry |
|
47 |
||
48 |
end |