--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 18:48:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 21:04:50 2013 +0200
@@ -909,9 +909,10 @@
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
- folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
- dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
- rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms, ...}, lthy)) =
+ un_folds = fp_folds0, co_recs = fp_recs0, co_induct = fp_induct,
+ strong_co_induct = fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects,
+ map_thms = fp_map_thms, set_thmss = fp_set_thmss, rel_thms = fp_rel_thms,
+ un_fold_thms = fp_fold_thms, co_rec_thms = fp_rec_thms, ...}, lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
no_defs_lthy0;
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 02 18:48:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 02 21:04:50 2013 +0200
@@ -13,18 +13,18 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- folds: term list,
- recs: term list,
- induct: thm,
- strong_induct: thm,
+ un_folds: term list,
+ co_recs: term list,
+ co_induct: thm,
+ strong_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
map_thms: thm list,
set_thmss: thm list list,
rel_thms: thm list,
- fold_thms: thm list,
- rec_thms: thm list}
+ un_fold_thms: thm list,
+ co_rec_thms: thm list}
val morph_fp_result: morphism -> fp_result -> fp_result
val eq_fp_result: fp_result * fp_result -> bool
@@ -183,37 +183,38 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- folds: term list,
- recs: term list,
- induct: thm,
- strong_induct: thm,
+ un_folds: term list,
+ co_recs: term list,
+ co_induct: thm,
+ strong_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
map_thms: thm list,
set_thmss: thm list list,
rel_thms: thm list,
- fold_thms: thm list,
- rec_thms: thm list};
+ un_fold_thms: thm list,
+ co_rec_thms: thm list};
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors,
- ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, un_folds, co_recs, co_induct, strong_co_induct,
+ dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, un_fold_thms,
+ co_rec_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
dtors = map (Morphism.term phi) dtors,
- folds = map (Morphism.term phi) folds,
- recs = map (Morphism.term phi) recs,
- induct = Morphism.thm phi induct,
- strong_induct = Morphism.thm phi strong_induct,
+ un_folds = map (Morphism.term phi) un_folds,
+ co_recs = map (Morphism.term phi) co_recs,
+ co_induct = Morphism.thm phi co_induct,
+ strong_co_induct = Morphism.thm phi strong_co_induct,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
ctor_injects = map (Morphism.thm phi) ctor_injects,
map_thms = map (Morphism.thm phi) map_thms,
set_thmss = map (map (Morphism.thm phi)) set_thmss,
rel_thms = map (Morphism.thm phi) rel_thms,
- fold_thms = map (Morphism.thm phi) fold_thms,
- rec_thms = map (Morphism.thm phi) rec_thms};
+ un_fold_thms = map (Morphism.thm phi) un_fold_thms,
+ co_rec_thms = map (Morphism.thm phi) co_rec_thms};
fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
eq_list eq_bnf (bnfs1, bnfs2);
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 18:48:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu May 02 21:04:50 2013 +0200
@@ -3027,12 +3027,12 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, folds = unfolds, recs = corecs,
- induct = dtor_coinduct_thm, strong_induct = dtor_strong_coinduct_thm,
+ ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, un_folds = unfolds, co_recs = corecs,
+ co_induct = dtor_coinduct_thm, strong_co_induct = dtor_strong_coinduct_thm,
dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss',
- rel_thms = dtor_Jrel_thms, fold_thms = ctor_dtor_unfold_thms,
- rec_thms = ctor_dtor_corec_thms},
+ rel_thms = dtor_Jrel_thms, un_fold_thms = ctor_dtor_unfold_thms,
+ co_rec_thms = ctor_dtor_corec_thms},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 02 18:48:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu May 02 21:04:50 2013 +0200
@@ -1850,11 +1850,11 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, folds = folds, recs = recs,
- induct = ctor_induct_thm, strong_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
+ ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, un_folds = folds, co_recs = recs,
+ co_induct = ctor_induct_thm, strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms,
- set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, fold_thms = ctor_fold_thms,
- rec_thms = ctor_rec_thms},
+ set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, un_fold_thms = ctor_fold_thms,
+ co_rec_thms = ctor_rec_thms},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;