src/HOL/Tools/res_blacklist.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/res_blacklist.ML	Thu Oct 29 16:06:15 2009 +0100
@@ -0,0 +1,43 @@
+(*  Title:      HOL/Tools/res_blacklist.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Makarius
+
+Theorems blacklisted to sledgehammer.  These theorems typically
+produce clauses that are prolific (match too many equality or
+membership literals) and relate to seldom-used facts.  Some duplicate
+other rules.
+*)
+
+signature RES_BLACKLIST =
+sig
+  val setup: theory -> theory
+  val blacklisted: Proof.context -> thm -> bool
+  val add: attribute
+  val del: attribute
+end;
+
+structure ResBlacklist: RES_BLACKLIST =
+struct
+
+structure Data = GenericDataFun
+(
+  type T = thm Termtab.table;
+  val empty = Termtab.empty;
+  val extend = I;
+  fun merge _ tabs = Termtab.merge (K true) tabs;
+);
+
+fun blacklisted ctxt th =
+  Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
+
+fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
+fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
+
+val add = Thm.declaration_attribute add_thm;
+val del = Thm.declaration_attribute del_thm;
+
+val setup =
+  Attrib.setup @{binding noatp} (Attrib.add_del add del) "sledgehammer blacklisting" #>
+  PureThy.add_thms_dynamic (@{binding noatp}, map #2 o Termtab.dest o Data.get);
+
+end;