# HG changeset patch # User traytel # Date 1459671917 -7200 # Node ID 609f97d79bc282c710c071df90c650eff59857d0 # Parent eb94e570c1a45d43a2d691631d70b4137c918f5f tuned names diff -r eb94e570c1a4 -r 609f97d79bc2 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sat Apr 02 23:29:05 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Apr 03 10:25:17 2016 +0200 @@ -191,10 +191,10 @@ val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm - val mk_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list -> + val mk_xtor_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list - val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list -> + val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list val fixpoint_bnf: (binding -> binding) -> @@ -560,7 +560,7 @@ |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]})) end; -fun mk_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy = +fun mk_xtor_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy = let val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels; val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; @@ -579,7 +579,7 @@ |> split_conj_thm end; -fun mk_xtor_un_fold_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps +fun mk_xtor_co_iter_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps map_cong0s = let val n = length sym_map_comps; diff -r eb94e570c1a4 -r 609f97d79bc2 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Sat Apr 02 23:29:05 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Sun Apr 03 10:25:17 2016 +0200 @@ -2630,10 +2630,10 @@ |> mk_Frees "R" JphiTs ||>> mk_Frees "S" activephiTs; - val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m + val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) sym_map_comps map_cong0s; - val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m + val dtor_corec_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP true m dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms) sym_map_comps map_cong0s; @@ -2642,7 +2642,7 @@ else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs; val dtor_unfold_transfer_thms = - mk_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis + mk_xtor_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs) dtor_unfold_thms) @@ -2654,7 +2654,7 @@ val corec_activephis = map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis; val dtor_corec_transfer_thms = - mk_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis + mk_xtor_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs) (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms) diff -r eb94e570c1a4 -r 609f97d79bc2 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Sat Apr 02 23:29:05 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sun Apr 03 10:25:17 2016 +0200 @@ -1886,9 +1886,9 @@ ||>> mk_Frees "S" activephiTs ||>> mk_Frees "IR" activeIphiTs; - val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm + val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; - val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm + val ctor_rec_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP true m ctor_rec_unique_thm ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s; val Irels = if m = 0 then map HOLogic.eq_const Ts @@ -1900,7 +1900,7 @@ val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; val ctor_fold_transfer_thms = - mk_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis + mk_xtor_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs) (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms) @@ -1912,7 +1912,7 @@ val rec_activephis = map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis; val ctor_rec_transfer_thms = - mk_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis + mk_xtor_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs) (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms)