# HG changeset patch
# User blanchet
# Date 1282827525 -7200
# Node ID 71c9f61516cdaddcd64d6dc99633312fd4dfd50f
# Parent  61cf050f8b2ef21c51ec9a3251d9cf3d5fc4a2fa
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem

diff -r 61cf050f8b2e -r 71c9f61516cd src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 14:05:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 14:58:45 2010 +0200
@@ -108,24 +108,24 @@
 val abs_name = "Sledgehammer.abs"
 val skolem_prefix = "Sledgehammer.sko"
 
-(* Add a pseudoconstant to the table, but a [] entry means a standard
-   connective, which we ignore.*)
-fun add_pseudoconst_to_table also_skolem (c, ctyps) =
-  if also_skolem orelse not (String.isPrefix skolem_prefix c) then
-    Symtab.map_default (c, [ctyps])
-                       (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
-  else
-    I
-
-fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-
-val flip = Option.map not
 (* These are typically simplified away by "Meson.presimplify". *)
 val boring_consts =
   [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
 
+(* Add a pseudoconstant to the table, but a [] entry means a standard
+   connective, which we ignore.*)
+fun add_pseudoconst_to_table also_skolem (c, Ts) =
+  if member (op =) boring_consts c orelse
+     (not also_skolem andalso String.isPrefix skolem_prefix c) then
+    I
+  else
+    Symtab.map_default (c, [Ts]) (fn Tss => insert (op =) Ts Tss)
+
+fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
+
 fun get_pseudoconsts thy also_skolems pos ts =
   let
+    val flip = Option.map not
     (* We include free variables, as well as constants, to handle locales. For
        each quantifiers that must necessarily be skolemized by the ATP, we
        introduce a fresh constant to simulate the effect of Skolemization. *)
@@ -179,10 +179,7 @@
       | (t0 as Const (_, @{typ bool})) $ t1 =>
         do_term t0 #> do_formula pos t1  (* theory constant *)
       | _ => do_term t
-  in
-    Symtab.empty |> fold (Symtab.update o rpair []) boring_consts
-                 |> fold (do_formula pos) ts
-  end
+  in Symtab.empty |> fold (do_formula pos) ts end
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   takes the given theory into account.*)
@@ -295,12 +292,12 @@
     in if Real.isFinite res then res else 0.0 end
 *)
 
-fun pseudoconsts_of_term thy t =
+fun pseudoconsts_in_axiom thy t =
   Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
               (get_pseudoconsts thy true (SOME true) [t]) []
 fun pair_consts_axiom theory_relevant thy axiom =
   (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
-                |> pseudoconsts_of_term thy)
+                |> pseudoconsts_in_axiom thy)
 
 type annotated_thm =
   (((unit -> string) * locality) * thm) * (string * pseudotype list) list
@@ -330,6 +327,14 @@
     (accepts, more_rejects @ rejects)
   end
 
+fun if_empty_replace_with_locality thy axioms loc tab =
+  if Symtab.is_empty tab then
+    get_pseudoconsts thy false (SOME false)
+        (map_filter (fn ((_, loc'), th) =>
+                        if loc' = loc then SOME (prop_of th) else NONE) axioms)
+  else
+    tab
+
 (* FUDGE *)
 val threshold_divisor = 2.0
 val ridiculous_threshold = 0.1
@@ -339,8 +344,12 @@
                      ({add, del, ...} : relevance_override) axioms goal_ts =
   let
     val thy = ProofContext.theory_of ctxt
-    val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
-                         Symtab.empty
+    val const_tab =
+      fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
+    val goal_const_tab =
+      get_pseudoconsts thy false (SOME false) goal_ts
+      |> fold (if_empty_replace_with_locality thy axioms)
+              [Chained, Local, Theory]
     val add_thms = maps (ProofContext.get_fact ctxt) add
     val del_thms = maps (ProofContext.get_fact ctxt) del
     val max_max_imperfect =
@@ -434,8 +443,7 @@
   in
     axioms |> filter_out (member Thm.eq_thm del_thms o snd)
            |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
-           |> iter 0 max_relevant threshold0
-                   (get_pseudoconsts thy false (SOME false) goal_ts) []
+           |> iter 0 max_relevant threshold0 goal_const_tab []
            |> tap (fn res => trace_msg (fn () =>
                                 "Total relevant: " ^ Int.toString (length res)))
   end