merged
authorblanchet
Tue, 31 Aug 2010 21:02:07 +0200
changeset 38945 53a9563fa221
parent 38936 5cdba14d20fa (current diff)
parent 38944 827c98e8ba8b (diff)
child 38946 da5e4f182f69
merged
--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 31 19:14:18 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 31 21:02:07 2010 +0200
@@ -447,7 +447,7 @@
 \label{relevance-filter}
 
 \begin{enum}
-\opdefault{relevance\_thresholds}{int\_pair}{45~90}
+\opdefault{relevance\_thresholds}{int\_pair}{45~85}
 Specifies the thresholds above which facts are considered relevant by the
 relevance filter. The first threshold is used for the first iteration of the
 relevance filter and the second threshold is used for the last iteration (if it
--- a/etc/isar-keywords.el	Tue Aug 31 19:14:18 2010 +0200
+++ b/etc/isar-keywords.el	Tue Aug 31 21:02:07 2010 +0200
@@ -245,6 +245,7 @@
     "thus"
     "thy_deps"
     "translations"
+    "try"
     "txt"
     "txt_raw"
     "typ"
@@ -398,6 +399,7 @@
     "thm"
     "thm_deps"
     "thy_deps"
+    "try"
     "typ"
     "unused_thms"
     "value"
--- a/src/HOL/HOL.thy	Tue Aug 31 19:14:18 2010 +0200
+++ b/src/HOL/HOL.thy	Tue Aug 31 21:02:07 2010 +0200
@@ -30,6 +30,7 @@
   "~~/src/Tools/induct.ML"
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
+  "Tools/try.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
--- a/src/HOL/IsaMakefile	Tue Aug 31 19:14:18 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Aug 31 21:02:07 2010 +0200
@@ -213,6 +213,7 @@
   Tools/sat_funcs.ML \
   Tools/sat_solver.ML \
   Tools/split_rule.ML \
+  Tools/try.ML \
   Tools/typedef.ML \
   Transitive_Closure.thy \
   Typedef.thy \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 19:14:18 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Tue Aug 31 21:02:07 2010 +0200
@@ -6,10 +6,15 @@
 struct
 
 val relevance_filter_args =
-  [("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
+  [("worse_irrel_freq", Sledgehammer_Fact_Filter.worse_irrel_freq),
+   ("higher_order_irrel_weight",
+    Sledgehammer_Fact_Filter.higher_order_irrel_weight),
+   ("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
    ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
    ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
-   ("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus),
+   ("intro_bonus", Sledgehammer_Fact_Filter.intro_bonus),
+   ("elim_bonus", Sledgehammer_Fact_Filter.elim_bonus),
+   ("simp_bonus", Sledgehammer_Fact_Filter.simp_bonus),
    ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
    ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
    ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 31 19:14:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 31 21:02:07 2010 +0200
@@ -5,7 +5,7 @@
 
 signature SLEDGEHAMMER_FACT_FILTER =
 sig
-  datatype locality = General | Theory | Local | Chained
+  datatype locality = General | Intro | Elim | Simp | Local | Chained
 
   type relevance_override =
     {add: Facts.ref list,
@@ -13,10 +13,14 @@
      only: bool}
 
   val trace : bool Unsynchronized.ref
+  val worse_irrel_freq : real Unsynchronized.ref
+  val higher_order_irrel_weight : real Unsynchronized.ref
   val abs_rel_weight : real Unsynchronized.ref
   val abs_irrel_weight : real Unsynchronized.ref
   val skolem_irrel_weight : real Unsynchronized.ref
-  val theory_bonus : real Unsynchronized.ref
+  val intro_bonus : real Unsynchronized.ref
+  val elim_bonus : real Unsynchronized.ref
+  val simp_bonus : real Unsynchronized.ref
   val local_bonus : real Unsynchronized.ref
   val chained_bonus : real Unsynchronized.ref
   val max_imperfect : real Unsynchronized.ref
@@ -44,7 +48,7 @@
 
 val respect_no_atp = true
 
-datatype locality = General | Theory | Local | Chained
+datatype locality = General | Intro | Elim | Simp | Local | Chained
 
 type relevance_override =
   {add: Facts.ref list,
@@ -77,13 +81,22 @@
 
 (*** constants with types ***)
 
+fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) =
+    order_of_type T1 (* cheat: pretend sets are first-order *)
+  | order_of_type (Type (@{type_name fun}, [T1, T2])) =
+    Int.max (order_of_type T1 + 1, order_of_type T2)
+  | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
+  | order_of_type _ = 0
+
 (* An abstraction of Isabelle types and first-order terms *)
 datatype pattern = PVar | PApp of string * pattern list
+datatype ptype = PType of int * pattern list
 
 fun string_for_pattern PVar = "_"
   | string_for_pattern (PApp (s, ps)) =
     if null ps then s else s ^ string_for_patterns ps
 and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
+fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
 
 (*Is the second type an instance of the first one?*)
 fun match_pattern (PVar, _) = true
@@ -94,17 +107,18 @@
   | match_patterns ([], _) = false
   | match_patterns (p :: ps, q :: qs) =
     match_pattern (p, q) andalso match_patterns (ps, qs)
+fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
 
 (* Is there a unifiable constant? *)
 fun pconst_mem f consts (s, ps) =
-  exists (curry (match_patterns o f) ps)
+  exists (curry (match_ptype o f) ps)
          (map snd (filter (curry (op =) s o fst) consts))
 fun pconst_hyper_mem f const_tab (s, ps) =
-  exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s))
+  exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
 
-fun ptype (Type (s, Ts)) = PApp (s, map ptype Ts)
-  | ptype (TFree (s, _)) = PApp (s, [])
-  | ptype (TVar _) = PVar
+fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
+  | pattern_for_type (TFree (s, _)) = PApp (s, [])
+  | pattern_for_type (TVar _) = PVar
 
 fun pterm thy t =
   case strip_comb t of
@@ -113,14 +127,17 @@
   | (Var x, []) => PVar
   | _ => PApp ("?", [])  (* equivalence class of higher-order constructs *)
 (* Pairs a constant with the list of its type instantiations. *)
-and pconst_args thy const (s, T) ts =
-  (if const then map ptype (these (try (Sign.const_typargs thy) (s, T)))
+and ptype thy const x ts =
+  (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
    else []) @
   (if term_patterns then map (pterm thy) ts else [])
-and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts)
+and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts)
+and rich_ptype thy const (s, T) ts =
+  PType (order_of_type T, ptype thy const (s, T) ts)
+and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts)
 
-fun string_for_hyper_pconst (s, pss) =
-  s ^ "{" ^ commas (map string_for_patterns pss) ^ "}"
+fun string_for_hyper_pconst (s, ps) =
+  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
 
 val abs_name = "Sledgehammer.abs"
 val skolem_prefix = "Sledgehammer.sko"
@@ -133,12 +150,12 @@
 
 (* Add a pconstant to the table, but a [] entry means a standard
    connective, which we ignore.*)
-fun add_pconst_to_table also_skolem (c, ps) =
+fun add_pconst_to_table also_skolem (c, p) =
   if member (op =) boring_consts c orelse
      (not also_skolem andalso String.isPrefix skolem_prefix c) then
     I
   else
-    Symtab.map_default (c, [ps]) (insert (op =) ps)
+    Symtab.map_default (c, [p]) (insert (op =) p)
 
 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
 
@@ -149,38 +166,40 @@
        each quantifiers that must necessarily be skolemized by the ATP, we
        introduce a fresh constant to simulate the effect of Skolemization. *)
     fun do_const const (s, T) ts =
-      add_pconst_to_table also_skolems (pconst thy const (s, T) ts)
+      add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts)
       #> fold do_term ts
     and do_term t =
       case strip_comb t of
         (Const x, ts) => do_const true x ts
       | (Free x, ts) => do_const false x ts
-      | (Abs (_, _, t'), ts) =>
-        (null ts ? add_pconst_to_table true (abs_name, []))
+      | (Abs (_, T, t'), ts) =>
+        (null ts
+         ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
         #> fold do_term (t' :: ts)
       | (_, ts) => fold do_term ts
-    fun do_quantifier will_surely_be_skolemized body_t =
+    fun do_quantifier will_surely_be_skolemized abs_T body_t =
       do_formula pos body_t
       #> (if also_skolems andalso will_surely_be_skolemized then
-            add_pconst_to_table true (gensym skolem_prefix, [])
+            add_pconst_to_table true
+                         (gensym skolem_prefix, PType (order_of_type abs_T, []))
           else
             I)
     and do_term_or_formula T =
       if is_formula_type T then do_formula NONE else do_term
     and do_formula pos t =
       case t of
-        Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
-        do_quantifier (pos = SOME false) body_t
+        Const (@{const_name all}, _) $ Abs (_, T, t') =>
+        do_quantifier (pos = SOME false) T t'
       | @{const "==>"} $ t1 $ t2 =>
         do_formula (flip pos) t1 #> do_formula pos t2
       | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
         fold (do_term_or_formula T) [t1, t2]
       | @{const Trueprop} $ t1 => do_formula pos t1
       | @{const Not} $ t1 => do_formula (flip pos) t1
-      | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
-        do_quantifier (pos = SOME false) body_t
-      | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
-        do_quantifier (pos = SOME true) body_t
+      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
+        do_quantifier (pos = SOME false) T t'
+      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
+        do_quantifier (pos = SOME true) T t'
       | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
       | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
       | @{const HOL.implies} $ t1 $ t2 =>
@@ -190,14 +209,14 @@
       | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
         $ t1 $ t2 $ t3 =>
         do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3]
-      | Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) =>
-        do_quantifier (is_some pos) body_t
-      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) =>
-        do_quantifier (pos = SOME false)
-                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t))
-      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) =>
-        do_quantifier (pos = SOME true)
-                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t))
+      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
+        do_quantifier (is_some pos) T t'
+      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
+        do_quantifier (pos = SOME false) T
+                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
+      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
+        do_quantifier (pos = SOME true) T
+                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
       | (t0 as Const (_, @{typ bool})) $ t1 =>
         do_term t0 #> do_formula pos t1  (* theory constant *)
       | _ => do_term t
