# HG changeset patch # User blanchet # Date 1406154240 -7200 # Node ID 4ff8c090d5809967b2a219200d9881003da64782 # Parent 231e90cf2892586ed131bffa76ad62067b4b2634 repaired named derivations diff -r 231e90cf2892 -r 4ff8c090d580 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jul 24 00:24:00 2014 +0200 @@ -163,7 +163,7 @@ co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk, sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk} - |> morph_fp_sugar (substitute_noted_thm noted)) Ts + |> morph_fp_sugar (substitute_noted_thm noted)) Ts; in register_fp_sugars fp_sugars end; @@ -601,11 +601,7 @@ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses abs_inverses fp_nesting_set_maps pre_set_defss) - |> singleton (Proof_Context.export names_lthy lthy) - (* for "datatype_realizer.ML": *) - |> Thm.name_derivation (fst (dest_Type (hd fpTs)) ^ Long_Name.separator ^ - (if nn > 1 then space_implode "_" (tl fp_b_names) ^ Long_Name.separator else "") ^ - inductN); + |> singleton (Proof_Context.export names_lthy lthy); in `(conj_dests nn) thm end; @@ -1702,7 +1698,8 @@ (if nn > 1 then [(inductN, [induct_thm], induct_attrs), (rel_inductN, common_rel_induct_thms, common_rel_induct_attrs)] - else []) + else + []) |> massage_simple_notes fp_common_name; val notes = @@ -1715,6 +1712,9 @@ lthy |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss) |> Local_Theory.notes (common_notes @ notes) + (* for "datatype_realizer.ML": *) + |>> name_noted_thms + (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN |-> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss diff -r 231e90cf2892 -r 4ff8c090d580 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Jul 24 00:24:00 2014 +0200 @@ -163,7 +163,8 @@ in lthy |> Local_Theory.raw_theory register_interpret - |> Local_Theory.notes all_notes |> snd + |> Local_Theory.notes all_notes + |> snd end; val _ = diff -r 231e90cf2892 -r 4ff8c090d580 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Jul 24 00:24:00 2014 +0200 @@ -481,8 +481,8 @@ mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps def_thms rec_thm |> K |> Goal.prove_sorry lthy' [] [] user_eqn + |> singleton (Proof_Context.export lthy' lthy) (* for code extraction from proof terms: *) - |> singleton (Proof_Context.export lthy' lthy) |> Thm.name_derivation (Sign.full_name thy (Binding.name fun_name) ^ Long_Name.separator ^ simpsN ^ (if js = [0] then "" else "_" ^ string_of_int (j + 1)))) diff -r 231e90cf2892 -r 4ff8c090d580 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Jul 24 00:24:00 2014 +0200 @@ -629,14 +629,9 @@ val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss; - fun after_qed thmss lthy = + fun after_qed ([exhaust_thm] :: thmss) lthy = let - val ([exhaust_thm0], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss)); - (* for "datatype_realizer.ML": *) - val exhaust_thm = - Thm.name_derivation (fcT_name ^ Long_Name.separator ^ exhaustN) exhaust_thm0; - - val inject_thms = flat inject_thmss; + val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat; val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As); @@ -1011,7 +1006,9 @@ (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms) (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms)) I) - |> Local_Theory.notes (anonymous_notes @ notes); + |> Local_Theory.notes (anonymous_notes @ notes) + (* for "datatype_realizer.ML": *) + |>> name_noted_thms fcT_name exhaustN; val ctr_sugar = {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm, diff -r 231e90cf2892 -r 4ff8c090d580 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Jul 24 00:24:00 2014 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Thu Jul 24 00:24:00 2014 +0200 @@ -68,6 +68,7 @@ val certifyT: Proof.context -> typ -> ctyp val certify: Proof.context -> term -> cterm + val name_noted_thms: string -> string -> (string * thm list) list -> (string * thm list) list val substitute_noted_thm: (string * thm list) list -> morphism val standard_binding: binding @@ -233,14 +234,23 @@ fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) -fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); -fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); +val certifyT = Thm.ctyp_of o Proof_Context.theory_of; +val certify = Thm.cterm_of o Proof_Context.theory_of; + +fun name_noted_thms _ _ [] = [] + | name_noted_thms qualifier base ((local_name, thms) :: noted) = + if Long_Name.base_name local_name = base then + (local_name, + map_index (uncurry (fn j => Thm.name_derivation (qualifier ^ Long_Name.separator ^ base ^ + (if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted + else + ((local_name, thms) :: name_noted_thms qualifier base noted); fun substitute_noted_thm noted = let val tab = fold (fold (Termtab.default o `Thm.full_prop_of) o snd) noted Termtab.empty in Morphism.thm_morphism "Ctr_Sugar_Util.substitute_noted_thm" (perhaps (Termtab.lookup tab o Thm.full_prop_of) o Drule.zero_var_indexes) - end + end; (* The standard binding stands for a name generated following the canonical convention (e.g., "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no