src/HOL/Tools/Sledgehammer/named_thm_set.ML
author blanchet
Fri Apr 16 14:48:34 2010 +0200 (2010-04-16)
changeset 36169 27b1cc58715e
parent 36060 4d27652ffb40
permissions -rw-r--r--
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet@36060
     1
(*  Title:      HOL/Tools/Sledgehammer/named_thm_set.ML
blanchet@36060
     2
    Author:     Makarius
blanchet@36060
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@36060
     4
blanchet@36060
     5
Named sets of theorems.
blanchet@36060
     6
*)
blanchet@36060
     7
blanchet@36060
     8
signature NAMED_THM_SET =
blanchet@36060
     9
sig
blanchet@36060
    10
  val member: Proof.context -> thm -> bool
blanchet@36060
    11
  val add_thm: thm -> Context.generic -> Context.generic
blanchet@36060
    12
  val del_thm: thm -> Context.generic -> Context.generic
blanchet@36060
    13
  val add: attribute
blanchet@36060
    14
  val del: attribute
blanchet@36060
    15
  val setup: theory -> theory
blanchet@36060
    16
end;
blanchet@36060
    17
blanchet@36060
    18
functor Named_Thm_Set(val name: string val description: string)
blanchet@36060
    19
        : NAMED_THM_SET =
blanchet@36060
    20
struct
blanchet@36060
    21
blanchet@36060
    22
structure Data = Generic_Data
blanchet@36060
    23
(
blanchet@36060
    24
  type T = thm Termtab.table;
blanchet@36060
    25
  val empty = Termtab.empty;
blanchet@36060
    26
  val extend = I;
blanchet@36060
    27
  fun merge tabs = Termtab.merge (K true) tabs;
blanchet@36060
    28
);
blanchet@36060
    29
blanchet@36060
    30
fun member ctxt th =
blanchet@36060
    31
  Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
blanchet@36060
    32
blanchet@36060
    33
fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
blanchet@36060
    34
fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
blanchet@36060
    35
blanchet@36060
    36
val add = Thm.declaration_attribute add_thm;
blanchet@36060
    37
val del = Thm.declaration_attribute del_thm;
blanchet@36060
    38
blanchet@36060
    39
val setup =
blanchet@36060
    40
  Attrib.setup (Binding.name name) (Attrib.add_del add del)
blanchet@36060
    41
               ("declaration of " ^ description) #>
blanchet@36060
    42
  PureThy.add_thms_dynamic (Binding.name name,
blanchet@36060
    43
                            map #2 o Termtab.dest o Data.get);
blanchet@36060
    44
blanchet@36060
    45
end;