@@ -227,16 +246,17 @@
   | (PApp _, PVar) => GREATER
   | (PApp q1, PApp q2) =>
     prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
+fun ptype_ord (PType p, PType q) =
+  prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
 
-structure CTtab =
-  Table(type key = pattern list val ord = dict_ord pattern_ord)
+structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
 
 fun count_axiom_consts theory_relevant thy =
   let
     fun do_const const (s, T) ts =
       (* Two-dimensional table update. Constant maps to types maps to count. *)
-      CTtab.map_default (pconst_args thy const (s, T) ts, 0) (Integer.add 1)
-      |> Symtab.map_default (s, CTtab.empty)
+      PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1)
+      |> Symtab.map_default (s, PType_Tab.empty)
       #> fold do_term ts
     and do_term t =
       case strip_comb t of
@@ -249,19 +269,38 @@
 
 (**** Actual Filtering Code ****)
 
+fun pow_int x 0 = 1.0
+  | pow_int x 1 = x
+  | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
+
 (*The frequency of a constant is the sum of those of all instances of its type.*)
 fun pconst_freq match const_tab (c, ps) =
-  CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
-             (the (Symtab.lookup const_tab c)) 0
+  PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
+                 (the (Symtab.lookup const_tab c)) 0
 
 
 (* A surprising number of theorems contain only a few significant constants.
    These include all induction rules, and other general theorems. *)
 
 (* "log" seems best in practice. A constant function of one ignores the constant
-   frequencies. *)
-fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
-fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
+   frequencies. Rare constants give more points if they are relevant than less
+   rare ones. *)
+fun rel_weight_for order freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
+
+(* FUDGE *)
+val worse_irrel_freq = Unsynchronized.ref 100.0
+val higher_order_irrel_weight = Unsynchronized.ref 1.05
+
+(* Irrelevant constants are treated differently. We associate lower penalties to
+   very rare constants and very common ones -- the former because they can't
+   lead to the inclusion of too many new facts, and the latter because they are
+   so common as to be of little interest. *)
+fun irrel_weight_for order freq =
+  let val (k, x) = !worse_irrel_freq |> `Real.ceil in
+    (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
+     else rel_weight_for order freq / rel_weight_for order k)
+    * pow_int (!higher_order_irrel_weight) (order - 1)
+  end
 
 (* FUDGE *)
 val abs_rel_weight = Unsynchronized.ref 0.5
@@ -269,24 +308,29 @@
 val skolem_irrel_weight = Unsynchronized.ref 0.75
 
 (* Computes a constant's weight, as determined by its frequency. *)
-fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) =
+fun generic_pconst_weight abs_weight skolem_weight weight_for f const_tab
+                          (c as (s, PType (m, _))) =
   if s = abs_name then abs_weight
   else if String.isPrefix skolem_prefix s then skolem_weight
-  else logx (pconst_freq (match_patterns o f) const_tab c)
+  else weight_for m (pconst_freq (match_ptype o f) const_tab c)
 
-fun rel_weight const_tab =
-  generic_weight (!abs_rel_weight) 0.0 rel_log I const_tab
-fun irrel_weight const_tab =
-  generic_weight (!abs_irrel_weight) (!skolem_irrel_weight) irrel_log swap
-                 const_tab
+fun rel_pconst_weight const_tab =
+  generic_pconst_weight (!abs_rel_weight) 0.0 rel_weight_for I const_tab
+fun irrel_pconst_weight const_tab =
+  generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
+                        irrel_weight_for swap const_tab
 
 (* FUDGE *)
-val theory_bonus = Unsynchronized.ref 0.1
+val intro_bonus = Unsynchronized.ref 0.15
+val elim_bonus = Unsynchronized.ref 0.15
+val simp_bonus = Unsynchronized.ref 0.15
 val local_bonus = Unsynchronized.ref 0.55
 val chained_bonus = Unsynchronized.ref 1.5
 
 fun locality_bonus General = 0.0
-  | locality_bonus Theory = !theory_bonus
+  | locality_bonus Intro = !intro_bonus
+  | locality_bonus Elim = !elim_bonus
+  | locality_bonus Simp = !simp_bonus
   | locality_bonus Local = !local_bonus
   | locality_bonus Chained = !chained_bonus
 
@@ -297,10 +341,11 @@
   | (rel, irrel) =>
     let
       val irrel = irrel |> filter_out (pconst_mem swap rel)
-      val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) rel
+      val rel_weight =
+        0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
       val irrel_weight =
         ~ (locality_bonus loc)
-        |> fold (curry (op +) o irrel_weight const_tab) irrel
+        |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
       val res = rel_weight / (rel_weight + irrel_weight)
     in if Real.isFinite res then res else 0.0 end
 
@@ -311,14 +356,15 @@
     ([], _) => 0.0
   | (rel, irrel) =>
     let
-val _ = tracing (PolyML.makestring ("REL: ", rel))
-val _ = tracing (PolyML.makestring ("IRREL: ", irrel))(*###*)
       val irrel = irrel |> filter_out (pconst_mem swap rel)
-      val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) rel
-      val irrel_weight =
+      val rels_weight =
+        0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
+      val irrels_weight =
         ~ (locality_bonus loc)
-        |> fold (curry (op +) o irrel_weight const_tab) irrel
-      val res = rel_weight / (rel_weight + irrel_weight)
+        |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel))
+val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel))
+      val res = rels_weight / (rels_weight + irrels_weight)
     in if Real.isFinite res then res else 0.0 end
 *)
 
@@ -332,10 +378,10 @@
   | consts => SOME ((axiom, consts), NONE)
 
 type annotated_thm =
-  (((unit -> string) * locality) * thm) * (string * pattern list) list
+  (((unit -> string) * locality) * thm) * (string * ptype) list
 
 (* FUDGE *)
-val max_imperfect = Unsynchronized.ref 10.0
+val max_imperfect = Unsynchronized.ref 11.5
 val max_imperfect_exp = Unsynchronized.ref 1.0
 
 fun take_most_relevant max_relevant remaining_max
@@ -380,8 +426,7 @@
       fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
     val goal_const_tab =
       pconsts_in_terms thy false (SOME false) goal_ts
-      |> fold (if_empty_replace_with_locality thy axioms)
-              [Chained, Local, Theory]
+      |> fold (if_empty_replace_with_locality thy axioms) [Chained, Local]
     val add_thms = maps (ProofContext.get_fact ctxt) add
     val del_thms = maps (ProofContext.get_fact ctxt) del
     fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
@@ -448,7 +493,7 @@
                 | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
 (* FIXME: experiment
 val name = fst (fst (fst ax)) ()
-val _ = if String.isSubstring "abs_of_neg" name then
+val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then
 tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
 else
 ()
@@ -493,9 +538,9 @@
      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   end;
 
-fun make_fact_table xs =
-  fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
-fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) []
+fun mk_fact_table f xs =
+  fold (Termtab.update o `(prop_of o f)) xs Termtab.empty
+fun uniquify xs = Termtab.fold (cons o snd) (mk_fact_table snd xs) []
 
 (* FIXME: put other record thms here, or declare as "no_atp" *)
 val multi_base_blacklist =
