--- a/NEWS Tue Jun 07 11:12:05 2011 +0200
+++ b/NEWS Tue Jun 07 11:24:16 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 11:12:05 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 11:24:16 2011 +0200
@@ -495,30 +495,36 @@
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 are the \textit{full\_types} and \textit{no\_types} arguments 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
+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.
+
+Incidentally, 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.
\point{Are generated proofs minimal?}
@@ -529,11 +535,11 @@
improves Metis's speed and success rate, while also removing superfluous clutter
from the proof scripts.
-In earlier versions of Sledgehammer, generated proofs were accompanied by a
-suggestion to invoke the minimization tool. This step is now performed
-implicitly if it can be done in a reasonable amount of time (something that can
-be guessed from the number of facts in the original proof and the time it took
-to find it or replay it).
+In earlier versions of Sledgehammer, generated proofs were systematically
+accompanied by a suggestion to invoke the minimization tool. This step is now
+performed implicitly if it can be done in a reasonable amount of time (something
+that can be guessed from the number of facts in the original proof and the time
+it took to find it or replay it).
In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
@@ -662,10 +668,11 @@
where \qty{type\_sys} is a type system specification with the same semantics as
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})''.
+\qty{facts} is a list of arbitrary facts. In addition to the values listed in
+\S\ref{problem-encoding}, \qty{type\_sys} may also be \textit{full\_types}, in
+which case an appropriate type-sound encoding is chosen, \textit{partial\_types}
+(the default type-unsound encoding), or \textit{no\_types}, a synonym for
+\textit{erased}.
\section{Option Reference}
\label{option-reference}
@@ -764,7 +771,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 +914,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/IsaMakefile Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Jun 07 11:24:16 2011 +0200
@@ -1046,8 +1046,8 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
- ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
- ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
+ ex/ATP_Export.thy ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \
+ ex/BT.thy ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
ex/CASC_Setup.thy ex/CTL.thy ex/Case_Product.thy \
ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
@@ -1068,7 +1068,7 @@
ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
ex/sledgehammer_tactics.ML ex/Sqrt.thy \
ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
- ex/TPTP_Export.thy ex/Transfer_Ex.thy ex/Tree23.thy \
+ ex/Transfer_Ex.thy ex/Tree23.thy \
ex/Unification.thy ex/While_Combinator_Example.thy \
ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
ex/svc_test.thy \
--- a/src/HOL/Metis_Examples/Clausification.thy Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Metis_Examples/Clausification.thy Tue Jun 07 11:24:16 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 11:12:05 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy Tue Jun 07 11:24:16 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 11:12:05 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 07 11:24:16 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/SMT.thy Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/SMT.thy Tue Jun 07 11:24:16 2011 +0200
@@ -245,14 +245,14 @@
construction whose cycles are limited by the following option.
*}
-declare [[ smt_monomorph_limit = 10 ]]
+declare [[ monomorph_max_rounds = 5 ]]
text {*
In addition, the number of generated monomorphic instances is limited
by the following option.
*}
-declare [[ smt_monomorph_instances = 500 ]]
+declare [[ monomorph_max_new_instances = 500 ]]
--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 07 11:24:16 2011 +0200
@@ -70,7 +70,7 @@
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
val is_format_typed : format -> bool
- val tptp_strings_for_atp_problem : format -> string problem -> string list
+ val tptp_lines_for_atp_problem : format -> string problem -> string list
val ensure_cnf_problem :
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
@@ -283,7 +283,7 @@
| (_, SOME tm) =>
", " ^ string_for_term format (source |> the_default default_source) ^
", " ^ string_for_term format tm) ^ ").\n"
-fun tptp_strings_for_atp_problem format problem =
+fun tptp_lines_for_atp_problem format problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
maps (fn (_, []) => []
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 11:24:16 2011 +0200
@@ -16,7 +16,8 @@
datatype reconstructor =
Metis |
- MetisFT |
+ Metis_Full_Types |
+ Metis_No_Types |
SMT of string
datatype play =
@@ -41,7 +42,6 @@
Proof.context -> type_sys -> int list list -> int
-> (string * locality) list vector -> 'a proof -> string list option
val uses_typed_helpers : int list -> 'a proof -> bool
- val reconstructor_name : reconstructor -> string
val one_line_proof_text : one_line_params -> string
val make_tvar : string -> typ
val make_tfree : Proof.context -> string -> typ
@@ -67,7 +67,8 @@
datatype reconstructor =
Metis |
- MetisFT |
+ Metis_Full_Types |
+ Metis_No_Types |
SMT of string
datatype play =
@@ -251,9 +252,11 @@
(** Soft-core proof reconstruction: Metis one-liner **)
-fun reconstructor_name Metis = "metis"
- | reconstructor_name MetisFT = "metisFT"
- | reconstructor_name (SMT _) = "smt"
+(* unfortunate leaking abstraction *)
+fun name_of_reconstructor Metis = "metis"
+ | name_of_reconstructor Metis_Full_Types = "metis (full_types)"
+ | name_of_reconstructor Metis_No_Types = "metis (no_types)"
+ | name_of_reconstructor (SMT _) = "smt"
fun reconstructor_settings (SMT settings) = settings
| reconstructor_settings _ = ""
@@ -279,7 +282,7 @@
fun reconstructor_command reconstructor i n (ls, ss) =
using_labels ls ^
apply_on_subgoal (reconstructor_settings reconstructor) i n ^
- command_call (reconstructor_name reconstructor) ss
+ command_call (name_of_reconstructor reconstructor) ss
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
@@ -1042,7 +1045,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/ATP/atp_translate.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 07 11:24:16 2011 +0200
@@ -130,7 +130,7 @@
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_sys
-> bool option -> bool -> bool -> term list -> term
- -> ((string * locality) * thm) list
+ -> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
* (string * locality) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
@@ -1386,10 +1386,10 @@
facts =
let
val thy = Proof_Context.theory_of ctxt
- val fact_ts = facts |> map (prop_of o snd)
+ val fact_ts = facts |> map snd
val (facts, fact_names) =
- facts |> map (fn (name, th) =>
- (name, prop_of th)
+ facts |> map (fn (name, t) =>
+ (name, t)
|> make_fact ctxt format type_sys false true true true
|> rpair name)
|> map_filter (try (apfst the))
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 07 11:24:16 2011 +0200
@@ -11,10 +11,6 @@
sig
exception METIS of string * string
- val trace : bool Config.T
- val trace_msg : Proof.context -> (unit -> string) -> unit
- val verbose : bool Config.T
- val verbose_warning : Proof.context -> string -> unit
val hol_clause_from_metis :
Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
-> term
@@ -38,13 +34,6 @@
exception METIS of string * string
-val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
-val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
-
-fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
-fun verbose_warning ctxt msg =
- if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
-
datatype term_or_type = SomeTerm of term | SomeType of typ
fun terms_of [] = []
--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Jun 07 11:24:16 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/Metis/metis_translate.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 11:24:16 2011 +0200
@@ -20,6 +20,10 @@
val metis_app_op : string
val metis_type_tag : string
val metis_generated_var_prefix : string
+ val trace : bool Config.T
+ val verbose : bool Config.T
+ val trace_msg : Proof.context -> (unit -> string) -> unit
+ val verbose_warning : Proof.context -> string -> unit
val metis_name_table : ((string * int) * (string * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val prepare_metis_problem :
@@ -39,6 +43,13 @@
val metis_type_tag = ":"
val metis_generated_var_prefix = "_"
+val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
+val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
+
+fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
+fun verbose_warning ctxt msg =
+ if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
+
val metis_name_table =
[((tptp_equal, 2), (metis_equal, false)),
((tptp_old_equal, 2), (metis_equal, false)),
@@ -180,7 +191,7 @@
prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
false false props @{prop False} []
(*
-val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem))
+val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
*)
(* "rev" is for compatibility *)
val axioms =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 11:24:16 2011 +0200
@@ -10,10 +10,11 @@
sig
type failure = ATP_Proof.failure
type locality = ATP_Translate.locality
- type relevance_fudge = Sledgehammer_Filter.relevance_fudge
type type_sys = ATP_Translate.type_sys
+ type reconstructor = ATP_Reconstruct.reconstructor
type play = ATP_Reconstruct.play
type minimize_command = ATP_Reconstruct.minimize_command
+ type relevance_fudge = Sledgehammer_Filter.relevance_fudge
datatype mode = Auto_Try | Try | Normal | Minimize
@@ -79,6 +80,7 @@
val smt_slice_min_secs : int Config.T
val das_tool : string
val select_smt_solver : string -> Proof.context -> Proof.context
+ val prover_name_for_reconstructor : reconstructor -> string option
val is_metis_prover : string -> bool
val is_atp : theory -> string -> bool
val is_smt_prover : Proof.context -> string -> bool
@@ -128,13 +130,24 @@
"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 prover_name_for_reconstructor =
+ AList.find (op =) metis_prover_infos #> try hd
+
+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 =
- Context.proof_map o SMT_Config.select_solver
+val select_smt_solver = Context.proof_map o SMT_Config.select_solver
fun is_smt_prover ctxt name =
member (op =) (SMT_Solver.available_solvers_of ctxt) name
@@ -155,7 +168,7 @@
is_metis_prover orf is_smt_prover ctxt orf
is_atp_installed (Proof_Context.theory_of ctxt)
-fun get_slices num_facts slicing slices =
+fun get_slices slicing slices =
(0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
val metis_default_max_relevant = 20
@@ -166,8 +179,7 @@
metis_default_max_relevant
else if is_atp thy name then
fold (Integer.max o fst o snd o snd o snd)
- (get_slices 16384 (* large number *) slicing
- (#best_slices (get_atp thy name) ctxt)) 0
+ (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
end
@@ -266,7 +278,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)
@@ -408,8 +420,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 =
@@ -520,17 +535,22 @@
(case preplay of
Played (reconstructor, time) =>
if Time.<= (time, metis_minimize_max_time) then
- reconstructor_name reconstructor
+ prover_name_for_reconstructor reconstructor |> the_default name
else
name
| _ => name)
|> minimize_command
+fun repair_monomorph_context max_iters max_new_instances =
+ Config.put Monomorph.max_rounds max_iters
+ #> Config.put Monomorph.max_new_instances max_new_instances
+ #> Config.put Monomorph.keep_partial_instances false
+
fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
- Config.put SMT_Config.verbose debug
- #> Config.put SMT_Config.monomorph_full false
+ (not debug ? Config.put SMT_Config.verbose false)
#> Config.put SMT_Config.monomorph_limit max_mono_iters
#> Config.put SMT_Config.monomorph_instances max_mono_instances
+ #> Config.put SMT_Config.monomorph_full false
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
@@ -579,25 +599,23 @@
let
(* If slicing is disabled, we expand the last slice to fill the
entire time available. *)
- val actual_slices =
- get_slices (length facts) slicing (best_slices ctxt)
+ val actual_slices = get_slices slicing (best_slices ctxt)
val num_actual_slices = length actual_slices
fun monomorphize_facts facts =
let
+ val ctxt =
+ ctxt |> repair_monomorph_context max_mono_iters
+ max_new_mono_instances
(* pseudo-theorem involving the same constants as the subgoal *)
val subgoal_th =
Logic.list_implies (hyp_ts, concl_t)
|> Skip_Proof.make_thm thy
- val indexed_facts =
- (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
- val max_mono_instances = max_new_mono_instances + length facts
in
- ctxt |> repair_smt_monomorph_context debug max_mono_iters
- max_mono_instances
- |> SMT_Monomorph.monomorph indexed_facts
- |> fst |> sort (int_ord o pairself fst)
- |> filter_out (curry (op =) ~1 o fst)
- |> map (apfst (fst o nth facts))
+ Monomorph.monomorph Monomorph.all_schematic_consts_of
+ (subgoal_th :: map snd facts |> map (pair 0)) ctxt
+ |> fst |> tl
+ |> curry ListPair.zip (map fst facts)
+ |> maps (fn (name, rths) => map (pair name o snd) rths)
end
fun run_slice blacklist (slice, (time_frac, (complete,
(best_max_relevant, best_type_systems))))
@@ -618,6 +636,7 @@
? filter_out (member (op =) blacklist o fst)
|> polymorphism_of_type_sys type_sys <> Polymorphic
? monomorphize_facts
+ |> map (apsnd prop_of)
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
((real_ms time_left
@@ -653,7 +672,7 @@
"exec " ^ core) ^ " 2>&1"
val _ =
atp_problem
- |> tptp_strings_for_atp_problem format
+ |> tptp_lines_for_atp_problem format
|> cons ("% " ^ command ^ "\n")
|> File.write_list prob_file
val conjecture_shape =
@@ -776,7 +795,7 @@
|> map snd
in
play_one_line_proof debug preplay_timeout used_ths state subgoal
- [Metis, MetisFT]
+ metis_reconstructors
end,
fn preplay =>
let
@@ -858,14 +877,14 @@
let
val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
val repair_context =
- select_smt_solver name
- #> (if overlord then
- Config.put SMT_Config.debug_files
- (overlord_file_location_for_prover name
- |> (fn (path, name) => path ^ "/" ^ name))
- else
- I)
- #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
+ select_smt_solver name
+ #> (if overlord then
+ Config.put SMT_Config.debug_files
+ (overlord_file_location_for_prover name
+ |> (fn (path, name) => path ^ "/" ^ name))
+ else
+ I)
+ #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
val state = state |> Proof.map_context repair_context
fun do_slice timeout slice outcome0 time_so_far facts =
let
@@ -970,7 +989,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,
@@ -1000,9 +1019,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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jun 07 11:24:16 2011 +0200
@@ -102,7 +102,8 @@
(case preplay of
Played (reconstructor, timeout) =>
if can_min_fast_enough (Time.toMilliseconds timeout) then
- (true, reconstructor_name reconstructor)
+ (true, prover_name_for_reconstructor reconstructor
+ |> the_default name)
else
(prover_fast_enough, name)
| _ => (prover_fast_enough, name),
--- a/src/HOL/Tools/monomorph.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML Tue Jun 07 11:24:16 2011 +0200
@@ -37,7 +37,7 @@
(* configuration options *)
val max_rounds: int Config.T
val max_new_instances: int Config.T
- val complete_instances: bool Config.T
+ val keep_partial_instances: bool Config.T
(* monomorphization *)
val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
@@ -66,8 +66,8 @@
val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
val max_new_instances =
Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
-val complete_instances =
- Attrib.setup_config_bool @{binding monomorph_complete_instances} (K true)
+val keep_partial_instances =
+ Attrib.setup_config_bool @{binding monomorph_keep_partial_instances} (K true)
@@ -161,7 +161,7 @@
fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
let
val thy = Proof_Context.theory_of ctxt
- val count_partial = Config.get ctxt complete_instances
+ val count_partial = Config.get ctxt keep_partial_instances
fun add_new_ground subst n T =
let val T' = Envir.subst_type subst T
@@ -287,7 +287,7 @@
in (map inst thm_infos, ctxt) end
fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
- if Config.get ctxt complete_instances then
+ if Config.get ctxt keep_partial_instances then
let fun is_refined ((_, _, refined), _) = refined
in
(Inttab.map (K (filter_out is_refined)) subs, thm_infos)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/ATP_Export.thy Tue Jun 07 11:24:16 2011 +0200
@@ -0,0 +1,36 @@
+theory ATP_Export
+imports Complex_Main
+uses "atp_export.ML"
+begin
+
+ML {*
+val do_it = false; (* switch to true to generate files *)
+val thy = @{theory Complex_Main};
+val ctxt = @{context}
+*}
+
+ML {*
+if do_it then
+ ATP_Export.generate_tptp_inference_file_for_theory ctxt thy true
+ "/tmp/infs_full_types.tptp"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ ATP_Export.generate_tptp_inference_file_for_theory ctxt thy false
+ "/tmp/infs_partial_types.tptp"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ ATP_Export.generate_tptp_graph_file_for_theory ctxt thy
+ "/tmp/graph.out"
+else
+ ()
+*}
+
+end
--- a/src/HOL/ex/ROOT.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/HOL/ex/ROOT.ML Tue Jun 07 11:24:16 2011 +0200
@@ -12,7 +12,7 @@
"Hebrew",
"Chinese",
"Serbian",
- "TPTP_Export"
+ "ATP_Export"
];
use_thys [
--- a/src/HOL/ex/TPTP_Export.thy Tue Jun 07 11:12:05 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-theory TPTP_Export
-imports Complex_Main
-uses "tptp_export.ML"
-begin
-
-ML {*
-val do_it = false; (* switch to true to generate files *)
-val thy = @{theory Complex_Main};
-val ctxt = @{context}
-*}
-
-ML {*
-if do_it then
- TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true
- "/tmp/infs_full_types.tptp"
-else
- ()
-*}
-
-ML {*
-if do_it then
- TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy false
- "/tmp/infs_partial_types.tptp"
-else
- ()
-*}
-
-ML {*
-if do_it then
- TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy
- "/tmp/graph.out"
-else
- ()
-*}
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/atp_export.ML Tue Jun 07 11:24:16 2011 +0200
@@ -0,0 +1,121 @@
+(* Title: HOL/ex/atp_export.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2011
+
+Export Isabelle theories as first-order TPTP inferences, exploiting
+Sledgehammer's translation.
+*)
+
+signature ATP_EXPORT =
+sig
+ val generate_tptp_graph_file_for_theory :
+ Proof.context -> theory -> string -> unit
+ val generate_tptp_inference_file_for_theory :
+ Proof.context -> theory -> bool -> string -> unit
+end;
+
+structure ATP_Export : ATP_EXPORT =
+struct
+
+val ascii_of = ATP_Translate.ascii_of
+
+val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of
+
+fun facts_of thy =
+ Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
+ true (K true) [] []
+
+fun fold_body_thms f =
+ let
+ fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+ if Inttab.defined seen i then (x, seen)
+ else
+ let
+ val body' = Future.join body;
+ val (x', seen') = app (n + (if name = "" then 0 else 1)) body' (x, Inttab.update (i, ()) seen);
+ in (x' |> n = 1 ? f (name, prop, body'), seen') end);
+ in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end;
+
+fun theorems_mentioned_in_proof_term thm =
+ let
+ fun collect (s, _, _) = if s <> "" then insert (op =) s else I
+ val names =
+ [] |> fold_body_thms collect [Thm.proof_body_of thm] |> map fact_name_of
+ in names end
+
+fun interesting_const_names ctxt =
+ let val thy = ProofContext.theory_of ctxt in
+ Sledgehammer_Filter.const_names_in_fact thy
+ (Sledgehammer_Provers.is_built_in_const_for_prover ctxt ATP_Systems.eN)
+ end
+
+fun generate_tptp_graph_file_for_theory ctxt thy file_name =
+ let
+ val path = file_name |> Path.explode
+ val _ = File.write path ""
+ val axioms = Theory.all_axioms_of thy |> map fst
+ fun do_thm thm =
+ let
+ val name = Thm.get_name_hint thm
+ val s =
+ "[" ^ Thm.legacy_get_kind thm ^ "] " ^
+ (if member (op =) axioms name then "A" else "T") ^ " " ^
+ prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^
+ commas (theorems_mentioned_in_proof_term thm) ^ "; " ^
+ commas (map (prefix ATP_Translate.const_prefix o ascii_of)
+ (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
+ in File.append path s end
+ val thms = facts_of thy |> map (snd o snd)
+ val _ = map do_thm thms
+ in () end
+
+fun inference_term [] = NONE
+ | inference_term ss =
+ ATP_Problem.ATerm ("inference",
+ [ATP_Problem.ATerm ("isabelle", []),
+ ATP_Problem.ATerm ("[]", []),
+ ATP_Problem.ATerm ("[]",
+ map (fn s => ATP_Problem.ATerm (s, [])) ss)])
+ |> SOME
+fun inference infers ident =
+ these (AList.lookup (op =) infers ident) |> inference_term
+fun add_inferences_to_problem_line infers
+ (ATP_Problem.Formula (ident, ATP_Problem.Axiom, phi, NONE, NONE)) =
+ ATP_Problem.Formula (ident, ATP_Problem.Lemma, phi, inference infers ident,
+ NONE)
+ | add_inferences_to_problem_line _ line = line
+val add_inferences_to_problem =
+ map o apsnd o map o add_inferences_to_problem_line
+
+fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name =
+ let
+ val format = ATP_Problem.FOF
+ val type_sys =
+ ATP_Translate.Preds
+ (ATP_Translate.Polymorphic,
+ if full_types then ATP_Translate.All_Types
+ else ATP_Translate.Const_Arg_Types,
+ ATP_Translate.Heavyweight)
+ val path = file_name |> Path.explode
+ val _ = File.write path ""
+ val facts0 = facts_of thy
+ val facts =
+ facts0 |> map (fn ((_, loc), (_, th)) =>
+ ((Thm.get_name_hint th, loc), prop_of th))
+ val explicit_apply = NONE
+ val (atp_problem, _, _, _, _, _, _) =
+ ATP_Translate.prepare_atp_problem ctxt format
+ ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
+ [] @{prop False} facts
+ val infers =
+ facts0 |> map (fn (_, (_, th)) =>
+ (fact_name_of (Thm.get_name_hint th),
+ theorems_mentioned_in_proof_term th))
+ val infers =
+ infers |> map (apsnd (filter (member (op = o apsnd fst) infers)))
+ val atp_problem = atp_problem |> add_inferences_to_problem infers
+ val ss = ATP_Problem.tptp_lines_for_atp_problem ATP_Problem.FOF atp_problem
+ val _ = app (File.append path) ss
+ in () end
+
+end;
--- a/src/HOL/ex/tptp_export.ML Tue Jun 07 11:12:05 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,122 +0,0 @@
-(* Title: HOL/ex/tptp_export.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2011
-
-Export Isabelle theories as first-order TPTP inferences, exploiting
-Sledgehammer's translation.
-*)
-
-signature TPTP_EXPORT =
-sig
- val generate_tptp_graph_file_for_theory :
- Proof.context -> theory -> string -> unit
- val generate_tptp_inference_file_for_theory :
- Proof.context -> theory -> bool -> string -> unit
-end;
-
-structure TPTP_Export : TPTP_EXPORT =
-struct
-
-val ascii_of = ATP_Translate.ascii_of
-
-val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of
-
-fun facts_of thy =
- Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
- true (K true) [] []
-
-fun fold_body_thms f =
- let
- fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
- if Inttab.defined seen i then (x, seen)
- else
- let
- val body' = Future.join body;
- val (x', seen') = app (n + (if name = "" then 0 else 1)) body' (x, Inttab.update (i, ()) seen);
- in (x' |> n = 1 ? f (name, prop, body'), seen') end);
- in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end;
-
-fun theorems_mentioned_in_proof_term thm =
- let
- fun collect (s, _, _) = if s <> "" then insert (op =) s else I
- val names =
- [] |> fold_body_thms collect [Thm.proof_body_of thm] |> map fact_name_of
- in names end
-
-fun interesting_const_names ctxt =
- let val thy = ProofContext.theory_of ctxt in
- Sledgehammer_Filter.const_names_in_fact thy
- (Sledgehammer_Provers.is_built_in_const_for_prover ctxt ATP_Systems.eN)
- end
-
-fun generate_tptp_graph_file_for_theory ctxt thy file_name =
- let
- val path = file_name |> Path.explode
- val _ = File.write path ""
- val axioms = Theory.all_axioms_of thy |> map fst
- fun do_thm thm =
- let
- val name = Thm.get_name_hint thm
- val s =
- "[" ^ Thm.legacy_get_kind thm ^ "] " ^
- (if member (op =) axioms name then "A" else "T") ^ " " ^
- prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^
- commas (theorems_mentioned_in_proof_term thm) ^ "; " ^
- commas (map (prefix ATP_Translate.const_prefix o ascii_of)
- (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
- in File.append path s end
- val thms = facts_of thy |> map (snd o snd)
- val _ = map do_thm thms
- in () end
-
-fun inference_term [] = NONE
- | inference_term ss =
- ATP_Problem.ATerm ("inference",
- [ATP_Problem.ATerm ("isabelle", []),
- ATP_Problem.ATerm ("[]", []),
- ATP_Problem.ATerm ("[]",
- map (fn s => ATP_Problem.ATerm (s, [])) ss)])
- |> SOME
-fun inference infers ident =
- these (AList.lookup (op =) infers ident) |> inference_term
-fun add_inferences_to_problem_line infers
- (ATP_Problem.Formula (ident, ATP_Problem.Axiom, phi, NONE, NONE)) =
- ATP_Problem.Formula (ident, ATP_Problem.Lemma, phi, inference infers ident,
- NONE)
- | add_inferences_to_problem_line _ line = line
-val add_inferences_to_problem =
- map o apsnd o map o add_inferences_to_problem_line
-
-fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name =
- let
- val format = ATP_Problem.FOF
- val type_sys =
- ATP_Translate.Preds
- (ATP_Translate.Polymorphic,
- if full_types then ATP_Translate.All_Types
- else ATP_Translate.Const_Arg_Types,
- ATP_Translate.Heavyweight)
- val path = file_name |> Path.explode
- val _ = File.write path ""
- val facts0 = facts_of thy
- val facts =
- facts0 |> map (fn ((_, loc), (_, th)) =>
- ((Thm.get_name_hint th, loc), th))
- val explicit_apply = NONE
- val (atp_problem, _, _, _, _, _, _) =
- ATP_Translate.prepare_atp_problem ctxt format
- ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
- [] @{prop False} facts
- val infers =
- facts0 |> map (fn (_, (_, th)) =>
- (fact_name_of (Thm.get_name_hint th),
- theorems_mentioned_in_proof_term th))
- val infers =
- infers |> map (apsnd (filter (member (op = o apsnd fst) infers)))
- val atp_problem = atp_problem |> add_inferences_to_problem infers
- val ss =
- ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.FOF atp_problem
- val _ = app (File.append path) ss
- in () end
-
-end;
--- a/src/Pure/Isar/isar_syn.ML Tue Jun 07 11:12:05 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Jun 07 11:24:16 2011 +0200
@@ -119,7 +119,7 @@
val _ =
Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
(Scan.repeat1 type_abbrev >> (fn specs => fn lthy =>
- (legacy_feature "Old 'types' commands -- use 'type_synonym' instead";
+ (legacy_feature "Old 'types' command -- use 'type_synonym' instead";
fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs) specs lthy)));
val _ =