--- a/src/Pure/Proof/extraction.ML Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Mon Aug 19 21:37:34 2019 +0200
@@ -622,7 +622,7 @@
val corr_prf = mkabsp shyps corr_prf0;
val corr_prop = Proofterm.prop_of corr_prf;
val corr_header =
- Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
+ Proofterm.thm_header (serial ()) pos theory_name
(corr_name name vs') corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf);
@@ -743,7 +743,7 @@
SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Proofterm.prop_of corr_prf';
val corr_header =
- Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
+ Proofterm.thm_header (serial ()) pos theory_name
(corr_name s vs') corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf');
--- a/src/Pure/ROOT.ML Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/ROOT.ML Mon Aug 19 21:37:34 2019 +0200
@@ -175,6 +175,7 @@
ML_file "more_thm.ML";
ML_file "facts.ML";
+ML_file "thm_name.ML";
ML_file "global_theory.ML";
ML_file "pure_thy.ML";
ML_file "drule.ML";
--- a/src/Pure/Thy/export_theory.ML Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML Mon Aug 19 21:37:34 2019 +0200
@@ -218,7 +218,7 @@
(#constants (Consts.dest (Sign.consts_of thy)));
- (* axioms and facts *)
+ (* axioms *)
fun standard_prop used extra_shyps raw_prop raw_proof =
let
@@ -236,12 +236,26 @@
fun encode_axiom used prop =
encode_prop (#1 (standard_prop used [] prop NONE));
+ val _ =
+ export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
+ Theory.axiom_space (Theory.axioms_of thy);
+
+
+ (* theorems *)
+
val clean_thm =
Thm.transfer thy
#> Thm.check_hyps (Context.Theory thy)
#> Thm.strip_shyps;
- val encode_fact = clean_thm #> (fn thm =>
+ fun entity_markup_thm (serial, (name, i)) =
+ let
+ val space = Facts.space_of (Global_Theory.facts_of thy);
+ val xname = Name_Space.extern_shortest thy_ctxt space name;
+ val {pos, ...} = Name_Space.the_entry space name;
+ in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
+
+ val encode_thm = clean_thm #> (fn thm =>
standard_prop Name.context
(Thm.extra_shyps thm)
(Thm.full_prop_of thm)
@@ -249,13 +263,16 @@
let open XML.Encode Term_XML.Encode
in pair encode_prop (option Proofterm.encode_full) end);
- val _ =
- export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
- Theory.axiom_space (Theory.axioms_of thy);
- val _ =
- export_entities "facts" (K (SOME o XML.Encode.list encode_fact))
- (Facts.space_of o Global_Theory.facts_of)
- (Facts.dest_static true [] (Global_Theory.facts_of thy));
+ fun export_thms thms =
+ let val elems =
+ thms |> map (fn (serial, thm_name) =>
+ let
+ val markup = entity_markup_thm (serial, thm_name);
+ val body = encode_thm (Global_Theory.get_thm_name thy (thm_name, Position.none));
+ in XML.Elem (markup, body) end)
+ in if null elems then () else export_body thy "thms" elems end;
+
+ val _ = export_thms (Global_Theory.dest_thm_names thy);
(* type classes *)
--- a/src/Pure/Thy/export_theory.scala Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala Mon Aug 19 21:37:34 2019 +0200
@@ -28,7 +28,7 @@
types: Boolean = true,
consts: Boolean = true,
axioms: Boolean = true,
- facts: Boolean = true,
+ thms: Boolean = true,
classes: Boolean = true,
locales: Boolean = true,
locale_dependencies: Boolean = true,
@@ -44,7 +44,7 @@
Export.read_theory_names(db, session_name).map((theory_name: String) =>
read_theory(Export.Provider.database(db, session_name, theory_name),
session_name, theory_name, types = types, consts = consts,
- axioms = axioms, facts = facts, classes = classes, locales = locales,
+ axioms = axioms, thms = thms, classes = classes, locales = locales,
locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
typedefs = typedefs, cache = Some(cache)))
}
@@ -70,8 +70,8 @@
sealed case class Theory(name: String, parents: List[String],
types: List[Type],
consts: List[Const],
- axioms: List[Fact_Single],
- facts: List[Fact_Multi],
+ axioms: List[Axiom],
+ thms: List[Thm],
classes: List[Class],
locales: List[Locale],
locale_dependencies: List[Locale_Dependency],
@@ -86,7 +86,7 @@
types.iterator.map(_.entity.serial) ++
consts.iterator.map(_.entity.serial) ++
axioms.iterator.map(_.entity.serial) ++
- facts.iterator.map(_.entity.serial) ++
+ thms.iterator.map(_.entity.serial) ++
classes.iterator.map(_.entity.serial) ++
locales.iterator.map(_.entity.serial) ++
locale_dependencies.iterator.map(_.entity.serial)
@@ -97,7 +97,7 @@
types.map(_.cache(cache)),
consts.map(_.cache(cache)),
axioms.map(_.cache(cache)),
- facts.map(_.cache(cache)),
+ thms.map(_.cache(cache)),
classes.map(_.cache(cache)),
locales.map(_.cache(cache)),
locale_dependencies.map(_.cache(cache)),
@@ -113,7 +113,7 @@
types: Boolean = true,
consts: Boolean = true,
axioms: Boolean = true,
- facts: Boolean = true,
+ thms: Boolean = true,
classes: Boolean = true,
locales: Boolean = true,
locale_dependencies: Boolean = true,
@@ -134,7 +134,7 @@
if (types) read_types(provider) else Nil,
if (consts) read_consts(provider) else Nil,
if (axioms) read_axioms(provider) else Nil,
- if (facts) read_facts(provider) else Nil,
+ if (thms) read_thms(provider) else Nil,
if (classes) read_classes(provider) else Nil,
if (locales) read_locales(provider) else Nil,
if (locale_dependencies) read_locale_dependencies(provider) else Nil,
@@ -166,7 +166,7 @@
val TYPE = Value("type")
val CONST = Value("const")
val AXIOM = Value("axiom")
- val FACT = Value("fact")
+ val THM = Value("thm")
val CLASS = Value("class")
val LOCALE = Value("locale")
val LOCALE_DEPENDENCY = Value("locale_dependency")
@@ -285,7 +285,7 @@
})
- /* axioms and facts */
+ /* axioms */
sealed case class Prop(
typargs: List[(String, Term.Sort)],
@@ -310,62 +310,40 @@
Prop(typargs, args, t)
}
-
- sealed case class Fact(prop: Prop, proof: Option[Term.Proof])
+ sealed case class Axiom(entity: Entity, prop: Prop)
{
- def cache(cache: Term.Cache): Fact =
- Fact(prop.cache(cache), proof.map(cache.proof _))
- }
-
- def decode_fact(body: XML.Body): Fact =
- {
- val (prop, proof) =
- {
- import XML.Decode._
- pair(decode_prop _, option(Term_XML.Decode.proof))(body)
- }
- Fact(prop, proof)
+ def cache(cache: Term.Cache): Axiom =
+ Axiom(entity.cache(cache), prop.cache(cache))
}
- sealed case class Fact_Single(entity: Entity, fact: Fact)
- {
- def cache(cache: Term.Cache): Fact_Single =
- Fact_Single(entity.cache(cache), fact.cache(cache))
-
- def prop: Prop = fact.prop
- def proof: Option[Term.Proof] = fact.proof
- }
-
- sealed case class Fact_Multi(entity: Entity, facts: List[Fact])
- {
- def cache(cache: Term.Cache): Fact_Multi =
- Fact_Multi(entity.cache(cache), facts.map(_.cache(cache)))
-
- def props: List[Prop] = facts.map(_.prop)
-
- def split: List[Fact_Single] =
- facts match {
- case List(fact) => List(Fact_Single(entity, fact))
- case _ =>
- for ((fact, i) <- facts.zipWithIndex)
- yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), fact)
- }
- }
-
- def read_axioms(provider: Export.Provider): List[Fact_Single] =
+ def read_axioms(provider: Export.Provider): List[Axiom] =
provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.AXIOM, tree)
val prop = decode_prop(body)
- Fact_Single(entity, Fact(prop, None))
+ Axiom(entity, prop)
})
- def read_facts(provider: Export.Provider): List[Fact_Multi] =
- provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
+
+ /* theorems */
+
+ sealed case class Thm(entity: Entity, prop: Prop, proof: Option[Term.Proof])
+ {
+ def cache(cache: Term.Cache): Thm =
+ Thm(entity.cache(cache), prop.cache(cache), proof.map(cache.proof _))
+ }
+
+ def read_thms(provider: Export.Provider): List[Thm] =
+ provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
{
- val (entity, body) = decode_entity(Kind.FACT, tree)
- val facts = XML.Decode.list(decode_fact)(body)
- Fact_Multi(entity, facts)
+ val (entity, body) = decode_entity(Kind.THM, tree)
+ val (prop, prf) =
+ {
+ import XML.Decode._
+ import Term_XML.Decode._
+ pair(decode_prop _, option(proof))(body)
+ }
+ Thm(entity, prop, prf)
})
def read_proof(
--- a/src/Pure/build-jars Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/build-jars Mon Aug 19 21:37:34 2019 +0200
@@ -171,6 +171,7 @@
pure_thy.scala
term.scala
term_xml.scala
+ thm_name.scala
../Tools/Graphview/graph_file.scala
../Tools/Graphview/graph_panel.scala
../Tools/Graphview/graphview.scala
--- a/src/Pure/facts.ML Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/facts.ML Mon Aug 19 21:37:34 2019 +0200
@@ -6,6 +6,8 @@
signature FACTS =
sig
+ val err_selection: string * Position.T -> int -> thm list -> 'a
+ val err_single: string * Position.T -> thm list -> 'a
val the_single: string * Position.T -> thm list -> thm
datatype interval = FromTo of int * int | From of int | Single of int
datatype ref =
@@ -44,12 +46,6 @@
val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
- type thm_name = string * int
- val thm_name_ord: thm_name * thm_name -> order
- val thm_name_print: thm_name -> string
- val thm_name_flat: thm_name -> string
- val thm_name_list: string -> thm list -> (thm_name * thm) list
- val get_thm: Context.generic -> T -> thm_name * Position.T -> thm
end;
structure Facts: FACTS =
@@ -60,13 +56,13 @@
fun length_msg (thms: thm list) pos =
" (length " ^ string_of_int (length thms) ^ ")" ^ Position.here pos;
-fun err_single (name, pos) thms =
- error ("Expected singleton fact " ^ quote name ^ length_msg thms pos);
-
fun err_selection (name, pos) i thms =
error ("Bad fact selection " ^ quote (name ^ enclose "(" ")" (string_of_int i)) ^
length_msg thms pos);
+fun err_single (name, pos) thms =
+ error ("Expected singleton fact " ^ quote name ^ length_msg thms pos);
+
fun the_single _ [thm] = thm
| the_single name_pos thms = err_single name_pos thms;
@@ -300,36 +296,4 @@
fun hide fully name (Facts {facts, props}) =
make_facts (Name_Space.hide_table fully name facts) props;
-
-
-(** get individual theorems **)
-
-type thm_name = string * int;
-val thm_name_ord = prod_ord string_ord int_ord;
-
-fun thm_name_print (name, i) =
- if name = "" orelse i = 0 then name
- else name ^ enclose "(" ")" (string_of_int i);
-
-fun thm_name_flat (name, i) =
- if name = "" orelse i = 0 then name
- else name ^ "_" ^ string_of_int i;
-
-fun thm_name_list name [thm: thm] = [((name, 0), thm)]
- | thm_name_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
-
-fun get_thm context facts ((name, i), pos) =
- let
- fun print_name () =
- markup_extern (Context.proof_of context) facts name |-> Markup.markup;
- in
- (case (lookup context facts name, i) of
- (NONE, _) => error ("Undefined fact " ^ quote (print_name ()) ^ Position.here pos)
- | (SOME {thms = [thm], ...}, 0) => thm
- | (SOME {thms, ...}, 0) => err_single (print_name (), pos) thms
- | (SOME {thms, ...}, _) =>
- if i > 0 andalso i <= length thms then nth thms (i - 1)
- else err_selection (print_name (), pos) i thms)
- end;
-
end;
--- a/src/Pure/global_theory.ML Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/global_theory.ML Mon Aug 19 21:37:34 2019 +0200
@@ -12,14 +12,15 @@
val defined_fact: theory -> string -> bool
val alias_fact: binding -> string -> theory -> theory
val hide_fact: bool -> string -> theory -> theory
- val dest_thms: bool -> theory list -> theory -> (Facts.thm_name * thm) list
- val dest_thm_names: theory -> (proof_serial * Facts.thm_name) list
- val lookup_thm_id: theory -> Proofterm.thm_id -> Facts.thm_name option
- val lookup_thm: theory -> thm -> Facts.thm_name option
+ val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
+ val dest_thm_names: theory -> (serial * Thm_Name.T) list
+ val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
+ val lookup_thm: theory -> thm -> Thm_Name.T option
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 get_thm_name: theory -> Thm_Name.T * Position.T -> thm
val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
val burrow_facts: ('a list -> 'b list) ->
('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
@@ -59,7 +60,7 @@
structure Data = Theory_Data
(
- type T = Facts.T * Facts.thm_name Inttab.table lazy option;
+ type T = Facts.T * Thm_Name.T Inttab.table lazy option;
val empty: T = (Facts.empty, NONE);
fun extend (facts, _) = (facts, NONE);
fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE);
@@ -82,7 +83,7 @@
fun dest_thms verbose prev_thys thy =
Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy)
- |> maps (uncurry Facts.thm_name_list);
+ |> maps (uncurry Thm_Name.make_list);
(* thm_name vs. derivation_id *)
@@ -102,8 +103,8 @@
(case Inttab.lookup thm_names serial of
SOME thm_name' =>
raise THM ("Duplicate use of derivation identity for " ^
- Facts.thm_name_print thm_name ^ " vs. " ^
- Facts.thm_name_print thm_name', 0, [thm])
+ Thm_Name.print thm_name ^ " vs. " ^
+ Thm_Name.print thm_name', 0, [thm])
| NONE => Inttab.update (serial, thm_name) thm_names)));
fun get_thm_names thy =
@@ -166,6 +167,21 @@
else append (map (`(Thm.get_name_hint) o transfer) ths);
in Facts.fold_static add facts [] end;
+fun get_thm_name thy ((name, i), pos) =
+ let
+ val facts = facts_of thy;
+ fun print_name () =
+ Facts.markup_extern (Proof_Context.init_global thy) facts name |-> Markup.markup;
+ in
+ (case (Facts.lookup (Context.Theory thy) facts name, i) of
+ (NONE, _) => error ("Undefined fact " ^ quote (print_name ()) ^ Position.here pos)
+ | (SOME {thms = [thm], ...}, 0) => thm
+ | (SOME {thms, ...}, 0) => Facts.err_single (print_name (), pos) thms
+ | (SOME {thms, ...}, _) =>
+ if i > 0 andalso i <= length thms then nth thms (i - 1)
+ else Facts.err_selection (print_name (), pos) i thms)
+ end;
+
(** store theorems **)
@@ -201,7 +217,7 @@
end;
fun name_multi (name, pos) =
- Facts.thm_name_list name #> (map o apfst) (fn thm_name => (Facts.thm_name_flat thm_name, pos));
+ Thm_Name.make_list name #> (map o apfst) (fn thm_name => (Thm_Name.flatten thm_name, pos));
fun name_thms name_flags name_pos =
name_multi name_pos #> map (uncurry (name_thm name_flags));
--- a/src/Pure/proofterm.ML Mon Aug 19 18:41:03 2019 +0200
+++ b/src/Pure/proofterm.ML Mon Aug 19 21:37:34 2019 +0200
@@ -6,12 +6,11 @@
infix 8 % %% %>;
-signature BASIC_PROOFTERM =
+signature PROOFTERM =
sig
type thm_node
- type proof_serial = int
type thm_header =
- {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
+ {serial: serial, pos: Position.T list, theory_name: string, name: string,
prop: term, types: typ list option}
type thm_body
datatype proof =
@@ -28,21 +27,16 @@
| PThm of thm_header * thm_body
and proof_body = PBody of
{oracles: (string * term option) Ord_List.T,
- thms: (proof_serial * thm_node) Ord_List.T,
+ thms: (serial * thm_node) Ord_List.T,
proof: proof}
val %> : proof * term -> proof
-end;
-
-signature PROOFTERM =
-sig
- include BASIC_PROOFTERM
val proofs: int Unsynchronized.ref
exception MIN_PROOF
- type pthm = proof_serial * thm_node
+ type pthm = serial * thm_node
type oracle = string * term option
val proof_of: proof_body -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
- val thm_header: proof_serial -> Position.T list -> string -> string -> term -> typ list option ->
+ val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
thm_header
val thm_body: proof_body -> thm_body
val thm_body_proof_raw: thm_body -> proof
@@ -53,7 +47,7 @@
val join_proof: proof_body future -> proof
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
val fold_body_thms:
- ({serial: proof_serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
+ ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a
val consolidate: proof_body list -> unit
@@ -168,7 +162,6 @@
val standard_vars: Name.context -> term * proof option -> term * proof option
val standard_vars_term: Name.context -> term -> term
- val proof_serial: unit -> proof_serial
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> (class * class -> proof) ->
(string * class list list * class -> proof) -> string * Position.T -> sort list ->
@@ -177,7 +170,7 @@
(string * class list list * class -> proof) -> sort list -> term ->
(serial * proof_body future) list -> proof_body -> pthm * proof
val get_approximative_name: sort list -> term list -> term -> proof -> string
- type thm_id = {serial: proof_serial, theory_name: string}
+ type thm_id = {serial: serial, theory_name: string}
val get_id: sort list -> term list -> term -> proof -> thm_id option
end
@@ -186,10 +179,8 @@
(** datatype proof **)
-type proof_serial = int;
-
type thm_header =
- {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
+ {serial: serial, pos: Position.T list, theory_name: string, name: string,
prop: term, types: typ list option};
datatype proof =
@@ -206,7 +197,7 @@
| PThm of thm_header * thm_body
and proof_body = PBody of
{oracles: (string * term option) Ord_List.T,
- thms: (proof_serial * thm_node) Ord_List.T,
+ thms: (serial * thm_node) Ord_List.T,
proof: proof}
and thm_body =
Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future}
@@ -218,7 +209,7 @@
type oracle = string * term option;
val oracle_prop = the_default Term.dummy;
-type pthm = proof_serial * thm_node;
+type pthm = serial * thm_node;
fun proof_of (PBody {proof, ...}) = proof;
val join_proof = Future.join #> proof_of;
@@ -302,11 +293,11 @@
let
fun collect (PBody {oracles, thms, ...}) =
(if null oracles then I else apfst (cons oracles)) #>
- (tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
- if Inttab.defined seen i then (x, seen)
+ (tap join_thms thms |> fold (fn (i, thm_node) => fn (res, seen) =>
+ if Inttab.defined seen i then (res, seen)
else
let val body = Future.join (thm_node_body thm_node)
- in collect body (x, Inttab.update (i, ()) seen) end));
+ in collect body (res, Inttab.update (i, ()) seen) end));
in fold collect bodies ([], Inttab.empty) |> #1 |> unions_oracles end;
fun approximate_proof_body prf =
@@ -2067,8 +2058,6 @@
(* PThm nodes *)
-val proof_serial = Counter.make ();
-
local
fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) =
@@ -2156,7 +2145,7 @@
fun new_prf () =
let
- val i = proof_serial ();
+ val i = serial ();
val unconstrainT =
unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
val postproc = map_proof_of unconstrainT #> named ? publish i;
@@ -2165,12 +2154,12 @@
val (i, body') =
(*non-deterministic, depends on unknown promises*)
(case strip_combt (fst (strip_combP prf)) of
- (PThm ({serial, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+ (PThm ({serial = ser, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
if (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 proof_serial () else serial;
- in (i, body' |> serial <> i ? Future.map (publish i)) end
+ val i = if a = "" andalso named then serial () else ser;
+ in (i, body' |> ser <> i ? Future.map (publish i)) end
else new_prf ()
| _ => new_prf ());
@@ -2218,7 +2207,7 @@
Option.map #name (get_identity shyps hyps prop prf) |> the_default "";
-type thm_id = {serial: proof_serial, theory_name: string};
+type thm_id = {serial: serial, theory_name: string};
fun get_id shyps hyps prop prf : thm_id option =
(case get_identity shyps hyps prop prf of
@@ -2228,5 +2217,11 @@
end;
-structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
+structure Basic_Proofterm =
+struct
+ datatype proof = datatype Proofterm.proof
+ datatype proof_body = datatype Proofterm.proof_body
+ val op %> = Proofterm.%>
+end;
+
open Basic_Proofterm;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/thm_name.ML Mon Aug 19 21:37:34 2019 +0200
@@ -0,0 +1,36 @@
+(* Title: Pure/thm_name.ML
+ Author: Makarius
+
+Systematic naming of individual theorems, as selections from multi-facts.
+
+ (NAME, 0): the single entry of a singleton fact NAME
+ (NAME, i): entry i of a non-singleton fact (1 <= i <= length)
+*)
+
+signature THM_NAME =
+sig
+ type T = string * int
+ val ord: T * T -> order
+ val print: T -> string
+ val flatten: T -> string
+ val make_list: string -> thm list -> (T * thm) list
+end;
+
+structure Thm_Name: THM_NAME =
+struct
+
+type T = string * int;
+val ord = prod_ord string_ord int_ord;
+
+fun print (name, index) =
+ if name = "" orelse index = 0 then name
+ else name ^ enclose "(" ")" (string_of_int index);
+
+fun flatten (name, index) =
+ if name = "" orelse index = 0 then name
+ else name ^ "_" ^ string_of_int index;
+
+fun make_list name [thm: thm] = [((name, 0), thm)]
+ | make_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/thm_name.scala Mon Aug 19 21:37:34 2019 +0200
@@ -0,0 +1,44 @@
+/* Title: Pure/thm_name.scala
+ Author: Makarius
+
+Systematic naming of individual theorems, as selections from multi-facts.
+*/
+
+package isabelle
+
+
+import scala.math.Ordering
+
+
+object Thm_Name
+{
+ object Ordering extends scala.math.Ordering[Thm_Name]
+ {
+ def compare(thm_name1: Thm_Name, thm_name2: Thm_Name): Int =
+ thm_name1.name compare thm_name2.name match {
+ case 0 => thm_name1.index compare thm_name2.index
+ case ord => ord
+ }
+ }
+
+ def graph[A]: Graph[Thm_Name, A] = Graph.empty(Ordering)
+
+ private val Thm_Name_Regex = """^(.)+\((\d+)\)$""".r
+
+ def parse(s: String): Thm_Name =
+ s match {
+ case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
+ case _ => Thm_Name(s, 0)
+ }
+}
+
+sealed case class Thm_Name(name: String, index: Int)
+{
+ def print: String =
+ if (name == "" || index == 0) name
+ else name + "(" + index + ")"
+
+ def flatten: String =
+ if (name == "" || index == 0) name
+ else name + "_" + index
+}