additional user-specified simp (naturality) rules used in friend_of_corec
authortraytel
Mon Oct 24 16:53:32 2016 +0200 (2016-10-24)
changeset 6437971f42dcaa1df
parent 64378 e9eb0b99a44c
child 64380 4b22e1268779
additional user-specified simp (naturality) rules used in friend_of_corec
src/HOL/Corec_Examples/Tests/Iterate_GPV.thy
src/HOL/Library/BNF_Corec.thy
src/HOL/ROOT
src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Corec_Examples/Tests/Iterate_GPV.thy	Mon Oct 24 16:53:32 2016 +0200
     1.3 @@ -0,0 +1,57 @@
     1.4 +theory Iterate_GPV imports
     1.5 +  "~~/src/HOL/Library/BNF_Axiomatization"
     1.6 +  "~~/src/HOL/Library/BNF_Corec"
     1.7 +begin
     1.8 +
     1.9 +declare [[typedef_overloaded]]
    1.10 +
    1.11 +datatype 'a spmf = return_spmf 'a
    1.12 +
    1.13 +primrec (transfer) bind_spmf where
    1.14 +  "bind_spmf (return_spmf a) f = f a"
    1.15 +
    1.16 +datatype (generat_pures: 'a, generat_outs: 'b, generat_conts: 'c) generat
    1.17 +  = Pure (result: 'a)
    1.18 +  | IO ("output": 'b) (continuation: "'c")
    1.19 +
    1.20 +codatatype (results'_gpv: 'a, outs'_gpv: 'out, 'in) gpv
    1.21 +  = GPV (the_gpv: "('a, 'out, 'in \<Rightarrow> ('a, 'out, 'in) gpv) generat spmf")
    1.22 +
    1.23 +declare gpv.rel_eq [relator_eq]
    1.24 +
    1.25 +primcorec bind_gpv :: "('a, 'out, 'in) gpv \<Rightarrow> ('a \<Rightarrow> ('b, 'out, 'in) gpv) \<Rightarrow> ('b, 'out, 'in) gpv"
    1.26 +where
    1.27 +  "bind_gpv r f = GPV (map_spmf (map_generat id id (op \<circ> (case_sum id (\<lambda>r. bind_gpv r f))))
    1.28 +     (bind_spmf (the_gpv r)
    1.29 +      (case_generat
    1.30 +        (\<lambda>x. map_spmf (map_generat id id (op \<circ> Inl)) (the_gpv (f x)))
    1.31 +        (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
    1.32 +
    1.33 +context includes lifting_syntax begin
    1.34 +
    1.35 +lemma bind_gpv_parametric [transfer_rule]:
    1.36 +  "(rel_gpv A C ===> (A ===> rel_gpv B C) ===> rel_gpv B C) bind_gpv bind_gpv"
    1.37 +unfolding bind_gpv_def by transfer_prover
    1.38 +
    1.39 +end
    1.40 +
    1.41 +lemma [friend_of_corec_simps]:
    1.42 +  "map_spmf f (bind_spmf x h) = bind_spmf x (map_spmf f o h)"
    1.43 +  by (cases x) auto
    1.44 +
    1.45 +lemma [friend_of_corec_simps]:
    1.46 +  "bind_spmf (map_spmf f x) h = bind_spmf x (h o f)"
    1.47 +  by (cases x) auto
    1.48 +
    1.49 +friend_of_corec bind_gpv :: "('a, 'out, 'in) gpv \<Rightarrow> ('a \<Rightarrow> ('a, 'out, 'in) gpv) \<Rightarrow> ('a, 'out, 'in) gpv"
    1.50 +where "bind_gpv r f = GPV (map_spmf (map_generat id id (op \<circ> (case_sum id (\<lambda>r. bind_gpv r f))))
    1.51 +     (bind_spmf (the_gpv r)
    1.52 +      (case_generat
    1.53 +        (\<lambda>x. map_spmf (map_generat id id (op \<circ> Inl)) (the_gpv (f x)))
    1.54 +        (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))))))"
    1.55 +apply(rule bind_gpv.ctr)
    1.56 +apply transfer_prover
    1.57 +apply transfer_prover
    1.58 +done
    1.59 +
    1.60 +end
    1.61 \ No newline at end of file
     2.1 --- a/src/HOL/Library/BNF_Corec.thy	Mon Oct 24 16:53:32 2016 +0200
     2.2 +++ b/src/HOL/Library/BNF_Corec.thy	Mon Oct 24 16:53:32 2016 +0200
     2.3 @@ -199,6 +199,8 @@
     2.4  
     2.5  end
     2.6  
     2.7 +named_theorems friend_of_corec_simps
     2.8 +
     2.9  ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML"
    2.10  ML_file "../Tools/BNF/bnf_gfp_grec.ML"
    2.11  ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML"
     3.1 --- a/src/HOL/ROOT	Mon Oct 24 16:53:32 2016 +0200
     3.2 +++ b/src/HOL/ROOT	Mon Oct 24 16:53:32 2016 +0200
     3.3 @@ -804,6 +804,7 @@
     3.4      Paper_Examples
     3.5      Stream_Processor
     3.6      "Tests/Simple_Nesting"
     3.7 +    "Tests/Iterate_GPV"
     3.8    theories [quick_and_dirty]
     3.9      "Tests/GPV_Bare_Bones"
    3.10      "Tests/Merge_D"
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Mon Oct 24 16:53:32 2016 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Mon Oct 24 16:53:32 2016 +0200
     4.3 @@ -118,7 +118,10 @@
     4.4      val case_dtor' = unfold_thms ctxt shared_simps case_dtor;
     4.5      val disc_sel_eq_cases' = map (mk_abs_def
     4.6        o unfold_thms ctxt (case_dtor' :: ctr_defs @ shared_simps)) disc_sel_eq_cases;
     4.7 -    val const_pointful_naturals' = map (unfold_thms ctxt shared_simps) const_pointful_naturals;
     4.8 +    val extra_naturals = Facts.retrieve (Context.Proof ctxt) (Proof_Context.facts_of ctxt)
     4.9 +      ("friend_of_corec_simps", Position.none) |> #thms;
    4.10 +    val const_pointful_naturals' = map (unfold_thms ctxt shared_simps)
    4.11 +      (extra_naturals @ const_pointful_naturals);
    4.12      val const_pointful_naturals_sym' = map (fn thm => thm RS sym) const_pointful_naturals';
    4.13      val case_eq_ifs' = map mk_abs_def (@{thm sum.case_eq_if} :: case_eq_ifs);
    4.14