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