1theory Iterate_GPV imports
2  "HOL-Library.BNF_Axiomatization"
3  "HOL-Library.BNF_Corec"
4begin
5
6declare [[typedef_overloaded]]
7
8datatype 'a spmf = return_spmf 'a
9
10primrec (transfer) bind_spmf where
11  "bind_spmf (return_spmf a) f = f a"
12
13datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat
14  = Pure (result: 'a)
15  | IO ("output": 'b) (continuation: "'c")
16
17codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv
18  = GPV (the_gpv: "('a, 'out, 'in \<Rightarrow> ('a, 'out, 'in) gpv) generat spmf")
19
20declare gpv.rel_eq [relator_eq]
21
22primcorec bind_gpv :: "('a, 'out, 'in) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'out, 'in) gpv) \<Rightarrow> ('b, 'out, 'in) gpv"
23where
24  "bind_gpv r f = GPV (map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. bind_gpv r f))))
25     (bind_spmf (the_gpv r)
26      (case_generat
27        (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (f x)))
28        (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
29
30context includes lifting_syntax begin
31
32lemma bind_gpv_parametric [transfer_rule]:
33  "(rel_gpv A C ===> (A ===> rel_gpv B C) ===> rel_gpv B C) bind_gpv bind_gpv"
34unfolding bind_gpv_def by transfer_prover
35
36end
37
38lemma [friend_of_corec_simps]:
39  "map_spmf f (bind_spmf x h) = bind_spmf x (map_spmf f o h)"
40  by (cases x) auto
41
42lemma [friend_of_corec_simps]:
43  "bind_spmf (map_spmf f x) h = bind_spmf x (h o f)"
44  by (cases x) auto
45
46friend_of_corec bind_gpv :: "('a, 'out, 'in) gpv \<Rightarrow> ('a \<Rightarrow> ('a, 'out, 'in) gpv) \<Rightarrow> ('a, 'out, 'in) gpv"
47where "bind_gpv r f = GPV (map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. bind_gpv r f))))
48     (bind_spmf (the_gpv r)
49      (case_generat
50        (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (f x)))
51        (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
52apply(rule bind_gpv.ctr)
53apply transfer_prover
54apply transfer_prover
55done
56
57end
58