# HG changeset patch
# User blanchet
# Date 1282488965 -7200
# Node ID 25bbbaf7ce65022115ba5bdb3215852435e76b57
# Parent  9cde57cdd0e379f346d4e37a444fbaedf846edc2
don't penalize abstractions in relevance filter + support nameless `foo`-style facts

diff -r 9cde57cdd0e3 -r 25bbbaf7ce65 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sun Aug 22 16:56:05 2010 +0200
@@ -84,11 +84,10 @@
   Symtab.map_default (c, [ctyps])
                      (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
 
-val fresh_prefix = "Sledgehammer.Fresh."
+val fresh_prefix = "Sledgehammer.FRESH."
 val flip = Option.map not
 (* These are typically simplified away by "Meson.presimplify". *)
-val boring_consts =
-  [@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)]
+val boring_consts = [@{const_name If}, @{const_name Let}]
 
 fun get_consts_typs thy pos ts =
   let
@@ -100,10 +99,7 @@
         Const x => add_const_type_to_table (const_with_typ thy x)
       | Free (s, _) => add_const_type_to_table (s, [])
       | t1 $ t2 => do_term t1 #> do_term t2
-      | Abs (_, _, t) =>
-        (* Abstractions lead to combinators, so we add a penalty for them. *)
-        add_const_type_to_table (gensym fresh_prefix, [])
-        #> do_term t
+      | Abs (_, _, t') => do_term t'
       | _ => I
     fun do_quantifier will_surely_be_skolemized body_t =
       do_formula pos body_t
@@ -502,17 +498,23 @@
 fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
-    val local_facts = ProofContext.facts_of ctxt;
+    val local_facts = ProofContext.facts_of ctxt
+    val named_locals = local_facts |> Facts.dest_static []
+    val unnamed_locals =
+      local_facts |> Facts.props
+      |> filter_out (fn th => exists (fn (_, ths) => member Thm.eq_thm ths th)
+                                     named_locals)
+      |> map (pair "" o single)
     val full_space =
       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
-
-    fun valid_facts facts =
-      (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
-        if (Facts.is_concealed facts name orelse
+    fun valid_facts facts pairs =
+      (pairs, []) |-> fold (fn (name, ths0) =>
+        if name <> "" andalso
+           forall (not o member Thm.eq_thm add_thms) ths0 andalso
+           (Facts.is_concealed facts name orelse
             (respect_no_atp andalso is_package_def name) orelse
             member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
-            String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso
-           forall (not o member Thm.eq_thm add_thms) ths0 then
+            String.isSuffix "_def_raw" (* FIXME: crude hack *) name) then
           I
         else
           let
@@ -523,17 +525,26 @@
             val name1 = Facts.extern facts name;
             val name2 = Name_Space.extern full_space name;
             val ths =
-             ths0 |> map Clausifier.transform_elim_theorem
-                  |> filter ((not o is_theorem_bad_for_atps full_types) orf
-                             member Thm.eq_thm add_thms)
+              ths0 |> map Clausifier.transform_elim_theorem
+                   |> filter ((not o is_theorem_bad_for_atps full_types) orf
+                              member Thm.eq_thm add_thms)
+            val name' =
+              case find_first check_thms [name1, name2, name] of
+                SOME name' => name'
+              | NONE =>
+                ths |> map (fn th =>
+                               "`" ^ Print_Mode.setmp [Print_Mode.input]
+                                         (Syntax.string_of_term ctxt)
+                                         (prop_of th) ^ "`")
+                    |> space_implode " "
           in
-            case find_first check_thms [name1, name2, name] of
-              NONE => I
-            | SOME name' =>
-              cons (name' |> forall (member Thm.eq_thm chained_ths) ths
-                             ? prefix chained_prefix, ths)
+            cons (name' |> forall (member Thm.eq_thm chained_ths) ths
+                           ? prefix chained_prefix, ths)
           end)
-  in valid_facts global_facts @ valid_facts local_facts end;
+  in
+    valid_facts local_facts (unnamed_locals @ named_locals) @
+    valid_facts global_facts (Facts.dest_static [] global_facts)
+  end
 
 fun multi_name a th (n, pairs) =
   (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);