--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy Mon Oct 24 16:53:32 2016 +0200
@@ -0,0 +1,57 @@
+theory Iterate_GPV imports
+ "~~/src/HOL/Library/BNF_Axiomatization"
+ "~~/src/HOL/Library/BNF_Corec"
+begin
+
+declare [[typedef_overloaded]]
+
+datatype 'a spmf = return_spmf 'a
+
+primrec (transfer) bind_spmf where
+ "bind_spmf (return_spmf a) f = f a"
+
+datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat
+ = Pure (result: 'a)
+ | IO ("output": 'b) (continuation: "'c")
+
+codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv
+ = GPV (the_gpv: "('a, 'out, 'in \<Rightarrow> ('a, 'out, 'in) gpv) generat spmf")
+
+declare gpv.rel_eq [relator_eq]
+
+primcorec bind_gpv :: "('a, 'out, 'in) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'out, 'in) gpv) \<Rightarrow> ('b, 'out, 'in) gpv"
+where
+ "bind_gpv r f = GPV (map_spmf (map_generat id id (op \<circ> (case_sum id (\<lambda>r. bind_gpv r f))))
+ (bind_spmf (the_gpv r)
+ (case_generat
+ (\<lambda>x. map_spmf (map_generat id id (op \<circ> Inl)) (the_gpv (f x)))
+ (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
+
+context includes lifting_syntax begin
+
+lemma bind_gpv_parametric [transfer_rule]:
+ "(rel_gpv A C ===> (A ===> rel_gpv B C) ===> rel_gpv B C) bind_gpv bind_gpv"
+unfolding bind_gpv_def by transfer_prover
+
+end
+
+lemma [friend_of_corec_simps]:
+ "map_spmf f (bind_spmf x h) = bind_spmf x (map_spmf f o h)"
+ by (cases x) auto
+
+lemma [friend_of_corec_simps]:
+ "bind_spmf (map_spmf f x) h = bind_spmf x (h o f)"
+ by (cases x) auto
+
+friend_of_corec bind_gpv :: "('a, 'out, 'in) gpv \<Rightarrow> ('a \<Rightarrow> ('a, 'out, 'in) gpv) \<Rightarrow> ('a, 'out, 'in) gpv"
+where "bind_gpv r f = GPV (map_spmf (map_generat id id (op \<circ> (case_sum id (\<lambda>r. bind_gpv r f))))
+ (bind_spmf (the_gpv r)
+ (case_generat
+ (\<lambda>x. map_spmf (map_generat id id (op \<circ> Inl)) (the_gpv (f x)))
+ (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
+apply(rule bind_gpv.ctr)
+apply transfer_prover
+apply transfer_prover
+done
+
+end
\ No newline at end of file
--- a/src/HOL/Library/BNF_Corec.thy Mon Oct 24 16:53:32 2016 +0200
+++ b/src/HOL/Library/BNF_Corec.thy Mon Oct 24 16:53:32 2016 +0200
@@ -199,6 +199,8 @@
end
+named_theorems friend_of_corec_simps
+
ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML"
ML_file "../Tools/BNF/bnf_gfp_grec.ML"
ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML"
--- a/src/HOL/ROOT Mon Oct 24 16:53:32 2016 +0200
+++ b/src/HOL/ROOT Mon Oct 24 16:53:32 2016 +0200
@@ -804,6 +804,7 @@
Paper_Examples
Stream_Processor
"Tests/Simple_Nesting"
+ "Tests/Iterate_GPV"
theories [quick_and_dirty]
"Tests/GPV_Bare_Bones"
"Tests/Merge_D"
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Mon Oct 24 16:53:32 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Mon Oct 24 16:53:32 2016 +0200
@@ -118,7 +118,10 @@
val case_dtor' = unfold_thms ctxt shared_simps case_dtor;
val disc_sel_eq_cases' = map (mk_abs_def
o unfold_thms ctxt (case_dtor' :: ctr_defs @ shared_simps)) disc_sel_eq_cases;
- val const_pointful_naturals' = map (unfold_thms ctxt shared_simps) const_pointful_naturals;
+ val extra_naturals = Facts.retrieve (Context.Proof ctxt) (Proof_Context.facts_of ctxt)
+ ("friend_of_corec_simps", Position.none) |> #thms;
+ val const_pointful_naturals' = map (unfold_thms ctxt shared_simps)
+ (extra_naturals @ const_pointful_naturals);
val const_pointful_naturals_sym' = map (fn thm => thm RS sym) const_pointful_naturals';
val case_eq_ifs' = map mk_abs_def (@{thm sum.case_eq_if} :: case_eq_ifs);