@@ -625,14 +670,26 @@
     is_that_fact thm
   end
 
+fun clasimpset_rules_of ctxt =
+  let
+    val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
+    val intros = safeIs @ hazIs
+    val elims = map Classical.classical_rule (safeEs @ hazEs)
+    val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
+  in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
+
 fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
   let
     val thy = ProofContext.theory_of ctxt
-    val thy_prefix = Context.theory_name thy ^ Long_Name.separator
     val global_facts = PureThy.facts_of thy
     val local_facts = ProofContext.facts_of ctxt
     val named_locals = local_facts |> Facts.dest_static []
     val is_chained = member Thm.eq_thm chained_ths
+    val (intros, elims, simps) =
+      if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then
+        clasimpset_rules_of ctxt
+      else
+        (Termtab.empty, Termtab.empty, Termtab.empty)
     (* Unnamed nonchained formulas with schematic variables are omitted, because
        they are rejected by the backticks (`...`) parser for some reason. *)
     fun is_good_unnamed_local th =
@@ -655,10 +712,6 @@
           I
         else
           let
-            val base_loc =
-              if not global then Local
-              else if String.isPrefix thy_prefix name0 then Theory
-              else General
             val multi = length ths > 1
             fun backquotify th =
               "`" ^ Print_Mode.setmp [Print_Mode.input]
