add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"

--- a/src/HOL/ATP.thy	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/ATP.thy	Mon May 21 10:39:32 2012 +0200
@@ -29,6 +29,9 @@
 definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
 "fNot P \<longleftrightarrow> \<not> P"
 
+definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+"fComp P = (\<lambda>x. \<not> P x)"
+
 definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
 "fconj P Q \<longleftrightarrow> P \<and> Q"
 
@@ -47,6 +50,86 @@
 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
 "fEx P \<longleftrightarrow> Ex P"
 
+lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
+unfolding fFalse_def fTrue_def by simp
+
+lemma fNot_table:
+"fNot fFalse = fTrue"
+"fNot fTrue = fFalse"
+unfolding fFalse_def fTrue_def fNot_def by auto
+
+lemma fconj_table:
+"fconj fFalse P = fFalse"
+"fconj P fFalse = fFalse"
+"fconj fTrue fTrue = fTrue"
+unfolding fFalse_def fTrue_def fconj_def by auto
+
+lemma fdisj_table:
+"fdisj fTrue P = fTrue"
+"fdisj P fTrue = fTrue"
+"fdisj fFalse fFalse = fFalse"
+unfolding fFalse_def fTrue_def fdisj_def by auto
+
+lemma fimplies_table:
+"fimplies P fTrue = fTrue"
+"fimplies fFalse P = fTrue"
+"fimplies fTrue fFalse = fFalse"
+unfolding fFalse_def fTrue_def fimplies_def by auto
+
+lemma fequal_table:
+"fequal x x = fTrue"
+"x = y \<or> fequal x y = fFalse"
+unfolding fFalse_def fTrue_def fequal_def by auto
+
+lemma fAll_table:
+"Ex (fComp P) \<or> fAll P = fTrue"
+"All P \<or> fAll P = fFalse"
+unfolding fFalse_def fTrue_def fComp_def fAll_def by auto
+
+lemma fEx_table:
+"All (fComp P) \<or> fEx P = fTrue"
+"Ex P \<or> fEx P = fFalse"
+unfolding fFalse_def fTrue_def fComp_def fEx_def by auto
+
+lemma fNot_law:
+"fNot P \<noteq> P"
+unfolding fNot_def by auto
+
+lemma fComp_law:
+"fComp P x \<longleftrightarrow> \<not> P x"
+unfolding fComp_def ..
+
+lemma fconj_laws:
+"fconj P P \<longleftrightarrow> P"
+"fconj P Q \<longleftrightarrow> fconj Q P"
+"fNot (fconj P Q) \<longleftrightarrow> fdisj (fNot P) (fNot Q)"
+unfolding fNot_def fconj_def fdisj_def by auto
+
+lemma fdisj_laws:
+"fdisj P P \<longleftrightarrow> P"
+"fdisj P Q \<longleftrightarrow> fdisj Q P"
+"fNot (fdisj P Q) \<longleftrightarrow> fconj (fNot P) (fNot Q)"
+unfolding fNot_def fconj_def fdisj_def by auto
+
+lemma fimplies_laws:
+"fimplies P Q \<longleftrightarrow> fdisj (\<not> P) Q"
+"fNot (fimplies P Q) \<longleftrightarrow> fconj P (fNot Q)"
+unfolding fNot_def fconj_def fdisj_def fimplies_def by auto
+
+lemma fequal_laws:
+"fequal x y = fequal y x"
+"fequal x y = fFalse \<or> fequal y z = fFalse \<or> fequal x z = fTrue"
+"fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
+unfolding fFalse_def fTrue_def fequal_def by auto
+
+lemma fAll_law:
+"fNot (fAll R) \<longleftrightarrow> fEx (fComp R)"
+unfolding fNot_def fComp_def fAll_def fEx_def by auto
+
+lemma fEx_law:
+"fNot (fEx R) \<longleftrightarrow> fAll (fComp R)"
+unfolding fNot_def fComp_def fAll_def fEx_def by auto
+
 subsection {* Setup *}
 
 use "Tools/ATP/atp_problem_generate.ML"

