src/Pure/Tools/named_theorems.ML
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 62848 e4140efe699e
child 67146 909dcdec2122
permissions -rw-r--r--
tuned signature;
wenzelm@57886
     1
(*  Title:      Pure/Tools/named_theorems.ML
wenzelm@57886
     2
    Author:     Makarius
wenzelm@57886
     3
wenzelm@57886
     4
Named collections of theorems in canonical order.
wenzelm@57886
     5
*)
wenzelm@57886
     6
wenzelm@57886
     7
signature NAMED_THEOREMS =
wenzelm@57886
     8
sig
wenzelm@57886
     9
  val member: Proof.context -> string -> thm -> bool
wenzelm@57886
    10
  val get: Proof.context -> string -> thm list
wenzelm@61900
    11
  val clear: string -> Context.generic -> Context.generic
wenzelm@57886
    12
  val add_thm: string -> thm -> Context.generic -> Context.generic
wenzelm@57886
    13
  val del_thm: string -> thm -> Context.generic -> Context.generic
wenzelm@57886
    14
  val add: string -> attribute
wenzelm@57886
    15
  val del: string -> attribute
wenzelm@59920
    16
  val check: Proof.context -> string * Position.T -> string
wenzelm@57888
    17
  val declare: binding -> string -> local_theory -> string * local_theory
wenzelm@57886
    18
end;
wenzelm@57886
    19
wenzelm@57886
    20
structure Named_Theorems: NAMED_THEOREMS =
wenzelm@57886
    21
struct
wenzelm@57886
    22
wenzelm@57886
    23
(* context data *)
wenzelm@57886
    24
wenzelm@57886
    25
structure Data = Generic_Data
wenzelm@57886
    26
(
wenzelm@57886
    27
  type T = thm Item_Net.T Symtab.table;
wenzelm@57886
    28
  val empty: T = Symtab.empty;
wenzelm@57886
    29
  val extend = I;
wenzelm@57965
    30
  val merge : T * T -> T = Symtab.join (K Item_Net.merge);
wenzelm@57886
    31
);
wenzelm@57886
    32
wenzelm@57886
    33
fun new_entry name =
wenzelm@57886
    34
  Data.map (fn data =>
wenzelm@57886
    35
    if Symtab.defined data name
wenzelm@57886
    36
    then error ("Duplicate declaration of named theorems: " ^ quote name)
wenzelm@57886
    37
    else Symtab.update (name, Thm.full_rules) data);
wenzelm@57886
    38
wenzelm@59920
    39
fun undeclared name = "Undeclared named theorems " ^ quote name;
wenzelm@59920
    40
wenzelm@57886
    41
fun the_entry context name =
wenzelm@57886
    42
  (case Symtab.lookup (Data.get context) name of
wenzelm@59920
    43
    NONE => error (undeclared name)
wenzelm@57886
    44
  | SOME entry => entry);
wenzelm@57886
    45
wenzelm@57886
    46
fun map_entry name f context =
wenzelm@57886
    47
  (the_entry context name; Data.map (Symtab.map_entry name f) context);
wenzelm@57886
    48
wenzelm@57886
    49
wenzelm@57886
    50
(* maintain content *)
wenzelm@57886
    51
wenzelm@57886
    52
fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt);
wenzelm@57886
    53
wenzelm@61049
    54
fun content context =
wenzelm@61049
    55
  rev o map (Thm.transfer (Context.theory_of context)) o Item_Net.content o the_entry context;
wenzelm@61049
    56
wenzelm@57886
    57
val get = content o Context.Proof;
wenzelm@57886
    58
wenzelm@61900
    59
fun clear name = map_entry name (K Thm.full_rules);
wenzelm@61900
    60
wenzelm@61049
    61
fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
wenzelm@57886
    62
fun del_thm name = map_entry name o Item_Net.remove;
wenzelm@57886
    63
wenzelm@57886
    64
val add = Thm.declaration_attribute o add_thm;
wenzelm@57886
    65
val del = Thm.declaration_attribute o del_thm;
wenzelm@57886
    66
wenzelm@57886
    67
wenzelm@59920
    68
(* check *)
wenzelm@59920
    69
wenzelm@59920
    70
fun check ctxt (xname, pos) =
wenzelm@59920
    71
  let
wenzelm@59920
    72
    val context = Context.Proof ctxt;
wenzelm@59920
    73
    val fact_ref = Facts.Named ((xname, Position.none), NONE);
wenzelm@59920
    74
    fun err () = error (undeclared xname ^ Position.here pos);
wenzelm@59920
    75
  in
wenzelm@59920
    76
    (case try (Proof_Context.get_fact_generic context) fact_ref of
wenzelm@59920
    77
      SOME (SOME name, _) => if can (the_entry context) name then name else err ()
wenzelm@59920
    78
    | _ => err ())
wenzelm@59920
    79
  end;
wenzelm@59920
    80
wenzelm@59920
    81
wenzelm@57886
    82
(* declaration *)
wenzelm@57886
    83
wenzelm@57888
    84
fun declare binding descr lthy =
wenzelm@57886
    85
  let
wenzelm@59879
    86
    val name = Local_Theory.full_name lthy binding;
wenzelm@57886
    87
    val description =
wenzelm@57886
    88
      "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
wenzelm@57888
    89
    val lthy' = lthy
wenzelm@57929
    90
      |> Local_Theory.background_theory (Context.theory_map (new_entry name))
wenzelm@57929
    91
      |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
wenzelm@57929
    92
      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
wenzelm@57927
    93
      |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
wenzelm@57888
    94
  in (name, lthy') end;
wenzelm@57886
    95
wenzelm@57886
    96
wenzelm@57886
    97
(* ML antiquotation *)
wenzelm@57886
    98
wenzelm@57886
    99
val _ = Theory.setup
wenzelm@57886
   100
  (ML_Antiquotation.inline @{binding named_theorems}
wenzelm@59920
   101
    (Args.context -- Scan.lift (Parse.position Args.name) >>
wenzelm@59920
   102
      (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
wenzelm@57886
   103
wenzelm@57886
   104
end;