|
1 (* Title: Pure/Tools/named_theorems.ML |
|
2 Author: Makarius |
|
3 |
|
4 Named collections of theorems in canonical order. |
|
5 *) |
|
6 |
|
7 signature NAMED_THEOREMS = |
|
8 sig |
|
9 val member: Proof.context -> string -> thm -> bool |
|
10 val get: Proof.context -> string -> thm list |
|
11 val add_thm: string -> thm -> Context.generic -> Context.generic |
|
12 val del_thm: string -> thm -> Context.generic -> Context.generic |
|
13 val add: string -> attribute |
|
14 val del: string -> attribute |
|
15 val declare: binding -> string -> theory -> string * theory |
|
16 end; |
|
17 |
|
18 structure Named_Theorems: NAMED_THEOREMS = |
|
19 struct |
|
20 |
|
21 (* context data *) |
|
22 |
|
23 structure Data = Generic_Data |
|
24 ( |
|
25 type T = thm Item_Net.T Symtab.table; |
|
26 val empty: T = Symtab.empty; |
|
27 val extend = I; |
|
28 val merge = Symtab.join (K Item_Net.merge); |
|
29 ); |
|
30 |
|
31 fun new_entry name = |
|
32 Data.map (fn data => |
|
33 if Symtab.defined data name |
|
34 then error ("Duplicate declaration of named theorems: " ^ quote name) |
|
35 else Symtab.update (name, Thm.full_rules) data); |
|
36 |
|
37 fun the_entry context name = |
|
38 (case Symtab.lookup (Data.get context) name of |
|
39 NONE => error ("Undeclared named theorems " ^ quote name) |
|
40 | SOME entry => entry); |
|
41 |
|
42 fun map_entry name f context = |
|
43 (the_entry context name; Data.map (Symtab.map_entry name f) context); |
|
44 |
|
45 |
|
46 (* maintain content *) |
|
47 |
|
48 fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt); |
|
49 |
|
50 fun content context = rev o Item_Net.content o the_entry context; |
|
51 val get = content o Context.Proof; |
|
52 |
|
53 fun add_thm name = map_entry name o Item_Net.update; |
|
54 fun del_thm name = map_entry name o Item_Net.remove; |
|
55 |
|
56 val add = Thm.declaration_attribute o add_thm; |
|
57 val del = Thm.declaration_attribute o del_thm; |
|
58 |
|
59 |
|
60 (* declaration *) |
|
61 |
|
62 fun declare binding descr thy = |
|
63 let |
|
64 (* FIXME proper result from Global_Theory.add_thms_dynamic *) |
|
65 val naming = Name_Space.naming_of (Context.Theory thy); |
|
66 val name = Name_Space.full_name naming binding; |
|
67 |
|
68 val thy' = thy |
|
69 |> Global_Theory.add_thms_dynamic (binding, fn context => content context name); |
|
70 |
|
71 val description = |
|
72 "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); |
|
73 val thy'' = thy' |
|
74 |> Context.theory_map (new_entry name) |
|
75 |> Attrib.setup binding (Attrib.add_del (add name) (del name)) description; |
|
76 in (name, thy'') end; |
|
77 |
|
78 val _ = |
|
79 Outer_Syntax.command @{command_spec "named_theorems"} |
|
80 "declare named collection of theorems" |
|
81 (Parse.binding -- Scan.optional Parse.text "" |
|
82 >> (fn (binding, descr) => Toplevel.theory (snd o declare binding descr))); |
|
83 |
|
84 |
|
85 (* ML antiquotation *) |
|
86 |
|
87 val _ = Theory.setup |
|
88 (ML_Antiquotation.inline @{binding named_theorems} |
|
89 (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (xname, pos)) => |
|
90 let |
|
91 val thy = Proof_Context.theory_of ctxt; |
|
92 val name = Global_Theory.check_fact thy (xname, pos); |
|
93 val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos); |
|
94 in ML_Syntax.print_string name end))); |
|
95 |
|
96 end; |