--- a/src/Doc/Sledgehammer/document/root.tex Sat Nov 14 12:57:28 2020 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Sat Nov 14 13:01:12 2020 +0100
@@ -47,6 +47,8 @@
\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+\hyphenation{Isa-belle super-posi-tion zipper-posi-tion}
+
\begin{document}
%%% TYPESETTING
@@ -103,13 +105,13 @@
historical.}
%
The supported ATPs include agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
-\cite{schulz-2002}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III
+\cite{schulz-2019}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III
\cite{leo3}, Satallax \cite{satallax}, SPASS \cite{weidenbach-et-al-2009},
Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and
Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely
via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT
solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009},
-and Z3 \cite{z3}. These are always run locally.
+and Z3 \cite{de-moura-2008}. These are always run locally.
The problem passed to the external provers (or solvers) consists of your current
goal together with a heuristic selection of hundreds of facts (theorems) from the
@@ -129,15 +131,15 @@
\newbox\boxA
\setbox\boxA=\hbox{\texttt{NOSPAM}}
-\newcommand\authoremail{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
-in.\allowbreak tum.\allowbreak de}}
+\newcommand\authoremail{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
+google.\allowbreak com}}
To run Sledgehammer, you must make sure that the theory \textit{Sledgehammer} is
imported---this is rarely a problem in practice since it is part of
-\textit{Main}. Examples of Sledgehammer use can be found in Isabelle's
-\texttt{src/HOL/Metis\_Examples} directory.
-Comments and bug reports concerning Sledgehammer or this manual should be
-directed to the author at \authoremail.
+\textit{Main}. Examples of Sledgehammer use can be found in the
+\texttt{src/HOL/Metis\_Examples} directory. Comments and bug reports
+concerning Sledgehammer or this manual should be directed to the author at
+\authoremail.
\section{Installation}
@@ -158,21 +160,21 @@
\begin{sloppy}
\begin{enum}
\item[\labelitemi] If you installed an official Isabelle package, it should
-already include properly setup executables for CVC4, E, SPASS, Vampire, and Z3,
-ready to use. To use Vampire, you must confirm that you are a noncommercial
-user, as indicated by the message that is displayed when Sledgehammer is
-invoked the first time.
+already include properly set up executables for CVC4, E, SPASS, Vampire, veriT,
+and Z3, ready to use. To use Vampire, you must confirm that you are a
+noncommercial user, as indicated by the message that is displayed when
+Sledgehammer is invoked the first time.
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3,
-CVC4, E, SPASS, Vampire, and Z3 binary packages from \download. Extract the
-archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash
-components}%
+CVC4, E, SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract
+the archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash
+etc\slash components}%
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
startup. Its value can be retrieved by executing \texttt{isabelle}
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
-file with the absolute path to CVC3, CVC4, E, SPASS, Vampire, or Z3. For
-example, if the \texttt{components} file does not exist yet and you extracted
-SPASS to \texttt{/usr/local/spass-3.8ds}, create it with the single line
+file with the absolute path to the prover. For example, if the
+\texttt{components} file does not exist yet and you extracted SPASS to
+\texttt{/usr/local/spass-3.8ds}, create it with the single line
\prew
\texttt{/usr/local/spass-3.8ds}
@@ -201,7 +203,7 @@
variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER},
\texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path
of the executable, \emph{including the file name}. Sledgehammer has been tested
-with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2019, and Z3 4.3.2.
+with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT 2020.10-rmx, and Z3 4.3.2.
Since Z3's output format is somewhat unstable, other versions of the solver
might not work well with Sledgehammer. Ideally, also set
\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or
@@ -219,7 +221,7 @@
(\texttt{libwww-perl}) installed. If you must use a proxy server to access the
Internet, set the \texttt{http\_proxy} environment variable to the proxy, either
in the environment in which Isabelle is launched or in your
-\texttt{\$ISABELLE\_HOME\_USER/etc/settings} file. Here are a few
+\texttt{\$ISABELLE\_HOME\_USER/etc/\allowbreak settings} file. Here are a few
examples:
\prew
@@ -245,8 +247,8 @@
\postw
Instead of issuing the \textbf{sledgehammer} command, you can also use the
-Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output
-after a few seconds:
+Sledgehammer panel in Isabelle/jEdit. Sledgehammer might produce something like
+the following output after a few seconds:
\prew
\slshape
@@ -265,9 +267,9 @@
provers are installed and how many processor cores are available, some of the
provers might be missing or present with a \textit{remote\_} prefix.
-For each successful prover, Sledgehammer gives a one-line \textit{metis} or
-\textit{smt} method call. Rough timings are shown in parentheses, indicating how
-fast the call is. You can click the proof to insert it into the theory text.
+For each successful prover, Sledgehammer gives a one-line Isabelle proof. Rough
+timings are shown in parentheses, indicating how fast the call is. You can
+click the proof to insert it into the theory text.
In addition, you can ask Sledgehammer for an Isar text proof by enabling the
\textit{isar\_proofs} option (\S\ref{output-format}):
@@ -277,8 +279,8 @@
\postw
When Isar proof construction is successful, it can yield proofs that are more
-readable and also faster than the \textit{metis} or \textit{smt} one-line
-proofs. This feature is experimental and is only available for ATPs.
+readable and also faster than \textit{metis} or \textit{smt} one-line
+proofs. This feature is experimental.
\section{Hints}
@@ -360,16 +362,16 @@
\begin{enum}
\item[\labelitemi]
-The traditional relevance filter, called \emph{MePo}
-(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available fact
-(lemma, theorem, definition, or axiom) based upon how many constants that fact
-shares with the conjecture. This process iterates to include facts relevant to
-those just accepted. The constants are weighted to give unusual ones greater
-significance. MePo copes best when the conjecture contains some unusual
-constants; if all the constants are common, it is unable to discriminate among
-the hundreds of facts that are picked up. The filter is also memoryless: It has
-no information about how many times a particular fact has been used in a proof,
-and it cannot learn.
+The traditional relevance filter, \emph{MePo}
+(\underline{Me}ng--\underline{Pau}lson), assigns a score to every available
+fact (lemma, theorem, definition, or axiom) based upon how many constants that
+fact shares with the conjecture. This process iterates to include facts
+relevant to those just accepted. The constants are weighted to give unusual
+ones greater significance. MePo copes best when the conjecture contains some
+unusual constants; if all the constants are common, it is unable to
+discriminate among the hundreds of facts that are picked up. The filter is also
+memoryless: It has no information about how many times a particular fact has
+been used in a proof, and it cannot learn.
\item[\labelitemi]
An alternative to MePo is \emph{MaSh} (\underline{Ma}chine Learner for
@@ -438,32 +440,7 @@
strongly encouraged to report this to the author at \authoremail.
-\point{How can I tell whether a suggested proof is sound?}
-
-Earlier versions of Sledgehammer often suggested unsound proofs---either proofs
-of nontheorems or simply proofs that rely on type-unsound inferences. This
-is a thing of the past, unless you explicitly specify an unsound encoding
-using \textit{type\_enc} (\S\ref{problem-encoding}).
-%
-Officially, the only form of ``unsoundness'' that lurks in the sound
-encodings is related to missing characteristic theorems of datatypes. For
-example,
-
-\prew
-\textbf{lemma}~``$\exists \mathit{xs}.\; \mathit{xs} \neq []$'' \\
-\textbf{sledgehammer} ()
-\postw
-
-suggests an argumentless \textit{metis} call that fails. However, the conjecture
-does actually hold, and the \textit{metis} call can be repaired by adding
-\textit{list.distinct}.
-%
-We hope to address this problem in a future version of Isabelle. In the
-meantime, you can avoid it by passing the \textit{strict} option
-(\S\ref{problem-encoding}).
-
-
-\point{What are the \textit{full\_types}, \textit{no\_types}, and
+\point{What are the \textit{full\_types}, \textit{no\_types}, and \\
\textit{mono\_tags} arguments to Metis?}
The \textit{metis}~(\textit{full\_types}) proof method
@@ -471,15 +448,10 @@
versions 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 = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
-higher-order places (e.g., in set comprehensions). The method is automatically
-tried 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 sets of option for up to 1~second each time to ensure that the generated
-one-line proofs actually work and to display timing information. This can be
-configured using the \textit{preplay\_timeout} and \textit{dont\_preplay}
-options (\S\ref{timeouts}).)
+higher-order places (e.g., in set comprehensions). The method is tried 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.
%
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
@@ -499,29 +471,25 @@
\textit{full\_types} option to \textit{metis} directly.
-\point{And what are the \textit{lifting} and \textit{hide\_lams} arguments
+\point{And what are the \textit{lifting} and \textit{hide\_lams} \\ arguments
to Metis?}
Orthogonally to the encoding of types, it is important to choose an appropriate
-translation of $\lambda$-abstractions. Metis supports three translation schemes,
-in decreasing order of power: Curry combinators (the default),
+translation of $\lambda$-abstractions. Metis supports three translation
+schemes, in decreasing order of power: Curry combinators (the default),
$\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under
$\lambda$-abstractions. The more powerful schemes also give the automatic
-provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details.
+provers more rope to hang themselves. See the \textit{lam\_trans} option
+(\S\ref{problem-encoding}) for details.
\point{Are the generated proofs minimal?}
Automatic provers frequently use many more facts than are necessary.
-Sledgehammer includes a minimization tool that takes a set of facts returned by
+Sledgehammer includes a proof minimization tool that takes a set of facts returned by
a given prover and repeatedly calls a prover or proof method with subsets of
those facts to find a minimal set. Reducing the number of facts typically helps
-reconstruction, while also removing superfluous clutter from the proof scripts.
-
-In earlier versions of Sledgehammer, generated proofs were systematically
-accompanied by a suggestion to invoke the minimization tool. This step is now
-performed by default but can be disabled using the \textit{minimize} option
-(\S\ref{mode-of-operation}).
+reconstruction, while decluttering the proof scripts.
\point{A strange error occurred---what should I do?}
@@ -541,9 +509,9 @@
\point{Why are there so many options?}
-Sledgehammer's philosophy should work out of the box, without user guidance.
-Many of the options are meant to be used mostly by the Sledgehammer developers
-for experiments. Of course, feel free to try them out if you are so inclined.
+Sledgehammer's philosophy is that it should work out of the box, without user
+guidance. Most of the options are meant to be used by the Sledgehammer
+developers for experiments.
\section{Command Syntax}
@@ -758,7 +726,7 @@
1.5-prerelease.
\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
-developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
+developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
install the prebuilt E package from \download. Sledgehammer has been tested with
@@ -775,27 +743,27 @@
higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
with support for the TPTP typed higher-order syntax (TH0). To use LEO-II, set
the environment variable \texttt{LEO2\_HOME} to the directory that contains the
-\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
+\texttt{leo} executable. Sledgehammer has been tested with version 1.3.4.
\item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic
higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph
Benzm\"uller et al.\ \cite{leo3},
with support for the TPTP typed higher-order syntax (TH0). To use Leo-III, set
the environment variable \texttt{LEO3\_HOME} to the directory that contains the
-\texttt{leo3} executable. Sledgehammer requires version 1.1 or above.
+\texttt{leo3} executable. Sledgehammer has been tested with version 1.1.
\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
support for the TPTP typed higher-order syntax (TH0). To use Satallax, set the
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
-\texttt{satallax} executable. Sledgehammer requires version 2.2 or above.
+\texttt{satallax} executable. Sledgehammer has been tested with version 2.2.
\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the
version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
-\download. Sledgehammer requires version 3.8ds or above.
+\download. Sledgehammer has been tested with version 3.8ds.
\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order
resolution prover developed by Andrei Voronkov and his colleagues
@@ -807,29 +775,29 @@
\item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an
SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues.
-It is specifically designed to produce detailed proofs for reconstruction in
-proof assistants. To use veriT, set the environment variable
-\texttt{VERIT\_SOLVER} to the complete path of the executable, including the
-file name. Sledgehammer has been tested with version smtcomp2019.
+It is designed to produce detailed proofs for reconstruction in proof
+assistants. To use veriT, set the environment variable \texttt{VERIT\_SOLVER}
+to the complete path of the executable, including the file name. Sledgehammer
+has been tested with version 2020.10-rmx.
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
-Microsoft Research \cite{z3}. To use Z3, set the environment variable
+Microsoft Research \cite{de-moura-2008}. To use Z3, set the environment variable
\texttt{Z3\_SOLVER} to the complete path of the executable, including the
file name. Sledgehammer has been tested with a pre-release version of 4.4.0.
\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to
-be an ATP, exploiting Z3's support for the TPTP typed first-order format
-(TF0). It is included for experimental purposes. It requires version 4.3.1 of
-Z3 or above. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME}
+be an ATP, exploiting Z3's support for the TPTP typed first-order format (TF0).
+It is included for experimental purposes. Sledgehammer has been tested with
+version 4.3.1. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME}
to the directory that contains the \texttt{z3\_tptp} executable.
\item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition
\cite{cruanes-2014} is a higher-order superposition prover developed by Simon
-Cruanes and colleagues. To use Zipperposition, set the environment variable
-\texttt{ZIPPERPOSITION\_HOME} to the directory that contains the
-\texttt{zipperposition} executable and \texttt{ZIPPERPOSITION\_VERSION} to the
-version number (e.g., ``2.0.1''). Sledgehammer has been tested with version
-2.0.1.
+Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the
+environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that
+contains the \texttt{zipperposition} executable and
+\texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1'').
+Sledgehammer has been tested with version 2.0.1.
\end{enum}
\end{sloppy}
@@ -892,8 +860,8 @@
{\small See also \textit{verbose} (\S\ref{output-format}).}
\optrue{minimize}{dont\_minimize}
-Specifies whether the minimization tool should be invoked automatically after
-proof search.
+Specifies whether the proof minimization tool should be invoked automatically
+after proof search.
\nopagebreak
{\small See also \textit{preplay\_timeout} (\S\ref{timeouts})
@@ -982,7 +950,7 @@
are relevant and 1 only theorems that refer to previously seen constants.
\optrue{learn}{dont\_learn}
-Specifies whether MaSh should be run automatically by Sledgehammer to learn the
+Specifies whether Sledgehammer invocations should run MaSh to learn the
available theories (and hence provide more accurate results). Learning takes
place only if MaSh is enabled.
@@ -1098,10 +1066,10 @@
\item[\labelitemi]
\textbf{%
\textit{mono\_guards}, \textit{mono\_tags} (sound);
-\textit{mono\_args} (unsound):} \\
+\textit{mono\_args} \\ (unsound):} \\
Similar to
\textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
-\textit{raw\_mono\_args}, respectively but types are mangled in constant names
+\textit{raw\_mono\_\allowbreak args}, respectively but types are mangled in constant names
instead of being supplied as ground term arguments. The binary predicate
$\const{g}(\tau, t)$ becomes a unary predicate
$\const{g\_}\tau(t)$, and the binary function
@@ -1112,14 +1080,23 @@
first-order types if the prover supports the TF0, TF1, TH0, or TH1 syntax;
otherwise, falls back on \textit{mono\_guards}. The problem is monomorphized.
-\item[\labelitemi] \textbf{\textit{mono\_native\_higher} (sound):} Exploits
-native higher-order types if the prover supports the TH0 syntax; otherwise,
-falls back on \textit{mono\_native} or \textit{mono\_guards}. The problem is
-monomorphized.
+\item[\labelitemi] \textbf{\textit{mono\_native\_fool} (sound):} Exploits native
+first-order types, including Booleans, if the prover supports the TFX0, TFX1,
+TH0, or TH1 syntax; otherwise, falls back on \textit{mono\_native}. The problem
+is monomorphized.
-\item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native
-first-order polymorphic types if the prover supports the TF1 or TH1 syntax;
-otherwise, falls back on \textit{mono\_native}.
+\item[\labelitemi] \textbf{\textit{mono\_native\_higher},
+\textit{mono\_native\_higher\_fool} \\ (sound):} Exploits native higher-order
+types, including Booleans if ending with ``\textit{\_fool}'', if the prover
+supports the TH0 syntax; otherwise, falls back on \textit{mono\_native} or
+\textit{mono\_native\_fool}. The problem is monomorphized.
+
+\item[\labelitemi] \textbf{\textit{poly\_native}, \textit{poly\_native\_fool},
+\textit{poly\_native\_higher}, \\ \textit{poly\_native\_higher\_fool} (sound):}
+Exploits native first-order polymorphic types if the prover supports the TF1,
+TFX1, or TH1 syntax; otherwise, falls back on \textit{mono\_native},
+\textit{mono\_native\_fool}, \textit{mono\_native\_higher}, or
+\textit{mono\_native\_higher\_fool}.
\item[\labelitemi]
\textbf{%
@@ -1326,9 +1303,8 @@
sledgehammer[prover=e,prover_timeout=10] Huffman.thy
\end{verbatim}
-This command specifies Sledgehammer as the action, using E as the prover with a
-timeout of 10 seconds. The results are written to the file
-\texttt{output/Huffman.log}.
+This command specifies Sledgehammer as the action, using the E prover with a
+timeout of 10 seconds. The results are written to \texttt{output/Huffman.log}.
\subsection{Example of Benchmarking Another Tool}
@@ -1337,7 +1313,7 @@
\end{verbatim}
This command specifies the \textbf{try0} command as the action, with a timeout
-of 10 seconds. The results are written to the file \texttt{output/Huffman.log}.
+of 10 seconds. The results are written to \texttt{output/Huffman.log}.
\subsection{Example of Generating TPTP Files}
--- a/src/Doc/manual.bib Sat Nov 14 12:57:28 2020 +0100
+++ b/src/Doc/manual.bib Sat Nov 14 13:01:12 2020 +0100
@@ -587,6 +587,25 @@
publisher = CUP,
year = 1990}
+@inproceedings{de-moura-2008,
+ author = {Leonardo de Moura and
+ Nikolaj Bj{\o}rner},
+ editor = {C. R. Ramakrishnan and
+ Jakob Rehof},
+ title = {{Z3}: An Efficient {SMT} Solver},
+ booktitle = {Tools and Algorithms for the Construction and Analysis of Systems --- TACAS 2008},
+ series = {Lecture Notes in Computer Science},
+ volume = {4963},
+ pages = {337--340},
+ publisher = {Springer},
+ year = {2008},
+ url = {https://doi.org/10.1007/978-3-540-78800-3\_24},
+ doi = {10.1007/978-3-540-78800-3\_24},
+ timestamp = {Tue, 14 May 2019 10:00:53 +0200},
+ biburl = {https://dblp.org/rec/conf/tacas/MouraB08.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
@Book{devlin79,
author = {Keith J. Devlin},
title = {Fundamentals of Contemporary Set Theory},
@@ -1107,10 +1126,23 @@
title = {The Objective Caml system -- Documentation and user's manual},
note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}}
-@misc{agsyHOL,
- author = "Fredrik Lindblad",
- title = "{agsyHOL}",
- note = "\url{https://github.com/frelindb/agsyHOL}"}
+@inproceedings{agsyHOL,
+ author = {Fredrik Lindblad},
+ editor = {St{\'{e}}phane Demri and
+ Deepak Kapur and
+ Christoph Weidenbach},
+ title = {A Focused Sequent Calculus for Higher-Order Logic},
+ booktitle = {Automated Reasoning --- IJCAR 2014},
+ series = {Lecture Notes in Computer Science},
+ volume = {8562},
+ pages = {61--75},
+ publisher = {Springer},
+ year = {2014},
+ url = {https://doi.org/10.1007/978-3-319-08587-6\_5},
+ doi = {10.1007/978-3-319-08587-6\_5},
+ timestamp = {Tue, 14 May 2019 10:00:39 +0200},
+ biburl = {https://dblp.org/rec/conf/cade/Lindblad14.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}}
@incollection{lochbihler-2010,
title = "Coinductive",
@@ -1819,14 +1851,23 @@
number = 4
}
-@article{schulz-2002,
- author = "Stephan Schulz",
- title = "E---A Brainiac Theorem Prover",
- journal = "Journal of AI Communications",
- year = 2002,
- volume = 15,
- number ="2/3",
- pages = "111--126"}
+@inproceedings{schulz-2019,
+ author = {Stephan Schulz and
+ Simon Cruanes and
+ Petar Vukmirovi\'c},
+ editor = {Pascal Fontaine},
+ title = {Faster, Higher, Stronger: {E} 2.3},
+ booktitle = {Automated Deduction --- {CADE}-27},
+ series = {Lecture Notes in Computer Science},
+ volume = {11716},
+ pages = {495--507},
+ publisher = {Springer},
+ year = {2019},
+ url = {https://doi.org/10.1007/978-3-030-29436-6\_29},
+ doi = {10.1007/978-3-030-29436-6\_29},
+ timestamp = {Sat, 19 Oct 2019 20:28:03 +0200},
+ biburl = {https://dblp.org/rec/conf/cade/0001CV19.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}}
@inproceedings{slind-tfl,
author = {Konrad Slind},
@@ -2019,10 +2060,28 @@
note = {\url{http://x-symbol.sourceforge.net}}
}
-@misc{weidenbach-et-al-2009,
- author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski",
- title = "{SPASS} Version 3.5",
- note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}
+@inproceedings{weidenbach-et-al-2009,
+ author = {Christoph Weidenbach and
+ Dilyana Dimova and
+ Arnaud Fietzke and
+ Rohit Kumar and
+ Martin Suda and
+ Patrick Wischnewski},
+ editor = {Renate A. Schmidt},
+ title = {{SPASS} Version 3.5},
+ booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
+ Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
+ series = {Lecture Notes in Computer Science},
+ volume = {5663},
+ pages = {140--145},
+ publisher = {Springer},
+ year = {2009},
+ url = {https://doi.org/10.1007/978-3-642-02959-2\_10},
+ doi = {10.1007/978-3-642-02959-2\_10},
+ timestamp = {Tue, 14 May 2019 10:00:39 +0200},
+ biburl = {https://dblp.org/rec/conf/cade/WeidenbachDFKSW09.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
@manual{isabelle-system,
author = {Makarius Wenzel},
@@ -2255,13 +2314,6 @@
title = {On the Implementation of an Extensible Declarative Proof Language},
crossref = {tphols99}}
-%Z
-
-@misc{z3,
- key = "Z3",
- title = "Z3: An Efficient {SMT} Solver",
- note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"}
-
% CROSS REFERENCES
--- a/src/HOL/Data_Structures/Interval_Tree.thy Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Data_Structures/Interval_Tree.thy Sat Nov 14 13:01:12 2020 +0100
@@ -78,7 +78,7 @@
fun inv_max_hi :: "('a::{linorder,order_bot}) ivl_tree \<Rightarrow> bool" where
"inv_max_hi Leaf \<longleftrightarrow> True" |
-"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (inv_max_hi l \<and> inv_max_hi r \<and> m = max3 a (max_hi l) (max_hi r))"
+"inv_max_hi (Node l (a, m) r) \<longleftrightarrow> (m = max3 a (max_hi l) (max_hi r) \<and> inv_max_hi l \<and> inv_max_hi r)"
lemma max_hi_is_max:
"inv_max_hi t \<Longrightarrow> a \<in> set_tree t \<Longrightarrow> high a \<le> max_hi t"
--- a/src/HOL/Data_Structures/RBT_Set.thy Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy Sat Nov 14 13:01:12 2020 +0100
@@ -108,7 +108,7 @@
fun invc :: "'a rbt \<Rightarrow> bool" where
"invc Leaf = True" |
"invc (Node l (a,c) r) =
- (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
+ ((c = Red \<longrightarrow> color l = Black \<and> color r = Black) \<and> invc l \<and> invc r)"
text \<open>Weaker version:\<close>
abbreviation invc2 :: "'a rbt \<Rightarrow> bool" where
@@ -116,7 +116,7 @@
fun invh :: "'a rbt \<Rightarrow> bool" where
"invh Leaf = True" |
-"invh (Node l (x, c) r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
+"invh (Node l (x, c) r) = (bheight l = bheight r \<and> invh l \<and> invh r)"
lemma invc2I: "invc t \<Longrightarrow> invc2 t"
by (cases t rule: tree2_cases) simp+
--- a/src/HOL/Data_Structures/Tree2.thy Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Data_Structures/Tree2.thy Sat Nov 14 13:01:12 2020 +0100
@@ -21,11 +21,11 @@
fun set_tree :: "('a*'b) tree \<Rightarrow> 'a set" where
"set_tree Leaf = {}" |
-"set_tree (Node l (a,_) r) = Set.insert a (set_tree l \<union> set_tree r)"
+"set_tree (Node l (a,_) r) = {a} \<union> set_tree l \<union> set_tree r"
fun bst :: "('a::linorder*'b) tree \<Rightarrow> bool" where
"bst Leaf = True" |
-"bst (Node l (a, _) r) = (bst l \<and> bst r \<and> (\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x))"
+"bst (Node l (a, _) r) = ((\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x) \<and> bst l \<and> bst r)"
lemma finite_set_tree[simp]: "finite(set_tree t)"
by(induction t) auto
--- a/src/HOL/Data_Structures/Tree23.thy Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Data_Structures/Tree23.thy Sat Nov 14 13:01:12 2020 +0100
@@ -36,9 +36,9 @@
fun complete :: "'a tree23 \<Rightarrow> bool" where
"complete Leaf = True" |
-"complete (Node2 l _ r) = (complete l & complete r & height l = height r)" |
+"complete (Node2 l _ r) = (height l = height r \<and> complete l & complete r)" |
"complete (Node3 l _ m _ r) =
- (complete l & complete m & complete r & height l = height m & height m = height r)"
+ (height l = height m & height m = height r & complete l & complete m & complete r)"
lemma ht_sz_if_complete: "complete t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
by (induction t) auto
--- a/src/HOL/Library/Tree.thy Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Library/Tree.thy Sat Nov 14 13:01:12 2020 +0100
@@ -28,7 +28,7 @@
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
"subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" |
-"subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)"
+"subtrees (\<langle>l, a, r\<rangle>) = {\<langle>l, a, r\<rangle>} \<union> subtrees l \<union> subtrees r"
fun mirror :: "'a tree \<Rightarrow> 'a tree" where
"mirror \<langle>\<rangle> = Leaf" |
@@ -53,7 +53,7 @@
fun complete :: "'a tree \<Rightarrow> bool" where
"complete Leaf = True" |
-"complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)"
+"complete (Node l x r) = (height l = height r \<and> complete l \<and> complete r)"
text \<open>Almost complete:\<close>
definition acomplete :: "'a tree \<Rightarrow> bool" where
@@ -90,7 +90,7 @@
fun bst_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool" where
"bst_wrt P \<langle>\<rangle> \<longleftrightarrow> True" |
"bst_wrt P \<langle>l, a, r\<rangle> \<longleftrightarrow>
- bst_wrt P l \<and> bst_wrt P r \<and> (\<forall>x\<in>set_tree l. P x a) \<and> (\<forall>x\<in>set_tree r. P a x)"
+ (\<forall>x\<in>set_tree l. P x a) \<and> (\<forall>x\<in>set_tree r. P a x) \<and> bst_wrt P l \<and> bst_wrt P r"
abbreviation bst :: "('a::linorder) tree \<Rightarrow> bool" where
"bst \<equiv> bst_wrt (<)"
@@ -98,7 +98,7 @@
fun (in linorder) heap :: "'a tree \<Rightarrow> bool" where
"heap Leaf = True" |
"heap (Node l m r) =
- (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
+ ((\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x) \<and> heap l \<and> heap r)"
subsection \<open>\<^const>\<open>map_tree\<close>\<close>
--- a/src/HOL/TPTP/ATP_Theory_Export.thy Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Sat Nov 14 13:01:12 2020 +0100
@@ -25,8 +25,8 @@
ML \<open>
if do_it then
"/tmp/isa_filter"
- |> generate_casc_lbt_isa_files_for_theory ctxt thy (THF (Polymorphic, THF_Without_Choice))
- infer_policy "poly_native_higher"
+ |> generate_casc_lbt_isa_files_for_theory ctxt thy
+ (THF (Without_FOOL, Polymorphic, THF_Without_Choice)) infer_policy "poly_native_higher"
else
()
\<close>
--- a/src/HOL/TPTP/atp_problem_import.ML Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Sat Nov 14 13:01:12 2020 +0100
@@ -298,8 +298,9 @@
val (format, type_enc, lam_trans) =
(case format_str of
"FOF" => (FOF, "mono_guards??", liftingN)
- | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
- | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
+ | "TF0" => (TFF (Without_FOOL, Monomorphic), "mono_native", liftingN)
+ | "TH0" => (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher",
+ keep_lamsN)
| "DFG" => (DFG Monomorphic, "mono_native", liftingN)
| _ => error ("Unknown format " ^ quote format_str ^
" (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
--- a/src/HOL/TPTP/atp_theory_export.ML Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Sat Nov 14 13:01:12 2020 +0100
@@ -36,12 +36,12 @@
val prefix = Library.prefix
val fact_name_of = prefix fact_prefix o ascii_of
-fun atp_of_format (THF (Polymorphic, _)) = leo3N
- | atp_of_format (THF (Monomorphic, _)) = satallaxN
+fun atp_of_format (THF (_, Polymorphic, _)) = leo3N
+ | atp_of_format (THF (_, Monomorphic, _)) = satallaxN
| atp_of_format (DFG Polymorphic) = pirateN
| atp_of_format (DFG Monomorphic) = spassN
- | atp_of_format (TFF Polymorphic) = alt_ergoN
- | atp_of_format (TFF Monomorphic) = vampireN
+ | atp_of_format (TFF (_, Polymorphic)) = alt_ergoN
+ | atp_of_format (TFF (_, Monomorphic)) = vampireN
| atp_of_format FOF = eN (* FIXME? *)
| atp_of_format CNF_UEQ = waldmeisterN
| atp_of_format CNF = eN (* FIXME? *)
--- a/src/HOL/Tools/ATP/atp_problem.ML Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Nov 14 13:01:12 2020 +0100
@@ -31,15 +31,16 @@
gen_prec : bool,
gen_simp : bool}
+ datatype fool = Without_FOOL | With_FOOL
datatype polymorphism = Monomorphic | Polymorphic
- datatype thf_choice = THF_Predicate_Free | THF_Without_Choice | THF_With_Choice
+ datatype thf_choice = THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
CNF_UEQ |
FOF |
- TFF of polymorphism |
- THF of polymorphism * thf_choice |
+ TFF of fool * polymorphism |
+ THF of fool * polymorphism * thf_choice |
DFG of polymorphism
datatype atp_formula_role =
@@ -188,15 +189,16 @@
gen_prec : bool,
gen_simp : bool}
+datatype fool = Without_FOOL | With_FOOL
datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_choice = THF_Predicate_Free | THF_Without_Choice | THF_With_Choice
+datatype thf_choice = THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
CNF_UEQ |
FOF |
- TFF of polymorphism |
- THF of polymorphism * thf_choice |
+ TFF of fool * polymorphism |
+ THF of fool * polymorphism * thf_choice |
DFG of polymorphism
datatype atp_formula_role =
@@ -915,9 +917,6 @@
end
in add 1 |> apsnd SOME end)
-fun avoid_clash_with_alt_ergo_type_vars s =
- if is_tptp_variable s then s else s ^ "_"
-
fun avoid_clash_with_dfg_keywords s =
let val n = String.size s in
if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
@@ -936,8 +935,7 @@
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
val avoid_clash =
(case format of
- TFF Polymorphic => avoid_clash_with_alt_ergo_type_vars
- | DFG _ => avoid_clash_with_dfg_keywords
+ DFG _ => avoid_clash_with_dfg_keywords
| _ => I)
val nice_name = nice_name avoid_clash
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Nov 14 13:01:12 2020 +0100
@@ -153,7 +153,7 @@
No_Types
datatype type_enc =
- Native of order * polymorphism * type_level |
+ Native of order * fool * polymorphism * type_level |
Guards of polymorphism * type_level |
Tags of polymorphism * type_level
@@ -162,13 +162,12 @@
fun is_type_enc_native (Native _) = true
| is_type_enc_native _ = false
-fun is_type_enc_full_higher_order (Native (Higher_Order THF_Predicate_Free, _, _)) = false
- | is_type_enc_full_higher_order (Native (Higher_Order _, _, _)) = true
- | is_type_enc_full_higher_order _ = false
-fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
+fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true
+ | is_type_enc_fool _ = false
+fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_higher_order _ = false
-fun polymorphism_of_type_enc (Native (_, poly, _)) = poly
+fun polymorphism_of_type_enc (Native (_, _, poly, _)) = poly
| polymorphism_of_type_enc (Guards (poly, _)) = poly
| polymorphism_of_type_enc (Tags (poly, _)) = poly
@@ -181,7 +180,7 @@
fun is_type_enc_mangling type_enc =
polymorphism_of_type_enc type_enc = Mangled_Monomorphic
-fun level_of_type_enc (Native (_, _, level)) = level
+fun level_of_type_enc (Native (_, _, _, level)) = level
| level_of_type_enc (Guards (_, level)) = level
| level_of_type_enc (Tags (_, level)) = level
@@ -381,7 +380,7 @@
fun default c = const_prefix ^ lookup_const c
in
fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
- | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _))) c =
+ | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _))) c =
if c = choice_const then tptp_choice else default c
| make_fixed_const _ c = default c
end
@@ -600,102 +599,125 @@
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
fun type_enc_of_string strictness s =
- (case try (unprefix "tc_") s of
- SOME s => (SOME Type_Class_Polymorphic, s)
- | NONE =>
- (case try (unprefix "poly_") s of
- SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
- | NONE =>
- (case try (unprefix "ml_poly_") s of
- SOME s => (SOME (Raw_Polymorphic Without_Phantom_Type_Vars), s)
+ let
+ val (poly, s) =
+ (case try (unprefix "tc_") s of
+ SOME s => (SOME Type_Class_Polymorphic, s)
| NONE =>
- (case try (unprefix "raw_mono_") s of
- SOME s => (SOME Raw_Monomorphic, s)
+ (case try (unprefix "poly_") s of
+ SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
| NONE =>
- (case try (unprefix "mono_") s of
- SOME s => (SOME Mangled_Monomorphic, s)
- | NONE => (NONE, s))))))
- ||> (fn s =>
- (case try_unsuffixes queries s of
- SOME s =>
- (case try_unsuffixes queries s of
- SOME s => (Nonmono_Types (strictness, Non_Uniform), s)
- | NONE => (Nonmono_Types (strictness, Uniform), s))
- | NONE =>
- (case try_unsuffixes ats s of
- SOME s => (Undercover_Types, s)
- | NONE => (All_Types, s))))
- |> (fn (poly, (level, core)) =>
- (case (core, (poly, level)) of
- ("native", (SOME poly, _)) =>
+ (case try (unprefix "ml_poly_") s of
+ SOME s => (SOME (Raw_Polymorphic Without_Phantom_Type_Vars), s)
+ | NONE =>
+ (case try (unprefix "raw_mono_") s of
+ SOME s => (SOME Raw_Monomorphic, s)
+ | NONE =>
+ (case try (unprefix "mono_") s of
+ SOME s => (SOME Mangled_Monomorphic, s)
+ | NONE => (NONE, s))))))
+
+ val (level, s) =
+ case try_unsuffixes queries s of
+ SOME s =>
+ (case try_unsuffixes queries s of
+ SOME s => (Nonmono_Types (strictness, Non_Uniform), s)
+ | NONE => (Nonmono_Types (strictness, Uniform), s))
+ | NONE =>
+ (case try_unsuffixes ats s of
+ SOME s => (Undercover_Types, s)
+ | NONE => (All_Types, s))
+
+ fun native_of_string s =
+ let
+ val (fool, core) =
+ (case try (unsuffix "_fool") s of
+ SOME s => (With_FOOL, s)
+ | NONE => (Without_FOOL, s))
+ in
+ (case (core, poly) of
+ ("native", SOME poly) =>
(case (poly, level) of
(Mangled_Monomorphic, _) =>
- if is_type_level_uniform level then Native (First_Order, Mangled_Monomorphic, level)
- else raise Same.SAME
+ if is_type_level_uniform level then
+ Native (First_Order, fool, Mangled_Monomorphic, level)
+ else
+ raise Same.SAME
| (Raw_Monomorphic, _) => raise Same.SAME
- | (poly, All_Types) => Native (First_Order, poly, All_Types))
- | ("native_higher", (SOME poly, _)) =>
+ | (poly, All_Types) => Native (First_Order, fool, poly, All_Types))
+ | ("native_higher", SOME poly) =>
(case (poly, level) of
(_, Nonmono_Types _) => raise Same.SAME
| (_, Undercover_Types) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
- Native (Higher_Order THF_With_Choice, Mangled_Monomorphic, level)
+ Native (Higher_Order THF_With_Choice, Without_FOOL, Mangled_Monomorphic, level)
else
raise Same.SAME
| (poly as Raw_Polymorphic _, All_Types) =>
- Native (Higher_Order THF_With_Choice, poly, All_Types)
- | _ => raise Same.SAME)
- | ("guards", (SOME poly, _)) =>
- if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
- poly = Type_Class_Polymorphic then
- raise Same.SAME
- else
- Guards (poly, level)
- | ("tags", (SOME poly, _)) =>
- if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
- poly = Type_Class_Polymorphic then
- raise Same.SAME
- else
- Tags (poly, level)
- | ("args", (SOME poly, All_Types (* naja *))) =>
- if poly = Type_Class_Polymorphic then raise Same.SAME
- else Guards (poly, Const_Types Without_Ctr_Optim)
- | ("args", (SOME poly, Nonmono_Types (_, Uniform) (* naja *))) =>
- if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then
- raise Same.SAME
- else
- Guards (poly, Const_Types With_Ctr_Optim)
- | ("erased", (NONE, All_Types (* naja *))) =>
- Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
- | _ => raise Same.SAME))
+ Native (Higher_Order THF_With_Choice, Without_FOOL, poly, All_Types)
+ | _ => raise Same.SAME))
+ end
+
+ fun nonnative_of_string core =
+ (case (core, poly, level) of
+ ("guards", SOME poly, _) =>
+ if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
+ poly = Type_Class_Polymorphic then
+ raise Same.SAME
+ else
+ Guards (poly, level)
+ | ("tags", SOME poly, _) =>
+ if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse
+ poly = Type_Class_Polymorphic then
+ raise Same.SAME
+ else
+ Tags (poly, level)
+ | ("args", SOME poly, All_Types (* naja *)) =>
+ if poly = Type_Class_Polymorphic then raise Same.SAME
+ else Guards (poly, Const_Types Without_Ctr_Optim)
+ | ("args", SOME poly, Nonmono_Types (_, Uniform) (* naja *)) =>
+ if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then
+ raise Same.SAME
+ else
+ Guards (poly, Const_Types With_Ctr_Optim)
+ | ("erased", NONE, All_Types (* naja *)) =>
+ Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
+ | _ => raise Same.SAME)
+ in
+ if String.isPrefix "native" s then
+ native_of_string s
+ else
+ nonnative_of_string s
+ end
handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
-fun min_hologic THF_Predicate_Free _ = THF_Predicate_Free
- | min_hologic _ THF_Predicate_Free = THF_Predicate_Free
- | min_hologic THF_Without_Choice _ = THF_Without_Choice
+fun min_hologic THF_Without_Choice _ = THF_Without_Choice
| min_hologic _ THF_Without_Choice = THF_Without_Choice
| min_hologic _ _ = THF_With_Choice
fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic')
| adjust_hologic _ type_enc = type_enc
+fun adjust_fool Without_FOOL _ = Without_FOOL
+ | adjust_fool _ fool = fool
+
fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars
| no_type_classes poly = poly
-fun adjust_type_enc (THF (Polymorphic, hologic)) (Native (order, poly, level)) =
- Native (adjust_hologic hologic order, no_type_classes poly, level)
- | adjust_type_enc (THF (Monomorphic, hologic)) (Native (order, _, level)) =
- Native (adjust_hologic hologic order, Mangled_Monomorphic, level)
- | adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
- Native (First_Order, Mangled_Monomorphic, level)
- | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
- Native (First_Order, poly, level)
- | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) =
- Native (First_Order, Mangled_Monomorphic, level)
- | adjust_type_enc (TFF _) (Native (_, poly, level)) =
- Native (First_Order, no_type_classes poly, level)
- | adjust_type_enc format (Native (_, poly, level)) =
+fun adjust_type_enc (THF (fool, Polymorphic, hologic)) (Native (order, fool', poly, level)) =
+ Native (adjust_hologic hologic order, adjust_fool fool fool', no_type_classes poly, level)
+ | adjust_type_enc (THF (fool, Monomorphic, hologic)) (Native (order, fool', _, level)) =
+ Native (adjust_hologic hologic order, adjust_fool fool fool', Mangled_Monomorphic, level)
+ | adjust_type_enc (TFF (fool, Monomorphic)) (Native (_, fool', _, level)) =
+ Native (First_Order, adjust_fool fool fool', Mangled_Monomorphic, level)
+ | adjust_type_enc (DFG Polymorphic) (Native (_, _, poly, level)) =
+ Native (First_Order, Without_FOOL, poly, level)
+ | adjust_type_enc (DFG Monomorphic) (Native (_, _, _, level)) =
+ Native (First_Order, Without_FOOL, Mangled_Monomorphic, level)
+ | adjust_type_enc (TFF (fool, _)) (Native (_, fool', poly, level)) =
+ Native (First_Order, adjust_fool fool fool', no_type_classes poly, level)
+ | adjust_type_enc format (Native (_, _, poly, level)) =
adjust_type_enc format (Guards (no_type_classes poly, level))
| adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
(if is_type_enc_sound type_enc then Tags else Guards) stuff
@@ -838,8 +860,8 @@
T_args
else
(case type_enc of
- Native (_, Raw_Polymorphic _, _) => T_args
- | Native (_, Type_Class_Polymorphic, _) => T_args
+ Native (_, _, Raw_Polymorphic _, _) => T_args
+ | Native (_, _, Type_Class_Polymorphic, _) => T_args
| _ =>
let
fun gen_type_args _ _ [] = []
@@ -889,7 +911,8 @@
AType
((if s = \<^type_name>\<open>fun\<close> andalso is_type_enc_higher_order type_enc then
`I tptp_fun_type
- else if s = \<^type_name>\<open>bool\<close> andalso is_type_enc_full_higher_order type_enc then
+ else if s = \<^type_name>\<open>bool\<close> andalso
+ (is_type_enc_higher_order type_enc orelse is_type_enc_fool type_enc) then
`I tptp_bool_type
else
`make_fixed_type_const s, []), map term Ts)
@@ -934,17 +957,11 @@
fun to_ho (ty as AType (((s, _), _), tys)) =
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
| to_ho _ = raise Fail "unexpected type"
- fun to_lfho (ty as AType (((s, _), _), tys)) =
- if s = tptp_fun_type then to_afun to_ho to_lfho tys
- else if pred_sym then bool_atype
- else to_atype ty
- | to_lfho _ = raise Fail "unexpected type"
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
| to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
| to_fo _ _ = raise Fail "unexpected type"
in
- if is_type_enc_full_higher_order type_enc then to_ho
- else if is_type_enc_higher_order type_enc then to_lfho
+ if is_type_enc_higher_order type_enc then to_ho
else to_fo ary
end
@@ -974,7 +991,7 @@
val tm_args =
tm_args @
(case type_enc of
- Native (_, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+ Native (_, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
[ATerm ((TYPE_name, ty_args), [])]
| _ => [])
in AAtom (ATerm ((cl, ty_args), tm_args)) end
@@ -1078,8 +1095,7 @@
fun introduce_proxies_in_iterm type_enc =
let
fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
- | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
- _ =
+ | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) _ =
(* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
limitation. This works in conjuction with special code in
"ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
@@ -1093,38 +1109,49 @@
fun intro top_level args (IApp (tm1, tm2)) =
IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
| intro top_level args (IConst (name as (s, _), T, T_args)) =
+ (* is_type_enc_fool *)
(case proxify_const s of
SOME proxy_base =>
- if top_level orelse is_type_enc_full_higher_order type_enc then
- (case (top_level, s) of
- (_, "c_False") => IConst (`I tptp_false, T, [])
- | (_, "c_True") => IConst (`I tptp_true, T, [])
- | (false, "c_Not") => IConst (`I tptp_not, T, [])
- | (false, "c_conj") => IConst (`I tptp_and, T, [])
- | (false, "c_disj") => IConst (`I tptp_or, T, [])
- | (false, "c_implies") => IConst (`I tptp_implies, T, [])
- | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
- | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
- | (false, s) =>
- if is_tptp_equal s then
- if length args = 2 then
- IConst (`I tptp_equal, T, [])
+ let
+ val argc = length args
+ val plain_const = IConst (name, T, [])
+ fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args)
+ fun if_card_matches card x = if card = argc then x else plain_const
+ val is_fool = is_type_enc_fool type_enc
+ in
+ if top_level orelse is_fool orelse is_type_enc_higher_order type_enc then
+ (case (top_level, s) of
+ (_, "c_False") => IConst (`I tptp_false, T, [])
+ | (_, "c_True") => IConst (`I tptp_true, T, [])
+ | (false, "c_Not") => if_card_matches 1 (IConst (`I tptp_not, T, []))
+ | (false, "c_conj") => if_card_matches 2 (IConst (`I tptp_and, T, []))
+ | (false, "c_disj") => if_card_matches 2 (IConst (`I tptp_or, T, []))
+ | (false, "c_implies") => if_card_matches 2 (IConst (`I tptp_implies, T, []))
+ | (false, "c_All") => if_card_matches 1 (tweak_ho_quant tptp_ho_forall T args)
+ | (false, "c_Ex") => if_card_matches 1 (tweak_ho_quant tptp_ho_exists T args)
+ | (false, s) =>
+ if is_tptp_equal s then
+ if argc = 2 then
+ IConst (`I tptp_equal, T, [])
+ else if is_fool then
+ proxy_const ()
+ else
+ (* Eta-expand partially applied THF equality, because the
+ LEO-II and Satallax parsers complain about not being able to
+ infer the type of "=". *)
+ let val i_T = domain_type T in
+ IAbs ((`I "Y", i_T),
+ IAbs ((`I "Z", i_T),
+ IApp (IApp (IConst (`I tptp_equal, T, []),
+ IConst (`I "Y", i_T, [])),
+ IConst (`I "Z", i_T, []))))
+ end
else
- (* Eta-expand partially applied THF equality, because the
- LEO-II and Satallax parsers complain about not being able to
- infer the type of "=". *)
- let val i_T = domain_type T in
- IAbs ((`I "Y", i_T),
- IAbs ((`I "Z", i_T),
- IApp (IApp (IConst (`I tptp_equal, T, []),
- IConst (`I "Y", i_T, [])),
- IConst (`I "Z", i_T, []))))
- end
- else
- IConst (name, T, [])
- | _ => IConst (name, T, []))
- else
- IConst (proxy_base |>> prefix const_prefix, T, T_args)
+ plain_const
+ | _ => plain_const)
+ else
+ IConst (proxy_base |>> prefix const_prefix, T, T_args)
+ end
| NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
else IConst (name, T, T_args))
| intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
@@ -1251,7 +1278,7 @@
|> transform_elim_prop
|> Object_Logic.atomize_term ctxt
val need_trueprop = (fastype_of t = \<^typ>\<open>bool\<close>)
- val is_ho = is_type_enc_full_higher_order type_enc
+ val is_ho = is_type_enc_higher_order type_enc
in
t |> need_trueprop ? HOLogic.mk_Trueprop
|> (if is_ho then unextensionalize_def
@@ -1264,7 +1291,7 @@
(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
reasons. *)
fun should_use_iff_for_eq CNF _ = false
- | should_use_iff_for_eq (THF _) format = not (is_type_enc_full_higher_order format)
+ | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
| should_use_iff_for_eq _ _ = true
fun make_formula ctxt format type_enc iff_for_eq name stature role t =
@@ -1397,7 +1424,7 @@
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @
([tptp_equal, tptp_old_equal]
|> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false}))
- |> not (is_type_enc_full_higher_order type_enc)
+ |> not (is_type_enc_fool type_enc orelse is_type_enc_higher_order type_enc)
? cons (prefixed_predicator_name,
{pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false})
@@ -1596,8 +1623,9 @@
if is_pred_sym sym_tab s then tm else predicatify completish tm
| _ => predicatify completish tm)
val do_iterm =
- (not (is_type_enc_higher_order type_enc) ? introduce_app_ops)
- #> (not (is_type_enc_full_higher_order type_enc) ? introduce_predicators)
+ (not (is_type_enc_higher_order type_enc) ?
+ (introduce_app_ops #>
+ not (is_type_enc_fool type_enc) ? introduce_predicators))
#> filter_type_args_in_iterm thy ctrss type_enc
in update_iformula (formula_map do_iterm) end
@@ -1679,10 +1707,10 @@
|> class_membs_of_types type_enc add_sorts_on_tvar
|> map (class_atom type_enc)))
#> (case type_enc of
- Native (_, Type_Class_Polymorphic, _) =>
+ Native (_, _, Type_Class_Polymorphic, _) =>
mk_atyquant AForall (map (fn TVar (z as (_, S)) =>
(AType ((tvar_name z, []), []), map (`make_class) (normalize_classes S) )) Ts)
- | Native (_, Raw_Polymorphic _, _) =>
+ | Native (_, _, Raw_Polymorphic _, _) =>
mk_atyquant AForall (map (fn TVar (z as _) => (AType ((tvar_name z, []), []), [])) Ts)
| _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts)))
@@ -2101,7 +2129,7 @@
fun decl_lines_of_classes type_enc =
(case type_enc of
- Native (_, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
+ Native (_, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms)
| _ => K [])
fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
@@ -2161,7 +2189,7 @@
? (fold (fold add_fact_syms) [conjs, facts]
#> fold add_iterm_syms extra_tms
#> (case type_enc of
- Native (_, Raw_Polymorphic phantoms, _) =>
+ Native (_, _, Raw_Polymorphic phantoms, _) =>
phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
| Native _ => I
| _ => fold add_undefined_const (var_types ())))
--- a/src/HOL/Tools/ATP/atp_proof.ML Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sat Nov 14 13:01:12 2020 +0100
@@ -58,6 +58,7 @@
val z3_tptpN : string
val zipperpositionN : string
val remote_prefix : string
+ val dummy_tfxN : string
val agsyhol_core_rule : string
val spass_input_rule : string
@@ -120,6 +121,7 @@
val z3_tptpN = "z3_tptp"
val zipperpositionN = "zipperposition"
val remote_prefix = "remote_"
+val dummy_tfxN = "dummy_tfx"
val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
val spass_input_rule = "Inp"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/dummy_atp Sat Nov 14 13:01:12 2020 +0100
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+echo "SZS status Unknown"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sat Nov 14 12:57:28 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sat Nov 14 13:01:12 2020 +0100
@@ -173,7 +173,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((60, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -195,7 +195,7 @@
prem_role = Hypothesis,
best_slices = fn _ =>
(* FUDGE *)
- [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
+ [(1.0, (((100, ""), TFF (Without_FOOL, Polymorphic), "poly_native", liftingN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -293,10 +293,12 @@
best_slices = fn ctxt =>
let
val heuristic = Config.get ctxt e_selection_heuristic
- val ehoh = string_ord (getenv "E_VERSION", "2.3") <> LESS
+ val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS
val (format, enc) =
- if ehoh then (THF (Monomorphic, THF_Predicate_Free), "mono_native_higher")
- else (TFF Monomorphic, "mono_native")
+ if modern then
+ (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool")
+ else
+ (TFF (Without_FOOL, Monomorphic), "mono_native")
in
(* FUDGE *)
if heuristic = e_smartN then
@@ -355,7 +357,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -376,7 +378,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((150, ""), THF (Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -399,7 +401,7 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (((150, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+ K [(1.0, (((150, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -504,9 +506,9 @@
prem_role = Hypothesis,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (((500, meshN), TFF Monomorphic, "mono_native", combs_or_liftingN, false), sosN)),
- (0.333, (((150, meshN), TFF Monomorphic, "poly_tags??", combs_or_liftingN, false), sosN)),
- (0.334, (((50, meshN), TFF Monomorphic, "mono_native", combs_or_liftingN, false), no_sosN))]
+ [(0.333, (((500, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), sosN)),
+ (0.333, (((150, meshN), TFF (Without_FOOL, Monomorphic), "poly_tags??", combs_or_liftingN, false), sosN)),
+ (0.334, (((50, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), no_sosN))]
|> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
@@ -525,10 +527,10 @@
prem_role = Hypothesis,
best_slices =
(* FUDGE *)
- K [(0.5, (((250, meshN), TFF Monomorphic, "mono_native", combsN, false), "")),
- (0.25, (((125, mepoN), TFF Monomorphic, "mono_native", combsN, false), "")),
- (0.125, (((62, mashN), TFF Monomorphic, "mono_native", combsN, false), "")),
- (0.125, (((31, meshN), TFF Monomorphic, "mono_native", combsN, false), ""))],
+ K [(0.5, (((250, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")),
+ (0.25, (((125, mepoN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")),
+ (0.125, (((62, mashN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")),
+ (0.125, (((31, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), ""))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
@@ -551,9 +553,9 @@
prem_role = Conjecture,
best_slices = fn _ =>
(* FUDGE *)
- [(0.333, (((128, "meshN"), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
- (0.333, (((32, "meshN"), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
- (0.334, (((512, "meshN"), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
+ [(0.333, (((128, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
+ (0.333, (((32, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
+ (0.334, (((512, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}
@@ -636,29 +638,50 @@
val remote_agsyhol =
remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
- (K (((60, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_alt_ergo =
remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"]
- (K (((250, ""), TFF Polymorphic, "poly_native", keep_lamsN, false), "") (* FUDGE *))
+ (K (((250, ""), TFF (Without_FOOL, Polymorphic), "poly_native", keep_lamsN, false), "") (* FUDGE *))
val remote_e =
remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
- (K (((750, ""), TFF Monomorphic, "mono_native", combsN, false), "") (* FUDGE *))
+ (K (((750, ""), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "") (* FUDGE *))
val remote_iprover =
remotify_atp iprover "iProver" ["0.99"]
(K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
- (K (((40, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *))
+ (K (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *))
val remote_leo3 =
remotify_atp leo3 "Leo-III" ["1.1"]
- (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["THF-4.4"]
- (K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *))
+ (K (((400, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *))
val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
val remote_zipperposition =
remotify_atp zipperposition "Zipperpin" ["2.0"]
- (K (((512, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+ (K (((512, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+
+
+(* Dummy prover *)
+
+fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
+ {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
+ arguments = K (K (K (K (K (K ""))))),
+ proof_delims = [],
+ known_failures = known_szs_status_failures,
+ prem_role = prem_role,
+ best_slices =
+ K [(1.0, (((200, ""), format, type_enc,
+ if is_format_higher_order format then keep_lamsN
+ else combsN, uncurried_aliases), ""))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = default_max_new_mono_instances}
+
+val dummy_tfx_format = TFF (With_FOOL, Polymorphic)
+
+val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false
+val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
(* Setup *)
@@ -696,7 +719,7 @@
val atps =
[agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
- remote_vampire, remote_waldmeister, remote_zipperposition]
+ remote_vampire, remote_waldmeister, remote_zipperposition, dummy_tfx]
val _ = Theory.setup (fold add_atp atps)