obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be

--- a/NEWS	Tue Jun 07 07:57:24 2011 +0200
+++ b/NEWS	Tue Jun 07 08:52:35 2011 +0200
@@ -86,7 +86,8 @@
   - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
 
 * Metis:
-  - Obsoleted "metisF" -- use "metis" instead.
+  - Removed "metisF" -- use "metis" instead.
+  - Obsoleted "metisFT" -- use "metis (full_types)" instead.
 
 * "try":
   - Added "simp:", "intro:", and "elim:" options.

--- a/doc-src/Sledgehammer/sledgehammer.tex	Tue Jun 07 07:57:24 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Jun 07 08:52:35 2011 +0200
@@ -495,30 +495,35 @@
 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
 value or to try several provers and keep the nicest-looking proof.
 
-\point{What is metisFT?}
+\point{What is the \textit{full\_types}/\textit{no\_types} argument to Metis?}
 
-The \textit{metisFT} proof method is the fully-typed version of Metis. It is
-much slower than \textit{metis}, but the proof search is fully typed, and it
-also includes more powerful rules such as the axiom ``$x = \mathit{True}
-\mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places (e.g.,
-in set comprehensions). The method kicks in automatically as a fallback when
-\textit{metis} fails, and it is sometimes generated by Sledgehammer instead of
-\textit{metis} if the proof obviously requires type information or if
-\textit{metis} failed when Sledgehammer preplayed the proof. (By default,
-Sledgehammer tries to run \textit{metis} and/or \textit{metisFT} for 4 seconds
-to ensure that the generated one-line proofs actually work and to display timing
-information. This can be configured using the \textit{preplay\_timeout} option
-(\S\ref{timeouts}).)
+The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed
+version of Metis. It is somewhat slower than \textit{metis}, but the proof
+search is fully typed, and it also includes more powerful rules such as the
+axiom ``$x = \mathit{True} \mathrel{\lor} x = \mathit{False}$'' for reasoning in
+higher-order places (e.g., in set comprehensions). The method kicks in
+automatically as a fallback when \textit{metis} fails, and it is sometimes
+generated by Sledgehammer instead of \textit{metis} if the proof obviously
+requires type information or if \textit{metis} failed when Sledgehammer
+preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
+various options for up to 4 seconds to ensure that the generated one-line proofs
+actually work and to display timing information. This can be configured using
+the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
 
 If you see the warning
 
 \prew
 \slshape
-Metis: Falling back on ``\textit{metisFT\/}''.
+Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
 \postw
 
-in a successful Metis proof, you can advantageously replace the \textit{metis}
-call with \textit{metisFT}.
+in a successful Metis proof, you can advantageously pass the
+\textit{full\_types} option to \textit{metis} directly.
+
+At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
+uses no type information at all during the proof search, which is more efficient
+but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
+generated by Sledgehammer.
 
 \point{Are generated proofs minimal?}
 
@@ -664,8 +669,8 @@
 Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and
 \qty{facts} is a list of arbitrary facts. \qty{type\_sys} may also be
 \textit{full\_types}, in which case an appropriate type-sound encoding is
-chosen. The companion proof method \textit{metisFT} is an abbreviation for
-``\textit{metis}~(\textit{full\_types})''.
+chosen, \textit{partial\_types} (the default), or \textit{no\_types}, a synonym
+for \textit{erased}.
 
 \section{Option Reference}
 \label{option-reference}
@@ -764,7 +769,11 @@
 \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
 the external provers, Metis itself can be used for proof search.
 
-\item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis.
+\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
+Metis, corresponding to \textit{metis} (\textit{full\_types}).
+
+\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
+corresponding to \textit{metis} (\textit{no\_types}).
 \end{enum}
 
 In addition, the following remote provers are supported:
@@ -903,14 +912,12 @@
 arguments, to resolve overloading.
 
 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
-tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. This
-coincides with the encoding used by the \textit{metisFT} command.
+tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
 
 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
 Like for \textit{poly\_preds} constants are annotated with their types to
 resolve overloading, but otherwise no type information is encoded. This
