author | wenzelm |
Fri, 07 Jun 2024 23:53:31 +0200 | |
changeset 80295 | 8a9588ffc133 |
parent 80289 | 40a6a6ac1669 |
child 80296 | a1162cbda70c |
permissions | -rw-r--r-- |
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 |
80295
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
14 |
structure Set: SET |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
15 |
structure Table: TABLE |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
16 |
val empty: T |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
17 |
val is_empty: T -> bool |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
18 |
val print: T -> string |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
19 |
val short: T -> string |
80289 | 20 |
type P = T * Position.T |
21 |
val none: P |
|
22 |
val list: string * Position.T -> 'a list -> (P * 'a) list |
|
23 |
val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list |
|
70574 | 24 |
end; |
25 |
||
26 |
structure Thm_Name: THM_NAME = |
|
27 |
struct |
|
28 |
||
29 |
type T = string * int; |
|
30 |
val ord = prod_ord string_ord int_ord; |
|
31 |
||
80295
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
32 |
structure Set = Set(type key = T val ord = ord); |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
33 |
structure Table = Table(Set.Key); |
80289 | 34 |
|
80295
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
35 |
val empty: T = ("", 0); |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
36 |
fun is_empty ((a, _): T) = a = ""; |
80286 | 37 |
|
70575 | 38 |
fun print (name, index) = |
39 |
if name = "" orelse index = 0 then name |
|
40 |
else name ^ enclose "(" ")" (string_of_int index); |
|
70574 | 41 |
|
80295
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
42 |
fun short (name, index) = |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
43 |
if name = "" orelse index = 0 then name |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
44 |
else name ^ "_" ^ string_of_int index; |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
45 |
|
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
46 |
|
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
47 |
type P = T * Position.T; |
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
48 |
|
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
49 |
val none: P = (empty, Position.none); |
70574 | 50 |
|
80289 | 51 |
fun list (name, pos) [thm] = [(((name, 0), pos): P, thm)] |
80295
8a9588ffc133
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
wenzelm
parents:
80289
diff
changeset
|
52 |
| list ("", pos) thms = map (fn thm => ((empty, pos), thm)) thms |
79371 | 53 |
| list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms; |
70574 | 54 |
|
79377 | 55 |
fun expr name = burrow_fst (burrow (list name)); |
79372 | 56 |
|
70574 | 57 |
end; |