--- a/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100
@@ -266,8 +266,13 @@
datatype_new 'a F = F0 | F 'a "'a F"
datatype_compat F
+datatype_new 'a T = T 'a "'a T F"
primrec f where
"f (F x y) = F x (f y)"
+primrec h and g where
+ "h (T x ts) = T x (g ts)" |
+ "g F0 = F0"
+
end
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100
@@ -1006,9 +1006,9 @@
(unsorted_As ~~ transpose set_boss);
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
- dtors = dtors0, xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors,
+ 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_iter_thmss, ...},
+ xtor_co_rec_thms, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
(map dest_TFree killed_As) fp_eqs no_defs_lthy0
@@ -1094,8 +1094,7 @@
val mss = map (map length) ctr_Tsss;
val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
- mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss (map co_rec_of xtor_co_iterss0)
- lthy;
+ mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
@@ -1314,9 +1313,9 @@
(recs, rec_defs)), lthy) =
let
val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, iter_attrs)) =
- derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
- (map co_rec_of xtor_co_iter_thmss) nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss
- abs_inverses type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
+ derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct xtor_co_rec_thms
+ nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
+ abs_inverses ctrss ctr_defss recs rec_defs lthy;
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
@@ -1359,8 +1358,8 @@
(disc_corec_iff_thmss, disc_corec_iff_attrs),
(sel_corec_thmsss, sel_corec_attrs)) =
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
- dtor_injects dtor_ctors (map co_rec_of xtor_co_iter_thmss) nesting_bnfs fpTs Cs Xs
- ctrXs_Tsss kss mss ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
+ dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
+ abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
(Proof_Context.export lthy' no_defs_lthy) lthy;
val sel_corec_thmss = map flat sel_corec_thmsss;
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 03 12:48:20 2014 +0100
@@ -236,7 +236,8 @@
|> mk_Frees' "s" fold_strTs
||>> mk_Frees' "s" rec_strTs;
- val co_iters = of_fp_res #xtor_co_iterss;
+ val co_folds = of_fp_res #xtor_co_folds;
+ val co_recs = of_fp_res #xtor_co_recs;
val ns = map (length o #Ts o #fp_res) fp_sugars;
fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
@@ -245,11 +246,11 @@
val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
- fun force_iter is_rec i TU TU_rec raw_iters =
+ fun force_iter is_rec i TU TU_rec raw_fold raw_rec =
let
val thy = Proof_Context.theory_of lthy;
- val approx_fold = un_fold_of raw_iters
+ val approx_fold = raw_fold
|> force_typ names_lthy
(replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
val subst = Term.typ_subst_atomic fold_thetaAs;
@@ -269,9 +270,8 @@
val js = find_indices Type.could_unify TUs cands;
val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
- val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
in
- force_typ names_lthy (Tpats ---> TU) iter
+ force_typ names_lthy (Tpats ---> TU) (if is_rec then raw_rec else raw_fold)
end;
fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
@@ -286,10 +286,11 @@
val i = find_index (fn T => x = T) Xs;
val TUiter =
(case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
- NONE => nth co_iters i
- |> force_iter is_rec i
+ NONE =>
+ force_iter is_rec i
(TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
- (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
+ (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
+ (nth co_folds i) (nth co_recs i)
| SOME f => f);
val TUs = binder_fun_types (fastype_of TUiter);
@@ -373,6 +374,9 @@
val un_folds = map (Morphism.term phi) raw_un_folds;
val co_recs = map (Morphism.term phi) raw_co_recs;
+ val fp_fold_o_maps = of_fp_res #xtor_co_fold_o_map_thms;
+ val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
+
val (xtor_un_fold_thms, xtor_co_rec_thms) =
let
val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
@@ -419,13 +423,9 @@
val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
- val fp_xtor_co_iterss = of_fp_res #xtor_co_iter_thmss;
- val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss;
- val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss;
+ val fp_xtor_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_co_fold_thms);
+ val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
- val fp_co_iter_o_mapss = of_fp_res #xtor_co_iter_o_map_thmss;
- val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss;
- val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss;
val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @
@{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
@@ -464,12 +464,8 @@
(* These results are half broken. This is deliberate. We care only about those fields that are
used by "primrec", "primcorecursive", and "datatype_compat". *)
val fp_res =
- ({Ts = fpTs,
- bnfs = of_fp_res #bnfs,
- dtors = dtors,
- ctors = ctors,
- xtor_co_iterss = transpose [un_folds, co_recs],
- xtor_co_induct = xtor_co_induct_thm,
+ ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors, xtor_co_folds = un_folds,
+ xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
ctor_injects = of_fp_res #ctor_injects (*too general types*),
@@ -477,9 +473,10 @@
xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
- xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
- xtor_co_iter_o_map_thmss = of_fp_res #xtor_co_iter_o_map_thmss
- (*theorem about old constant*),
+ xtor_co_fold_thms = xtor_un_fold_thms,
+ xtor_co_rec_thms = xtor_co_rec_thms,
+ xtor_co_fold_o_map_thms = fp_fold_o_maps (*theorems about old constants*),
+ xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100
@@ -223,8 +223,8 @@
val fp_absT_infos = map #absT_info fp_sugars0;
- val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
- dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
+ val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
+ dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
no_defs_lthy0;
@@ -240,10 +240,8 @@
val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
- val xtor_co_rec_thms = map co_rec_of xtor_co_iter_thmss;
val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
- mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss (map co_rec_of xtor_co_iterss0)
- lthy;
+ mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:20 2014 +0100
@@ -13,7 +13,8 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- xtor_co_iterss: term list list,
+ xtor_co_folds: term list,
+ xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
@@ -22,8 +23,10 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_co_iter_thmss: thm list list,
- xtor_co_iter_o_map_thmss: thm list list,
+ xtor_co_fold_thms: thm list,
+ xtor_co_rec_thms: thm list,
+ xtor_co_fold_o_map_thms: thm list,
+ xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm}
val morph_fp_result: morphism -> fp_result -> fp_result
@@ -193,7 +196,8 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- xtor_co_iterss: term list list,
+ xtor_co_folds: term list,
+ xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
@@ -202,18 +206,22 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_co_iter_thmss: thm list list,
- xtor_co_iter_o_map_thmss: thm list list,
+ xtor_co_fold_thms: thm list,
+ xtor_co_rec_thms: thm list,
+ xtor_co_fold_o_map_thms: thm list,
+ xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm};
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, dtor_ctors,
- ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_iter_thmss, xtor_co_iter_o_map_thmss, rel_xtor_co_induct_thm} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_folds, 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_fold_thms, xtor_co_rec_thms, xtor_co_fold_o_map_thms,
+ xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
{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_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss,
+ xtor_co_folds = map (Morphism.term phi) xtor_co_folds,
+ xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
xtor_co_induct = Morphism.thm phi xtor_co_induct,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
@@ -222,8 +230,10 @@
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_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss,
- xtor_co_iter_o_map_thmss = map (map (Morphism.thm phi)) xtor_co_iter_o_map_thmss,
+ xtor_co_fold_thms = map (Morphism.thm phi) xtor_co_fold_thms,
+ xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
+ xtor_co_fold_o_map_thms = map (Morphism.thm phi) xtor_co_fold_o_map_thms,
+ xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
fun un_fold_of [f, _] = f;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 03 12:48:20 2014 +0100
@@ -2600,16 +2600,13 @@
val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
in
timer;
- ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
- xtor_co_iterss = transpose [unfolds, corecs],
- xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
- ctor_dtors = ctor_dtor_thms,
- ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
+ ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_folds = unfolds,
+ xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
+ ctor_dtors = ctor_dtor_thms, 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_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
- xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_Jmap_thms, dtor_corec_o_Jmap_thms],
- rel_xtor_co_induct_thm = Jrel_coinduct_thm},
+ xtor_rel_thms = dtor_Jrel_thms, xtor_co_fold_thms = dtor_unfold_thms,
+ xtor_co_rec_thms = dtor_corec_thms, xtor_co_fold_o_map_thms = dtor_unfold_o_Jmap_thms,
+ xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm},
lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd)
end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 03 12:48:20 2014 +0100
@@ -1854,14 +1854,13 @@
val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
in
timer;
- ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
- xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
- ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
+ ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_folds = folds,
+ xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
+ ctor_dtors = ctor_dtor_thms, 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_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
- xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_Imap_thms, ctor_rec_o_Imap_thms],
- rel_xtor_co_induct_thm = Irel_induct_thm},
+ xtor_rel_thms = ctor_Irel_thms, xtor_co_fold_thms = ctor_fold_thms,
+ xtor_co_rec_thms = ctor_rec_thms, xtor_co_fold_o_map_thms = ctor_fold_o_Imap_thms,
+ xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm},
lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd)
end;