# 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 \ ('a, 'out, 'in) gpv) generat spmf") + +declare gpv.rel_eq [relator_eq] + +primcorec bind_gpv :: "('a, 'out, 'in) gpv \ ('a \ ('b, 'out, 'in) gpv) \ ('b, 'out, 'in) gpv" +where + "bind_gpv r f = GPV (map_spmf (map_generat id id (op \ (case_sum id (\r. bind_gpv r f)))) + (bind_spmf (the_gpv r) + (case_generat + (\x. map_spmf (map_generat id id (op \ Inl)) (the_gpv (f x))) + (\out c. return_spmf (IO out (\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 \ ('a \ ('a, 'out, 'in) gpv) \ ('a, 'out, 'in) gpv" +where "bind_gpv r f = GPV (map_spmf (map_generat id id (op \ (case_sum id (\r. bind_gpv r f)))) + (bind_spmf (the_gpv r) + (case_generat + (\x. map_spmf (map_generat id id (op \ Inl)) (the_gpv (f x))) + (\out c. return_spmf (IO out (\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);