@@ -688,7 +741,15 @@
                               case find_first check_thms [name1, name2, name0] of
                                 SOME name => repair_name reserved multi j name
                               | NONE => ""
-                            end), if is_chained th then Chained else base_loc),
+                            end),
+                      let val t = prop_of th in
+                        if is_chained th then Chained
+                        else if not global then Local
+                        else if Termtab.defined intros t then Intro
+                        else if Termtab.defined elims t then Elim
+                        else if Termtab.defined simps t then Simp
+                        else General
+                      end),
                       (multi, th)) :: rest)) ths
             #> snd
           end)
@@ -722,7 +783,7 @@
        else
          all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
       |> name_thm_pairs ctxt (respect_no_atp andalso not only)
-      |> make_unique
+      |> uniquify
   in
     trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
                         " theorems");
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 19:14:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 21:02:07 2010 +0200
@@ -67,7 +67,7 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("explicit_apply", "false"),
-   ("relevance_thresholds", "45 90"),
+   ("relevance_thresholds", "45 85"),
    ("max_relevant", "smart"),
    ("theory_relevant", "smart"),
    ("isar_proof", "false"),
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/try.ML	Tue Aug 31 21:02:07 2010 +0200
@@ -0,0 +1,79 @@
+(*  Title:      HOL/Tools/try.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Try a combination of proof methods.
+*)
+
+signature TRY =
+sig
+  val invoke_try : Proof.state -> unit
+end;
+
+structure Try : TRY =
+struct
+
+val timeout = Time.fromSeconds 5
+
+fun can_apply pre post tac st =
+  let val {goal, ...} = Proof.goal st in
+    case TimeLimit.timeLimit timeout (Seq.pull o tac) (pre st) of
+      SOME (x, _) => nprems_of (post x) < nprems_of goal
+    | NONE => false
+  end
+
+fun do_generic command pre post apply st =
+  let val timer = Timer.startRealTimer () in
+    if can_apply pre post apply st then
+      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
+    else
+      NONE
+  end
+
+fun named_method thy name =
+  Method.method thy (Args.src ((name, []), Position.none))
+
+fun apply_named_method name ctxt =
+  let val thy = ProofContext.theory_of ctxt in
+    Method.apply (named_method thy name) ctxt []
+  end
+
+fun do_named_method name st =
+  do_generic name (#goal o Proof.goal) snd
+             (apply_named_method name (Proof.context_of st)) st
+
+fun apply_named_method_on_first_goal name ctxt =
+  let val thy = ProofContext.theory_of ctxt in
+    Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
+  end
+
+fun do_named_method_on_first_goal name st =
+  do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
+                      else "")) I (#goal o Proof.goal)
+             (apply_named_method_on_first_goal name (Proof.context_of st)) st
+
+val all_goals_named_methods = ["auto", "safe"]
+val first_goal_named_methods =
+  ["simp", "fast", "fastsimp", "force", "best", "blast"]
+val do_methods =
+  map do_named_method_on_first_goal all_goals_named_methods @
+  map do_named_method first_goal_named_methods
+
+fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
+
+fun invoke_try st =
+  case do_methods |> Par_List.map (fn f => f st)
+                  |> map_filter I |> sort (int_ord o pairself snd) of
+    [] => writeln "No proof found."
+  | xs as (s, _) :: _ =>
+    priority ("Try this command: " ^
+              Markup.markup Markup.sendback ("apply " ^ s) ^ ".\n" ^
+              "(" ^ space_implode "; " (map time_string xs) ^ ")\n")
+
+val tryN = "try"
+
+val _ =
+  Outer_Syntax.improper_command tryN
+      "try a combination of proof methods" Keyword.diag
+      (Scan.succeed (Toplevel.keep (invoke_try o Toplevel.proof_of)))
+
+end;