--- 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;
--- 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)
--- 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)