-coincides with the encoding used by the \textit{metis} command (before it falls
-back on \textit{metisFT}).
+coincides with the default encoding used by the \textit{metis} command.
 
 \item[$\bullet$]
 \textbf{%

--- a/src/HOL/Metis_Examples/Clausification.thy	Tue Jun 07 07:57:24 2011 +0200
+++ b/src/HOL/Metis_Examples/Clausification.thy	Tue Jun 07 08:52:35 2011 +0200
@@ -28,13 +28,13 @@
 by (metis qax)
 
 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
-by (metisFT qax)
+by (metis (full_types) qax)
 
 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
 by (metis qax)
 
 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-by (metisFT qax)
+by (metis (full_types) qax)
 
 declare [[metis_new_skolemizer]]
 
@@ -42,13 +42,13 @@
 by (metis qax)
 
 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
-by (metisFT qax)
+by (metis (full_types) qax)
 
 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
 by (metis qax)
 
 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
-by (metisFT qax)
+by (metis (full_types) qax)
 
 declare [[meson_max_clauses = 60]]
 
@@ -64,7 +64,7 @@
 by (metis rax)
 
 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
-by (metisFT rax)
+by (metis (full_types) rax)
 
 declare [[metis_new_skolemizer]]
 
@@ -72,7 +72,7 @@
 by (metis rax)
 
 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
-by (metisFT rax)
+by (metis (full_types) rax)
 
 lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
        (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
@@ -84,7 +84,7 @@
        (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
        (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
        (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
-by (metisFT rax)
+by (metis (full_types) rax)
 
 
 text {* Definitional CNF for goal *}
@@ -100,7 +100,7 @@
 
 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
-by (metisFT pax)
+by (metis (full_types) pax)
 
 declare [[metis_new_skolemizer]]
 
@@ -110,7 +110,7 @@
 
 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
-by (metisFT pax)
+by (metis (full_types) pax)
 
 
 text {* New Skolemizer *}
@@ -134,7 +134,7 @@
   assumes a: "Quotient R Abs Rep"
   shows "symp R"
 using a unfolding Quotient_def using sympI
-by metisFT
+by (metis (full_types))
 
 lemma
   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>

--- a/src/HOL/Metis_Examples/Proxies.thy	Tue Jun 07 07:57:24 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Tue Jun 07 08:52:35 2011 +0200
@@ -66,7 +66,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
-by (metisFT id_apply)
+by (metis (full_types) id_apply)
 
 lemma "id True"
 sledgehammer [type_sys = erased, expect = some] (id_apply)
@@ -127,7 +127,7 @@
 sledgehammer [type_sys = mangled_tags, expect = some] ()
 sledgehammer [type_sys = mangled_preds?, expect = some] ()
 sledgehammer [type_sys = mangled_preds, expect = some] ()
-by metisFT
+by (metis (full_types))
 
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
 sledgehammer [type_sys = erased, expect = some] (id_apply)

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 07 07:57:24 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 07 08:52:35 2011 +0200
@@ -342,7 +342,8 @@
   (case AList.lookup (op =) args reconstructorK of
     SOME name => name
   | NONE =>
-    if String.isSubstring "metisFT" msg then "metisFT"
+    if String.isSubstring "metis (full_types)" msg then "metis (full_types)"
+    else if String.isSubstring "metis (no_types)" msg then "metis (no_types)"
     else if String.isSubstring "metis" msg then "metis"
     else "smt")
 
@@ -541,8 +542,10 @@
             Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
        else if !reconstructor = "smt" then
          SMT_Solver.smt_tac
-       else if full orelse !reconstructor = "metisFT" then
-         Metis_Tactics.metisFT_tac
+       else if full orelse !reconstructor = "metis (full_types)" then
+         Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
+       else if !reconstructor = "metis (no_types)" then
+         Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
        else
          Metis_Tactics.metis_tac []) ctxt thms
     fun apply_reconstructor thms =

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Jun 07 07:57:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Jun 07 08:52:35 2011 +0200
@@ -16,7 +16,8 @@
 
   datatype reconstructor =
     Metis |
-    MetisFT |
+    Metis_Full_Types |
+    Metis_No_Types |
     SMT of string
 
   datatype play =
@@ -67,7 +68,8 @@
 
 datatype reconstructor =
   Metis |
-  MetisFT |
+  Metis_Full_Types |
+  Metis_No_Types |
   SMT of string
 
 datatype play =
@@ -251,8 +253,10 @@
 
 (** Soft-core proof reconstruction: Metis one-liner **)
 
+(* unfortunate leaking abstraction *)
 fun reconstructor_name Metis = "metis"
-  | reconstructor_name MetisFT = "metisFT"
+  | reconstructor_name Metis_Full_Types = "metis (full_types)"
+  | reconstructor_name Metis_No_Types = "metis (no_types)"
   | reconstructor_name (SMT _) = "smt"
 
 fun reconstructor_settings (SMT settings) = settings
@@ -1042,7 +1046,7 @@
        else
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
-    val reconstructor = if full_types then MetisFT else Metis
+    val reconstructor = if full_types then Metis_Full_Types else Metis
     fun do_facts (ls, ss) =
       reconstructor_command reconstructor 1 1
           (ls |> sort_distinct (prod_ord string_ord int_ord),

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Jun 07 07:57:24 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Jun 07 08:52:35 2011 +0200
@@ -10,14 +10,16 @@
 signature METIS_TACTICS =
 sig
   val metisN : string
-  val metisFT_N : string
-  val default_unsound_type_sys : string
-  val default_sound_type_sys : string
+  val full_typesN : string
+  val partial_typesN : string
+  val no_typesN : string
+  val full_type_sys : string
+  val partial_type_sys : string
+  val no_type_sys : string
   val trace : bool Config.T
   val verbose : bool Config.T
   val new_skolemizer : bool Config.T
   val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
-  val metisFT_tac : Proof.context -> thm list -> int -> tactic
   val setup : theory -> theory
 end
 
@@ -29,18 +31,25 @@
 open Metis_Reconstruct
 
 val metisN = Binding.qualified_name_of @{binding metis}
-val metisFT_N = Binding.qualified_name_of @{binding metisFT}
+
 val full_typesN = "full_types"
+val partial_typesN = "partial_types"
+val no_typesN = "no_types"
 
-val default_unsound_type_sys = "poly_args"
-val default_sound_type_sys = "poly_preds_heavy_query"
+val full_type_sys = "poly_preds_heavy_query"
+val partial_type_sys = "poly_args"
+val no_type_sys = "erased"
+
+val type_sys_aliases =
+  [(full_typesN, full_type_sys),
+   (partial_typesN, partial_type_sys),
+   (no_typesN, no_type_sys)]
 
 fun method_call_for_type_sys type_sys =
-  if type_sys = default_sound_type_sys then
-    (@{binding metisFT}, "")
-  else
-    (@{binding metis},
-     if type_sys = default_unsound_type_sys then "" else type_sys)
+  metisN ^ " (" ^
+  (case AList.find (op =) type_sys_aliases type_sys of
+     [alias] => alias
+   | _ => type_sys) ^ ")"
 
 val new_skolemizer =
   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
@@ -168,13 +177,10 @@
                         (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
                          else ""))
          | type_sys :: _ =>
-           let val (binding, arg) = method_call_for_type_sys type_sys in
-             (verbose_warning ctxt
-                  ("Falling back on " ^
-                   quote (Binding.qualified_name_of binding ^
-                          (arg |> arg <> "" ? enclose " (" ")")) ^ "...");
-              FOL_SOLVE fallback_type_syss ctxt cls ths0)
-            end
+           (verbose_warning ctxt
+                ("Falling back on " ^
+                 quote (method_call_for_type_sys type_sys) ^ "...");
+            FOL_SOLVE fallback_type_syss ctxt cls ths0)
 
 val neg_clausify =
   single
@@ -207,12 +213,11 @@
       Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
   end
 
-val metis_default_type_syss = [default_unsound_type_sys, default_sound_type_sys]
-val metisFT_type_syss = [default_sound_type_sys]
+val metis_default_type_syss = [partial_type_sys, full_type_sys]
+val metisFT_type_syss = [full_type_sys]
 
 fun metis_tac [] = generic_metis_tac metis_default_type_syss
   | metis_tac type_syss = generic_metis_tac type_syss
-val metisFT_tac = generic_metis_tac metisFT_type_syss
 
 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
    "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
@@ -224,6 +229,12 @@
 
 fun method type_syss (type_sys, ths) ctxt facts =
   let
+    val _ =
+      if type_syss = metisFT_type_syss then
+        legacy_feature "Old 'metisFT' method -- \
+                       \use 'metis (full_types)' instead"
+      else
+        ()
     val (schem_facts, nonschem_facts) = List.partition has_tvar facts
     val type_syss = type_sys |> Option.map single |> the_default type_syss
   in
@@ -232,19 +243,20 @@
               o generic_metis_tac type_syss ctxt (schem_facts @ ths))
   end
 
-fun setup_method (type_syss as type_sys :: _) =
+fun setup_method (binding, type_syss as type_sys :: _) =
   (if type_syss = metis_default_type_syss then
      (Args.parens Parse.short_ident
-      >> (fn s => if s = full_typesN then default_sound_type_sys else s))
+      >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s))
      |> Scan.option |> Scan.lift
    else
      Scan.succeed NONE)
   -- Attrib.thms >> (METHOD oo method type_syss)
-  |> Method.setup (fst (method_call_for_type_sys type_sys))
+  |> Method.setup binding
 
 val setup =
-  [(metis_default_type_syss, "Metis for FOL and HOL problems"),
-   (metisFT_type_syss,
+  [((@{binding metis}, metis_default_type_syss),
+    "Metis for FOL and HOL problems"),
+   ((@{binding metisFT}, metisFT_type_syss),
     "Metis for FOL/HOL problems with fully-typed translation")]
   |> fold (uncurry setup_method)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 07:57:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 08:52:35 2011 +0200
@@ -128,9 +128,18 @@
    "Async_Manager". *)
 val das_tool = "Sledgehammer"
 
-val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N]
+val metisN = Metis_Tactics.metisN
+val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN
+val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN
 
-val is_metis_prover = member (op =) metis_prover_names
+val metis_prover_infos =
+  [(metisN, Metis),
+   (metis_full_typesN, Metis_Full_Types),
+   (metis_no_typesN, Metis_No_Types)]
+
+val metis_reconstructors = map snd metis_prover_infos
+
+val is_metis_prover = AList.defined (op =) metis_prover_infos
 val is_atp = member (op =) o supported_atps
 
 val select_smt_solver =
@@ -265,7 +274,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val (remote_provers, local_provers) =
-      metis_prover_names @
+      map fst metis_prover_infos @
       sort_strings (supported_atps thy) @
       sort_strings (SMT_Solver.available_solvers_of ctxt)
       |> List.partition (String.isPrefix remote_prefix)
@@ -407,8 +416,11 @@
   in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
 
 fun tac_for_reconstructor Metis =
-    Metis_Tactics.metis_tac [Metis_Tactics.default_unsound_type_sys]
-  | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
+    Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys]
+  | tac_for_reconstructor Metis_Full_Types =
+    Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
+  | tac_for_reconstructor Metis_No_Types =
+    Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
   | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
 
 fun timed_reconstructor reconstructor debug timeout ths =