--- a/src/HOL/Metis.thy	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/Metis.thy	Mon May 21 10:39:32 2012 +0200
@@ -47,10 +47,13 @@
 
 setup {* Metis_Tactic.setup *}
 
-hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda
-hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
-    fequal_def select_def not_atomize atomize_not_select not_atomize_select
-    select_FalseI lambda_def eq_lambdaI
+hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal
+    lambda
+hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select
+    select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
+    fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table
+    fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
+    fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
 
 
 subsection {* Try0 *}

--- a/src/HOL/TPTP/atp_problem_import.ML	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Mon May 21 10:39:32 2012 +0200
@@ -15,7 +15,8 @@
   val can_tac : Proof.context -> tactic -> term -> bool
   val SOLVE_TIMEOUT :  int -> string -> tactic -> tactic
   val atp_tac :
-    Proof.context -> (string * string) list -> int -> string -> int -> tactic
+    Proof.context -> int -> (string * string) list -> int -> string -> int
+    -> tactic
   val smt_solver_tac : string -> Proof.context -> int -> tactic
   val freeze_problem_consts : theory -> term -> term
   val make_conj : term list * term list -> term list -> term
@@ -177,31 +178,51 @@
       in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
   end
 
-fun atp_tac ctxt override_params timeout prover =
-  Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
-      ([("debug", if debug then "true" else "false"),
-        ("overlord", if overlord then "true" else "false"),
-        ("provers", prover),
-        ("timeout", string_of_int timeout)] @ override_params)
-      {add = [(Facts.named (Thm.derivation_name ext), [])],
-       del = [], only = true}
+fun atp_tac ctxt aggressivity override_params timeout prover =
+  let
+    val ctxt =
+      ctxt |> Config.put Sledgehammer_Provers.aggressive (aggressivity > 0)
+  in
+    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
+        ([("debug", if debug then "true" else "false"),
+          ("overlord", if overlord then "true" else "false"),
+          ("provers", prover),
+          ("timeout", string_of_int timeout)] @
+         (if aggressivity > 0 then
+            [("type_enc",
+              if aggressivity = 1 then "mono_native" else "poly_guards??"),
+             ("slicing", "false")]
+          else
+            []) @
+         override_params)
+        {add = [(Facts.named (Thm.derivation_name ext), [])],
+         del = [], only = true}
+  end
 
 fun sledgehammer_tac demo ctxt timeout i =
   let
-    val frac = if demo then 6 else 4
-    fun slice prover =
-      SOLVE_TIMEOUT (timeout div frac) prover
-                    (atp_tac ctxt [] (timeout div frac) prover i)
+    val frac = if demo then 16 else 12
+    fun slice mult aggressivity prover =
+      SOLVE_TIMEOUT (mult * timeout div frac)
+          (prover ^
+           (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
+            else ""))
+          (atp_tac ctxt aggressivity [] (timeout div frac) prover i)
   in
-    (if demo then
-       slice ATP_Systems.satallaxN
-       ORELSE slice ATP_Systems.leo2N
-     else
-       no_tac)
-    ORELSE slice ATP_Systems.spassN
-    ORELSE slice ATP_Systems.vampireN
-    ORELSE slice ATP_Systems.eN
-    ORELSE slice ATP_Systems.z3_tptpN
+    slice 2 0 ATP_Systems.spassN
+    ORELSE slice 2 0 ATP_Systems.vampireN
+    ORELSE slice 2 0 ATP_Systems.eN
+    ORELSE slice 2 0 ATP_Systems.z3_tptpN
+    ORELSE slice 1 1 ATP_Systems.spassN
+    ORELSE slice 1 2 ATP_Systems.eN
+    ORELSE slice 1 1 ATP_Systems.vampireN
+    ORELSE slice 1 2 ATP_Systems.vampireN
+    ORELSE
+      (if demo then
+         slice 2 0 ATP_Systems.satallaxN
+         ORELSE slice 2 0 ATP_Systems.leo2N
+       else
+         no_tac)
   end
 
 fun smt_solver_tac solver ctxt =
