--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 22:01:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 08:48:59 2013 +0200
@@ -818,6 +818,7 @@
(Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
mk_Trueprop_eq (fcoiter $ c, Term.list_comb (ctr, take m cfs'))));
+ (* TODO: get rid of "mk_U" *)
val mk_U = typ_subst_nonatomic (map2 pair Cs fpTs);
fun intr_coiters fcoiters [] [cf] =
@@ -1049,9 +1050,9 @@
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts;
val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
- xtor_un_folds = xtor_un_folds0, xtor_co_recs = xtor_co_recs0, xtor_co_induct,
- xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms,
- xtor_set_thmss, xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms, ...}, lthy)) =
+ xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, xtor_strong_co_induct, dtor_ctors,
+ ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
+ xtor_co_iter_thmss, ...}, lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
no_defs_lthy0;
@@ -1098,14 +1099,13 @@
val kss = map (fn n => 1 upto n) ns;
val mss = map (map length) ctr_Tsss;
- val (([xtor_un_folds, xtor_co_recs], fold_rec_args_types, unfold_corec_args_types), lthy) =
- mk_un_fold_co_rec_prelims fp fpTs Cs ns mss [xtor_un_folds0, xtor_co_recs0] lthy;
+ val ((xtor_co_iterss', fold_rec_args_types, unfold_corec_args_types), lthy) =
+ mk_un_fold_co_rec_prelims fp fpTs Cs ns mss (transpose xtor_co_iterss0) lthy;
- fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
- xtor_un_fold), xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def),
- pre_set_defs), pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms),
- ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss)
- no_defs_lthy =
+ fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
+ xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
+ pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings),
+ ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
let
val fp_b_name = Binding.name_of fp_b;
@@ -1295,7 +1295,7 @@
##>>
(if fp = Least_FP then define_iters [foldN, recN] (the fold_rec_args_types)
else define_coiters [unfoldN, corecN] (the unfold_corec_args_types))
- mk_binding fpTs Cs [xtor_un_fold, xtor_co_rec]
+ mk_binding fpTs Cs xtor_co_iters
#> massage_res, lthy')
end;
@@ -1316,9 +1316,9 @@
let
val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
(rec_thmss, rec_attrs)) =
- derive_induct_fold_rec_thms_for_types pre_bnfs [xtor_un_folds, xtor_co_recs]
- (the fold_rec_args_types) xtor_co_induct [xtor_un_fold_thms, xtor_co_rec_thms]
- nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy;
+ derive_induct_fold_rec_thms_for_types pre_bnfs xtor_co_iterss'
+ (the fold_rec_args_types) xtor_co_induct (transpose xtor_co_iter_thmss) nesting_bnfs
+ nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy;
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
@@ -1353,10 +1353,9 @@
(disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
(disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
(sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
- derive_coinduct_unfold_corec_thms_for_types pre_bnfs [xtor_un_folds, xtor_co_recs]
- xtor_co_induct xtor_strong_co_induct dtor_ctors [xtor_un_fold_thms, xtor_co_rec_thms]
- nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss'
- coiter_defss' lthy;
+ derive_coinduct_unfold_corec_thms_for_types pre_bnfs xtor_co_iterss' xtor_co_induct
+ xtor_strong_co_induct dtor_ctors (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs
+ fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss' coiter_defss' lthy;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
@@ -1404,7 +1403,7 @@
val lthy' = lthy
|> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~
- xtor_un_folds ~~ xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
+ (transpose xtor_co_iterss') ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~
kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~
sel_bindingsss ~~ raw_sel_defaultsss)
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jun 06 22:01:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Jun 07 08:48:59 2013 +0200
@@ -15,8 +15,7 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- xtor_un_folds: term list,
- xtor_co_recs: term list,
+ xtor_co_iterss: term list list,
xtor_co_induct: thm,
xtor_strong_co_induct: thm,
dtor_ctors: thm list,
@@ -25,8 +24,7 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_un_fold_thms: thm list,
- xtor_co_rec_thms: thm list}
+ xtor_co_iter_thmss: thm list list}
val morph_fp_result: morphism -> fp_result -> fp_result
val eq_fp_result: fp_result * fp_result -> bool
@@ -185,8 +183,7 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- xtor_un_folds: term list,
- xtor_co_recs: term list,
+ xtor_co_iterss: term list list,
xtor_co_induct: thm,
xtor_strong_co_induct: thm,
dtor_ctors: thm list,
@@ -195,18 +192,16 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_un_fold_thms: thm list,
- xtor_co_rec_thms: thm list};
+ xtor_co_iter_thmss: thm list list};
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct,
xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss,
- xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms} =
+ xtor_rel_thms, xtor_co_iter_thmss} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
dtors = map (Morphism.term phi) dtors,
- xtor_un_folds = map (Morphism.term phi) xtor_un_folds,
- xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
+ xtor_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss,
xtor_co_induct = Morphism.thm phi xtor_co_induct,
xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
@@ -215,8 +210,7 @@
xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
- xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
- xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms};
+ xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss};
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 Jun 06 22:01:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Jun 07 08:48:59 2013 +0200
@@ -3107,13 +3107,13 @@
bs thmss)
in
timer;
- ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds,
- xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm,
+ ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
+ xtor_co_iterss = transpose [unfolds, corecs], xtor_co_induct = dtor_coinduct_thm,
xtor_strong_co_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
- xtor_rel_thms = dtor_Jrel_thms, xtor_un_fold_thms = ctor_dtor_unfold_thms,
- xtor_co_rec_thms = ctor_dtor_corec_thms},
+ xtor_rel_thms = dtor_Jrel_thms,
+ xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms]},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 22:01:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Jun 07 08:48:59 2013 +0200
@@ -1856,13 +1856,13 @@
bs thmss)
in
timer;
- ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds,
- xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm,
+ ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
+ xtor_co_induct = ctor_induct_thm,
xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss',
- xtor_rel_thms = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms,
- xtor_co_rec_thms = ctor_rec_thms},
+ xtor_rel_thms = ctor_Irel_thms,
+ xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms]},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;