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