@@ -212,15 +233,15 @@
 fun auto_etc_tac ctxt timeout i =
   SOLVE_TIMEOUT (timeout div 20) "nitpick"
       (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "simp"
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
       (asm_full_simp_tac (simpset_of ctxt) i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
       (auto_tac ctxt
-       THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "z3" (smt_solver_tac "z3" ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "cvc3" (smt_solver_tac "cvc3" ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
+       THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Systems.spassN))
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
@@ -264,11 +285,11 @@
     val (conjs, assms, ctxt) =
       read_tptp_file thy (freeze_problem_consts thy) file_name
     val conj = make_conj assms conjs
-    val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.spassN
+    val last_hope = if demo then ATP_Systems.satallaxN else ATP_Systems.vampireN
   in
     (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
      can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
-     can_tac ctxt (atp_tac ctxt [] timeout last_hope 1) conj)
+     can_tac ctxt (atp_tac ctxt 2 [] timeout last_hope 1) conj)
     |> print_szs_from_success conjs
   end
 

--- a/src/HOL/TPTP/atp_theory_export.ML	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Mon May 21 10:39:32 2012 +0200
@@ -183,8 +183,8 @@
       |> map (fn ((_, loc), th) =>
                  ((Thm.get_name_hint th, loc),
                    th |> prop_of |> mono ? monomorphize_term ctxt))
-      |> prepare_atp_problem ctxt format Axiom type_enc true combsN false false
-                             true [] @{prop False}
+      |> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false
+                             false true [] @{prop False}
       |> #1
     val atp_problem =
       atp_problem

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon May 21 10:39:32 2012 +0200
@@ -15,6 +15,8 @@
   type formula_kind = ATP_Problem.formula_kind
   type 'a problem = 'a ATP_Problem.problem
 
+  datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
+
   datatype scope = Global | Local | Assum | Chained
   datatype status =
     General | Induction | Intro | Inductive | Elim | Simp | Def
@@ -95,12 +97,12 @@
     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   val unmangled_const : string -> string * (string, 'b) ho_term list
   val unmangled_const_name : string -> string list
-  val helper_table : ((string * bool) * thm list) list
+  val helper_table : ((string * bool) * (status * thm) list) list
   val trans_lams_from_string :
     Proof.context -> type_enc -> string -> term list -> term list * term list
   val factsN : string
   val prepare_atp_problem :
-    Proof.context -> atp_format -> formula_kind -> type_enc -> bool -> string
+    Proof.context -> atp_format -> formula_kind -> type_enc -> mode -> string
     -> bool -> bool -> bool -> term list -> term
     -> ((string * stature) * term) list
     -> string problem * string Symtab.table * (string * stature) list vector
@@ -117,6 +119,8 @@
 
 type name = string * string
 
+datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter
+
 datatype scope = Global | Local | Assum | Chained
 datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def
 type stature = scope * status
@@ -1587,12 +1591,21 @@
     pred_sym andalso min_ary = max_ary
   | NONE => false
 
-val app_op = `(make_fixed_const NONE) app_op_name
-val predicator_combconst =
+val fTrue_iconst =
+  IConst ((const_prefix ^ "fTrue", @{const_name ATP.fTrue}), @{typ bool}, [])
+val predicator_iconst =
   IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
 
+fun predicatify aggressive tm =
+  if aggressive then
+    IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm),
+          fTrue_iconst)
+  else
+    IApp (predicator_iconst, tm)
+
+val app_op = `(make_fixed_const NONE) app_op_name
+
 fun list_app head args = fold (curry (IApp o swap)) args head
-fun predicator tm = IApp (predicator_combconst, tm)
 
 fun mk_app_op type_enc head arg =
   let
@@ -1603,7 +1616,8 @@
       |> mangle_type_args_in_iterm type_enc
   in list_app app [head, arg] end
 
-fun firstorderize_fact thy monom_constrs type_enc sym_tab uncurried_aliases =
+fun firstorderize_fact thy monom_constrs type_enc sym_tab uncurried_aliases
+                       aggressive =
   let
     fun do_app arg head = mk_app_op type_enc head arg
     fun list_app_ops head args = fold do_app args head
@@ -1625,8 +1639,8 @@
     fun introduce_predicators tm =
       case strip_iterm_comb tm of
         (IConst ((s, _), _, _), _) =>
-        if is_pred_sym sym_tab s then tm else predicator tm
-      | _ => predicator tm
+        if is_pred_sym sym_tab s then tm else predicatify aggressive tm
+      | _ => predicatify aggressive tm
     val do_iterm =
       not (is_type_enc_higher_order type_enc)
       ? (introduce_app_ops #> introduce_predicators)
@@ -1639,45 +1653,75 @@
 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
 
 (* The Boolean indicates that a fairly sound type encoding is needed. *)
+val base_helper_table =
+  [(("COMBI", false), [(Def, @{thm Meson.COMBI_def})]),
+   (("COMBK", false), [(Def, @{thm Meson.COMBK_def})]),
+   (("COMBB", false), [(Def, @{thm Meson.COMBB_def})]),
+   (("COMBC", false), [(Def, @{thm Meson.COMBC_def})]),
+   (("COMBS", false), [(Def, @{thm Meson.COMBS_def})]),
+   ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
+   (("fFalse", false), [(General, not_ffalse)]),
+   (("fFalse", true), [(General, @{thm True_or_False})]),
+   (("fTrue", false), [(General, ftrue)]),
+   (("fTrue", true), [(General, @{thm True_or_False})]),
+   (("If", true),
+    [(Def, @{thm if_True}), (Def, @{thm if_False}),
+     (General, @{thm True_or_False})])]
+
 val helper_table =
-  [(("COMBI", false), @{thms Meson.COMBI_def}),
-   (("COMBK", false), @{thms Meson.COMBK_def}),
-   (("COMBB", false), @{thms Meson.COMBB_def}),
-   (("COMBC", false), @{thms Meson.COMBC_def}),
-   (("COMBS", false), @{thms Meson.COMBS_def}),
-   ((predicator_name, false), [not_ffalse, ftrue]),
-   ((predicator_name, true), @{thms True_or_False}),
-(* FIXME: Metis doesn't like existentials in helpers
-   ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]),
-*)
-   (("fFalse", false), [not_ffalse]),
-   (("fFalse", true), @{thms True_or_False}),
-   (("fTrue", false), [ftrue]),
-   (("fTrue", true), @{thms True_or_False}),
-   (("fNot", false),
+  base_helper_table @
+  [(("fNot", false),
     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
-           fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
+           fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
+    |> map (pair Def)),
    (("fconj", false),
     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
-        by (unfold fconj_def) fast+}),
+        by (unfold fconj_def) fast+}
+    |> map (pair General)),
    (("fdisj", false),
     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
-        by (unfold fdisj_def) fast+}),
+        by (unfold fdisj_def) fast+}
+    |> map (pair General)),
    (("fimplies", false),
     @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
-        by (unfold fimplies_def) fast+}),
+        by (unfold fimplies_def) fast+}
+    |> map (pair General)),
    (("fequal", true),
     (* This is a lie: Higher-order equality doesn't need a sound type encoding.
        However, this is done so for backward compatibility: Including the
        equality helpers by default in Metis breaks a few existing proofs. *)
     @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
-           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
+           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
+    |> map (pair General)),
    (* Partial characterization of "fAll" and "fEx". A complete characterization
       would require the axiom of choice for replay with Metis. *)
