src/Pure/Tools/named_theorems.ML
author wenzelm
Mon Dec 22 16:44:24 2014 +0100 (2014-12-22 ago)
changeset 59175 bf465f335e85
parent 59028 df7476e79558
child 59878 05362c246a64
permissions -rw-r--r--
system option "pretty_margin" is superseded by "thy_output_margin";
     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 -> local_theory -> string * local_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 : T * T -> T = 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 lthy =
    63   let
    64     val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding;
    65     val description =
    66       "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
    67     val lthy' = lthy
    68       |> Local_Theory.background_theory (Context.theory_map (new_entry name))
    69       |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
    70       |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
    71       |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
    72   in (name, lthy') end;
    73 
    74 val _ =
    75   Outer_Syntax.local_theory @{command_spec "named_theorems"}
    76     "declare named collection of theorems"
    77     (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
    78       fold (fn (b, descr) => snd o declare b descr));
    79 
    80 
    81 (* ML antiquotation *)
    82 
    83 val _ = Theory.setup
    84   (ML_Antiquotation.inline @{binding named_theorems}
    85     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (xname, pos)) =>
    86       let
    87         val thy = Proof_Context.theory_of ctxt;
    88         val name = Global_Theory.check_fact thy (xname, pos);
    89         val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos);
    90       in ML_Syntax.print_string name end)));
    91 
    92 end;