# HG changeset patch
# User traytel
# Date 1477320812 -7200
# Node ID 71f42dcaa1df2f3732d339a81d3c94d746c21ca3
# Parent  e9eb0b99a44cb9a3935b627cebb14d28f4321f0a
additional user-specified simp (naturality) rules used in friend_of_corec

diff -r e9eb0b99a44c -r 71f42dcaa1df src/HOL/Corec_Examples/Tests/Iterate_GPV.thy
--- /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
diff -r e9eb0b99a44c -r 71f42dcaa1df src/HOL/Library/BNF_Corec.thy
--- 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"
diff -r e9eb0b99a44c -r 71f42dcaa1df src/HOL/ROOT
--- 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"
diff -r e9eb0b99a44c -r 71f42dcaa1df src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
--- 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);