-   (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
-   (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
-   (("If", true), @{thms if_True if_False True_or_False})]
-  |> map (apsnd (map zero_var_indexes))
+   (("fAll", false),
+    [(General, @{lemma "~ fAll P | P x" by (auto simp: fAll_def)})]),
+   (("fEx", false),
+    [(General, @{lemma "~ P x | fEx P" by (auto simp: fEx_def)})])]
+  |> map (apsnd (map (apsnd zero_var_indexes)))
+
+val aggressive_helper_table =
+  base_helper_table @
+  [((predicator_name, true),
+    @{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
+   ((app_op_name, true),
+    [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
+   (("fconj", false),
+    @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Def)),
+   (("fdisj", false),
+    @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Def)),
+   (("fimplies", false),
+    @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
+    |> map (pair Def)),
+   (("fequal", false),
+    (@{thms fequal_table} |> map (pair Def)) @
+    (@{thms fequal_laws} |> map (pair General))),
+   (("fAll", false),
+    @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
+   (("fEx", false),
+    @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
+  |> map (apsnd (map (apsnd zero_var_indexes)))
 
 fun atype_of_type_vars (Native (_, Polymorphic, _)) = SOME atype_of_types
   | atype_of_type_vars _ = NONE
@@ -1705,19 +1749,22 @@
 
 val type_tag = `(make_fixed_const NONE) type_tag_name
 
-fun should_specialize_helper type_enc t =
+fun could_specialize_helpers type_enc =
   polymorphism_of_type_enc type_enc <> Polymorphic andalso
-  level_of_type_enc type_enc <> No_Types andalso
+  level_of_type_enc type_enc <> No_Types
+fun should_specialize_helper type_enc t =
+  could_specialize_helpers type_enc andalso
   not (null (Term.hidden_polymorphism t))
 
-fun add_helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
+fun add_helper_facts_for_sym ctxt format type_enc aggressive
+                             (s, {types, ...} : sym_info) =
   case unprefix_and_unascii const_prefix s of
     SOME mangled_s =>
     let
       val thy = Proof_Context.theory_of ctxt
       val unmangled_s = mangled_s |> unmangled_const_name |> hd
       fun dub needs_fairly_sound j k =
-        unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
+        ascii_of unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
         (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
         (if needs_fairly_sound then typed_helper_suffix
          else untyped_helper_suffix)
@@ -1729,30 +1776,35 @@
           in monomorphic_term tyenv t end
         else
           specialize_type thy (invert_const unmangled_s, T) t
-      fun dub_and_inst needs_fairly_sound (t, j) =
+      fun dub_and_inst needs_fairly_sound ((status, t), j) =
         (if should_specialize_helper type_enc t then
-           map (specialize_helper t) types
+           map_filter (try (specialize_helper t)) types
          else
            [t])
         |> tag_list 1
-        |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Def)), t))
+        |> map (fn (k, t) =>
+                   ((dub needs_fairly_sound j k, (Global, status)), t))
       val make_facts = map_filter (make_fact ctxt format type_enc false)
       val fairly_sound = is_type_enc_fairly_sound type_enc
+      val could_specialize = could_specialize_helpers type_enc
     in
       fold (fn ((helper_s, needs_fairly_sound), ths) =>
-               if helper_s <> unmangled_s orelse
-                  (needs_fairly_sound andalso not fairly_sound) then
+               if (needs_fairly_sound andalso not fairly_sound) orelse
+                  (helper_s <> unmangled_s andalso
+                   (not aggressive orelse could_specialize)) then
                  I
                else
                  ths ~~ (1 upto length ths)
-                 |> maps (dub_and_inst needs_fairly_sound o apfst prop_of)
+                 |> maps (dub_and_inst needs_fairly_sound
+                          o apfst (apsnd prop_of))
                  |> make_facts
                  |> union (op = o pairself #iformula))
-           helper_table
+           (if aggressive then aggressive_helper_table else helper_table)
     end
   | NONE => I
-fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
-  Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc) sym_tab []
+fun helper_facts_for_sym_table ctxt format type_enc aggressive sym_tab =
+  Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc aggressive)
+                  sym_tab []
 
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
@@ -2602,7 +2654,7 @@
 
 val app_op_and_predicator_threshold = 50
 
-fun prepare_atp_problem ctxt format prem_kind type_enc exporter lam_trans
+fun prepare_atp_problem ctxt format prem_kind type_enc mode lam_trans
                         uncurried_aliases readable_names preproc hyp_ts concl_t
                         facts =
   let
@@ -2613,11 +2665,16 @@
        ruin everything. Hence we do it only if there are few facts (which is
        normally the case for "metis" and the minimizer). *)
     val app_op_level =
-      if length facts > app_op_and_predicator_threshold then
+      if mode = Sledgehammer_Aggressive then
+        Full_App_Op_And_Predicator
+      else if length facts + length hyp_ts
+              > app_op_and_predicator_threshold then
         if polymorphism_of_type_enc type_enc = Polymorphic then Min_App_Op
         else Sufficient_App_Op
       else
         Sufficient_App_Op_And_Predicator
+    val exporter = (mode = Exporter)
+    val aggressive = (mode = Sledgehammer_Aggressive)
     val lam_trans =
       if lam_trans = keep_lamsN andalso
          not (is_type_enc_higher_order type_enc) then
@@ -2637,7 +2694,7 @@
       |>> map (make_fixed_const (SOME type_enc))
     fun firstorderize in_helper =
       firstorderize_fact thy monom_constrs type_enc sym_tab0
-                         (uncurried_aliases andalso not in_helper)
+          (uncurried_aliases andalso not in_helper) aggressive
     val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
     val (ho_stuff, sym_tab) =
       sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
@@ -2649,7 +2706,7 @@
       |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
               uncurried_alias_eq_tms
     val helpers =
-      sym_tab |> helper_facts_for_sym_table ctxt format type_enc
+      sym_tab |> helper_facts_for_sym_table ctxt format type_enc aggressive
               |> map (firstorderize true)
     val mono_Ts =
       helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc

--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 10:39:32 2012 +0200
@@ -363,7 +363,7 @@
           |> try (single o hd) |> the_default []
 
 fun commute_eq (AAtom (ATerm (s, tms))) = AAtom (ATerm (s, rev tms))
-  | commute_eq t = raise Fail "expected equation"
+  | commute_eq _ = raise Fail "expected equation"
 
 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
             <formula> <extra_arguments>\).

--- a/src/HOL/Tools/Metis/metis_generate.ML	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Mon May 21 10:39:32 2012 +0200
@@ -176,10 +176,10 @@
         case (String.isSuffix typed_helper_suffix ident,
               space_explode "_" ident) of
           (needs_fairly_sound, _ :: const :: j :: _) =>
-          nth ((const, needs_fairly_sound)
-               |> AList.lookup (op =) helper_table |> the)
+          nth (AList.lookup (op =) helper_table (const, needs_fairly_sound)
+               |> the)
               (the (Int.fromString j) - 1)
-          |> prepare_helper
+          |> snd |> prepare_helper
           |> Isa_Raw |> some
         | _ => raise Fail ("malformed helper identifier " ^ quote ident)
       else case try (unprefix fact_prefix) ident of
@@ -242,7 +242,7 @@
     *)
     val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
     val (atp_problem, _, _, lifted, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis type_enc false lam_trans false
+      prepare_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false
                           false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 21 10:39:31 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 21 10:39:32 2012 +0200
@@ -65,6 +65,7 @@
 
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
+  val aggressive : bool Config.T
   val atp_full_names : bool Config.T
   val smt_triggers : bool Config.T
   val smt_weights : bool Config.T
@@ -334,6 +335,8 @@
   Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
 val problem_prefix =
   Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
+val aggressive =
+  Attrib.setup_config_bool @{binding sledgehammer_aggressive} (K false)
 
 (* In addition to being easier to read, readable names are often much shorter,
    especially if types are mangled in names. This makes a difference for some
@@ -589,6 +592,9 @@
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
+    val atp_mode =
+      if Config.get ctxt aggressive then Sledgehammer_Aggressive
+      else Sledgehammer
     val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
     val (dest_dir, problem_prefix) =
       if overlord then overlord_file_location_for_prover name
@@ -710,9 +716,9 @@
                     |> polymorphism_of_type_enc type_enc <> Polymorphic
                        ? monomorphize_facts
                     |> map (apsnd prop_of)
-                    |> prepare_atp_problem ctxt format prem_kind type_enc false
-                           lam_trans uncurried_aliases readable_names true
-                           hyp_ts concl_t
+                    |> prepare_atp_problem ctxt format prem_kind type_enc
+                                           atp_mode lam_trans uncurried_aliases
+                                           readable_names true hyp_ts concl_t
                 fun sel_weights () = atp_problem_selection_weights atp_problem
                 fun ord_info () = atp_problem_term_order_info atp_problem
                 val ord = effective_term_order ctxt name