--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Jun 09 15:31:33 2024 +0200
@@ -235,7 +235,7 @@
val forbidden_consts = [\<^const_name>\<open>Pure.type\<close>]
-fun is_forbidden_theorem (s, th) =
+fun is_forbidden_theorem ((s, _): Thm_Name.T, th) =
let val consts = Term.add_const_names (Thm.prop_of th) [] in
exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
exists (member (op =) forbidden_consts) consts orelse
@@ -421,13 +421,13 @@
^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"
(*^ "\n" ^ string_of_reports reports*)
in
- "mutant of " ^ thm_name ^ ":\n" ^
+ "mutant of " ^ Thm_Name.short thm_name ^ ":\n" ^
YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^
space_implode "; " (map string_of_mtd_result results)
end
fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
- thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
+ Thm_Name.short thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ": " ^
Syntax.string_of_term_global thy t ^ "\n" ^
cat_lines (map (string_of_mutant_subentry' thy thm_name) mutant_subentries) ^ "\n"
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Sun Jun 09 15:31:33 2024 +0200
@@ -151,7 +151,7 @@
String.isSuffix "_raw" name
fun theorems_of thy =
- filter (fn (name, th) =>
+ filter (fn ((name, _), th) =>
not (is_forbidden_theorem name) andalso
Thm.theory_long_name th = Context.theory_long_name thy)
(Global_Theory.all_thms_of thy true)
@@ -186,7 +186,7 @@
val (nondef_ts, def_ts, _, _, _, _) =
Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
neg_t
- val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
+ val res = Thm_Name.print name ^ ": " ^ check_formulas (nondef_ts, def_ts)
in File.append path (res ^ "\n"); writeln res end
handle Timeout.TIMEOUT _ => ()
in thy |> theorems_of |> List.app check_theorem end
--- a/src/HOL/TPTP/atp_theory_export.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Sun Jun 09 15:31:33 2024 +0200
@@ -164,19 +164,19 @@
val problem =
facts
|> map (fn ((_, loc), th) =>
- ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
+ ((Thm_Name.short (Thm.get_name_hint th), loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
|> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true []
\<^prop>\<open>False\<close>
|> #1 |> sort_by (heading_sort_key o fst)
val prelude = fst (split_last problem)
- val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
+ val name_tabs = Sledgehammer_Fact.build_name_tables (Thm_Name.short o Thm.get_name_hint) facts
val infers =
if infer_policy = No_Inferences then
[]
else
facts
|> map (fn (_, th) =>
- (fact_name_of (Thm.get_name_hint th),
+ (fact_name_of (Thm_Name.short (Thm.get_name_hint th)),
th |> Sledgehammer_Util.thms_in_proof max_dependencies (SOME name_tabs)
|> these |> map fact_name_of))
val all_problem_names =
@@ -295,7 +295,7 @@
#> chop_maximal_groups (op = o apply2 theory_name_of_fact)
#> map (`(include_base_name_of_fact o hd)))
- val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm.get_name_hint th, fact)) facts)
+ val fact_tab = Symtab.make (map (fn fact as (_, th) => (Thm_Name.short (Thm.get_name_hint th), fact)) facts)
fun write_prelude () =
let val ss = lines_of_atp_problem format (K []) prelude in
@@ -318,7 +318,7 @@
val mepo = Sledgehammer_MePo.mepo_suggested_facts ctxt
(Sledgehammer_Commands.default_params thy []) max_facts NONE hyp_ts conj_t facts
in
- map (suffix "\n" o fact_name_of o Thm.get_name_hint o snd) mepo
+ map (suffix "\n" o fact_name_of o Thm_Name.short o Thm.get_name_hint o snd) mepo
end
fun write_problem_files _ _ _ _ [] = ()
--- a/src/HOL/TPTP/mash_export.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/TPTP/mash_export.ML Sun Jun 09 15:31:33 2024 +0200
@@ -172,7 +172,7 @@
j mod step <> 0 orelse
Thm.legacy_get_kind th = "" orelse
null (the_list isar_deps) orelse
- is_blacklisted_or_something (Thm.get_name_hint th)
+ is_blacklisted_or_something (Thm_Name.short (Thm.get_name_hint th))
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
let
--- a/src/HOL/Tools/ATP/atp_util.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Sun Jun 09 15:31:33 2024 +0200
@@ -417,7 +417,7 @@
fun short_thm_name ctxt th =
let
- val long = Thm.get_name_hint th
+ val long = Thm_Name.short (Thm.get_name_hint th)
val short = Long_Name.base_name long
in
(case try (singleton (Attrib.eval_thms ctxt)) (Facts.named short, []) of
--- a/src/HOL/Tools/Meson/meson.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Sun Jun 09 15:31:33 2024 +0200
@@ -459,7 +459,7 @@
(*Use "theorem naming" to label the clauses*)
fun name_thms label =
let fun name1 th (k, ths) =
- (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
+ (k-1, Thm.put_name_hint (label ^ string_of_int k, 0) th :: ths)
in fn ths => #2 (fold_rev name1 ths (length ths, [])) end;
(*Is the given disjunction an all-negative support clause?*)
--- a/src/HOL/Tools/Metis/metis_tactic.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sun Jun 09 15:31:33 2024 +0200
@@ -214,7 +214,8 @@
val _ = unused := maps (#2 o #2) unused_th_cls_pairs;
val _ =
if not (null unused_th_cls_pairs) then
- verbose_warning ctxt ("Unused theorems: " ^ commas_quote (map #1 unused_th_cls_pairs))
+ verbose_warning ctxt ("Unused theorems: " ^
+ commas_quote (map (Proof_Context.print_thm_name ctxt o #1) unused_th_cls_pairs))
else ();
val _ =
if not (null cls) andalso not (have_common_thm ctxt used cls) then
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Jun 09 15:31:33 2024 +0200
@@ -305,11 +305,11 @@
if Inttab.defined seen i then (x, seen)
else
let
- val name = Thm_Name.short (Proofterm.thm_node_name thm_node);
+ val name = Proofterm.thm_node_name thm_node;
val prop = Proofterm.thm_node_prop thm_node;
val body = Future.join (Proofterm.thm_node_body thm_node);
val (x', seen') =
- app (n + (if name = "" then 0 else 1)) body
+ app (n + (if Thm_Name.is_empty name then 0 else 1)) body
(x, Inttab.update (i, ()) seen);
in (x' |> n = 0 ? f (name, prop, body), seen') end);
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end;
@@ -319,7 +319,7 @@
fun theorems_in_proof_term thy thm =
let
val all_thms = Global_Theory.all_thms_of thy true;
- fun collect (s, _, _) = if s <> "" then insert (op =) s else I;
+ fun collect (name, _, _) = if Thm_Name.is_empty name then I else insert (op =) name;
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE;
fun resolve_thms names = map_filter (member_of names) all_thms;
in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end;
--- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sun Jun 09 15:31:33 2024 +0200
@@ -19,7 +19,7 @@
fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts);
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
- |> not (null names) ? suffix (":\n" ^ commas names)
+ |> not (null names) ? suffix (":\n" ^ commas (map Thm_Name.short names))
end
in ("", {run = run, finalize = K ""}) end
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sun Jun 09 15:31:33 2024 +0200
@@ -7,7 +7,7 @@
signature FIND_UNUSED_ASSMS =
sig
val check_unused_assms: Proof.context -> string * thm -> string * int list list option
- val find_unused_assms: Proof.context -> string -> (string * int list list option) list
+ val find_unused_assms: Proof.context -> string -> (Thm_Name.T * int list list option) list
val print_unused_assms: Proof.context -> string option -> unit
end
@@ -71,8 +71,8 @@
val thy = Proof_Context.theory_of ctxt
val all_thms =
thms_of thy thy_name
- |> filter (fn (name, _) => Long_Name.count name = 2) (* FIXME !? *)
- |> sort_by #1
+ |> filter (fn ((name, _), _) => Long_Name.count name = 2) (* FIXME !? *)
+ |> sort (Thm_Name.ord o apply2 #1)
val check = check_unused_assms ctxt
in rev (Par_List.map check all_thms) end
@@ -86,8 +86,8 @@
(flat (separate [Pretty.str " and", Pretty.brk 1]
(map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is))))
-fun pretty_thm (name, set_of_indexes) =
- Pretty.block (Pretty.str name :: Pretty.str ":" :: Pretty.brk 1 ::
+fun pretty_thm ctxt (name, set_of_indexes) =
+ Pretty.block (Proof_Context.pretty_thm_name ctxt name :: Pretty.str ":" :: Pretty.brk 1 ::
Pretty.str "unnecessary assumption " ::
separate (Pretty.str " or ") (map pretty_indexes set_of_indexes))
@@ -112,7 +112,7 @@
string_of_int total ^ " total) in the theory " ^ quote thy_name
in
[Pretty.str (msg ^ ":"), Pretty.str ""] @
- map pretty_thm with_superfluous_assumptions @
+ map (pretty_thm ctxt) with_superfluous_assumptions @
[Pretty.str "", Pretty.str end_msg]
end |> Pretty.writeln_chunks
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Jun 09 15:31:33 2024 +0200
@@ -223,7 +223,7 @@
fun is_that_fact th =
exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th)
- andalso String.isSuffix sep_that (Thm.get_name_hint th)
+ andalso String.isSuffix sep_that (Thm_Name.short (Thm.get_name_hint th))
datatype interest = Deal_Breaker | Interesting | Boring
@@ -359,7 +359,7 @@
let
fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (Thm.prop_of th)), th)
fun add_plain canon alias =
- Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias))
+ Symtab.update (Thm_Name.short (Thm.get_name_hint alias), name_of (if_thm_before canon alias))
fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name)
val prop_tab = fold cons_thm facts Termtab.empty
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 09 15:31:33 2024 +0200
@@ -789,7 +789,7 @@
fun nickname_of_thm th =
if Thm.has_name_hint th then
- let val hint = Thm.get_name_hint th in
+ let val hint = Thm_Name.short (Thm.get_name_hint th) in
(* There must be a better way to detect local facts. *)
(case Long_Name.dest_local hint of
SOME suf =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Jun 09 15:31:33 2024 +0200
@@ -108,7 +108,8 @@
NONE => NONE
| SOME body =>
let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in
- SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm_body body))
+ SOME (fold_body_thm max_thms (Thm_Name.short (Thm.get_name_hint th)) map_names
+ (Proofterm.strip_thm_body body))
handle TOO_MANY () => NONE
end)
--- a/src/Pure/Isar/element.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/Isar/element.ML Sun Jun 09 15:31:33 2024 +0200
@@ -228,7 +228,8 @@
let val head =
if Thm.has_name_hint th then
Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
- Proof_Context.pretty_name ctxt (Long_Name.base_name (Thm.get_name_hint th)), Pretty.str ":"]
+ Proof_Context.pretty_name ctxt (Long_Name.base_name (#1 (Thm.get_name_hint th))),
+ Pretty.str ":"]
else Pretty.keyword1 kind
in Pretty.block (Pretty.fbreaks (head :: prts)) end;
--- a/src/Pure/Proof/proof_checker.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/Proof/proof_checker.ML Sun Jun 09 15:31:33 2024 +0200
@@ -16,10 +16,13 @@
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
- let val tab = Symtab.build (Global_Theory.all_thms_of thy true |> fold_rev Symtab.update) in
- fn s =>
- (case Symtab.lookup tab s of
- NONE => error ("Unknown theorem " ^ quote s)
+ let
+ val tab =
+ Thm_Name.Table.build (Global_Theory.all_thms_of thy true |> fold_rev Thm_Name.Table.update);
+ in
+ fn name =>
+ (case Thm_Name.Table.lookup tab name of
+ NONE => error ("Unknown theorem " ^ quote (Thm_Name.print name))
| SOME thm => thm)
end;
@@ -87,8 +90,7 @@
fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) =
let
- val name = Thm_Name.short thm_name;
- val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
+ val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup thm_name));
val prop = Thm.prop_of thm;
val _ =
if is_equal prop prop' then ()
--- a/src/Pure/Proof/proof_syntax.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Sun Jun 09 15:31:33 2024 +0200
@@ -143,7 +143,7 @@
fun proof_of_term thy ty =
let
- val thms = Global_Theory.all_thms_of thy true;
+ val thms = Global_Theory.all_thms_of thy true |> map (apfst Thm_Name.short);
val axms = Theory.all_axioms_of thy;
fun mk_term t = (if ty then I else map_types (K dummyT))
@@ -200,7 +200,8 @@
fun read_term thy topsort =
let
- val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));
+ val thm_names =
+ filter_out (fn s => s = "") (map (Thm_Name.short o fst) (Global_Theory.all_thms_of thy true));
val axm_names = map fst (Theory.all_axioms_of thy);
val ctxt = thy
|> add_proof_syntax
--- a/src/Pure/Tools/simplifier_trace.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Sun Jun 09 15:31:33 2024 +0200
@@ -230,7 +230,7 @@
let
(* FIXME pretty printing via Proof_Context.pretty_fact *)
val pretty_thm = Pretty.block
- [Pretty.str ("Instance of " ^ name ^ ":"),
+ [Pretty.str ("Instance of " ^ Proof_Context.print_thm_name ctxt name ^ ":"),
Pretty.brk 1,
Syntax.pretty_term ctxt (Thm.prop_of thm)]
@@ -319,7 +319,7 @@
val pretty_thm =
(* FIXME pretty printing via Proof_Context.pretty_fact *)
Pretty.block
- [Pretty.str ("In an instance of " ^ name ^ ":"),
+ [Pretty.str ("In an instance of " ^ Proof_Context.print_thm_name ctxt name ^ ":"),
Pretty.brk 1,
Syntax.pretty_term ctxt (Thm.prop_of thm)]
--- a/src/Pure/global_theory.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/global_theory.ML Sun Jun 09 15:31:33 2024 +0200
@@ -23,7 +23,7 @@
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
val transfer_theories: theory -> thm -> thm
- val all_thms_of: theory -> bool -> (string * thm) list
+ val all_thms_of: theory -> bool -> (Thm_Name.T * thm) list
val get_thm_name: theory -> Thm_Name.T * Position.T -> thm
type name_flags
val unnamed: name_flags
@@ -259,7 +259,7 @@
|> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ?
Thm.name_derivation (name, pos)
|> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ?
- Thm.put_name_hint (Thm_Name.short name)));
+ Thm.put_name_hint name));
end;
--- a/src/Pure/more_thm.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/more_thm.ML Sun Jun 09 15:31:33 2024 +0200
@@ -88,8 +88,8 @@
val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
val make_def_binding: bool -> Binding.binding -> Binding.binding
val has_name_hint: thm -> bool
- val get_name_hint: thm -> string
- val put_name_hint: string -> thm -> thm
+ val get_name_hint: thm -> Thm_Name.T
+ val put_name_hint: Thm_Name.T -> thm -> thm
val theoremK: string
val legacy_get_kind: thm -> string
val kind_rule: string -> thm -> thm
@@ -607,10 +607,10 @@
(* unofficial theorem names *)
fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN;
-fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
-fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown";
+fun the_name_hint thm = Thm_Name.parse (the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN));
+fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else ("??.unknown", 0);
-fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
+fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, Thm_Name.print name);
(* theorem kinds *)
--- a/src/Pure/raw_simplifier.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/raw_simplifier.ML Sun Jun 09 15:31:33 2024 +0200
@@ -27,7 +27,7 @@
val empty_ss: simpset
val merge_ss: simpset * simpset -> simpset
val dest_ss: simpset ->
- {simps: (string * thm) list,
+ {simps: (Thm_Name.T * thm) list,
procs: (string * term list) list,
congs: (cong_name * thm) list,
weak_congs: cong_name list,
@@ -133,7 +133,7 @@
type rrule =
{thm: thm, (*the rewrite rule*)
- name: string, (*name of theorem from which rewrite rule was extracted*)
+ name: Thm_Name.T, (*name of theorem from which rewrite rule was extracted*)
lhs: term, (*the left-hand side*)
elhs: cterm, (*the eta-contracted lhs*)
extra: bool, (*extra variables outside of elhs*)
@@ -443,10 +443,15 @@
fun print_term ctxt s t =
s ^ "\n" ^ Syntax.string_of_term ctxt t;
-fun print_thm ctxt s (name, th) =
- print_term ctxt (if name = "" then s else s ^ " " ^ quote name ^ ":") (Thm.full_prop_of th);
+fun print_thm ctxt msg (name, th) =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val sffx =
+ if Thm_Name.is_empty name then ""
+ else " " ^ quote (Global_Theory.print_thm_name thy name) ^ ":";
+ in print_term ctxt (msg ^ sffx) (Thm.full_prop_of th) end;
-fun print_thm0 ctxt msg th = print_thm ctxt msg ("", th);
+fun print_thm0 ctxt msg th = print_thm ctxt msg (Thm_Name.empty, th);
@@ -931,7 +936,7 @@
in
if rewrite_rule_extra_vars prems lhs rhs
then (cond_warning ctxt (fn () => print_thm0 ctxt "Extra vars on rhs:" thm); [])
- else [mk_rrule2 {thm = thm', name = "", lhs = lhs, elhs = elhs, perm = false}]
+ else [mk_rrule2 {thm = thm', name = Thm_Name.empty, lhs = lhs, elhs = elhs, perm = false}]
end;