--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:37:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:38:13 2014 +0200
@@ -1935,7 +1935,7 @@
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms,
+ xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_induct_thms,
xtor_co_rec_transfer_thms, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
@@ -2195,7 +2195,7 @@
let
val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) =
derive_rel_induct_thms_for_types lthy fpTs As Bs ctrss ctr_Tsss
- (map #exhaust ctr_sugars) rel_xtor_co_induct_thm ctr_defss ctor_injects
+ (map #exhaust ctr_sugars) xtor_rel_co_induct ctr_defss ctor_injects
pre_rel_defs abs_inverses live_nesting_rel_eqs;
in
((map single rel_induct_thms, single common_rel_induct_thm),
@@ -2299,7 +2299,7 @@
val ((rel_coinduct_thms, common_rel_coinduct_thm),
(rel_coinduct_attrs, common_rel_coinduct_attrs)) =
derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
- abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm
+ abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss xtor_rel_co_induct
live_nesting_rel_eqs;
in
((map single rel_coinduct_thms, single common_rel_coinduct_thm),
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:37:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:38:13 2014 +0200
@@ -164,7 +164,7 @@
val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
- val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
+ val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
|> map (unfold_thms lthy (id_apply :: rel_unfolds));
val rel_defs = map rel_def_of_bnf bnfs;
@@ -185,8 +185,8 @@
val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
- val rel_xtor_co_induct_thm =
- mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
+ val xtor_rel_co_induct =
+ mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
lthy;
@@ -208,7 +208,7 @@
fun mk_type_copy_thms thm = map (curry op RS thm)
@{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
in
- cterm_instantiate_pos cts rel_xtor_co_induct_thm
+ cterm_instantiate_pos cts xtor_rel_co_induct
|> singleton (Proof_Context.export names_lthy lthy)
|> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
fp_or_nesting_rel_eqs)
@@ -225,7 +225,7 @@
let
val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
in
- cterm_instantiate_pos cts rel_xtor_co_induct_thm
+ cterm_instantiate_pos cts xtor_rel_co_induct
|> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
fp_or_nesting_rel_eqs)
|> funpow (2 * n) (fn thm => thm RS spec)
@@ -476,7 +476,7 @@
xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
xtor_co_rec_thms = xtor_co_rec_thms,
xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
- rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
+ xtor_rel_co_induct = xtor_rel_co_induct,
dtor_set_induct_thms = [],
xtor_co_rec_transfer_thms = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:37:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:38:13 2014 +0200
@@ -26,7 +26,7 @@
xtor_rel_thms: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_maps: thm list,
- rel_xtor_co_induct_thm: thm,
+ xtor_rel_co_induct: thm,
dtor_set_induct_thms: thm list,
xtor_co_rec_transfer_thms: thm list}
@@ -176,7 +176,7 @@
val mk_sum_Cinfinite: thm list -> thm
val mk_sum_card_order: thm list -> thm
- val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
+ 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 ->
@@ -218,13 +218,13 @@
xtor_rel_thms: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_maps: thm list,
- rel_xtor_co_induct_thm: thm,
+ xtor_rel_co_induct: thm,
dtor_set_induct_thms: thm list,
xtor_co_rec_transfer_thms: thm list};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
- xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, rel_xtor_co_induct_thm,
+ xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
dtor_set_induct_thms, xtor_co_rec_transfer_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
@@ -241,7 +241,7 @@
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
- rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
+ xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,
dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
@@ -500,7 +500,7 @@
fun mk_sum_card_order [thm] = thm
| mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
-fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
+fun mk_xtor_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
let
val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:37:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:38:13 2014 +0200
@@ -1659,7 +1659,7 @@
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
fun mk_Jrel_DEADID_coinduct_thm () =
- mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
+ mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
Jzs Jz's dtors dtor's (fn {context = ctxt, prems} =>
(unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy;
@@ -2255,7 +2255,7 @@
end;
val Jrel_coinduct_thm =
- mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
+ mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
Jrel_coinduct_tac lthy;
val le_Jrel_OO_thm =
@@ -2541,7 +2541,7 @@
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
- xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
+ xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
dtor_set_induct_thms = dtor_Jset_induct_thms,
xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
in
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:37:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:38:13 2014 +0200
@@ -1766,7 +1766,7 @@
val Irels = if m = 0 then map HOLogic.eq_const Ts
else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
val Irel_induct_thm =
- mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
+ mk_xtor_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
(fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
ctor_Irel_thms rel_mono_strong0s) lthy;
@@ -1828,7 +1828,7 @@
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
- xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
+ xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm,
dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
in
timer; (fp_res, lthy')
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:37:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:38:13 2014 +0200
@@ -46,7 +46,7 @@
xtor_rel_thms = [xtor_rel],
xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
xtor_co_rec_o_maps = [ctor_rec_o_map],
- rel_xtor_co_induct_thm = xtor_rel_induct,
+ xtor_rel_co_induct = xtor_rel_induct,
dtor_set_induct_thms = [],
xtor_co_rec_transfer_thms = []};