src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy
changeset 62696 7325d8573fb8
child 62726 5b2a7caa855b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,48 @@
     1.4 +(*  Title:      HOL/Corec_Examples/Tests/GPV_Bare_Bones
     1.5 +    Author:     Andreas Lochbihler, ETH Zuerich
     1.6 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     1.7 +    Copyright   2016
     1.8 +
     1.9 +A bare bones version of generative probabilistic values (GPVs).
    1.10 +*)
    1.11 +
    1.12 +section {* A Bare Bones Version of Generative Probabilistic Values (GPVs) *}
    1.13 +
    1.14 +theory GPV_Bare_Bones
    1.15 +imports "~~/src/HOL/Library/BNF_Corec"
    1.16 +begin
    1.17 +
    1.18 +datatype 'a pmf = return_pmf 'a
    1.19 +
    1.20 +type_synonym 'a spmf = "'a option pmf"
    1.21 +
    1.22 +abbreviation map_spmf :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a spmf \<Rightarrow> 'b spmf"
    1.23 +where "map_spmf f \<equiv> map_pmf (map_option f)"
    1.24 +
    1.25 +abbreviation return_spmf :: "'a \<Rightarrow> 'a spmf"
    1.26 +where "return_spmf x \<equiv> return_pmf (Some x)"
    1.27 +
    1.28 +datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat =
    1.29 +  Pure (result: 'a)
    1.30 +| IO ("output": 'b) (continuation: "'c")
    1.31 +
    1.32 +codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv =
    1.33 +  GPV (the_gpv: "('a, 'out, 'in \<Rightarrow> ('a, 'out, 'in) gpv) generat spmf")
    1.34 +
    1.35 +codatatype ('a, 'call, 'ret, 'x) gpv' =
    1.36 +  GPV' (the_gpv': "('a, 'call, 'ret \<Rightarrow> ('a, 'call, 'ret, 'x) gpv') generat spmf")
    1.37 +
    1.38 +consts bind_gpv' :: "('a, 'call, 'ret) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'call, 'ret, 'a) gpv') \<Rightarrow> ('b, 'call, 'ret, 'a) gpv'"
    1.39 +
    1.40 +definition bind_spmf :: "'a spmf \<Rightarrow> ('a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf"
    1.41 +where "bind_spmf x f = undefined x (\<lambda>a. case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> f a')"
    1.42 +
    1.43 +friend_of_corec bind_gpv'
    1.44 +where "bind_gpv' r f =
    1.45 +GPV' (map_spmf (map_generat id id (op \<circ> (case_sum id (\<lambda>r. bind_gpv' r f))))
    1.46 +      (bind_spmf (the_gpv r)
    1.47 +        (case_generat (\<lambda>x. map_spmf (map_generat id id (op \<circ> Inl)) (the_gpv' (f x)))
    1.48 +          (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
    1.49 +  sorry
    1.50 +
    1.51 +end