1.1 --- a/NEWS Tue Jun 07 11:12:05 2011 +0200
1.2 +++ b/NEWS Tue Jun 07 11:24:16 2011 +0200
1.3 @@ -86,7 +86,8 @@
1.4 - Added "type_sys", "max_mono_iters", and "max_new_mono_instances" options.
1.5
1.6 * Metis:
1.7 - - Obsoleted "metisF" -- use "metis" instead.
1.8 + - Removed "metisF" -- use "metis" instead.
1.9 + - Obsoleted "metisFT" -- use "metis (full_types)" instead.
1.10
1.11 * "try":
1.12 - Added "simp:", "intro:", and "elim:" options.
2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 11:12:05 2011 +0200
2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 07 11:24:16 2011 +0200
2.3 @@ -495,30 +495,36 @@
2.4 set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger
2.5 value or to try several provers and keep the nicest-looking proof.
2.6
2.7 -\point{What is metisFT?}
2.8 +\point{What are the \textit{full\_types} and \textit{no\_types} arguments to
2.9 +Metis?}
2.10
2.11 -The \textit{metisFT} proof method is the fully-typed version of Metis. It is
2.12 -much slower than \textit{metis}, but the proof search is fully typed, and it
2.13 -also includes more powerful rules such as the axiom ``$x = \mathit{True}
2.14 -\mathrel{\lor} x = \mathit{False}$'' for reasoning in higher-order places (e.g.,
2.15 -in set comprehensions). The method kicks in automatically as a fallback when
2.16 -\textit{metis} fails, and it is sometimes generated by Sledgehammer instead of
2.17 -\textit{metis} if the proof obviously requires type information or if
2.18 -\textit{metis} failed when Sledgehammer preplayed the proof. (By default,
2.19 -Sledgehammer tries to run \textit{metis} and/or \textit{metisFT} for 4 seconds
2.20 -to ensure that the generated one-line proofs actually work and to display timing
2.21 -information. This can be configured using the \textit{preplay\_timeout} option
2.22 -(\S\ref{timeouts}).)
2.23 +The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed
2.24 +version of Metis. It is somewhat slower than \textit{metis}, but the proof
2.25 +search is fully typed, and it also includes more powerful rules such as the
2.26 +axiom ``$x = \mathit{True} \mathrel{\lor} x = \mathit{False}$'' for reasoning in
2.27 +higher-order places (e.g., in set comprehensions). The method kicks in
2.28 +automatically as a fallback when \textit{metis} fails, and it is sometimes
2.29 +generated by Sledgehammer instead of \textit{metis} if the proof obviously
2.30 +requires type information or if \textit{metis} failed when Sledgehammer
2.31 +preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
2.32 +various options for up to 4 seconds to ensure that the generated one-line proofs
2.33 +actually work and to display timing information. This can be configured using
2.34 +the \textit{preplay\_timeout} option (\S\ref{timeouts}).)
2.35
2.36 -If you see the warning
2.37 +At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types})
2.38 +uses no type information at all during the proof search, which is more efficient
2.39 +but often fails. Calls to \textit{metis} (\textit{no\_types}) are occasionally
2.40 +generated by Sledgehammer.
2.41 +
2.42 +Incidentally, if you see the warning
2.43
2.44 \prew
2.45 \slshape
2.46 -Metis: Falling back on ``\textit{metisFT\/}''.
2.47 +Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
2.48 \postw
2.49
2.50 -in a successful Metis proof, you can advantageously replace the \textit{metis}
2.51 -call with \textit{metisFT}.
2.52 +in a successful Metis proof, you can advantageously pass the
2.53 +\textit{full\_types} option to \textit{metis} directly.
2.54
2.55 \point{Are generated proofs minimal?}
2.56
2.57 @@ -529,11 +535,11 @@
2.58 improves Metis's speed and success rate, while also removing superfluous clutter
2.59 from the proof scripts.
2.60
2.61 -In earlier versions of Sledgehammer, generated proofs were accompanied by a
2.62 -suggestion to invoke the minimization tool. This step is now performed
2.63 -implicitly if it can be done in a reasonable amount of time (something that can
2.64 -be guessed from the number of facts in the original proof and the time it took
2.65 -to find it or replay it).
2.66 +In earlier versions of Sledgehammer, generated proofs were systematically
2.67 +accompanied by a suggestion to invoke the minimization tool. This step is now
2.68 +performed implicitly if it can be done in a reasonable amount of time (something
2.69 +that can be guessed from the number of facts in the original proof and the time
2.70 +it took to find it or replay it).
2.71
2.72 In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
2.73 proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
2.74 @@ -662,10 +668,11 @@
2.75
2.76 where \qty{type\_sys} is a type system specification with the same semantics as
2.77 Sledgehammer's \textit{type\_sys} option (\S\ref{problem-encoding}) and
2.78 -\qty{facts} is a list of arbitrary facts. \qty{type\_sys} may also be
2.79 -\textit{full\_types}, in which case an appropriate type-sound encoding is
2.80 -chosen. The companion proof method \textit{metisFT} is an abbreviation for
2.81 -``\textit{metis}~(\textit{full\_types})''.
2.82 +\qty{facts} is a list of arbitrary facts. In addition to the values listed in
2.83 +\S\ref{problem-encoding}, \qty{type\_sys} may also be \textit{full\_types}, in
2.84 +which case an appropriate type-sound encoding is chosen, \textit{partial\_types}
2.85 +(the default type-unsound encoding), or \textit{no\_types}, a synonym for
2.86 +\textit{erased}.
2.87
2.88 \section{Option Reference}
2.89 \label{option-reference}
2.90 @@ -764,7 +771,11 @@
2.91 \item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
2.92 the external provers, Metis itself can be used for proof search.
2.93
2.94 -\item[$\bullet$] \textbf{\textit{metisFT}:} Fully typed version of Metis.
2.95 +\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
2.96 +Metis, corresponding to \textit{metis} (\textit{full\_types}).
2.97 +
2.98 +\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
2.99 +corresponding to \textit{metis} (\textit{no\_types}).
2.100 \end{enum}
2.101
2.102 In addition, the following remote provers are supported:
2.103 @@ -903,14 +914,12 @@
2.104 arguments, to resolve overloading.
2.105
2.106 \item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
2.107 -tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$. This
2.108 -coincides with the encoding used by the \textit{metisFT} command.
2.109 +tagged with its type using a function $\mathit{type\_info\/}(\tau, t)$.
2.110
2.111 \item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
2.112 Like for \textit{poly\_preds} constants are annotated with their types to
2.113 resolve overloading, but otherwise no type information is encoded. This
2.114 -coincides with the encoding used by the \textit{metis} command (before it falls
2.115 -back on \textit{metisFT}).
2.116 +coincides with the default encoding used by the \textit{metis} command.
2.117
2.118 \item[$\bullet$]
2.119 \textbf{%
3.1 --- a/src/HOL/IsaMakefile Tue Jun 07 11:12:05 2011 +0200
3.2 +++ b/src/HOL/IsaMakefile Tue Jun 07 11:24:16 2011 +0200
3.3 @@ -1046,8 +1046,8 @@
3.4
3.5 $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
3.6 Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
3.7 - ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
3.8 - ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
3.9 + ex/ATP_Export.thy ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \
3.10 + ex/BT.thy ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy \
3.11 ex/CASC_Setup.thy ex/CTL.thy ex/Case_Product.thy \
3.12 ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
3.13 ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
3.14 @@ -1068,7 +1068,7 @@
3.15 ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
3.16 ex/sledgehammer_tactics.ML ex/Sqrt.thy \
3.17 ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
3.18 - ex/TPTP_Export.thy ex/Transfer_Ex.thy ex/Tree23.thy \
3.19 + ex/Transfer_Ex.thy ex/Tree23.thy \
3.20 ex/Unification.thy ex/While_Combinator_Example.thy \
3.21 ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
3.22 ex/svc_test.thy \
4.1 --- a/src/HOL/Metis_Examples/Clausification.thy Tue Jun 07 11:12:05 2011 +0200
4.2 +++ b/src/HOL/Metis_Examples/Clausification.thy Tue Jun 07 11:24:16 2011 +0200
4.3 @@ -28,13 +28,13 @@
4.4 by (metis qax)
4.5
4.6 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
4.7 -by (metisFT qax)
4.8 +by (metis (full_types) qax)
4.9
4.10 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)"
4.11 by (metis qax)
4.12
4.13 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)"
4.14 -by (metisFT qax)
4.15 +by (metis (full_types) qax)
4.16
4.17 declare [[metis_new_skolemizer]]
4.18
4.19 @@ -42,13 +42,13 @@
4.20 by (metis qax)
4.21
4.22 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
4.23 -by (metisFT qax)
4.24 +by (metis (full_types) qax)
4.25
4.26 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)"
4.27 by (metis qax)
4.28
4.29 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)"
4.30 -by (metisFT qax)
4.31 +by (metis (full_types) qax)
4.32
4.33 declare [[meson_max_clauses = 60]]
4.34
4.35 @@ -64,7 +64,7 @@
4.36 by (metis rax)
4.37
4.38 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
4.39 -by (metisFT rax)
4.40 +by (metis (full_types) rax)
4.41
4.42 declare [[metis_new_skolemizer]]
4.43
4.44 @@ -72,7 +72,7 @@
4.45 by (metis rax)
4.46
4.47 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
4.48 -by (metisFT rax)
4.49 +by (metis (full_types) rax)
4.50
4.51 lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
4.52 (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
4.53 @@ -84,7 +84,7 @@
4.54 (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
4.55 (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
4.56 (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
4.57 -by (metisFT rax)
4.58 +by (metis (full_types) rax)
4.59
4.60
4.61 text {* Definitional CNF for goal *}
4.62 @@ -100,7 +100,7 @@
4.63
4.64 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>
4.65 (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
4.66 -by (metisFT pax)
4.67 +by (metis (full_types) pax)
4.68
4.69 declare [[metis_new_skolemizer]]
4.70
4.71 @@ -110,7 +110,7 @@
4.72
4.73 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>
4.74 (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
4.75 -by (metisFT pax)
4.76 +by (metis (full_types) pax)
4.77
4.78
4.79 text {* New Skolemizer *}
4.80 @@ -134,7 +134,7 @@
4.81 assumes a: "Quotient R Abs Rep"
4.82 shows "symp R"
4.83 using a unfolding Quotient_def using sympI
4.84 -by metisFT
4.85 +by (metis (full_types))
4.86
4.87 lemma
4.88 "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
5.1 --- a/src/HOL/Metis_Examples/Proxies.thy Tue Jun 07 11:12:05 2011 +0200
5.2 +++ b/src/HOL/Metis_Examples/Proxies.thy Tue Jun 07 11:24:16 2011 +0200
5.3 @@ -66,7 +66,7 @@
5.4 sledgehammer [type_sys = mangled_tags, expect = some] (id_apply)
5.5 sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply)
5.6 sledgehammer [type_sys = mangled_preds, expect = some] (id_apply)
5.7 -by (metisFT id_apply)
5.8 +by (metis (full_types) id_apply)
5.9
5.10 lemma "id True"
5.11 sledgehammer [type_sys = erased, expect = some] (id_apply)
5.12 @@ -127,7 +127,7 @@
5.13 sledgehammer [type_sys = mangled_tags, expect = some] ()
5.14 sledgehammer [type_sys = mangled_preds?, expect = some] ()
5.15 sledgehammer [type_sys = mangled_preds, expect = some] ()
5.16 -by metisFT
5.17 +by (metis (full_types))
5.18
5.19 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
5.20 sledgehammer [type_sys = erased, expect = some] (id_apply)
6.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 07 11:12:05 2011 +0200
6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jun 07 11:24:16 2011 +0200
6.3 @@ -342,7 +342,8 @@
6.4 (case AList.lookup (op =) args reconstructorK of
6.5 SOME name => name
6.6 | NONE =>
6.7 - if String.isSubstring "metisFT" msg then "metisFT"
6.8 + if String.isSubstring "metis (full_types)" msg then "metis (full_types)"
6.9 + else if String.isSubstring "metis (no_types)" msg then "metis (no_types)"
6.10 else if String.isSubstring "metis" msg then "metis"
6.11 else "smt")
6.12
6.13 @@ -541,8 +542,10 @@
6.14 Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
6.15 else if !reconstructor = "smt" then
6.16 SMT_Solver.smt_tac
6.17 - else if full orelse !reconstructor = "metisFT" then
6.18 - Metis_Tactics.metisFT_tac
6.19 + else if full orelse !reconstructor = "metis (full_types)" then
6.20 + Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
6.21 + else if !reconstructor = "metis (no_types)" then
6.22 + Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
6.23 else
6.24 Metis_Tactics.metis_tac []) ctxt thms
6.25 fun apply_reconstructor thms =
7.1 --- a/src/HOL/SMT.thy Tue Jun 07 11:12:05 2011 +0200
7.2 +++ b/src/HOL/SMT.thy Tue Jun 07 11:24:16 2011 +0200
7.3 @@ -245,14 +245,14 @@
7.4 construction whose cycles are limited by the following option.
7.5 *}
7.6
7.7 -declare [[ smt_monomorph_limit = 10 ]]
7.8 +declare [[ monomorph_max_rounds = 5 ]]
7.9
7.10 text {*
7.11 In addition, the number of generated monomorphic instances is limited
7.12 by the following option.
7.13 *}
7.14
7.15 -declare [[ smt_monomorph_instances = 500 ]]
7.16 +declare [[ monomorph_max_new_instances = 500 ]]
7.17
7.18
7.19
8.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 07 11:12:05 2011 +0200
8.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 07 11:24:16 2011 +0200
8.3 @@ -70,7 +70,7 @@
8.4 -> 'd -> 'd
8.5 val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
8.6 val is_format_typed : format -> bool
8.7 - val tptp_strings_for_atp_problem : format -> string problem -> string list
8.8 + val tptp_lines_for_atp_problem : format -> string problem -> string list
8.9 val ensure_cnf_problem :
8.10 (string * string) problem -> (string * string) problem
8.11 val filter_cnf_ueq_problem :
8.12 @@ -283,7 +283,7 @@
8.13 | (_, SOME tm) =>
8.14 ", " ^ string_for_term format (source |> the_default default_source) ^
8.15 ", " ^ string_for_term format tm) ^ ").\n"
8.16 -fun tptp_strings_for_atp_problem format problem =
8.17 +fun tptp_lines_for_atp_problem format problem =
8.18 "% This file was generated by Isabelle (most likely Sledgehammer)\n\
8.19 \% " ^ timestamp () ^ "\n" ::
8.20 maps (fn (_, []) => []
9.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 11:12:05 2011 +0200
9.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Jun 07 11:24:16 2011 +0200
9.3 @@ -16,7 +16,8 @@
9.4
9.5 datatype reconstructor =
9.6 Metis |
9.7 - MetisFT |
9.8 + Metis_Full_Types |
9.9 + Metis_No_Types |
9.10 SMT of string
9.11
9.12 datatype play =
9.13 @@ -41,7 +42,6 @@
9.14 Proof.context -> type_sys -> int list list -> int
9.15 -> (string * locality) list vector -> 'a proof -> string list option
9.16 val uses_typed_helpers : int list -> 'a proof -> bool
9.17 - val reconstructor_name : reconstructor -> string
9.18 val one_line_proof_text : one_line_params -> string
9.19 val make_tvar : string -> typ
9.20 val make_tfree : Proof.context -> string -> typ
9.21 @@ -67,7 +67,8 @@
9.22
9.23 datatype reconstructor =
9.24 Metis |
9.25 - MetisFT |
9.26 + Metis_Full_Types |
9.27 + Metis_No_Types |
9.28 SMT of string
9.29
9.30 datatype play =
9.31 @@ -251,9 +252,11 @@
9.32
9.33 (** Soft-core proof reconstruction: Metis one-liner **)
9.34
9.35 -fun reconstructor_name Metis = "metis"
9.36 - | reconstructor_name MetisFT = "metisFT"
9.37 - | reconstructor_name (SMT _) = "smt"
9.38 +(* unfortunate leaking abstraction *)
9.39 +fun name_of_reconstructor Metis = "metis"
9.40 + | name_of_reconstructor Metis_Full_Types = "metis (full_types)"
9.41 + | name_of_reconstructor Metis_No_Types = "metis (no_types)"
9.42 + | name_of_reconstructor (SMT _) = "smt"
9.43
9.44 fun reconstructor_settings (SMT settings) = settings
9.45 | reconstructor_settings _ = ""
9.46 @@ -279,7 +282,7 @@
9.47 fun reconstructor_command reconstructor i n (ls, ss) =
9.48 using_labels ls ^
9.49 apply_on_subgoal (reconstructor_settings reconstructor) i n ^
9.50 - command_call (reconstructor_name reconstructor) ss
9.51 + command_call (name_of_reconstructor reconstructor) ss
9.52 fun minimize_line _ [] = ""
9.53 | minimize_line minimize_command ss =
9.54 case minimize_command ss of
9.55 @@ -1042,7 +1045,7 @@
9.56 else
9.57 if member (op =) qs Show then "show" else "have")
9.58 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
9.59 - val reconstructor = if full_types then MetisFT else Metis
9.60 + val reconstructor = if full_types then Metis_Full_Types else Metis
9.61 fun do_facts (ls, ss) =
9.62 reconstructor_command reconstructor 1 1
9.63 (ls |> sort_distinct (prod_ord string_ord int_ord),
10.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 07 11:12:05 2011 +0200
10.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 07 11:24:16 2011 +0200
10.3 @@ -130,7 +130,7 @@
10.4 val prepare_atp_problem :
10.5 Proof.context -> format -> formula_kind -> formula_kind -> type_sys
10.6 -> bool option -> bool -> bool -> term list -> term
10.7 - -> ((string * locality) * thm) list
10.8 + -> ((string * locality) * term) list
10.9 -> string problem * string Symtab.table * int * int
10.10 * (string * locality) list vector * int list * int Symtab.table
10.11 val atp_problem_weights : string problem -> (string * real) list
10.12 @@ -1386,10 +1386,10 @@
10.13 facts =
10.14 let
10.15 val thy = Proof_Context.theory_of ctxt
10.16 - val fact_ts = facts |> map (prop_of o snd)
10.17 + val fact_ts = facts |> map snd
10.18 val (facts, fact_names) =
10.19 - facts |> map (fn (name, th) =>
10.20 - (name, prop_of th)
10.21 + facts |> map (fn (name, t) =>
10.22 + (name, t)
10.23 |> make_fact ctxt format type_sys false true true true
10.24 |> rpair name)
10.25 |> map_filter (try (apfst the))
11.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 07 11:12:05 2011 +0200
11.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Jun 07 11:24:16 2011 +0200
11.3 @@ -11,10 +11,6 @@
11.4 sig
11.5 exception METIS of string * string
11.6
11.7 - val trace : bool Config.T
11.8 - val trace_msg : Proof.context -> (unit -> string) -> unit
11.9 - val verbose : bool Config.T
11.10 - val verbose_warning : Proof.context -> string -> unit
11.11 val hol_clause_from_metis :
11.12 Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
11.13 -> term
11.14 @@ -38,13 +34,6 @@
11.15
11.16 exception METIS of string * string
11.17
11.18 -val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
11.19 -val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
11.20 -
11.21 -fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
11.22 -fun verbose_warning ctxt msg =
11.23 - if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
11.24 -
11.25 datatype term_or_type = SomeTerm of term | SomeType of typ
11.26
11.27 fun terms_of [] = []
12.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Jun 07 11:12:05 2011 +0200
12.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Jun 07 11:24:16 2011 +0200
12.3 @@ -10,14 +10,16 @@
12.4 signature METIS_TACTICS =
12.5 sig
12.6 val metisN : string
12.7 - val metisFT_N : string
12.8 - val default_unsound_type_sys : string
12.9 - val default_sound_type_sys : string
12.10 + val full_typesN : string
12.11 + val partial_typesN : string
12.12 + val no_typesN : string
12.13 + val full_type_sys : string
12.14 + val partial_type_sys : string
12.15 + val no_type_sys : string
12.16 val trace : bool Config.T
12.17 val verbose : bool Config.T
12.18 val new_skolemizer : bool Config.T
12.19 val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
12.20 - val metisFT_tac : Proof.context -> thm list -> int -> tactic
12.21 val setup : theory -> theory
12.22 end
12.23
12.24 @@ -29,18 +31,25 @@
12.25 open Metis_Reconstruct
12.26
12.27 val metisN = Binding.qualified_name_of @{binding metis}
12.28 -val metisFT_N = Binding.qualified_name_of @{binding metisFT}
12.29 +
12.30 val full_typesN = "full_types"
12.31 +val partial_typesN = "partial_types"
12.32 +val no_typesN = "no_types"
12.33
12.34 -val default_unsound_type_sys = "poly_args"
12.35 -val default_sound_type_sys = "poly_preds_heavy_query"
12.36 +val full_type_sys = "poly_preds_heavy_query"
12.37 +val partial_type_sys = "poly_args"
12.38 +val no_type_sys = "erased"
12.39 +
12.40 +val type_sys_aliases =
12.41 + [(full_typesN, full_type_sys),
12.42 + (partial_typesN, partial_type_sys),
12.43 + (no_typesN, no_type_sys)]
12.44
12.45 fun method_call_for_type_sys type_sys =
12.46 - if type_sys = default_sound_type_sys then
12.47 - (@{binding metisFT}, "")
12.48 - else
12.49 - (@{binding metis},
12.50 - if type_sys = default_unsound_type_sys then "" else type_sys)
12.51 + metisN ^ " (" ^
12.52 + (case AList.find (op =) type_sys_aliases type_sys of
12.53 + [alias] => alias
12.54 + | _ => type_sys) ^ ")"
12.55
12.56 val new_skolemizer =
12.57 Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
12.58 @@ -168,13 +177,10 @@
12.59 (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
12.60 else ""))
12.61 | type_sys :: _ =>
12.62 - let val (binding, arg) = method_call_for_type_sys type_sys in
12.63 - (verbose_warning ctxt
12.64 - ("Falling back on " ^
12.65 - quote (Binding.qualified_name_of binding ^
12.66 - (arg |> arg <> "" ? enclose " (" ")")) ^ "...");
12.67 - FOL_SOLVE fallback_type_syss ctxt cls ths0)
12.68 - end
12.69 + (verbose_warning ctxt
12.70 + ("Falling back on " ^
12.71 + quote (method_call_for_type_sys type_sys) ^ "...");
12.72 + FOL_SOLVE fallback_type_syss ctxt cls ths0)
12.73
12.74 val neg_clausify =
12.75 single
12.76 @@ -207,12 +213,11 @@
12.77 Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
12.78 end
12.79
12.80 -val metis_default_type_syss = [default_unsound_type_sys, default_sound_type_sys]
12.81 -val metisFT_type_syss = [default_sound_type_sys]
12.82 +val metis_default_type_syss = [partial_type_sys, full_type_sys]
12.83 +val metisFT_type_syss = [full_type_sys]
12.84
12.85 fun metis_tac [] = generic_metis_tac metis_default_type_syss
12.86 | metis_tac type_syss = generic_metis_tac type_syss
12.87 -val metisFT_tac = generic_metis_tac metisFT_type_syss
12.88
12.89 (* Whenever "X" has schematic type variables, we treat "using X by metis" as
12.90 "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
12.91 @@ -224,6 +229,12 @@
12.92
12.93 fun method type_syss (type_sys, ths) ctxt facts =
12.94 let
12.95 + val _ =
12.96 + if type_syss = metisFT_type_syss then
12.97 + legacy_feature "Old 'metisFT' method -- \
12.98 + \use 'metis (full_types)' instead"
12.99 + else
12.100 + ()
12.101 val (schem_facts, nonschem_facts) = List.partition has_tvar facts
12.102 val type_syss = type_sys |> Option.map single |> the_default type_syss
12.103 in
12.104 @@ -232,19 +243,20 @@
12.105 o generic_metis_tac type_syss ctxt (schem_facts @ ths))
12.106 end
12.107
12.108 -fun setup_method (type_syss as type_sys :: _) =
12.109 +fun setup_method (binding, type_syss as type_sys :: _) =
12.110 (if type_syss = metis_default_type_syss then
12.111 (Args.parens Parse.short_ident
12.112 - >> (fn s => if s = full_typesN then default_sound_type_sys else s))
12.113 + >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s))
12.114 |> Scan.option |> Scan.lift
12.115 else
12.116 Scan.succeed NONE)
12.117 -- Attrib.thms >> (METHOD oo method type_syss)
12.118 - |> Method.setup (fst (method_call_for_type_sys type_sys))
12.119 + |> Method.setup binding
12.120
12.121 val setup =
12.122 - [(metis_default_type_syss, "Metis for FOL and HOL problems"),
12.123 - (metisFT_type_syss,
12.124 + [((@{binding metis}, metis_default_type_syss),
12.125 + "Metis for FOL and HOL problems"),
12.126 + ((@{binding metisFT}, metisFT_type_syss),
12.127 "Metis for FOL/HOL problems with fully-typed translation")]
12.128 |> fold (uncurry setup_method)
12.129
13.1 --- a/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 11:12:05 2011 +0200
13.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 11:24:16 2011 +0200
13.3 @@ -20,6 +20,10 @@
13.4 val metis_app_op : string
13.5 val metis_type_tag : string
13.6 val metis_generated_var_prefix : string
13.7 + val trace : bool Config.T
13.8 + val verbose : bool Config.T
13.9 + val trace_msg : Proof.context -> (unit -> string) -> unit
13.10 + val verbose_warning : Proof.context -> string -> unit
13.11 val metis_name_table : ((string * int) * (string * bool)) list
13.12 val reveal_old_skolem_terms : (string * term) list -> term -> term
13.13 val prepare_metis_problem :
13.14 @@ -39,6 +43,13 @@
13.15 val metis_type_tag = ":"
13.16 val metis_generated_var_prefix = "_"
13.17
13.18 +val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
13.19 +val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)
13.20 +
13.21 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
13.22 +fun verbose_warning ctxt msg =
13.23 + if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
13.24 +
13.25 val metis_name_table =
13.26 [((tptp_equal, 2), (metis_equal, false)),
13.27 ((tptp_old_equal, 2), (metis_equal, false)),
13.28 @@ -180,7 +191,7 @@
13.29 prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
13.30 false false props @{prop False} []
13.31 (*
13.32 -val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem))
13.33 +val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
13.34 *)
13.35 (* "rev" is for compatibility *)
13.36 val axioms =
14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 11:12:05 2011 +0200
14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 11:24:16 2011 +0200
14.3 @@ -10,10 +10,11 @@
14.4 sig
14.5 type failure = ATP_Proof.failure
14.6 type locality = ATP_Translate.locality
14.7 - type relevance_fudge = Sledgehammer_Filter.relevance_fudge
14.8 type type_sys = ATP_Translate.type_sys
14.9 + type reconstructor = ATP_Reconstruct.reconstructor
14.10 type play = ATP_Reconstruct.play
14.11 type minimize_command = ATP_Reconstruct.minimize_command
14.12 + type relevance_fudge = Sledgehammer_Filter.relevance_fudge
14.13
14.14 datatype mode = Auto_Try | Try | Normal | Minimize
14.15
14.16 @@ -79,6 +80,7 @@
14.17 val smt_slice_min_secs : int Config.T
14.18 val das_tool : string
14.19 val select_smt_solver : string -> Proof.context -> Proof.context
14.20 + val prover_name_for_reconstructor : reconstructor -> string option
14.21 val is_metis_prover : string -> bool
14.22 val is_atp : theory -> string -> bool
14.23 val is_smt_prover : Proof.context -> string -> bool
14.24 @@ -128,13 +130,24 @@
14.25 "Async_Manager". *)
14.26 val das_tool = "Sledgehammer"
14.27
14.28 -val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N]
14.29 +val metisN = Metis_Tactics.metisN
14.30 +val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN
14.31 +val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN
14.32
14.33 -val is_metis_prover = member (op =) metis_prover_names
14.34 +val metis_prover_infos =
14.35 + [(metisN, Metis),
14.36 + (metis_full_typesN, Metis_Full_Types),
14.37 + (metis_no_typesN, Metis_No_Types)]
14.38 +
14.39 +val prover_name_for_reconstructor =
14.40 + AList.find (op =) metis_prover_infos #> try hd
14.41 +
14.42 +val metis_reconstructors = map snd metis_prover_infos
14.43 +
14.44 +val is_metis_prover = AList.defined (op =) metis_prover_infos
14.45 val is_atp = member (op =) o supported_atps
14.46
14.47 -val select_smt_solver =
14.48 - Context.proof_map o SMT_Config.select_solver
14.49 +val select_smt_solver = Context.proof_map o SMT_Config.select_solver
14.50
14.51 fun is_smt_prover ctxt name =
14.52 member (op =) (SMT_Solver.available_solvers_of ctxt) name
14.53 @@ -155,7 +168,7 @@
14.54 is_metis_prover orf is_smt_prover ctxt orf
14.55 is_atp_installed (Proof_Context.theory_of ctxt)
14.56
14.57 -fun get_slices num_facts slicing slices =
14.58 +fun get_slices slicing slices =
14.59 (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
14.60
14.61 val metis_default_max_relevant = 20
14.62 @@ -166,8 +179,7 @@
14.63 metis_default_max_relevant
14.64 else if is_atp thy name then
14.65 fold (Integer.max o fst o snd o snd o snd)
14.66 - (get_slices 16384 (* large number *) slicing
14.67 - (#best_slices (get_atp thy name) ctxt)) 0
14.68 + (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
14.69 else (* is_smt_prover ctxt name *)
14.70 SMT_Solver.default_max_relevant ctxt name
14.71 end
14.72 @@ -266,7 +278,7 @@
14.73 let
14.74 val thy = Proof_Context.theory_of ctxt
14.75 val (remote_provers, local_provers) =
14.76 - metis_prover_names @
14.77 + map fst metis_prover_infos @
14.78 sort_strings (supported_atps thy) @
14.79 sort_strings (SMT_Solver.available_solvers_of ctxt)
14.80 |> List.partition (String.isPrefix remote_prefix)
14.81 @@ -408,8 +420,11 @@
14.82 in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
14.83
14.84 fun tac_for_reconstructor Metis =
14.85 - Metis_Tactics.metis_tac [Metis_Tactics.default_unsound_type_sys]
14.86 - | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
14.87 + Metis_Tactics.metis_tac [Metis_Tactics.partial_type_sys]
14.88 + | tac_for_reconstructor Metis_Full_Types =
14.89 + Metis_Tactics.metis_tac [Metis_Tactics.full_type_sys]
14.90 + | tac_for_reconstructor Metis_No_Types =
14.91 + Metis_Tactics.metis_tac [Metis_Tactics.no_type_sys]
14.92 | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
14.93
14.94 fun timed_reconstructor reconstructor debug timeout ths =
14.95 @@ -520,17 +535,22 @@
14.96 (case preplay of
14.97 Played (reconstructor, time) =>
14.98 if Time.<= (time, metis_minimize_max_time) then
14.99 - reconstructor_name reconstructor
14.100 + prover_name_for_reconstructor reconstructor |> the_default name
14.101 else
14.102 name
14.103 | _ => name)
14.104 |> minimize_command
14.105
14.106 +fun repair_monomorph_context max_iters max_new_instances =
14.107 + Config.put Monomorph.max_rounds max_iters
14.108 + #> Config.put Monomorph.max_new_instances max_new_instances
14.109 + #> Config.put Monomorph.keep_partial_instances false
14.110 +
14.111 fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
14.112 - Config.put SMT_Config.verbose debug
14.113 - #> Config.put SMT_Config.monomorph_full false
14.114 + (not debug ? Config.put SMT_Config.verbose false)
14.115 #> Config.put SMT_Config.monomorph_limit max_mono_iters
14.116 #> Config.put SMT_Config.monomorph_instances max_mono_instances
14.117 + #> Config.put SMT_Config.monomorph_full false
14.118
14.119 fun run_atp mode name
14.120 ({exec, required_execs, arguments, proof_delims, known_failures,
14.121 @@ -579,25 +599,23 @@
14.122 let
14.123 (* If slicing is disabled, we expand the last slice to fill the
14.124 entire time available. *)
14.125 - val actual_slices =
14.126 - get_slices (length facts) slicing (best_slices ctxt)
14.127 + val actual_slices = get_slices slicing (best_slices ctxt)
14.128 val num_actual_slices = length actual_slices
14.129 fun monomorphize_facts facts =
14.130 let
14.131 + val ctxt =
14.132 + ctxt |> repair_monomorph_context max_mono_iters
14.133 + max_new_mono_instances
14.134 (* pseudo-theorem involving the same constants as the subgoal *)
14.135 val subgoal_th =
14.136 Logic.list_implies (hyp_ts, concl_t)
14.137 |> Skip_Proof.make_thm thy
14.138 - val indexed_facts =
14.139 - (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
14.140 - val max_mono_instances = max_new_mono_instances + length facts
14.141 in
14.142 - ctxt |> repair_smt_monomorph_context debug max_mono_iters
14.143 - max_mono_instances
14.144 - |> SMT_Monomorph.monomorph indexed_facts
14.145 - |> fst |> sort (int_ord o pairself fst)
14.146 - |> filter_out (curry (op =) ~1 o fst)
14.147 - |> map (apfst (fst o nth facts))
14.148 + Monomorph.monomorph Monomorph.all_schematic_consts_of
14.149 + (subgoal_th :: map snd facts |> map (pair 0)) ctxt
14.150 + |> fst |> tl
14.151 + |> curry ListPair.zip (map fst facts)
14.152 + |> maps (fn (name, rths) => map (pair name o snd) rths)
14.153 end
14.154 fun run_slice blacklist (slice, (time_frac, (complete,
14.155 (best_max_relevant, best_type_systems))))
14.156 @@ -618,6 +636,7 @@
14.157 ? filter_out (member (op =) blacklist o fst)
14.158 |> polymorphism_of_type_sys type_sys <> Polymorphic
14.159 ? monomorphize_facts
14.160 + |> map (apsnd prop_of)
14.161 val real_ms = Real.fromInt o Time.toMilliseconds
14.162 val slice_timeout =
14.163 ((real_ms time_left
14.164 @@ -653,7 +672,7 @@
14.165 "exec " ^ core) ^ " 2>&1"
14.166 val _ =
14.167 atp_problem
14.168 - |> tptp_strings_for_atp_problem format
14.169 + |> tptp_lines_for_atp_problem format
14.170 |> cons ("% " ^ command ^ "\n")
14.171 |> File.write_list prob_file
14.172 val conjecture_shape =
14.173 @@ -776,7 +795,7 @@
14.174 |> map snd
14.175 in
14.176 play_one_line_proof debug preplay_timeout used_ths state subgoal
14.177 - [Metis, MetisFT]
14.178 + metis_reconstructors
14.179 end,
14.180 fn preplay =>
14.181 let
14.182 @@ -858,14 +877,14 @@
14.183 let
14.184 val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
14.185 val repair_context =
14.186 - select_smt_solver name
14.187 - #> (if overlord then
14.188 - Config.put SMT_Config.debug_files
14.189 - (overlord_file_location_for_prover name
14.190 - |> (fn (path, name) => path ^ "/" ^ name))
14.191 - else
14.192 - I)
14.193 - #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
14.194 + select_smt_solver name
14.195 + #> (if overlord then
14.196 + Config.put SMT_Config.debug_files
14.197 + (overlord_file_location_for_prover name
14.198 + |> (fn (path, name) => path ^ "/" ^ name))
14.199 + else
14.200 + I)
14.201 + #> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
14.202 val state = state |> Proof.map_context repair_context
14.203 fun do_slice timeout slice outcome0 time_so_far facts =
14.204 let
14.205 @@ -970,7 +989,7 @@
14.206 else "smt_solver = " ^ maybe_quote name
14.207 in
14.208 case play_one_line_proof debug preplay_timeout used_ths state
14.209 - subgoal [Metis, MetisFT] of
14.210 + subgoal metis_reconstructors of
14.211 p as Played _ => p
14.212 | _ => Trust_Playable (SMT (smt_settings ()), NONE)
14.213 end,
14.214 @@ -1000,9 +1019,10 @@
14.215 fun run_metis mode name ({debug, timeout, ...} : params) minimize_command
14.216 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
14.217 let
14.218 - val reconstructor = if name = Metis_Tactics.metisN then Metis
14.219 - else if name = Metis_Tactics.metisFT_N then MetisFT
14.220 - else raise Fail ("unknown Metis version: " ^ quote name)
14.221 + val reconstructor =
14.222 + case AList.lookup (op =) metis_prover_infos name of
14.223 + SOME r => r
14.224 + | NONE => raise Fail ("unknown Metis version: " ^ quote name)
14.225 val (used_facts, used_ths) =
14.226 facts |> map untranslated_fact |> ListPair.unzip
14.227 in
15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jun 07 11:12:05 2011 +0200
15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jun 07 11:24:16 2011 +0200
15.3 @@ -102,7 +102,8 @@
15.4 (case preplay of
15.5 Played (reconstructor, timeout) =>
15.6 if can_min_fast_enough (Time.toMilliseconds timeout) then
15.7 - (true, reconstructor_name reconstructor)
15.8 + (true, prover_name_for_reconstructor reconstructor
15.9 + |> the_default name)
15.10 else
15.11 (prover_fast_enough, name)
15.12 | _ => (prover_fast_enough, name),
16.1 --- a/src/HOL/Tools/monomorph.ML Tue Jun 07 11:12:05 2011 +0200
16.2 +++ b/src/HOL/Tools/monomorph.ML Tue Jun 07 11:24:16 2011 +0200
16.3 @@ -37,7 +37,7 @@
16.4 (* configuration options *)
16.5 val max_rounds: int Config.T
16.6 val max_new_instances: int Config.T
16.7 - val complete_instances: bool Config.T
16.8 + val keep_partial_instances: bool Config.T
16.9
16.10 (* monomorphization *)
16.11 val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
16.12 @@ -66,8 +66,8 @@
16.13 val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
16.14 val max_new_instances =
16.15 Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
16.16 -val complete_instances =
16.17 - Attrib.setup_config_bool @{binding monomorph_complete_instances} (K true)
16.18 +val keep_partial_instances =
16.19 + Attrib.setup_config_bool @{binding monomorph_keep_partial_instances} (K true)
16.20
16.21
16.22
16.23 @@ -161,7 +161,7 @@
16.24 fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
16.25 let
16.26 val thy = Proof_Context.theory_of ctxt
16.27 - val count_partial = Config.get ctxt complete_instances
16.28 + val count_partial = Config.get ctxt keep_partial_instances
16.29
16.30 fun add_new_ground subst n T =
16.31 let val T' = Envir.subst_type subst T
16.32 @@ -287,7 +287,7 @@
16.33 in (map inst thm_infos, ctxt) end
16.34
16.35 fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
16.36 - if Config.get ctxt complete_instances then
16.37 + if Config.get ctxt keep_partial_instances then
16.38 let fun is_refined ((_, _, refined), _) = refined
16.39 in
16.40 (Inttab.map (K (filter_out is_refined)) subs, thm_infos)
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/HOL/ex/ATP_Export.thy Tue Jun 07 11:24:16 2011 +0200
17.3 @@ -0,0 +1,36 @@
17.4 +theory ATP_Export
17.5 +imports Complex_Main
17.6 +uses "atp_export.ML"
17.7 +begin
17.8 +
17.9 +ML {*
17.10 +val do_it = false; (* switch to true to generate files *)
17.11 +val thy = @{theory Complex_Main};
17.12 +val ctxt = @{context}
17.13 +*}
17.14 +
17.15 +ML {*
17.16 +if do_it then
17.17 + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy true
17.18 + "/tmp/infs_full_types.tptp"
17.19 +else
17.20 + ()
17.21 +*}
17.22 +
17.23 +ML {*
17.24 +if do_it then
17.25 + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy false
17.26 + "/tmp/infs_partial_types.tptp"
17.27 +else
17.28 + ()
17.29 +*}
17.30 +
17.31 +ML {*
17.32 +if do_it then
17.33 + ATP_Export.generate_tptp_graph_file_for_theory ctxt thy
17.34 + "/tmp/graph.out"
17.35 +else
17.36 + ()
17.37 +*}
17.38 +
17.39 +end
18.1 --- a/src/HOL/ex/ROOT.ML Tue Jun 07 11:12:05 2011 +0200
18.2 +++ b/src/HOL/ex/ROOT.ML Tue Jun 07 11:24:16 2011 +0200
18.3 @@ -12,7 +12,7 @@
18.4 "Hebrew",
18.5 "Chinese",
18.6 "Serbian",
18.7 - "TPTP_Export"
18.8 + "ATP_Export"
18.9 ];
18.10
18.11 use_thys [
19.1 --- a/src/HOL/ex/TPTP_Export.thy Tue Jun 07 11:12:05 2011 +0200
19.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
19.3 @@ -1,36 +0,0 @@
19.4 -theory TPTP_Export
19.5 -imports Complex_Main
19.6 -uses "tptp_export.ML"
19.7 -begin
19.8 -
19.9 -ML {*
19.10 -val do_it = false; (* switch to true to generate files *)
19.11 -val thy = @{theory Complex_Main};
19.12 -val ctxt = @{context}
19.13 -*}
19.14 -
19.15 -ML {*
19.16 -if do_it then
19.17 - TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true
19.18 - "/tmp/infs_full_types.tptp"
19.19 -else
19.20 - ()
19.21 -*}
19.22 -
19.23 -ML {*
19.24 -if do_it then
19.25 - TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy false
19.26 - "/tmp/infs_partial_types.tptp"
19.27 -else
19.28 - ()
19.29 -*}
19.30 -
19.31 -ML {*
19.32 -if do_it then
19.33 - TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy
19.34 - "/tmp/graph.out"
19.35 -else
19.36 - ()
19.37 -*}
19.38 -
19.39 -end
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/HOL/ex/atp_export.ML Tue Jun 07 11:24:16 2011 +0200
20.3 @@ -0,0 +1,121 @@
20.4 +(* Title: HOL/ex/atp_export.ML
20.5 + Author: Jasmin Blanchette, TU Muenchen
20.6 + Copyright 2011
20.7 +
20.8 +Export Isabelle theories as first-order TPTP inferences, exploiting
20.9 +Sledgehammer's translation.
20.10 +*)
20.11 +
20.12 +signature ATP_EXPORT =
20.13 +sig
20.14 + val generate_tptp_graph_file_for_theory :
20.15 + Proof.context -> theory -> string -> unit
20.16 + val generate_tptp_inference_file_for_theory :
20.17 + Proof.context -> theory -> bool -> string -> unit
20.18 +end;
20.19 +
20.20 +structure ATP_Export : ATP_EXPORT =
20.21 +struct
20.22 +
20.23 +val ascii_of = ATP_Translate.ascii_of
20.24 +
20.25 +val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of
20.26 +
20.27 +fun facts_of thy =
20.28 + Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
20.29 + true (K true) [] []
20.30 +
20.31 +fun fold_body_thms f =
20.32 + let
20.33 + fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
20.34 + if Inttab.defined seen i then (x, seen)
20.35 + else
20.36 + let
20.37 + val body' = Future.join body;
20.38 + val (x', seen') = app (n + (if name = "" then 0 else 1)) body' (x, Inttab.update (i, ()) seen);
20.39 + in (x' |> n = 1 ? f (name, prop, body'), seen') end);
20.40 + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end;
20.41 +
20.42 +fun theorems_mentioned_in_proof_term thm =
20.43 + let
20.44 + fun collect (s, _, _) = if s <> "" then insert (op =) s else I
20.45 + val names =
20.46 + [] |> fold_body_thms collect [Thm.proof_body_of thm] |> map fact_name_of
20.47 + in names end
20.48 +
20.49 +fun interesting_const_names ctxt =
20.50 + let val thy = ProofContext.theory_of ctxt in
20.51 + Sledgehammer_Filter.const_names_in_fact thy
20.52 + (Sledgehammer_Provers.is_built_in_const_for_prover ctxt ATP_Systems.eN)
20.53 + end
20.54 +
20.55 +fun generate_tptp_graph_file_for_theory ctxt thy file_name =
20.56 + let
20.57 + val path = file_name |> Path.explode
20.58 + val _ = File.write path ""
20.59 + val axioms = Theory.all_axioms_of thy |> map fst
20.60 + fun do_thm thm =
20.61 + let
20.62 + val name = Thm.get_name_hint thm
20.63 + val s =
20.64 + "[" ^ Thm.legacy_get_kind thm ^ "] " ^
20.65 + (if member (op =) axioms name then "A" else "T") ^ " " ^
20.66 + prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^
20.67 + commas (theorems_mentioned_in_proof_term thm) ^ "; " ^
20.68 + commas (map (prefix ATP_Translate.const_prefix o ascii_of)
20.69 + (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
20.70 + in File.append path s end
20.71 + val thms = facts_of thy |> map (snd o snd)
20.72 + val _ = map do_thm thms
20.73 + in () end
20.74 +
20.75 +fun inference_term [] = NONE
20.76 + | inference_term ss =
20.77 + ATP_Problem.ATerm ("inference",
20.78 + [ATP_Problem.ATerm ("isabelle", []),
20.79 + ATP_Problem.ATerm ("[]", []),
20.80 + ATP_Problem.ATerm ("[]",
20.81 + map (fn s => ATP_Problem.ATerm (s, [])) ss)])
20.82 + |> SOME
20.83 +fun inference infers ident =
20.84 + these (AList.lookup (op =) infers ident) |> inference_term
20.85 +fun add_inferences_to_problem_line infers
20.86 + (ATP_Problem.Formula (ident, ATP_Problem.Axiom, phi, NONE, NONE)) =
20.87 + ATP_Problem.Formula (ident, ATP_Problem.Lemma, phi, inference infers ident,
20.88 + NONE)
20.89 + | add_inferences_to_problem_line _ line = line
20.90 +val add_inferences_to_problem =
20.91 + map o apsnd o map o add_inferences_to_problem_line
20.92 +
20.93 +fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name =
20.94 + let
20.95 + val format = ATP_Problem.FOF
20.96 + val type_sys =
20.97 + ATP_Translate.Preds
20.98 + (ATP_Translate.Polymorphic,
20.99 + if full_types then ATP_Translate.All_Types
20.100 + else ATP_Translate.Const_Arg_Types,
20.101 + ATP_Translate.Heavyweight)
20.102 + val path = file_name |> Path.explode
20.103 + val _ = File.write path ""
20.104 + val facts0 = facts_of thy
20.105 + val facts =
20.106 + facts0 |> map (fn ((_, loc), (_, th)) =>
20.107 + ((Thm.get_name_hint th, loc), prop_of th))
20.108 + val explicit_apply = NONE
20.109 + val (atp_problem, _, _, _, _, _, _) =
20.110 + ATP_Translate.prepare_atp_problem ctxt format
20.111 + ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
20.112 + [] @{prop False} facts
20.113 + val infers =
20.114 + facts0 |> map (fn (_, (_, th)) =>
20.115 + (fact_name_of (Thm.get_name_hint th),
20.116 + theorems_mentioned_in_proof_term th))
20.117 + val infers =
20.118 + infers |> map (apsnd (filter (member (op = o apsnd fst) infers)))
20.119 + val atp_problem = atp_problem |> add_inferences_to_problem infers
20.120 + val ss = ATP_Problem.tptp_lines_for_atp_problem ATP_Problem.FOF atp_problem
20.121 + val _ = app (File.append path) ss
20.122 + in () end
20.123 +
20.124 +end;
21.1 --- a/src/HOL/ex/tptp_export.ML Tue Jun 07 11:12:05 2011 +0200
21.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
21.3 @@ -1,122 +0,0 @@
21.4 -(* Title: HOL/ex/tptp_export.ML
21.5 - Author: Jasmin Blanchette, TU Muenchen
21.6 - Copyright 2011
21.7 -
21.8 -Export Isabelle theories as first-order TPTP inferences, exploiting
21.9 -Sledgehammer's translation.
21.10 -*)
21.11 -
21.12 -signature TPTP_EXPORT =
21.13 -sig
21.14 - val generate_tptp_graph_file_for_theory :
21.15 - Proof.context -> theory -> string -> unit
21.16 - val generate_tptp_inference_file_for_theory :
21.17 - Proof.context -> theory -> bool -> string -> unit
21.18 -end;
21.19 -
21.20 -structure TPTP_Export : TPTP_EXPORT =
21.21 -struct
21.22 -
21.23 -val ascii_of = ATP_Translate.ascii_of
21.24 -
21.25 -val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of
21.26 -
21.27 -fun facts_of thy =
21.28 - Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
21.29 - true (K true) [] []
21.30 -
21.31 -fun fold_body_thms f =
21.32 - let
21.33 - fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
21.34 - if Inttab.defined seen i then (x, seen)
21.35 - else
21.36 - let
21.37 - val body' = Future.join body;
21.38 - val (x', seen') = app (n + (if name = "" then 0 else 1)) body' (x, Inttab.update (i, ()) seen);
21.39 - in (x' |> n = 1 ? f (name, prop, body'), seen') end);
21.40 - in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end;
21.41 -
21.42 -fun theorems_mentioned_in_proof_term thm =
21.43 - let
21.44 - fun collect (s, _, _) = if s <> "" then insert (op =) s else I
21.45 - val names =
21.46 - [] |> fold_body_thms collect [Thm.proof_body_of thm] |> map fact_name_of
21.47 - in names end
21.48 -
21.49 -fun interesting_const_names ctxt =
21.50 - let val thy = ProofContext.theory_of ctxt in
21.51 - Sledgehammer_Filter.const_names_in_fact thy
21.52 - (Sledgehammer_Provers.is_built_in_const_for_prover ctxt ATP_Systems.eN)
21.53 - end
21.54 -
21.55 -fun generate_tptp_graph_file_for_theory ctxt thy file_name =
21.56 - let
21.57 - val path = file_name |> Path.explode
21.58 - val _ = File.write path ""
21.59 - val axioms = Theory.all_axioms_of thy |> map fst
21.60 - fun do_thm thm =
21.61 - let
21.62 - val name = Thm.get_name_hint thm
21.63 - val s =
21.64 - "[" ^ Thm.legacy_get_kind thm ^ "] " ^
21.65 - (if member (op =) axioms name then "A" else "T") ^ " " ^
21.66 - prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^
21.67 - commas (theorems_mentioned_in_proof_term thm) ^ "; " ^
21.68 - commas (map (prefix ATP_Translate.const_prefix o ascii_of)
21.69 - (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n"
21.70 - in File.append path s end
21.71 - val thms = facts_of thy |> map (snd o snd)
21.72 - val _ = map do_thm thms
21.73 - in () end
21.74 -
21.75 -fun inference_term [] = NONE
21.76 - | inference_term ss =
21.77 - ATP_Problem.ATerm ("inference",
21.78 - [ATP_Problem.ATerm ("isabelle", []),
21.79 - ATP_Problem.ATerm ("[]", []),
21.80 - ATP_Problem.ATerm ("[]",
21.81 - map (fn s => ATP_Problem.ATerm (s, [])) ss)])
21.82 - |> SOME
21.83 -fun inference infers ident =
21.84 - these (AList.lookup (op =) infers ident) |> inference_term
21.85 -fun add_inferences_to_problem_line infers
21.86 - (ATP_Problem.Formula (ident, ATP_Problem.Axiom, phi, NONE, NONE)) =
21.87 - ATP_Problem.Formula (ident, ATP_Problem.Lemma, phi, inference infers ident,
21.88 - NONE)
21.89 - | add_inferences_to_problem_line _ line = line
21.90 -val add_inferences_to_problem =
21.91 - map o apsnd o map o add_inferences_to_problem_line
21.92 -
21.93 -fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name =
21.94 - let
21.95 - val format = ATP_Problem.FOF
21.96 - val type_sys =
21.97 - ATP_Translate.Preds
21.98 - (ATP_Translate.Polymorphic,
21.99 - if full_types then ATP_Translate.All_Types
21.100 - else ATP_Translate.Const_Arg_Types,
21.101 - ATP_Translate.Heavyweight)
21.102 - val path = file_name |> Path.explode
21.103 - val _ = File.write path ""
21.104 - val facts0 = facts_of thy
21.105 - val facts =
21.106 - facts0 |> map (fn ((_, loc), (_, th)) =>
21.107 - ((Thm.get_name_hint th, loc), th))
21.108 - val explicit_apply = NONE
21.109 - val (atp_problem, _, _, _, _, _, _) =
21.110 - ATP_Translate.prepare_atp_problem ctxt format
21.111 - ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true
21.112 - [] @{prop False} facts
21.113 - val infers =
21.114 - facts0 |> map (fn (_, (_, th)) =>
21.115 - (fact_name_of (Thm.get_name_hint th),
21.116 - theorems_mentioned_in_proof_term th))
21.117 - val infers =
21.118 - infers |> map (apsnd (filter (member (op = o apsnd fst) infers)))
21.119 - val atp_problem = atp_problem |> add_inferences_to_problem infers
21.120 - val ss =
21.121 - ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.FOF atp_problem
21.122 - val _ = app (File.append path) ss
21.123 - in () end
21.124 -
21.125 -end;
22.1 --- a/src/Pure/Isar/isar_syn.ML Tue Jun 07 11:12:05 2011 +0200
22.2 +++ b/src/Pure/Isar/isar_syn.ML Tue Jun 07 11:24:16 2011 +0200
22.3 @@ -119,7 +119,7 @@
22.4 val _ =
22.5 Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
22.6 (Scan.repeat1 type_abbrev >> (fn specs => fn lthy =>
22.7 - (legacy_feature "Old 'types' commands -- use 'type_synonym' instead";
22.8 + (legacy_feature "Old 'types' command -- use 'type_synonym' instead";
22.9 fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs) specs lthy)));
22.10
22.11 val _ =