# HG changeset patch
# User blanchet
# Date 1337185011 -7200
# Node ID 4e8e0245e8be9ca278e9076a4f08ff0007433861
# Parent  ce4178e037a7cd578f6931f7af274b3214df76ae
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect

diff -r ce4178e037a7 -r 4e8e0245e8be src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 16 18:16:51 2012 +0200
@@ -362,6 +362,12 @@
   if (not also_skolem andalso String.isPrefix skolem_prefix s) then I
   else Symtab.map_default (s, [p]) (insert (op =) p)
 
+(* Set constants tend to pull in too many irrelevant facts. We limit the damage
+   by treating them more or less as if they were built-in but add their
+   axiomatization at the end. *)
+val set_consts = [@{const_name Collect}, @{const_name Set.member}]
+val set_thms = @{thms Collect_mem_eq mem_Collect_eq}
+
 fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
   let
     val flip = Option.map not
@@ -369,16 +375,19 @@
        each quantifiers that must necessarily be skolemized by the automatic
        prover, we introduce a fresh constant to simulate the effect of
        Skolemization. *)
-    fun do_const const x ts =
+    fun do_const const ext_arg (x as (s, _)) ts =
       let val (built_in, ts) = is_built_in_const x ts in
-        (not built_in
-         ? add_pconst_to_table also_skolems (rich_pconst thy const x))
-        #> fold (do_term false) ts
+        if member (op =) set_consts s then
+          fold (do_term ext_arg) ts
+        else
+          (not built_in
+           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
+          #> fold (do_term false) ts
       end
     and do_term ext_arg t =
       case strip_comb t of
-        (Const x, ts) => do_const true x ts
-      | (Free x, ts) => do_const false x ts
+        (Const x, ts) => do_const true ext_arg x ts
+      | (Free x, ts) => do_const false ext_arg x ts
       | (Abs (_, T, t'), ts) =>
         ((null ts andalso not ext_arg)
          (* Since lambdas on the right-hand side of equalities are usually
@@ -750,6 +759,14 @@
       ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
        (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
       |> take max_relevant
+    fun uses_const s t =
+      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
+                  false
+    fun uses_const_anywhere accepts s =
+      exists (uses_const s o prop_of o snd) accepts orelse
+      exists (uses_const s) (concl_t :: hyp_ts)
+    fun add_set_const_thms accepts =
+      exists (uses_const_anywhere accepts) set_consts ? append set_thms
     fun insert_into_facts accepts [] = accepts
       | insert_into_facts accepts ths =
         let
@@ -761,6 +778,7 @@
         in bef @ add @ after end
     fun insert_special_facts accepts =
        [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
+          |> add_set_const_thms accepts
           |> insert_into_facts accepts
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)