@@ -519,7 +531,9 @@
   (case preplay of
      Played (reconstructor, time) =>
      if Time.<= (time, metis_minimize_max_time) then
-       reconstructor_name reconstructor
+       case AList.find (op =) metis_prover_infos reconstructor of
+         metis_name :: _ => metis_name
+       | [] => name
      else
        name
    | _ => name)
@@ -780,7 +794,7 @@
                         |> map snd
               in
                 play_one_line_proof debug preplay_timeout used_ths state subgoal
-                                    [Metis, MetisFT]
+                                    metis_reconstructors
               end,
            fn preplay =>
               let
@@ -974,7 +988,7 @@
                 else "smt_solver = " ^ maybe_quote name
             in
               case play_one_line_proof debug preplay_timeout used_ths state
-                                       subgoal [Metis, MetisFT] of
+                                       subgoal metis_reconstructors of
                 p as Played _ => p
               | _ => Trust_Playable (SMT (smt_settings ()), NONE)
             end,
@@ -1004,9 +1018,10 @@
 fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
               ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
-    val reconstructor = if name = Metis_Tactics.metisN then Metis
-                        else if name = Metis_Tactics.metisFT_N then MetisFT
-                        else raise Fail ("unknown Metis version: " ^ quote name)
+    val reconstructor =
+      case AList.lookup (op =) metis_prover_infos name of
+        SOME r => r
+      | NONE => raise Fail ("unknown Metis version: " ^ quote name)
     val (used_facts, used_ths) =
       facts |> map untranslated_fact |> ListPair.unzip
   in