--- 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
--- 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 _ =
--- 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))))
--- 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,
--- 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