# HG changeset patch
# User blanchet
# Date 1269866993 -7200
# Node ID 4d27652ffb40d0201b263736083080ff928233d2
# Parent  ab3dfdeb9603708eb182248cec769520dc48da7d
reintroduce efficient set structure to collect "no_atp" theorems

diff -r ab3dfdeb9603 -r 4d27652ffb40 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Mar 29 12:21:51 2010 +0200
+++ b/src/HOL/HOL.thy	Mon Mar 29 14:49:53 2010 +0200
@@ -30,6 +30,7 @@
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
   "~~/src/Tools/more_conv.ML"
+  "~~/src/HOL/Tools/Sledgehammer/named_thm_set.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -800,10 +801,10 @@
 *}
 
 ML {*
-structure No_ATPs = Named_Thms
+structure No_ATPs = Named_Thm_Set
 (
   val name = "no_atp"
-  val description = "theorems that should be avoided by Sledgehammer"
+  val description = "theorems that should be filtered out by Sledgehammer"
 )
 *}
 
diff -r ab3dfdeb9603 -r 4d27652ffb40 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Mar 29 12:21:51 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Mar 29 14:49:53 2010 +0200
@@ -99,7 +99,8 @@
 
 $(OUT)/Pure: Pure
 
-BASE_DEPENDENCIES = $(OUT)/Pure \
+BASE_DEPENDENCIES = $(SRC)/HOL/Tools/Sledgehammer/named_thm_set.ML \
+  $(OUT)/Pure \
   $(SRC)/Provers/blast.ML \
   $(SRC)/Provers/clasimp.ML \
   $(SRC)/Provers/classical.ML \
diff -r ab3dfdeb9603 -r 4d27652ffb40 src/HOL/Tools/Sledgehammer/named_thm_set.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/named_thm_set.ML	Mon Mar 29 14:49:53 2010 +0200
@@ -0,0 +1,45 @@
+(*  Title:      HOL/Tools/Sledgehammer/named_thm_set.ML
+    Author:     Makarius
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Named sets of theorems.
+*)
+
+signature NAMED_THM_SET =
+sig
+  val member: Proof.context -> thm -> bool
+  val add_thm: thm -> Context.generic -> Context.generic
+  val del_thm: thm -> Context.generic -> Context.generic
+  val add: attribute
+  val del: attribute
+  val setup: theory -> theory
+end;
+
+functor Named_Thm_Set(val name: string val description: string)
+        : NAMED_THM_SET =
+struct
+
+structure Data = Generic_Data
+(
+  type T = thm Termtab.table;
+  val empty = Termtab.empty;
+  val extend = I;
+  fun merge tabs = Termtab.merge (K true) tabs;
+);
+
+fun member 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.name name) (Attrib.add_del add del)
+               ("declaration of " ^ description) #>
+  PureThy.add_thms_dynamic (Binding.name name,
+                            map #2 o Termtab.dest o Data.get);
+
+end;
diff -r ab3dfdeb9603 -r 4d27652ffb40 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Mar 29 12:21:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Mar 29 14:49:53 2010 +0200
@@ -422,16 +422,7 @@
       List.partition is_multi (all_valid_thms respect_no_atp ctxt)
     val ps = [] |> fold add_multi_names mults
                 |> fold add_single_names singles
-  in
-    if respect_no_atp then
-      let
-        val blacklist = No_ATPs.get ctxt
-                        |> map (`Thm.full_prop_of) |> Termtab.make
-        val is_blacklisted = Termtab.defined blacklist o Thm.full_prop_of o snd
-      in ps |> filter_out is_blacklisted end
-    else
-      ps
-  end;
+  in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
 
 fun check_named ("", th) =
       (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)