1(*  Title:      Pure/Tools/named_theorems.ML
2    Author:     Makarius
3
4Named collections of theorems in canonical order.
5*)
6
7signature NAMED_THEOREMS =
8sig
9  val member: Proof.context -> string -> thm -> bool
10  val get: Proof.context -> string -> thm list
11  val clear: string -> Context.generic -> Context.generic
12  val add_thm: string -> thm -> Context.generic -> Context.generic
13  val del_thm: string -> thm -> Context.generic -> Context.generic
14  val add: string -> attribute
15  val del: string -> attribute
16  val check: Proof.context -> string * Position.T -> string
17  val declare: binding -> string -> local_theory -> string * local_theory
18end;
19
20structure Named_Theorems: NAMED_THEOREMS =
21struct
22
23(* context data *)
24
25structure Data = Generic_Data
26(
27  type T = thm Item_Net.T Symtab.table;
28  val empty: T = Symtab.empty;
29  val extend = I;
30  val merge : T * T -> T = Symtab.join (K Item_Net.merge);
31);
32
33fun new_entry name =
34  Data.map (fn data =>
35    if Symtab.defined data name
36    then error ("Duplicate declaration of named theorems: " ^ quote name)
37    else Symtab.update (name, Thm.full_rules) data);
38
39fun undeclared name = "Undeclared named theorems " ^ quote name;
40
41val defined_entry = Symtab.defined o Data.get;
42
43fun the_entry context name =
44  (case Symtab.lookup (Data.get context) name of
45    NONE => error (undeclared name)
46  | SOME entry => entry);
47
48fun map_entry name f context =
49  (the_entry context name; Data.map (Symtab.map_entry name f) context);
50
51
52(* maintain content *)
53
54fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt);
55
56fun content context =
57  rev o map (Thm.transfer'' context) o Item_Net.content o the_entry context;
58
59val get = content o Context.Proof;
60
61fun clear name = map_entry name (K Thm.full_rules);
62
63fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
64fun del_thm name = map_entry name o Item_Net.remove;
65
66val add = Thm.declaration_attribute o add_thm;
67val del = Thm.declaration_attribute o del_thm;
68
69
70(* check *)
71
72fun check ctxt (xname, pos) =
73  let
74    val context = Context.Proof ctxt;
75    val fact_ref = Facts.Named ((xname, Position.none), NONE);
76    fun err () =
77      let
78        val space = Facts.space_of (Proof_Context.facts_of ctxt);
79        val completion = Name_Space.completion context space (defined_entry context) (xname, pos);
80      in error (undeclared xname ^ Position.here pos ^ Completion.markup_report [completion]) end;
81  in
82    (case try (Proof_Context.get_fact_generic context) fact_ref of
83      SOME (SOME name, _) => if defined_entry context name then name else err ()
84    | _ => err ())
85  end;
86
87
88(* declaration *)
89
90fun declare binding descr lthy =
91  let
92    val name = Local_Theory.full_name lthy binding;
93    val description =
94      "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
95    val lthy' = lthy
96      |> Local_Theory.background_theory (Context.theory_map (new_entry name))
97      |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
98      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
99      |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
100  in (name, lthy') end;
101
102
103(* ML antiquotation *)
104
105val _ = Theory.setup
106  (ML_Antiquotation.inline_embedded \<^binding>\<open>named_theorems\<close>
107    (Args.context -- Scan.lift Args.embedded_position >>
108      (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
109
110end;
111