# HG changeset patch # User blanchet # Date 1393847300 -3600 # Node ID 37b99986d435eafbf87edf8a29bdf5a17f442efd # Parent 79b915f265339df251463eb7eb32f17263f72dda rationalized internals diff -r 79b915f26533 -r 37b99986d435 src/HOL/BNF_LFP.thy --- 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 diff -r 79b915f26533 -r 37b99986d435 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 79b915f26533 -r 37b99986d435 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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 diff -r 79b915f26533 -r 37b99986d435 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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; diff -r 79b915f26533 -r 37b99986d435 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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; diff -r 79b915f26533 -r 37b99986d435 src/HOL/Tools/BNF/bnf_gfp.ML --- 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; diff -r 79b915f26533 -r 37b99986d435 src/HOL/Tools/BNF/bnf_lfp.ML --- 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;