src/Pure/Tools/named_theorems.ML
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 62848 e4140efe699e
child 67146 909dcdec2122
permissions -rw-r--r--
tuned signature;
     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 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
    18 end;
    19 
    20 structure Named_Theorems: NAMED_THEOREMS =
    21 struct
    22 
    23 (* context data *)
    24 
    25 structure 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 
    33 fun 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 
    39 fun undeclared name = "Undeclared named theorems " ^ quote name;
    40 
    41 fun the_entry context name =
    42   (case Symtab.lookup (Data.get context) name of
    43     NONE => error (undeclared name)
    44   | SOME entry => entry);
    45 
    46 fun map_entry name f context =
    47   (the_entry context name; Data.map (Symtab.map_entry name f) context);
    48 
    49 
    50 (* maintain content *)
    51 
    52 fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt);
    53 
    54 fun content context =
    55   rev o map (Thm.transfer (Context.theory_of context)) o Item_Net.content o the_entry context;
    56 
    57 val get = content o Context.Proof;
    58 
    59 fun clear name = map_entry name (K Thm.full_rules);
    60 
    61 fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
    62 fun del_thm name = map_entry name o Item_Net.remove;
    63 
    64 val add = Thm.declaration_attribute o add_thm;
    65 val del = Thm.declaration_attribute o del_thm;
    66 
    67 
    68 (* check *)
    69 
    70 fun check ctxt (xname, pos) =
    71   let
    72     val context = Context.Proof ctxt;
    73     val fact_ref = Facts.Named ((xname, Position.none), NONE);
    74     fun err () = error (undeclared xname ^ Position.here pos);
    75   in
    76     (case try (Proof_Context.get_fact_generic context) fact_ref of
    77       SOME (SOME name, _) => if can (the_entry context) name then name else err ()
    78     | _ => err ())
    79   end;
    80 
    81 
    82 (* declaration *)
    83 
    84 fun declare binding descr lthy =
    85   let
    86     val name = Local_Theory.full_name lthy binding;
    87     val description =
    88       "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
    89     val lthy' = lthy
    90       |> Local_Theory.background_theory (Context.theory_map (new_entry name))
    91       |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
    92       |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
    93       |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
    94   in (name, lthy') end;
    95 
    96 
    97 (* ML antiquotation *)
    98 
    99 val _ = Theory.setup
   100   (ML_Antiquotation.inline @{binding named_theorems}
   101     (Args.context -- Scan.lift (Parse.position Args.name) >>
   102       (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
   103 
   104 end;