--- a/src/Doc/Implementation/Logic.thy Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Doc/Implementation/Logic.thy Fri Jun 07 23:53:31 2024 +0200
@@ -1293,7 +1293,7 @@
@{define_ML Proofterm.reconstruct_proof:
"theory -> term -> proof -> proof"} \\
@{define_ML Proofterm.expand_proof: "theory ->
- (Proofterm.thm_header -> string option) -> proof -> proof"} \\
+ (Proofterm.thm_header -> Thm_Name.T option) -> proof -> proof"} \\
@{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
@{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
@{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
--- a/src/HOL/Proofs/ex/Proof_Terms.thy Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy Fri Jun 07 23:53:31 2024 +0200
@@ -35,7 +35,7 @@
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
- (fn {name, ...} => insert (op =) name) [body] [];
+ (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
\<close>
text \<open>
--- a/src/HOL/TPTP/atp_problem_import.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Jun 07 23:53:31 2024 +0200
@@ -187,7 +187,7 @@
|> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 3 else 0)
|> Local_Theory.note ((\<^binding>\<open>thms\<close>, []), assm_ths0)
- fun ref_of th = (Facts.named (Thm.derivation_name th), [])
+ fun ref_of th = (Facts.named (Thm_Name.short (Thm.derivation_name th)), [])
val ref_of_assms = (Facts.named assm_name, [])
in
Sledgehammer_Tactics.sledgehammer_as_oracle_tac lthy
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Jun 07 23:53:31 2024 +0200
@@ -224,8 +224,7 @@
let
val name = Long_Name.append qualifier base;
val pos = Position.thread_data ();
- val thms' =
- Thm_Name.list (name, pos) thms |> map (uncurry (Thm.name_derivation o Thm_Name.short));
+ val thms' = Thm_Name.list (name, pos) thms |> map (uncurry Thm.name_derivation);
in (local_name, thms') :: noted end
else ((local_name, thms) :: name_noted_thms qualifier base noted);
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Fri Jun 07 23:53:31 2024 +0200
@@ -305,7 +305,7 @@
if Inttab.defined seen i then (x, seen)
else
let
- val name = Proofterm.thm_node_name thm_node;
+ val name = Thm_Name.short (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') =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jun 07 23:53:31 2024 +0200
@@ -76,7 +76,7 @@
let
fun app_thm map_name (_, thm_node) (accum as (num_thms, names)) =
let
- val name = Proofterm.thm_node_name thm_node
+ val name = Thm_Name.short (Proofterm.thm_node_name thm_node)
val body = Proofterm.thm_node_body thm_node
val (anonymous, enter_class) =
(* The "name = outer_name" case caters for the uncommon case where the proved theorem
--- a/src/HOL/Tools/datatype_realizer.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Jun 07 23:53:31 2024 +0200
@@ -127,7 +127,8 @@
val (thm', thy') = thy
|> Sign.root_path
|> Global_Theory.store_thm
- (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
+ (Binding.qualified_name
+ (space_implode "_" (Thm_Name.short ind_name :: vs @ ["correctness"])), thm)
||> Sign.restore_naming thy;
val ivs = rev (Term.add_vars (Logic.varify_global (Old_Datatype_Prop.make_ind [descr])) []);
@@ -201,7 +202,8 @@
val exh_name = Thm.derivation_name exhaust;
val (thm', thy') = thy
|> Sign.root_path
- |> Global_Theory.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
+ |> Global_Theory.store_thm
+ (Binding.qualified_name (Thm_Name.short exh_name ^ "_P_correctness"), thm)
||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
--- a/src/HOL/Tools/inductive_realizer.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jun 07 23:53:31 2024 +0200
@@ -13,11 +13,13 @@
structure InductiveRealizer : INDUCTIVE_REALIZER =
struct
-fun name_of_thm thm =
- (case Proofterm.fold_proof_atoms false (fn PThm ({name, ...}, _) => cons name | _ => I)
+fun thm_name_of thm =
+ (case Proofterm.fold_proof_atoms false (fn PThm ({thm_name, ...}, _) => cons thm_name | _ => I)
[Thm.proof_of thm] [] of
- [name] => name
- | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
+ [thm_name] => thm_name
+ | _ => raise THM ("thm_name_of: bad proof of theorem", 0, [thm]));
+
+val short_name_of = Thm_Name.short o thm_name_of;
fun prf_of thy =
Thm.transfer thy #>
@@ -61,7 +63,7 @@
(Logic.strip_imp_concl (Thm.prop_of (hd intrs))));
val params = map dest_Var (take nparms ts);
val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
- fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
+ fun constr_of_intr intr = (Binding.name (Long_Name.base_name (short_name_of intr)),
map (Logic.unvarifyT_global o snd)
(subtract (op =) params (rev (Term.add_vars (Thm.prop_of intr) []))) @
filter_out (equal Extraction.nullT)
@@ -193,7 +195,7 @@
then fold_rev (absfree o dest_Free) xs HOLogic.unit
else fold_rev (absfree o dest_Free) xs
(list_comb
- (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
+ (Free ("r" ^ Long_Name.base_name (short_name_of intr),
map fastype_of (rev args) ---> conclT), rev args))
end
@@ -216,7 +218,7 @@
end) (premss ~~ dummies);
val frees = fold Term.add_frees fs [];
val Ts = map fastype_of fs;
- fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr)
+ fun name_of_fn intr = "r" ^ Long_Name.base_name (short_name_of intr)
in
fst (fold_map (fn concl => fn names =>
let val T = Extraction.etype_of thy vs [] concl
@@ -273,7 +275,7 @@
fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
let
- val qualifier = Long_Name.qualifier (name_of_thm induct);
+ val qualifier = Long_Name.qualifier (short_name_of induct);
val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts");
val iTs = rev (Term.add_tvars (Thm.prop_of (hd intrs)) []);
val ar = length vs + length iTs;
@@ -354,11 +356,11 @@
{quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
no_elim = false, no_ind = false, skip_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
- ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
+ ((Binding.name (Long_Name.base_name (short_name_of intr)), []),
subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
(rintrs ~~ maps snd rss)) []) ||>
Sign.root_path;
- val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
+ val thy3 = fold (Global_Theory.hide_fact false o short_name_of) (#intrs ind_info) thy3';
(** realizer for induction rule **)
@@ -413,7 +415,7 @@
mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
realizers @ (case realizers of
[(((ind, corr), rlz), r)] =>
- [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
+ [mk_realizer thy'' (vs' @ Ps) ((Long_Name.qualify qualifier "induct", 0),
ind, corr, rlz, r)]
| _ => [])) thy''
end;
@@ -463,10 +465,10 @@
DEPTH_SOLVE_1 o
FIRST' [assume_tac ctxt, eresolve_tac ctxt [allE], eresolve_tac ctxt [impE]])) 1)]);
val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
- (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
+ (short_name_of elim :: vs @ Ps @ ["correctness"])), thm) thy
in
Extraction.add_realizers_i
- [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
+ [mk_realizer thy' (vs @ Ps) (thm_name_of elim, elim, thm', rlz, r)] thy'
end;
(** add realizers to theory **)
@@ -474,7 +476,7 @@
val thy4 = fold add_ind_realizer (subsets Ps) thy3;
val thy5 = Extraction.add_realizers_i
(map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
- (name_of_thm rule, rule, rrule, rlz,
+ (thm_name_of rule, rule, rrule, rlz,
list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (Thm.prop_of rule) []))))))
(maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
val elimps = map_filter (fn ((s, intrs), p) =>
--- a/src/HOL/Tools/rewrite_hol_proof.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Jun 07 23:53:31 2024 +0200
@@ -305,9 +305,9 @@
(** Replace congruence rules by substitution rules **)
-fun strip_cong ps (PThm ({name = "HOL.cong", ...}, _) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm ({thm_name = ("HOL.cong", 0), ...}, _) % _ % _ % SOME x % SOME y %%
prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
- | strip_cong ps (PThm ({name = "HOL.refl", ...}, _) % SOME f %% _) = SOME (f, ps)
+ | strip_cong ps (PThm ({thm_name = ("HOL.refl", 0), ...}, _) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst});
@@ -330,15 +330,15 @@
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
-fun elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
- | elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % P % _ %% prf) =
+ | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
(strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
- | elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % _ %% prf1 %% prf2) =
+ | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
- | elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % P %% prf) =
+ | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % P %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
| elim_cong_aux _ _ = NONE;
--- a/src/Pure/Build/export_theory.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Build/export_theory.ML Fri Jun 07 23:53:31 2024 +0200
@@ -283,11 +283,8 @@
val lookup_thm_id = Global_Theory.lookup_thm_id thy;
fun expand_name thm_id (header: Proofterm.thm_header) =
- if #serial header = #serial thm_id then ""
- else
- (case lookup_thm_id (Proofterm.thm_header_id header) of
- NONE => ""
- | SOME thm_name => Thm_Name.print thm_name);
+ if #serial header = #serial thm_id then Thm_Name.empty
+ else the_default Thm_Name.empty (lookup_thm_id (Proofterm.thm_header_id header));
fun entity_markup_thm (serial, (name, i)) =
let
--- a/src/Pure/Isar/generic_target.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Isar/generic_target.ML Fri Jun 07 23:53:31 2024 +0200
@@ -296,8 +296,8 @@
local
-val name_thm1 = Global_Theory.name_thm Global_Theory.official1 o Thm_Name.short;
-val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2 o Thm_Name.short;
+val name_thm1 = Global_Theory.name_thm Global_Theory.official1;
+val name_thm2 = Global_Theory.name_thm Global_Theory.unofficial2;
fun thm_def (name, pos) thm lthy =
if #1 name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
--- a/src/Pure/Proof/extraction.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Jun 07 23:53:31 2024 +0200
@@ -11,7 +11,7 @@
val add_realizes_eqns : string list -> theory -> theory
val add_typeof_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
val add_typeof_eqns : string list -> theory -> theory
- val add_realizers_i : (string * (string list * term * Proofterm.proof)) list
+ val add_realizers_i : (Thm_Name.T * (string list * term * Proofterm.proof)) list
-> theory -> theory
val add_realizers : (thm * (string list * string * string)) list
-> theory -> theory
@@ -118,8 +118,11 @@
val change_types = Proofterm.change_types o SOME;
-fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
-fun corr_name s vs = extr_name s vs ^ "_correctness";
+fun extr_name ((name, i): Thm_Name.T) vs =
+ (Long_Name.append "extr" (space_implode "_" (name :: vs)), i);
+
+fun corr_name thm_name vs =
+ extr_name thm_name vs |>> suffix "_correctness";
fun msg d s = writeln (Symbol.spaces d ^ s);
@@ -202,16 +205,16 @@
typeof_eqns : rules,
types : (string * ((term -> term option) list *
(term -> typ -> term -> typ -> term) option)) list,
- realizers : (string list * (term * proof)) list Symtab.table,
+ realizers : (string list * (term * proof)) list Thm_Name.Table.table,
defs : thm list,
- expand : string list,
+ expand : Thm_Name.T list,
prep : (theory -> proof -> proof) option}
val empty =
{realizes_eqns = empty_rules,
typeof_eqns = empty_rules,
types = [],
- realizers = Symtab.empty,
+ realizers = Thm_Name.Table.empty,
defs = [],
expand = [],
prep = NONE};
@@ -224,7 +227,7 @@
{realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
types = AList.merge (op =) (K true) (types1, types2),
- realizers = Symtab.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
+ realizers = Thm_Name.Table.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
defs = Library.merge Thm.eq_thm (defs1, defs2),
expand = Library.merge (op =) (expand1, expand2),
prep = if is_some prep1 then prep1 else prep2};
@@ -319,7 +322,7 @@
in
ExtractionData.put
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
- realizers = fold (Symtab.cons_list o prep_rlz thy) rs realizers,
+ realizers = fold (Thm_Name.Table.cons_list o prep_rlz thy) rs realizers,
defs = defs, expand = expand, prep = prep} thy
end
@@ -335,8 +338,8 @@
val rd = Proof_Syntax.read_proof thy' true false;
in fn (thm, (vs, s1, s2)) =>
let
- val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "add_realizers: unnamed theorem";
+ val thm_name = Thm.derivation_name thm;
+ val _ = if Thm_Name.is_empty thm_name then error "add_realizers: unnamed theorem" else ();
val prop = Thm.unconstrainT thm |> Thm.prop_of |>
Pattern.rewrite_term thy' (map (Logic.dest_equals o Thm.prop_of) defs) [];
val vars = vars_of prop;
@@ -357,7 +360,7 @@
val r = Logic.list_implies (shyps,
fold_rev Logic.all (map (get_var_type r') vars) r');
val prf = Proofterm.reconstruct_proof thy' r (rd s2);
- in (name, (vs, (t, prf))) end
+ in (thm_name, (vs, (t, prf))) end
end;
val add_realizers_i = gen_add_realizers
@@ -411,8 +414,8 @@
val {realizes_eqns, typeof_eqns, types, realizers,
defs, expand, prep} = ExtractionData.get thy;
- val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
+ val thm_name = Thm.derivation_name thm;
+ val _ = if Thm_Name.is_empty thm_name then error "add_expand_thm: unnamed theorem" else ();
in
thy |> ExtractionData.put
(if is_def then
@@ -425,7 +428,7 @@
else
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
realizers = realizers, defs = defs,
- expand = insert (op =) name expand, prep = prep})
+ expand = insert (op =) thm_name expand, prep = prep})
end;
fun extraction_expand is_def =
@@ -508,8 +511,9 @@
val procs = maps (rev o fst o snd) types;
val rtypes = map fst types;
val typroc = typeof_proc [];
- fun expand_name ({name, ...}: Proofterm.thm_header) =
- if name = "" orelse member (op =) expand name then SOME "" else NONE;
+ fun expand_name ({thm_name, ...}: Proofterm.thm_header) =
+ if Thm_Name.is_empty thm_name orelse member (op =) expand thm_name
+ then SOME Thm_Name.empty else NONE;
val prep = the_default (K I) prep thy' o
Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
Proofterm.expand_proof thy' expand_name;
@@ -539,7 +543,8 @@
(T, Sign.defaultS thy)) tye;
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
- fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
+ fun filter_thm_name (a: Thm_Name.T) =
+ map_filter (fn (b, x) => if a = b then SOME x else NONE);
fun app_rlz_rews Ts vs t =
strip_abs (length Ts)
@@ -618,7 +623,7 @@
| corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
let
- val {pos, theory_name, name, prop, ...} = thm_header;
+ val {pos, theory_name, thm_name, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -629,14 +634,16 @@
else snd (extr d vs ts Ts hs prf0 defs)
in
if T = nullT andalso realizes_null vs' prop aconv prop then (prf0, defs)
- else (case Symtab.lookup realizers name of
- NONE => (case find vs' (find' name defs') of
+ else (case Thm_Name.Table.lookup realizers thm_name of
+ NONE => (case find vs' (filter_thm_name thm_name defs') of
NONE =>
let
val _ = T = nullT orelse error "corr: internal error";
- val _ = msg d ("Building correctness proof for " ^ quote name ^
- (if null vs' then ""
- else " (relevant variables: " ^ commas_quote vs' ^ ")"));
+ val _ =
+ msg d ("Building correctness proof for " ^
+ quote (Thm_Name.short thm_name) ^
+ (if null vs' then ""
+ else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
(rev shyps) NONE prf' prf' defs';
@@ -644,7 +651,7 @@
val corr_prop = Proofterm.prop_of corr_prf;
val corr_header =
Proofterm.thm_header (serial ()) pos theory_name
- (corr_name name vs') corr_prop
+ (corr_name thm_name vs') corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_prf' =
Proofterm.proof_combP
@@ -656,15 +663,16 @@
mkabsp shyps
in
(Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs),
- (name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
+ (thm_name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
end
| SOME (_, (_, prf')) =>
(Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs'))
| SOME rs => (case find vs' rs of
SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
| NONE => error ("corr: no realizer for instance of theorem " ^
- quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
- (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
+ quote (Thm_Name.short thm_name) ^ ":\n" ^
+ Syntax.string_of_term_global thy'
+ (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
end
| corr d vs ts Ts hs cs _ (prf0 as PAxm (s, prop, SOME Ts')) _ defs =
@@ -674,7 +682,7 @@
in
if etype_of thy' vs' [] prop = nullT andalso
realizes_null vs' prop aconv prop then (prf0, defs)
- else case find vs' (Symtab.lookup_list realizers s) of
+ else case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
defs)
| NONE => error ("corr: no realizer for instance of axiom " ^
@@ -719,19 +727,20 @@
| extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
let
- val {pos, theory_name, name = s, prop, ...} = thm_header;
+ val {pos, theory_name, thm_name, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
- case Symtab.lookup realizers s of
- NONE => (case find vs' (find' s defs) of
+ case Thm_Name.Table.lookup realizers thm_name of
+ NONE => (case find vs' (filter_thm_name thm_name defs) of
NONE =>
let
- val _ = msg d ("Extracting " ^ quote s ^
- (if null vs' then ""
- else " (relevant variables: " ^ commas_quote vs' ^ ")"));
+ val _ =
+ msg d ("Extracting " ^ quote (Thm_Name.short thm_name) ^
+ (if null vs' then ""
+ else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
@@ -743,7 +752,7 @@
val args' = filter (fn v => Logic.occs (v, nt)) args;
val t' = mkabs args' nt;
val T = fastype_of t';
- val cname = extr_name s vs';
+ val cname = Thm_Name.short (extr_name thm_name vs');
val c = Const (cname, T);
val u = mkabs args (list_comb (c, args'));
val eqn = Logic.mk_equals (c, t');
@@ -764,7 +773,7 @@
val corr_prop = Proofterm.prop_of corr_prf';
val corr_header =
Proofterm.thm_header (serial ()) pos theory_name
- (corr_name s vs') corr_prop
+ (corr_name thm_name vs') corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_prf'' =
Proofterm.proof_combP (Proofterm.proof_combt
@@ -775,13 +784,14 @@
mkabsp shyps
in
(subst_TVars tye' u,
- (s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
+ (thm_name, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
end
| SOME ((_, u), _) => (subst_TVars tye' u, defs))
| SOME rs => (case find vs' rs of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of theorem " ^
- quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
+ quote (Thm_Name.short thm_name) ^ ":\n" ^
+ Syntax.string_of_term_global thy' (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
end
@@ -790,7 +800,7 @@
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
- case find vs' (Symtab.lookup_list realizers s) of
+ case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
@@ -805,26 +815,27 @@
val prop = Thm.prop_of thm;
val prf = Thm.proof_of thm;
val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "extraction: unnamed theorem";
+ val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else ();
val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
- quote name ^ " has no computational content")
+ quote (Thm_Name.short name) ^ " has no computational content")
in Proofterm.reconstruct_proof thy' prop prf end;
val defs =
fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
thm_vss [];
- fun add_def (s, (vs, ((t, u)))) thy =
+ fun add_def (name, (vs, ((t, u)))) thy =
let
val ft = Type.legacy_freeze t;
val fu = Type.legacy_freeze u;
val head = head_of (strip_abs_body fu);
- val b = Binding.qualified_name (extr_name s vs);
+ val b = Binding.qualified_name (Thm_Name.short (extr_name name vs));
in
thy
|> Sign.add_consts [(b, fastype_of ft, NoSyn)]
|> Global_Theory.add_def
- (Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head, ft))
+ (Binding.qualified_name (Thm.def_name (Thm_Name.short (extr_name name vs))),
+ Logic.mk_equals (head, ft))
|-> (fn def_thm =>
Spec_Rules.add_global b Spec_Rules.equational
[Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
@@ -836,7 +847,7 @@
val corr_prop = Proofterm.prop_of prf;
in
thy
- |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
+ |> Global_Theory.store_thm (Binding.qualified_name (Thm_Name.short (corr_name s vs)),
Thm.varifyT_global (funpow (length (vars_of corr_prop))
(Thm.forall_elim_var 0) (Thm.forall_intr_frees
(Proof_Checker.thm_of_proof thy
@@ -845,7 +856,7 @@
end;
fun add_def_and_corr (s, (vs, ((t, u), (prf, _)))) thy =
- if is_none (Sign.const_type thy (extr_name s vs))
+ if is_none (Sign.const_type thy (Thm_Name.short (extr_name s vs)))
then
thy
|> not (t = nullt) ? add_def (s, (vs, ((t, u))))
--- a/src/Pure/Proof/proof_checker.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/proof_checker.ML Fri Jun 07 23:53:31 2024 +0200
@@ -85,8 +85,9 @@
(Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
end;
- fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
+ 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 prop = Thm.prop_of thm;
val _ =
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jun 07 23:53:31 2024 +0200
@@ -39,12 +39,12 @@
val equal_elim_axm = ax Proofterm.equal_elim_axm [];
val symmetric_axm = ax Proofterm.symmetric_axm [propT];
- fun rew' (PThm ({name = "Pure.protectD", ...}, _) % _ %%
- (PThm ({name = "Pure.protectI", ...}, _) % _ %% prf)) = SOME prf
- | rew' (PThm ({name = "Pure.conjunctionD1", ...}, _) % _ % _ %%
- (PThm ({name = "Pure.conjunctionI", ...}, _) % _ % _ %% prf %% _)) = SOME prf
- | rew' (PThm ({name = "Pure.conjunctionD2", ...}, _) % _ % _ %%
- (PThm ({name = "Pure.conjunctionI", ...}, _) % _ % _ %% _ %% prf)) = SOME prf
+ fun rew' (PThm ({thm_name = ("Pure.protectD", 0), ...}, _) % _ %%
+ (PThm ({thm_name = ("Pure.protectI", 0), ...}, _) % _ %% prf)) = SOME prf
+ | rew' (PThm ({thm_name = ("Pure.conjunctionD1", 0), ...}, _) % _ % _ %%
+ (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% prf %% _)) = SOME prf
+ | rew' (PThm ({thm_name = ("Pure.conjunctionD2", 0), ...}, _) % _ % _ %%
+ (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% _ %% prf)) = SOME prf
| rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
(PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
| rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
@@ -54,14 +54,14 @@
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
_ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
- ((tg as PThm ({name = "Pure.protectI", ...}, _)) % _ %% prf2)) =
+ ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
(PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
_ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
- ((tg as PThm ({name = "Pure.protectI", ...}, _)) % _ %% prf2)) =
+ ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %%
(symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
@@ -245,8 +245,8 @@
(AbsP (s, t, fst (insert_refl defs Ts prf)), false)
| insert_refl defs Ts prf =
(case Proofterm.strip_combt prf of
- (PThm ({name = s, prop, types = SOME Ts, ...}, _), ts) =>
- if member (op =) defs s then
+ (PThm ({thm_name, prop, types = SOME Ts, ...}, _), ts) =>
+ if member (op =) defs thm_name then
let
val vs = vars_of prop;
val tvars = build_rev (Term.add_tvars prop);
@@ -271,11 +271,11 @@
let
val cnames = map (fst o dest_Const o fst) defs';
val expand = Proofterm.fold_proof_atoms true
- (fn PThm ({serial, name, prop, ...}, _) =>
- if member (op =) defnames name orelse
+ (fn PThm ({serial, thm_name, prop, ...}, _) =>
+ if member (op =) defnames thm_name orelse
not (exists_Const (member (op =) cnames o #1) prop)
then I
- else Inttab.update (serial, "")
+ else Inttab.update (serial, Thm_Name.empty)
| _ => I) [prf] Inttab.empty;
in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
else prf;
--- a/src/Pure/Proof/proof_syntax.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Fri Jun 07 23:53:31 2024 +0200
@@ -16,7 +16,7 @@
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
val pretty_proof_boxes_of: Proof.context ->
{full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
- val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
+ val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.T option} ->
thm -> Proofterm.proof
val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
@@ -104,9 +104,11 @@
let val U = Term.itselfT T --> propT
in Const ("Pure.PClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
-fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
+fun term_of _ (PThm ({serial = i, thm_name = a, types = Ts, ...}, _)) =
fold AppT (these Ts)
- (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
+ (Const
+ (Long_Name.append "thm"
+ (if Thm_Name.is_empty a then string_of_int i else Thm_Name.short a), proofT))
| term_of _ (PAxm (name, _, Ts)) =
fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
| term_of _ (PClass (T, c)) = AppT T (PClasst (T, c))
@@ -224,7 +226,8 @@
fun proof_syntax prf =
let
val thm_names = Symset.dest (Proofterm.fold_proof_atoms true
- (fn PThm ({name, ...}, _) => if name <> "" then Symset.insert name else I
+ (fn PThm ({thm_name, ...}, _) =>
+ if Thm_Name.is_empty thm_name then I else Symset.insert (Thm_Name.short thm_name)
| _ => I) [prf] Symset.empty);
val axm_names = Symset.dest (Proofterm.fold_proof_atoms true
(fn PAxm (name, _, _) => Symset.insert name | _ => I) [prf] Symset.empty);
--- a/src/Pure/Pure.thy Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Pure.thy Fri Jun 07 23:53:31 2024 +0200
@@ -1386,7 +1386,7 @@
NONE => (Theory.parents_of thy, [thy])
| SOME (xs, NONE) => (map check xs, [thy])
| SOME (xs, SOME ys) => (map check xs, map check ys))
- |> map pretty_thm |> Pretty.writeln_chunks
+ |> map (apfst Thm_Name.short #> pretty_thm) |> Pretty.writeln_chunks
end)));
in end\<close>
--- a/src/Pure/global_theory.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/global_theory.ML Fri Jun 07 23:53:31 2024 +0200
@@ -29,7 +29,7 @@
val official2: name_flags
val unofficial1: name_flags
val unofficial2: name_flags
- val name_thm: name_flags -> string * Position.T -> thm -> thm
+ val name_thm: name_flags -> Thm_Name.P -> thm -> thm
val name_thms: name_flags -> string * Position.T -> thm list -> thm list
val name_facts: name_flags -> string * Position.T -> (thm list * 'a) list -> (thm list * 'a) list
val check_thms_lazy: thm list lazy -> thm list lazy
@@ -251,21 +251,18 @@
No_Name_Flags => thm
| Name_Flags {post, official} =>
thm
- |> (official andalso (post orelse Thm.raw_derivation_name thm = "")) ?
+ |> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ?
Thm.name_derivation (name, pos)
- |> (name <> "" andalso (post orelse not (Thm.has_name_hint thm))) ?
- Thm.put_name_hint name));
+ |> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ?
+ Thm.put_name_hint (Thm_Name.short name)));
end;
-fun name_thm_short name_flags name =
- name_thm name_flags (Thm_Name.short name);
-
fun name_thms name_flags name_pos thms =
- Thm_Name.list name_pos thms |> map (uncurry (name_thm_short name_flags));
+ Thm_Name.list name_pos thms |> map (uncurry (name_thm name_flags));
fun name_facts name_flags name_pos facts =
- Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm_short name_flags));
+ Thm_Name.expr name_pos facts |> (map o apfst o map) (uncurry (name_thm name_flags));
(* store theorems and proofs *)
@@ -319,7 +316,7 @@
in ((thms', atts), thy2) end);
val unnamed = #1 name = "";
- val name_thm1 = if unnamed then #2 else uncurry (name_thm_short name_flags1);
+ val name_thm1 = if unnamed then #2 else uncurry (name_thm name_flags1);
val app_facts =
fold_maps (fn (named_thms, atts) => fn thy =>
--- a/src/Pure/proofterm.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/proofterm.ML Fri Jun 07 23:53:31 2024 +0200
@@ -9,7 +9,7 @@
signature PROOFTERM =
sig
type thm_header =
- {serial: serial, pos: Position.T list, theory_name: string, name: string,
+ {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
prop: term, types: typ list option}
type thm_body
type thm_node
@@ -38,13 +38,13 @@
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
- val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
+ val thm_header: serial -> Position.T list -> string -> Thm_Name.T -> term -> typ list option ->
thm_header
val thm_body: proof_body -> thm_body
val thm_body_proof_raw: thm_body -> proof
val thm_body_proof_open: thm_body -> proof
val thm_node_theory_name: thm_node -> string
- val thm_node_name: thm_node -> string
+ val thm_node_name: thm_node -> Thm_Name.T
val thm_node_prop: thm_node -> term
val thm_node_body: thm_node -> proof_body future
val thm_node_thms: thm_node -> thm list
@@ -52,7 +52,7 @@
val make_thm: thm_header -> thm_body -> thm
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms:
- ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
+ ({serial: serial, thm_name: Thm_Name.T, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a
val oracle_ord: oracle ord
val thm_ord: thm ord
@@ -170,8 +170,8 @@
val reconstruct_proof: theory -> term -> proof -> proof
val prop_of': term list -> proof -> term
val prop_of: proof -> term
- val expand_name_empty: thm_header -> string option
- val expand_proof: theory -> (thm_header -> string option) -> proof -> proof
+ val expand_name_empty: thm_header -> Thm_Name.T option
+ val expand_proof: theory -> (thm_header -> Thm_Name.T option) -> proof -> proof
val standard_vars: Name.context -> term * proof option -> term * proof option
val standard_vars_term: Name.context -> term -> term
@@ -183,13 +183,13 @@
val export_proof_boxes_required: theory -> bool
val export_proof_boxes: proof_body list -> unit
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
- val thm_proof: theory -> sorts_proof -> string * Position.T -> sort list -> term list ->
+ val thm_proof: theory -> sorts_proof -> Thm_Name.P -> sort list -> term list ->
term -> (serial * proof_body future) list -> proof_body -> proof_body
val unconstrain_thm_proof: theory -> sorts_proof -> sort list ->
term -> (serial * proof_body future) list -> proof_body -> term * proof_body
val get_identity: sort list -> term list -> term -> proof ->
- {serial: serial, theory_name: string, name: string} option
- val get_approximative_name: sort list -> term list -> term -> proof -> string
+ {serial: serial, theory_name: string, thm_name: Thm_Name.T} option
+ val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.T
type thm_id = {serial: serial, theory_name: string}
val make_thm_id: serial * string -> thm_id
val thm_header_id: thm_header -> thm_id
@@ -206,7 +206,7 @@
(** datatype proof **)
type thm_header =
- {serial: serial, pos: Position.T list, theory_name: string, name: string,
+ {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
prop: term, types: typ list option};
datatype proof =
@@ -230,7 +230,7 @@
and thm_body =
Thm_Body of {open_proof: proof -> proof, body: proof_body future}
and thm_node =
- Thm_Node of {theory_name: string, name: string, prop: term,
+ Thm_Node of {theory_name: string, thm_name: Thm_Name.T, prop: term,
body: proof_body future, export: unit lazy, consolidate: unit lazy};
type oracle = (string * Position.T) * term option;
@@ -253,8 +253,9 @@
fun no_proof (PBody {oracles, thms, zboxes, zproof, ...}) =
PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = MinProof};
-fun thm_header serial pos theory_name name prop types : thm_header =
- {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
+fun thm_header serial pos theory_name thm_name prop types : thm_header =
+ {serial = serial, pos = pos, theory_name = theory_name, thm_name = thm_name,
+ prop = prop, types = types};
fun thm_body body = Thm_Body {open_proof = I, body = Future.value body};
fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body;
@@ -262,7 +263,7 @@
fun rep_thm_node (Thm_Node args) = args;
val thm_node_theory_name = #theory_name o rep_thm_node;
-val thm_node_name = #name o rep_thm_node;
+val thm_node_name = #thm_name o rep_thm_node;
val thm_node_prop = #prop o rep_thm_node;
val thm_node_body = #body o rep_thm_node;
val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms);
@@ -276,21 +277,21 @@
maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
#> Lazy.consolidate #> map Lazy.force #> ignore;
-fun make_thm_node theory_name name prop body export =
+fun make_thm_node theory_name thm_name prop body export =
let
val consolidate =
Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
let val PBody {thms, ...} = Future.join body
in consolidate_bodies (join_thms thms) end);
in
- Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body,
+ Thm_Node {theory_name = theory_name, thm_name = thm_name, prop = prop, body = body,
export = export, consolidate = consolidate}
end;
val no_export = Lazy.value ();
-fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
- (serial, make_thm_node theory_name name prop body no_export);
+fun make_thm ({serial, theory_name, thm_name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+ (serial, make_thm_node theory_name thm_name prop body no_export);
(* proof atoms *)
@@ -317,11 +318,11 @@
if Intset.member seen i then (x, seen)
else
let
- val name = thm_node_name thm_node;
+ val thm_name = thm_node_name thm_node;
val prop = thm_node_prop thm_node;
val body = Future.join (thm_node_body thm_node);
val (x', seen') = app body (x, Intset.insert i seen);
- in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
+ in (f {serial = i, thm_name = thm_name, prop = prop, body = body} x', seen') end);
in fn bodies => fn x => #1 (fold app bodies (x, Intset.empty)) end;
@@ -341,8 +342,8 @@
| no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
| no_thm_names (prf % t) = no_thm_names prf % t
| no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2
- | no_thm_names (PThm ({serial, pos, theory_name, name = _, prop, types}, thm_body)) =
- PThm (thm_header serial pos theory_name "" prop types, thm_body)
+ | no_thm_names (PThm ({serial, pos, theory_name, thm_name = _, prop, types}, thm_body)) =
+ PThm (thm_header serial pos theory_name Thm_Name.empty prop types, thm_body)
| no_thm_names a = a;
fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
@@ -385,8 +386,8 @@
fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
fn PClass (a, b) => ([b], typ a),
fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
- fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
- ([int_atom serial, theory_name, name],
+ fn PThm ({serial, pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) =>
+ ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)],
pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
(map Position.properties_of pos,
(prop, (types, map_proof_of open_proof (Future.join body)))))]
@@ -394,7 +395,7 @@
triple (list (pair (pair string (properties o Position.properties_of))
(option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
and thm consts (a, thm_node) =
- pair int (pair string (pair string (pair (term consts) (proof_body consts))))
+ pair int (pair string (pair (pair string int) (pair (term consts) (proof_body consts))))
(a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
(Future.join (thm_node_body thm_node))))));
@@ -417,8 +418,8 @@
fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
fn PClass (T, c) => ([c], typ T),
fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
- fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
- ([int_atom serial, theory_name, name], list typ Ts)];
+ fn PThm ({serial, theory_name, thm_name, types = SOME Ts, ...}, _) =>
+ ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)], list typ Ts)];
in
@@ -447,12 +448,12 @@
fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
fn ([b], a) => PClass (typ a, b),
fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
- fn ([a, b, c], d) =>
+ fn ([a, b, c, d], e) =>
let
- val ((e, (f, (g, h)))) =
- pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d;
- val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
- in PThm (header, thm_body h) end]
+ val ((x, (y, (z, w)))) =
+ pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) e;
+ val header = thm_header (int_atom a) (map Position.of_properties x) b (c, int_atom d) y z;
+ in PThm (header, thm_body w) end]
and proof_body consts x =
let
val (a, b, c) =
@@ -462,7 +463,7 @@
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
- pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x
+ pair int (pair string (pair (pair string int) (pair (term consts) (proof_body consts)))) x
in (a, make_thm_node b c d (Future.value e) no_export) end;
in
@@ -556,8 +557,8 @@
| proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
| proof (PClass C) = ofclass C
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
- | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
- PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
+ | proof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) =
+ PThm (thm_header serial pos theory_name thm_name prop (SOME (typs Ts)), thm_body)
| proof _ = raise Same.SAME;
in proof end;
@@ -597,8 +598,8 @@
fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
| change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
| change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
- | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
- PThm (thm_header serial pos theory_name name prop types, thm_body)
+ | change_types types (PThm ({serial, pos, theory_name, thm_name, prop, types = _}, thm_body)) =
+ PThm (thm_header serial pos theory_name thm_name prop types, thm_body)
| change_types _ prf = prf;
@@ -762,8 +763,8 @@
PClass (norm_type_same T, c)
| norm (Oracle (a, prop, Ts)) =
Oracle (a, prop, Same.map_option norm_types_same Ts)
- | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
- PThm (thm_header i p theory_name a t
+ | norm (PThm ({serial = i, pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) =
+ PThm (thm_header i p theory_name thm_name t
(Same.map_option norm_types_same Ts), thm_body)
| norm _ = raise Same.SAME;
in Same.commit norm end;
@@ -1023,8 +1024,8 @@
| proof _ _ (PAxm (a, prop, Ts)) = PAxm (a, prop, typs Ts)
| proof _ _ (PClass (T, c)) = PClass (typ T, c)
| proof _ _ (Oracle (a, prop, Ts)) = Oracle (a, prop, typs Ts)
- | proof _ _ (PThm ({serial, pos, theory_name, name, prop, types}, thm_body)) =
- PThm (thm_header serial pos theory_name name prop (typs types), thm_body)
+ | proof _ _ (PThm ({serial, pos, theory_name, thm_name, prop, types}, thm_body)) =
+ PThm (thm_header serial pos theory_name thm_name prop (typs types), thm_body)
| proof _ _ _ = raise Same.SAME;
val k = length prems;
@@ -1399,8 +1400,8 @@
if c1 = c2 then matchT inst (T1, T2)
else raise PMatch
| mtch Ts i j inst
- (PThm ({name = name1, prop = prop1, types = types1, ...}, _),
- PThm ({name = name2, prop = prop2, types = types2, ...}, _)) =
+ (PThm ({thm_name = name1, prop = prop1, types = types1, ...}, _),
+ PThm ({thm_name = name2, prop = prop2, types = types2, ...}, _)) =
if name1 = name2 andalso prop1 = prop2
then optmatch matchTs inst (types1, types2)
else raise PMatch
@@ -1446,8 +1447,8 @@
| subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
| subst _ _ (PClass (T, c)) = PClass (substT T, c)
| subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
- | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
- PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
+ | subst _ _ (PThm ({serial = i, pos = p, theory_name, thm_name, prop, types}, thm_body)) =
+ PThm (thm_header i p theory_name thm_name prop (Same.map_option substTs types), thm_body)
| subst _ _ _ = raise Same.SAME;
in fn t => subst 0 0 t handle Same.SAME => t end;
@@ -1466,7 +1467,7 @@
| (Hyp (Var _), _) => true
| (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
| (PClass (_, c), PClass (_, d)) => c = d andalso matchrands prf1 prf2
- | (PThm ({name = a, prop = propa, ...}, _), PThm ({name = b, prop = propb, ...}, _)) =>
+ | (PThm ({thm_name = a, prop = propa, ...}, _), PThm ({thm_name = b, prop = propb, ...}, _)) =>
a = b andalso propa = propb andalso matchrands prf1 prf2
| (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
| (AbsP _, _) => true (*because of possible eta equality*)
@@ -1616,12 +1617,12 @@
(fn TVar ((a, i), S) => subst_same (TVar ((a, i - shift), S)) | A => subst_same A);
in Same.commit (map_proof_types_same subst_type_same) prf end;
-fun guess_name (PThm ({name, ...}, _)) = name
+fun guess_name (PThm ({thm_name, ...}, _)) = thm_name
| guess_name (prf %% Hyp _) = guess_name prf
| guess_name (prf %% PClass _) = guess_name prf
| guess_name (prf % NONE) = guess_name prf
| guess_name (prf % SOME (Var _)) = guess_name prf
- | guess_name _ = "";
+ | guess_name _ = Thm_Name.empty;
(* generate constraints for proof term *)
@@ -1733,7 +1734,7 @@
| SOME Ts => (Ts, env));
val prop' = subst_atomic_types (prop_types ~~ Ts)
(forall_intr_variables_term prop) handle ListPair.UnequalLengths =>
- error ("Wrong number of type arguments for " ^ quote (guess_name prf))
+ error ("Wrong number of type arguments for " ^ quote (Thm_Name.short (guess_name prf)))
in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
fun head_norm (prop, prf, cnstrts, env, vTs) =
@@ -1920,7 +1921,8 @@
(* expand and reconstruct subproofs *)
-fun expand_name_empty (header: thm_header) = if #name header = "" then SOME "" else NONE;
+fun expand_name_empty (header: thm_header) =
+ if Thm_Name.is_empty (#thm_name header) then SOME Thm_Name.empty else NONE;
fun expand_proof thy expand_name prf =
let
@@ -1939,10 +1941,10 @@
let val (seen', maxidx', prf') = expand seen maxidx prf
in (seen', maxidx', prf' % t) end
| expand seen maxidx (prf as PThm (header, thm_body)) =
- let val {serial, pos, theory_name, name, prop, types} = header in
+ let val {serial, pos, theory_name, thm_name, prop, types} = header in
(case expand_name header of
- SOME name' =>
- if name' = "" andalso is_some types then
+ SOME thm_name' =>
+ if #1 thm_name' = "" andalso is_some types then
let
val (seen', maxidx', prf') =
(case Inttab.lookup seen serial of
@@ -1959,8 +1961,9 @@
val prf'' = prf'
|> incr_indexes (maxidx + 1) |> app_types (maxidx + 1) prop (the types);
in (seen', maxidx' + maxidx + 1, prf'') end
- else if name' <> name then
- (seen, maxidx, PThm (thm_header serial pos theory_name name' prop types, thm_body))
+ else if thm_name' <> thm_name then
+ (seen, maxidx,
+ PThm (thm_header serial pos theory_name thm_name' prop types, thm_body))
else (seen, maxidx, prf)
| NONE => (seen, maxidx, prf))
end
@@ -2173,7 +2176,7 @@
(name, pos) shyps hyps concl promises
(PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zproof0, proof = proof0}) =
let
- val named = name <> "";
+ val named = not (Thm_Name.is_empty name);
val prop = Logic.list_implies (hyps, concl);
val args = prop_args prop;
@@ -2203,11 +2206,11 @@
if export_enabled () then new_prf ()
else
(case strip_combt (proof_head_of proof0) of
- (PThm ({serial = ser, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
- if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
+ (PThm ({serial = ser, thm_name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+ if (#1 a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
let
val Thm_Body {body = body', ...} = thm_body';
- val i = if a = "" andalso named then serial () else ser;
+ val i = if #1 a = "" andalso named then serial () else ser;
in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
else new_prf ()
| _ => new_prf ());
@@ -2257,7 +2260,7 @@
prepare_thm_proof false thy sorts_proof name shyps hyps concl promises #> #2;
fun unconstrain_thm_proof thy sorts_proof shyps concl promises body =
- prepare_thm_proof true thy sorts_proof ("", Position.none)
+ prepare_thm_proof true thy sorts_proof Thm_Name.none
shyps [] concl promises body;
end;
@@ -2268,14 +2271,14 @@
fun get_identity shyps hyps prop prf =
let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
(case term_head_of (proof_head_of prf) of
- PThm ({serial, theory_name, name, prop = prop', ...}, _) =>
+ PThm ({serial, theory_name, thm_name, prop = prop', ...}, _) =>
if prop = prop'
- then SOME {serial = serial, theory_name = theory_name, name = name} else NONE
+ then SOME {serial = serial, theory_name = theory_name, thm_name = thm_name} else NONE
| _ => NONE)
end;
fun get_approximative_name shyps hyps prop prf =
- Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
+ Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.empty;
(* thm_id *)
@@ -2294,8 +2297,8 @@
fun get_id shyps hyps prop prf : thm_id option =
(case get_identity shyps hyps prop prf of
NONE => NONE
- | SOME {name = "", ...} => NONE
- | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
+ | SOME {serial, theory_name, thm_name, ...} =>
+ if Thm_Name.is_empty thm_name then NONE else SOME (make_thm_id (serial, theory_name)));
fun this_id NONE _ = false
| this_id (SOME (thm_id: thm_id)) (thm_id': thm_id) = #serial thm_id = #serial thm_id';
--- a/src/Pure/term.scala Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/term.scala Fri Jun 07 23:53:31 2024 +0200
@@ -142,8 +142,8 @@
private lazy val hash: Int = ("Oracle", name, prop, types).hashCode()
override def hashCode(): Int = hash
}
- case class PThm(serial: Long, theory_name: String, name: String, types: List[Typ]) extends Proof {
- private lazy val hash: Int = ("PThm", serial, theory_name, name, types).hashCode()
+ case class PThm(serial: Long, theory_name: String, thm_name: Thm_Name, types: List[Typ]) extends Proof {
+ private lazy val hash: Int = ("PThm", serial, theory_name, thm_name, types).hashCode()
override def hashCode(): Int = hash
}
@@ -234,6 +234,10 @@
}
}
+ protected def cache_thm_name(x: Thm_Name): Thm_Name =
+ if (x == Thm_Name.empty) Thm_Name.empty
+ else lookup(x) getOrElse store(Thm_Name(cache_string(x.name), x.index))
+
protected def cache_proof(x: Proof): Proof = {
if (x == MinProof) MinProof
else {
@@ -253,8 +257,9 @@
case PClass(typ, cls) => store(PClass(cache_typ(typ), cache_string(cls)))
case Oracle(name, prop, types) =>
store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
- case PThm(serial, theory_name, name, types) =>
- store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
+ case PThm(serial, theory_name, thm_name, types) =>
+ store(PThm(serial, cache_string(theory_name), cache_thm_name(thm_name),
+ cache_typs(types)))
}
}
}
--- a/src/Pure/term_xml.scala Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/term_xml.scala Fri Jun 07 23:53:31 2024 +0200
@@ -92,7 +92,9 @@
{ case (List(a), b) => PAxm(a, list(typ)(b)) },
{ case (List(a), b) => PClass(typ(b), a) },
{ case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
- { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
+ { case (List(a, b, c, d), e) =>
+ PThm(long_atom(a), b, Thm_Name(c, int_atom(d)), list(typ)(e))
+ }))
proof
}
--- a/src/Pure/thm.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm.ML Fri Jun 07 23:53:31 2024 +0200
@@ -118,11 +118,11 @@
val extra_shyps: thm -> sort list
val strip_shyps: thm -> thm
val derivation_closed: thm -> bool
- val derivation_name: thm -> string
+ val derivation_name: thm -> Thm_Name.T
val derivation_id: thm -> Proofterm.thm_id option
- val raw_derivation_name: thm -> string
- val expand_name: thm -> Proofterm.thm_header -> string option
- val name_derivation: string * Position.T -> thm -> thm
+ val raw_derivation_name: thm -> Thm_Name.T
+ val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option
+ val name_derivation: Thm_Name.P -> thm -> thm
val close_derivation: Position.T -> thm -> thm
val trim_context: thm -> thm
val axiom: theory -> string -> thm
@@ -1130,7 +1130,9 @@
(case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of
NONE => K false
| SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
- fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE;
+ fun expand header =
+ if self_id header orelse Thm_Name.is_empty (#thm_name header)
+ then SOME Thm_Name.empty else NONE;
in expand end;
(*deterministic name of finished proof*)
@@ -1166,7 +1168,7 @@
fun close_derivation pos =
solve_constraints #> (fn thm =>
if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
- else name_derivation ("", pos) thm);
+ else name_derivation (Thm_Name.empty, pos) thm);
val trim_context = solve_constraints #> trim_context_thm;
--- a/src/Pure/thm_deps.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm_deps.ML Fri Jun 07 23:53:31 2024 +0200
@@ -12,7 +12,7 @@
val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
val pretty_thm_deps: theory -> thm list -> Pretty.T
- val unused_thms_cmd: theory list * theory list -> (string * thm) list
+ val unused_thms_cmd: theory list * theory list -> (Thm_Name.T * thm) list
end;
structure Thm_Deps: THM_DEPS =
@@ -96,9 +96,8 @@
else
let val {concealed, group, ...} = Name_Space.the_entry space name in
fold_rev (transfer #> (fn th =>
- (case Thm.derivation_name th of
- "" => I
- | a => cons (a, (th, concealed, group))))) ths
+ let val a = Thm.derivation_name th
+ in if Thm_Name.is_empty a then I else cons (a, (th, concealed, group)) end)) ths
end;
fun add_facts thy =
let
@@ -108,15 +107,15 @@
val new_thms =
fold add_facts thys []
- |> sort_distinct (string_ord o apply2 #1);
+ |> sort_distinct (Thm_Name.ord o apply2 #1);
val used =
Proofterm.fold_body_thms
- (fn {name = a, ...} => a <> "" ? Symset.insert a)
+ (fn {thm_name = a, ...} => not (Thm_Name.is_empty a) ? Thm_Name.Set.insert a)
(map Proofterm.strip_thm_body (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
- Symset.empty;
+ Thm_Name.Set.empty;
- fun is_unused a = not (Symset.member used a);
+ fun is_unused a = not (Thm_Name.Set.member used a);
(*groups containing at least one used theorem*)
val used_groups =
--- a/src/Pure/thm_name.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm_name.ML Fri Jun 07 23:53:31 2024 +0200
@@ -11,10 +11,14 @@
sig
type T = string * int
val ord: T ord
+ structure Set: SET
+ structure Table: TABLE
+ val empty: T
+ val is_empty: T -> bool
+ val print: T -> string
+ val short: T -> string
type P = T * Position.T
val none: P
- val print: T -> string
- val short: P -> string * Position.T
val list: string * Position.T -> 'a list -> (P * 'a) list
val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
end;
@@ -25,19 +29,27 @@
type T = string * int;
val ord = prod_ord string_ord int_ord;
-type P = T * Position.T;
+structure Set = Set(type key = T val ord = ord);
+structure Table = Table(Set.Key);
-val none: P = (("", 0), Position.none);
+val empty: T = ("", 0);
+fun is_empty ((a, _): T) = a = "";
fun print (name, index) =
if name = "" orelse index = 0 then name
else name ^ enclose "(" ")" (string_of_int index);
-fun short (((name, index), pos): P) =
- if name = "" orelse index = 0 then (name, pos)
- else (name ^ "_" ^ string_of_int index, pos);
+fun short (name, index) =
+ if name = "" orelse index = 0 then name
+ else name ^ "_" ^ string_of_int index;
+
+
+type P = T * Position.T;
+
+val none: P = (empty, Position.none);
fun list (name, pos) [thm] = [(((name, 0), pos): P, thm)]
+ | list ("", pos) thms = map (fn thm => ((empty, pos), thm)) thms
| list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
fun expr name = burrow_fst (burrow (list name));
--- a/src/Pure/thm_name.scala Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm_name.scala Fri Jun 07 23:53:31 2024 +0200
@@ -23,6 +23,8 @@
private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r
+ val empty: Thm_Name = Thm_Name("", 0)
+
def parse(s: String): Thm_Name =
s match {
case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
@@ -31,6 +33,8 @@
}
sealed case class Thm_Name(name: String, index: Int) {
+ def is_empty: Boolean = name.isEmpty
+
def print: String =
if (name == "" || index == 0) name
else name + "(" + index + ")"