treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
authorblanchet
Wed, 16 May 2012 18:16:51 +0200
changeset 47933 4e8e0245e8be
parent 47932 ce4178e037a7
child 47934 08d7aff8c7e6
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
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)