70574
|
1 |
(* Title: Pure/thm_name.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Systematic naming of individual theorems, as selections from multi-facts.
|
|
5 |
|
|
6 |
(NAME, 0): the single entry of a singleton fact NAME
|
|
7 |
(NAME, i): entry i of a non-singleton fact (1 <= i <= length)
|
|
8 |
*)
|
|
9 |
|
|
10 |
signature THM_NAME =
|
|
11 |
sig
|
|
12 |
type T = string * int
|
70586
|
13 |
val ord: T ord
|
80289
|
14 |
type P = T * Position.T
|
|
15 |
val none: P
|
70574
|
16 |
val print: T -> string
|
80289
|
17 |
val short: P -> string * Position.T
|
|
18 |
val list: string * Position.T -> 'a list -> (P * 'a) list
|
|
19 |
val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
|
70574
|
20 |
end;
|
|
21 |
|
|
22 |
structure Thm_Name: THM_NAME =
|
|
23 |
struct
|
|
24 |
|
|
25 |
type T = string * int;
|
|
26 |
val ord = prod_ord string_ord int_ord;
|
|
27 |
|
80289
|
28 |
type P = T * Position.T;
|
|
29 |
|
|
30 |
val none: P = (("", 0), Position.none);
|
80286
|
31 |
|
70575
|
32 |
fun print (name, index) =
|
|
33 |
if name = "" orelse index = 0 then name
|
|
34 |
else name ^ enclose "(" ")" (string_of_int index);
|
70574
|
35 |
|
80289
|
36 |
fun short (((name, index), pos): P) =
|
79358
|
37 |
if name = "" orelse index = 0 then (name, pos)
|
|
38 |
else (name ^ "_" ^ string_of_int index, pos);
|
70574
|
39 |
|
80289
|
40 |
fun list (name, pos) [thm] = [(((name, 0), pos): P, thm)]
|
79371
|
41 |
| list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
|
70574
|
42 |
|
79377
|
43 |
fun expr name = burrow_fst (burrow (list name));
|
79372
|
44 |
|
70574
|
45 |
end;
|