--- a/src/HOL/Basic_BNF_LFPs.thy Thu Mar 26 16:42:42 2015 +0100
+++ b/src/HOL/Basic_BNF_LFPs.thy Thu Mar 26 17:10:24 2015 +0100
@@ -99,8 +99,7 @@
declare prod.size[no_atp]
-lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
- by (induct n) simp_all
+lemmas size_nat = size_nat_def
hide_const (open) xtor ctor_rec
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Mar 26 16:42:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Mar 26 17:10:24 2015 +0100
@@ -553,7 +553,7 @@
b_names Ts thmss)
#> filter_out (null o fst o hd o snd);
-fun derive_map_set_rel_thms plugins fp n live As Bs abs_inverses ctr_defs' fp_nesting_set_maps
+fun derive_map_set_rel_thms plugins fp live As Bs abs_inverses ctr_defs' fp_nesting_set_maps
live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs fp_b_name fp_bnf fpT ctor
ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm
ctr_Tss abs
@@ -2093,11 +2093,11 @@
val ((xtor_co_recs, recs_args_types, corecs_args_types), 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 (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
+ fun define_ctrs_dtrs_for_type fp ((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
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), abs),
- abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss),
- disc_bindings), sel_bindingss), raw_sel_default_eqs) no_defs_lthy =
+ abs_inject), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings),
+ sel_bindingss), raw_sel_default_eqs) no_defs_lthy =
let
val fp_b_name = Binding.name_of fp_b;
@@ -2197,7 +2197,7 @@
in
(wrap_ctrs
#> (fn (ctr_sugar, lthy) =>
- derive_map_set_rel_thms plugins fp n live As Bs abs_inverses ctr_defs'
+ derive_map_set_rel_thms plugins fp live As Bs abs_inverses ctr_defs'
fp_nesting_set_maps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs
fp_b_name fp_bnf fpT ctor ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def
fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs ctr_sugar lthy
@@ -2257,8 +2257,7 @@
val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
- val rec_Ts as rec_T1 :: _ = map fastype_of recs;
- val rec_arg_Ts = binder_fun_types rec_T1;
+ val rec_arg_Ts = binder_fun_types (hd (map fastype_of recs));
val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
@@ -2409,8 +2408,7 @@
val fmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_fs)) maps0;
- val corec_Ts as corec_T1 :: _ = map fastype_of corecs;
- val corec_arg_Ts = binder_fun_types corec_T1;
+ val corec_arg_Ts = binder_fun_types (hd (map fastype_of corecs));
val B_ify = Term.subst_atomic_types (As ~~ Bs);
val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
@@ -2566,8 +2564,8 @@
|> fold_map (define_ctrs_dtrs_for_type fp) (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rels ~~ ns ~~ kss ~~ mss ~~
- abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
- ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss)
+ abss ~~ abs_injects ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~
+ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss)
|> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types
|> case_fp fp derive_note_induct_recs_thms_for_types
derive_note_coinduct_corecs_thms_for_types;
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 26 16:42:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 26 17:10:24 2015 +0100
@@ -478,7 +478,8 @@
used by "primrec", "primcorecursive", and "datatype_compat". *)
val fp_res =
({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors,
- xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
+ xtor_un_folds = co_recs (*wrong*), 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*),
@@ -486,11 +487,9 @@
xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
- xtor_co_rec_thms = xtor_co_rec_thms,
+ xtor_un_fold_thms = xtor_co_rec_thms (*wrong*), xtor_co_rec_thms = xtor_co_rec_thms,
xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
- xtor_rel_co_induct = xtor_rel_co_induct,
- dtor_set_inducts = [],
- xtor_co_rec_transfers = []}
+ xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = [], xtor_co_rec_transfers = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
(fp_res, lthy)
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 26 16:42:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 26 17:10:24 2015 +0100
@@ -15,6 +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_induct: thm,
dtor_ctors: thm list,
@@ -24,6 +25,7 @@
xtor_maps: thm list,
xtor_setss: thm list list,
xtor_rels: thm list,
+ xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_maps: thm list,
xtor_rel_co_induct: thm,
@@ -208,6 +210,7 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
+ xtor_un_folds: term list,
xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
@@ -217,20 +220,22 @@
xtor_maps: thm list,
xtor_setss: thm list list,
xtor_rels: thm list,
+ xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_maps: thm list,
xtor_rel_co_induct: thm,
dtor_set_inducts: thm list,
xtor_co_rec_transfers: 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_maps, xtor_setss,
- xtor_rels, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
- dtor_set_inducts, xtor_co_rec_transfers} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
+ dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
+ xtor_un_fold_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct, dtor_set_inducts,
+ xtor_co_rec_transfers} =
{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_induct = Morphism.thm phi xtor_co_induct,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
@@ -240,6 +245,7 @@
xtor_maps = map (Morphism.thm phi) xtor_maps,
xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
xtor_rels = map (Morphism.thm phi) xtor_rels,
+ 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_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Mar 26 16:42:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Mar 26 17:10:24 2015 +0100
@@ -2538,13 +2538,13 @@
val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes);
val fp_res =
- {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, 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_maps = dtor_Jmap_thms, xtor_setss = dtor_Jset_thmss',
- xtor_rels = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
- xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
- dtor_set_inducts = dtor_Jset_induct_thms,
+ {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_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_maps = dtor_Jmap_thms, xtor_setss = dtor_Jset_thmss',
+ xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms = dtor_unfold_thms,
+ xtor_co_rec_thms = dtor_corec_thms, xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms,
+ xtor_rel_co_induct = Jrel_coinduct_thm, dtor_set_inducts = dtor_Jset_induct_thms,
xtor_co_rec_transfers = dtor_corec_transfer_thms};
in
timer; (fp_res, lthy')
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Mar 26 16:42:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Mar 26 17:10:24 2015 +0100
@@ -1826,13 +1826,14 @@
val lthy' = lthy |> note_all ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes);
val fp_res =
- {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, 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_maps = ctor_Imap_thms, xtor_setss = ctor_Iset_thmss',
- xtor_rels = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
- xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm,
- dtor_set_inducts = [], xtor_co_rec_transfers = ctor_rec_transfer_thms};
+ {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_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_maps = ctor_Imap_thms, xtor_setss = ctor_Iset_thmss',
+ xtor_rels = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms,
+ xtor_co_rec_thms = ctor_rec_thms, xtor_co_rec_o_maps = ctor_rec_o_Imap_thms,
+ xtor_rel_co_induct = Irel_induct_thm, dtor_set_inducts = [],
+ xtor_co_rec_transfers = ctor_rec_transfer_thms};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Mar 26 16:42:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Mar 26 17:10:24 2015 +0100
@@ -17,9 +17,7 @@
open BNF_FP_Def_Sugar
fun trivial_absT_info_of fpT =
- {absT = fpT,
- repT = fpT,
- abs = Const (@{const_name id_bnf}, fpT --> fpT),
+ {absT = fpT, repT = fpT, abs = Const (@{const_name id_bnf}, fpT --> fpT),
rep = Const (@{const_name id_bnf}, fpT --> fpT),
abs_inject = @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV UNIV_I UNIV_I]},
abs_inverse = @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV UNIV_I]},
@@ -31,24 +29,19 @@
$> Morphism.term_morphism "BNF" (Term.map_types Logic.unvarifyT_global));
fun trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct =
- {Ts = [fpT],
- bnfs = [fp_bnf],
- ctors = [Const (@{const_name xtor}, fpT --> fpT)],
- dtors = [Const (@{const_name xtor}, fpT --> fpT)],
- xtor_co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))],
- xtor_co_induct = @{thm xtor_induct},
- dtor_ctors = @{thms xtor_xtor},
- ctor_dtors = @{thms xtor_xtor},
- ctor_injects = @{thms xtor_inject},
- dtor_injects = @{thms xtor_inject},
- xtor_maps = [xtor_map],
- xtor_setss = [xtor_sets],
- xtor_rels = [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],
- xtor_rel_co_induct = xtor_rel_induct,
- dtor_set_inducts = [],
- xtor_co_rec_transfers = []};
+ let
+ val xtors = [Const (@{const_name xtor}, fpT --> fpT)];
+ val co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))];
+ val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}];
+ in
+ {Ts = [fpT], bnfs = [fp_bnf], ctors = xtors, dtors = xtors, xtor_un_folds = co_recs,
+ xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor},
+ ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject},
+ dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], xtor_setss = [xtor_sets],
+ xtor_rels = [xtor_rel], xtor_un_fold_thms = co_rec_thms, xtor_co_rec_thms = co_rec_thms,
+ xtor_co_rec_o_maps = [ctor_rec_o_map], xtor_rel_co_induct = xtor_rel_induct,
+ dtor_set_inducts = [], xtor_co_rec_transfers = []}
+ end;
fun fp_sugar_of_sum ctxt =
let