# HG changeset patch # User blanchet # Date 1427386224 -3600 # Node ID dbec7f33093d49a0e23b5f6e54825be1d5c76a0a # Parent 41f0804b7309115ae866650ecff7bd293a2fdc6e store low-level (un)fold constants diff -r 41f0804b7309 -r dbec7f33093d src/HOL/Basic_BNF_LFPs.thy --- 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\nat) = n" - by (induct n) simp_all +lemmas size_nat = size_nat_def hide_const (open) xtor ctor_rec diff -r 41f0804b7309 -r dbec7f33093d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 41f0804b7309 -r dbec7f33093d src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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) diff -r 41f0804b7309 -r dbec7f33093d src/HOL/Tools/BNF/bnf_fp_util.ML --- 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, diff -r 41f0804b7309 -r dbec7f33093d src/HOL/Tools/BNF/bnf_gfp.ML --- 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') diff -r 41f0804b7309 -r dbec7f33093d src/HOL/Tools/BNF/bnf_lfp.ML --- 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; diff -r 41f0804b7309 -r dbec7f33093d src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- 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