quantHeuristics/doc/quantHeu.tex

\documentclass[a4paper,12pt,DIV=12,oneside]{scrbook}

\usepackage{amsthm}
\usepackage{palatino}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage[sort&compress]{natbib}
\usepackage{hyperref}
\usepackage{lmodern}
\usepackage{tabularx}
\usepackage{booktabs}
\newcommand{\tablehead}[1]{\addlinespace\multicolumn{2}{l}{\textit{#1}}\\}

\let\vec\relax
\DeclareMathAccent{\vec}{\mathord}{letters}{"7E}

\usepackage{accents}

\newcommand{\HOL}{{HOL}}
\newcommand{\fv}{\textit{fv}}

\newtheorem{lemma}{Lemma}[section]
\newtheorem{theorem}[lemma]{Theorem}

\theoremstyle{definition}
\newtheorem{definition}[lemma]{Definition}
\newtheorem{example}[lemma]{Example}

\theoremstyle{remark}
\newtheorem{remark}[lemma]{Remark}

\newcommand{\GE}{\ensuremath{G_\exists}}
\newcommand{\GEP}{\ensuremath{G_{\accentset{\bullet}{\exists}}}}
\newcommand{\GEG}{\ensuremath{G_{\accentset{\_\,\_}{\exists}}}}
\newcommand{\GU}{\ensuremath{G_\forall}}
\newcommand{\GUP}{\ensuremath{G_{\accentset{\bullet}{\forall}}}}
\newcommand{\GUG}{\ensuremath{G_{\accentset{\_\,\_}{\forall}}}}
\newcommand{\GO}{\ensuremath{G_{?}}}

\pagestyle{plain}

%------------------------------------------------------------------------------------------
% The title page
%------------------------------------------------------------------------------------------

\begin{document}

\title{Quantifier Heuristics Library}
\author{Thomas Tuerk}

\maketitle

\tableofcontents

\chapter{Introduction}
\section{Motivation}
\label{sec_motivation}

In interactive proofs it is often useful to be able to find instantiations
for quantifiers. The unwind library\footnote{see \texttt{src/simp/src/Unwind.sml}} allows
instantiations of ``trivial'' quantifiers:

\[ \forall x_1\ \ldots x_i \ldots x_n.\ P_1 \wedge \ldots \wedge x_i = c \wedge \ldots \wedge P_n \Longrightarrow Q \]
and
\[ \exists x_1\ \ldots x_i \ldots x_n.\ P_1 \wedge \ldots \wedge x_i =
c \wedge \ldots \wedge P_n \] can be simplified by
instantiating $x_i$ with $c$. Because unwind-conversions are
part of \texttt{bool\_ss}, they are used with nearly every call of the simplifier
and often simplify proofs considerably. However, the unwind library can only handle these common cases. If the term structure is
only slightly more complicated, it fails. For example, $\exists x.\ P(a) \Longrightarrow (x = 2) \wedge Q(x)$
cannot be tackled.

There is also the satisfy library\footnote{see \texttt{src/simp/src/Satisfy.sml}}, which uses unification to
show existentially quantified formulas. It can handle problems like
$\exists x.\ P_1(x,c_1)\ \wedge \ldots P_n(x,c_n)$ if given
theorems of the form $\forall x\ c.\ P_i(x, c)$. This is often handy, but still rather limited.

The quantifier heuristics library\footnote{see
  \texttt{src/quantHeur/quantHeuristicsLib.sml}} provides more power
and flexibility.  It can handle all the examples that the unwind and
satisfy libraries can handle. A few simple examples of what it can do
are shown in Table~\ref{table_examples}. Besides the power demonstrated
by these examples, the library is highly flexible as well.  At it's
core, there is a modular, syntax driven search for instantiation.
This search consists of a collection of interleaved heuristics.  Users
can easily configure existing heuristics and add own ones. Thereby, it
is easy to teach the library about new predicates, logical connectives
or datatypes.

\begin{table}[h]
\centering\scriptsize
\begin{tabularx}{\textwidth}{lll}\toprule
\textbf{Problem} & \textbf{Result} \\\midrule

\tablehead{basic examples}
$\exists x.\ x = 2 \wedge P (x)$ & $P(2)$ \\
$\forall x.\ x = 2 \Longrightarrow P (x)$ & $P(2)$ \\

\tablehead{solutions and counterexamples}
$\exists x.\ x = 2$ & $\textit{true}$ \\
$\forall x.\ x = 2$ & $\textit{false}$ \\

\tablehead{complicated nestings of standard operators}
$\exists x_1. \forall x_2.\ (x_1 = 2) \wedge P(x_1, x_2)$ &
$\forall x_2.\ P(2, x_2)$ \\

$\exists x_1, x_2.\ P_1(x_2) \Longrightarrow (x_1 = 2) \wedge P(x_1, x_2)$ &
$\exists x_2.\ P_1(x_2) \Longrightarrow P(2, x_2)$ \\
$\exists x.\ ((x = 2) \vee (2 = x)) \wedge P(x)$ & $P(2)$ \\

\tablehead{exploiting unification}
$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(10))$ & $P (f(10))$ \\
$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(x + 2))$ & $P (f(8 + 2))$ \\
$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f(x))$ & - (\text{no instantiation found}) \\

\tablehead{partial instantiation for datatypes}
$\forall p.\ c = \textsf{FST}(p) \Longrightarrow P(p)$ & $\forall p_2.\ P(c, p_2)$ \\

$\forall x.\ \textsf{IS\_NONE}(x) \vee P(x)$ & $\forall x'.\ P (\textsf{SOME}(x'))$ \\

$\forall l.\ l \neq [\,] \Longrightarrow P(l)$ & $\forall \textit{hd}, \textit{tl}.\
P(\textit{hd} :: \textit{tl})$ \\

\tablehead{context}
$P_1(c) \Longrightarrow \exists x.\ P_1(x) \vee P_2(x)$ & \textit{true} \\
$P_1(c) \Longrightarrow \forall x.\ \neg P_1(x) \wedge P_2(x)$ & $\neg P_1(c)$ \\

$(\forall x.\ P_1(x) \Rightarrow (x = 2)) \Longrightarrow (\forall x.\ P_1(x) \Rightarrow P_2(x))$ &
$(\forall x.\ P_1(x) \Rightarrow (x = 2)) \Rightarrow (P_1(2) \Rightarrow P_2(2))$ \\

$\big((\forall x.\ P_1(x) \Rightarrow P_2(x)) \wedge P_1(2)\big) \Longrightarrow \exists x.\ P_2(x)$ &
\textit{true} \\
\bottomrule
\end{tabularx}
\caption{Examples}
\label{table_examples}
\end{table}

\section{Structure}

This presentation of the quantifier heuristics library is structured into two parts.
The first part presents the logical foundations, whereas the second part presents the HOL~4 interface.
Readers not interested in the foundations, might skip the first part.

The first part starts with an introduction of the concept of guesses in Section~\ref{sec_guesses}. Then,
Section \ref{sec_base_guesses} shows how guesses can be derived for interesting terms like equations.
These guesses form the base cases of the search for instantiations. Then, Section \ref{sec_lifting_guesses}
discusses how these guesses are lifted over the term structure. Other concepts used for the search
are discussed in Section~\ref{sec_other_techniques}. In order to illustrate
this abstract presentation, Section~\ref{sec_examples} shows how
guess-search works for simple examples.

The second part starts with a high level presentation of the user-interface in
Section~\ref{sec_interface}. An important concept of the interface are
quantifier heuristic parameters, which allow configuring the behaviour of the library.
In Section~\ref{sec_qps} first predefined parameters are presented.
Then it is demonstrated using concrete examples, how own parameters can be developed.

The presentation closes with a short conclusion.


\chapter{Theoretical Foundations}

\section{Guesses}\label{sec_guesses}

\subsection{Weak Guesses for Existential Quantifiers}

In the introduction, it is stated that the core component of this work
is a search based on heuristics. Abstractly, given a term $\exists x.\
P(x)$ we want to find an instantiation $\lambda \fv. i(\fv)$ such that
$\exists x.\ P(x) \Longleftrightarrow \exists \fv.\ P(i(\fv))$
holds. In the following, such an $i$ is called a \emph{guess} for
variable $x$ in $P(x)$. In order to justify such a guess, we define
special predicates that capture the intended semantics.

\begin{definition}[Existential Guess]
  $i$ is an \emph{existential guess} for $P$ (denoted by $\GE(i, P)$)
  if and only if the equivalence $\exists x.\ P(x) \Longleftrightarrow
  \exists \fv.\ P(i(\fv))$ holds.
\end{definition}

\begin{example}
$\GE(K\ 2, \lambda x.\ x = 2)$ holds, because $\exists x.\ x = 2
\Longleftrightarrow 2 = 2$ holds. More interestingly,
$\GE(\lambda(x, xs').\ x::xs'), \lambda xs.\ xs \neq [] \wedge P(xs))$
holds. Therefore, $\exists xs.\ xs \neq []\ \wedge\ P(xs)$ can be simplified
to $\exists x\ xs'.\ x::xs' \neq []\ \wedge\ P(x::xs')$.
\end{example}

So, when trying to process $\exists x.\ P(x)$, we search
for an existential guess $i$ such that $\GE(i, \lambda x. P(x))$
holds. If such a guess is found, the original term can be simplified to
$\exists \fv.\ P(i(\fv))$, which is really \emph{simpler} provided sensible heuristics for creating
guesses are used. In particular, guesses $i$ that do not depend on $\fv$ frequently occur in practice.
The quantifier disappears completely in this common case.

\subsection{Strong Guesses for Existential Quantifiers}

The general idea for coming up with a guess $\GE(i, P)$ is preforming
a bottom-up search of the syntax tree of $P$. Unluckily, $\GE$ is
not well suited for such a search, because it is too weak to easily lift
guesses for subterms. Consider, for example, terms of the form
$\exists x.\ P_1(x) \vee P_2(x)$. If we have a guess $\GE(i, P_1)$, we unluckily can't lift it
to a guess $\GE(i, \lambda x.\ P_1(x) \vee P_2(x))$ in general. A counterexample
is $P_1(x) := \textit{false}$, $P_2(x) := (x = 2)$ and $i := K\ 3 = \lambda \fv.\ 3$.
Therefore, stronger types of guesses are introduced that work well with lifting:

\begin{definition}[Point Existenstial Guess]
$i$ is a \emph{point existential guess} for $P$ (denoted by $\GEP(i, P)$) if and only if $\forall \fv.\ P(i(\fv))$ holds.
\end{definition}

\begin{example}
  $\GEP(K\ 2, \lambda x.\ x=2)$ holds, because $2=2$ holds. In
  addition to weak existential guesses $\GE(i,P)$, point existential
  guesses $\GEP(i,P)$ carry information about the point $i$: the point
  $i$ satisfies $P$. For example $\GEP(\lambda (x,xs').\ x::xs',\ \lambda
  xs.\ xs \neq [])$ means that $\lambda xs.\ xs \neq []$ holds for all
  points of the form $x :: xs'$ (for arbitrary $x$, $xs'$).
\end{example}


\begin{definition}[Gap Existential Guess]
  $i$ is a \emph{gap existential guess} for $P$ (denoted by $\GEG(i, P)$)
  if and only if $\forall v.\ \big(\big(\forall \fv.\ v \neq
  i(\fv)\big) \Longrightarrow \neg P(v)\big)$ holds.
\end{definition}

\begin{example}
In addition to weak existential guesses $\GE(i,P)$, gap existential
guesses $\GEG(i,P)$ carry information about all points except the gap $i$.
The guess $\GEG(K\ 2, \lambda x.\ x = 2\ \wedge\ Q(x))$ holds, because $\lambda x.\ (x = 2)\ \wedge\ Q(x)$
does not hold for all values except possibly $2$. Since nothing is known about $Q$, we don't know,
whether $P$ holds for the point $2$. This point is a gap in the argument.
\end{example}

\noindent
Point and gap existential guesses are stronger than existential
guesses, i.\,e.\ $\GEP(i, P)$ and $\GEG(i, P)$ imply $\GE(i, P)$ for
all $i$, $P$. Therefore, they can also be used to instantiate
existential quantifiers.  Moreover, they allow lifting. For example,
the rule $\GEP(i, P_1) \Longrightarrow \GEP(i, \lambda x.\ P_1(x) \vee
P_2(x))$ holds.

\subsection{Guesses for Universal Quantifiers}

Existential and universal quantification are closely related to each
other by negation. In order to lift guesses over negation and also in
order to be able to instantiate universal quantifiers, it makes sense
to define corresponding guesses for universal quantification
exploiting this duality.

\begin{definition}[Universal Guess]
  $i$ is an \emph{universal guess} for $P$ (denoted by $\GU(i, P)$)
  if and only if the equivalence $\forall x.\ P(x) \Longleftrightarrow
  \forall \fv.\ P(i(\fv))$ holds.
\end{definition}

\begin{definition}[Point Universal Guess]
$i$ is a \emph{point universal guess} for $P$ (denoted by $\GUP(i, P)$) if and only if $\forall \fv.\ \neg\ P(i(\fv))$ holds.
\end{definition}

\begin{definition}[Gap Universal Guess]
  $i$ is a \emph{gap universal guess} for $P$ (denoted by $\GUG(i,
  P)$) if and only if $\forall v.\ \big(\big(\forall \fv.\ v \neq
  i(\fv)\big) \Longrightarrow P(v)\big)$ holds.
\end{definition}

Similar to guesses for existential quantification, we are mainly interested in weak universal guesses. Point and gap
universal guesses are stronger than universal ones and allow lifting.


\subsection{Overview}

Above, 6 types of guesses are formally introduced. Informally, they can be described by the following table:
%
\begin{center}
\begin{tabular}{cc@{\quad}|@{\quad}l}
\textbf{$i$ is a $\ldots$ guess for $P$} &  & \textbf{intuition} \\\hline
(weak) existential & ($\GE$) & $\exists x.\ P(x)$ can be safely instantiated with $i$ \\
(weak) universal & ($\GU$) & $\forall x.\ P(x)$ can be safely instantiated with $i$ \\
point existential & ($\GEP$) & $P(i)$ holds \\
point universal & ($\GUP$) & $\neg P(i)$ holds \\
gap existential & ($\GEG$) & all $v$ except possibly $i$ do not satisfy $P$\\
gap universal & ($\GUG$) & all $v$ except possibly $i$ satisfy $P$\\
\end{tabular}
\end{center}
%
This informal description also shows the relative strength of these guesses.
%
\begin{lemma}[Strength of Guesses]\label{lemma_guesses_strength}%
Point and gap guesses are stronger than weak guesses. This means that the following
implications hold for all $i$ and $P$:
\[
\begin{array}{rcl@{\qquad}rcl}
  \GEG(i, P) & \Longrightarrow & \GE(i, P) &
  \GEP(i, P) & \Longrightarrow & \GE(i, P) \\
  \GUG(i, P) & \Longrightarrow & \GU(i, P) &
  \GUP(i, P) & \Longrightarrow & \GU(i, P)
\end{array}
\]
\noindent
Point and gap guesses cannot be compared to each other in general.
\end{lemma}

So, the core of the framework searches for guesses. Once found, the guesses are used as described by the following theorem:

\begin{theorem}[Usage of Guesses]\label{lemma_guesses_usage}
Guesses are used to simplify formulae with quantifiers in various ways. In the most basic case, they can
be used to (partially) instantiate quantifiers as follows:
\[%
\begin{array}[t]{cccrclc}
  \GE(i, P) & \Longrightarrow & \Big( & \exists x.\ P(x) & \Leftrightarrow & \exists \fv.\ P(i(\fv)) & \Big) \\
  \GU(i, P) & \Longrightarrow & \Big( & \forall x.\ P(x) & \Leftrightarrow & \forall \fv.\ P(i(\fv)) & \Big) \\
\end{array}
\]
%
If the guess does not depend on a free variable (as denoted by $K\ i_c$), the quantifier can be removed completely:
\[
\begin{array}[t]{cccrclc}
  \GE(K\ i_c, P) & \Longrightarrow & \Big( & \exists x.\ P(x) & \Leftrightarrow & P(i_c) & \Big) \\
  \GU(K\ i_c, P) & \Longrightarrow & \Big( & \forall x.\ P(x) & \Leftrightarrow & P(i_c) & \Big) \\
\end{array}
\]
Point guesses lead to even more simplification:
\[
\begin{array}[t]{cccrclc}
  \GEP(i, P) & \Longrightarrow & \Big( & \exists x.\ P(x) & \Leftrightarrow & \textit{true} & \Big) \\
  \GUP(i, P) & \Longrightarrow & \Big( & \forall x.\ P(x) & \Leftrightarrow & \textit{false} & \Big) \\
\end{array}
\]
In contrast, the additional strength of gap guesses
is mainly important for lifting. For instantiating quantifiers the same rules as for
existential and universal guesses apply.
However, gap existential guesses are useful for handling unique existential quantification, provided
the guess does not contain free variables.
\[
\begin{array}[t]{cccrclc}
  \GE(K\ i_c, P) & \Longrightarrow & \Big( & \exists! x.\ P(x) & \Leftrightarrow &
    (P(i_c)\ \wedge\ \forall v.\ P(v) \Rightarrow v = i_c) & \Big) \\
  \GEG(K\ i_c, P) & \Longrightarrow & \Big( & \exists! x.\ P(x) & \Leftrightarrow &
    P(i_c) & \Big) \\
  \GEP(K\ i_c, P) & \Longrightarrow & \Big( & \exists! x.\ P(x) & \Leftrightarrow &
    (\forall v.\ P(v) \Rightarrow v = i_c) & \Big)
\end{array}
\]
\end{theorem}


\subsection{Oracle Guesses}

So far, we discussed guesses that carry semantic information and allow
proving equivalences. These are the ones interesting from a theoretical point of view.
For implementing an actual tool, guesses without justification are interesting as well.
The HOL~4 implementation supports also \emph{oracle guesses}.
\begin{definition}[Oracle Guess]
  $i$ is an \emph{oracle guess} for $P$ (denoted by $\GO(i,
  P)$) if the user says so. This means that $\GO(i, P)$ holds for all $i$ and $P$.
\end{definition}
%
An oracle guess carries no semantic information, it just states something
like ``\textit{Trust me! This is a sensible guess!}''. Therefore, oracle
guesses can only be used to prove implications instead of
equivalences.
%
\begin{lemma}[Usage of Oracle Guesses]
\[
\begin{array}[t]{cccrclc}
  \GO(i, P) & \Longrightarrow & \Big( & \exists x.\ P(x) & \Leftarrow & \exists \fv.\ P(i(\fv)) & \Big) \\
  \GO(i, P) & \Longrightarrow & \Big( & \forall x.\ P(x) & \Rightarrow & \forall \fv.\ P(i(\fv)) & \Big)
\end{array}
\]
\end{lemma}
%
Oracle guesses allow the user to instantiate quantifiers without formal justification.
Therefore, they require hardly any theoretical foundation and
are mainly interesting for tool implementation. Therefore, they won't be discussed much below.

\section{Base Guesses}
\label{sec_base_guesses}
After introducing guesses, guess-search can be presented now.
This presentation is twofold. In this section, guesses for basic terms are discussed. Lifting guesses
is presented in the next section.

\subsection{Equations}
The most basic, but also most common source of guesses are equations:

\begin{lemma}[Guesses for Equations with Variables at Top-Level]\label{lemma_guesses_equation_top}
Given an equation $x = t$ such that the variable $x$
does not occur in $t$, the term $t$ is both a point and gap existential guess for
$x$:
\[%
\begin{array}{ccc}
\GEP(K\ t,\ \lambda x.\ (x = t)) & \qquad\qquad & \GEG(K\ t,\ \lambda x.\ (x = t)) \\
\end{array}
\]
\end{lemma}
%
\begin{lemma}[Point Existential Guesses for Equations]\label{lemma_guesses_equation_T}
Given an equation $t_1(x) = t_2(x)$ and a term $i_c$ such that
the formula $t_1(i_c) = t_2(i_c)$ holds, the term $i_c$ is a point existential guess for
$x$. This means that the following holds.
\[
t_1(i_c) = t_2(i_c) \Longrightarrow
\GEP(K\ i_c,\ \lambda x.\ (t_1(x) = t_2(x)))
\]
\end{lemma}
\noindent
Therefore, unification can be used to find point existential guesses for equations.


\subsection{Dichotomies}\label{subsec_base_guesses_dichotomies}
Many datatype definitions provide dichotomy theorems of the form
\[
  \forall x.\ x = c_1\ \vee\ (\exists \fv.\ x = c_2(\fv)) \qquad \text{and} \qquad
  \forall \fv.\ c_1\ \neq c_2(\fv)
\]
The option- and list-datatypes of HOL~4, for example, provide the following theorems:
\[
\begin{array}{ccc}
  \forall x.\ x = \textsf{NONE}\ \vee\ (\exists v.\ x = \textsf{SOME}(v)) & \qquad \qquad &
  \forall v.\ \textsf{NONE} \neq \textsf{SOME}(v) \\

  \forall x.\ x = [\,]\ \vee\ (\exists \textit{hd}, \textit{tl}.\ x = \textit{hd}::\textit{tl}) & &
  \forall \textit{hd}, \textit{tl}.\ [\,] \neq \textit{hd}::\textit{tl}
\end{array}
\]
%
Such theorems can be exploited for creating guesses:
\begin{lemma}[Dichotomy Guesses]\label{lemma_guesses_dichotomy}
\[
\begin{array}{l@{\quad}l@{\quad}l}
(\forall \fv.\ c_1 \neq c_2(\fv)) & \Longrightarrow &
\GUP(\lambda \fv.\ c_2(\fv),\ \lambda x.\ (x = c_1)) \\

(\forall x.\ x = c_1\ \vee\ (\exists \fv.\ x = c_2(\fv))) & \Longrightarrow &
\GUG(\lambda \fv.\ c_2(\fv),\ \lambda x.\ (x = c_1))
\end{array}
\]
\end{lemma}
%
Exploiting dichotomy is very useful in practice. Holfoot uses it to reason about lists.
The variable \textit{pdata'} in the list-reversal example of the introduction can, for example,
be instantiated using the dichotomy of lists. Without this rule, Holfoot's inference rules for
singly-linked list predicates would need to unfold the data-content manually.

Many other datatypes unluckily have more than just two
cases. Currently, general $n$-chotomies cannot be exploited, because
this would require an extension of the guess concept.  However,
monochotomies can be handled.

\subsection{Monochotomies}
Datatypes like pairs and records do not have two cases, but only one. This
structure can be exploited as well. Notice, that for this case, the guess does not depend on the predicate $P$ any
more. It just depends on the type of the variable we try to instantiate.
%
\begin{lemma}[Monochotomy Guesses]\label{lemma_guesses_monochotomy}
\[
\begin{array}{l@{\quad}l@{\quad}l}
(\forall x.\ \exists \fv.\ x = c(\fv))) & \Longrightarrow &
\forall P.\ \GEG(\lambda \fv.\ c(\fv),\ P) \\
(\forall x.\ \exists \fv.\ x = c(\fv))) & \Longrightarrow &
\forall P.\ \GUG(\lambda \fv.\ c(\fv),\ P) \\
\end{array}
\]
\end{lemma}

\subsection{Other guesses}
The base guesses presented above are at the most important ones. However, other
trivial base guesses are exploited as well for the implementation.
The most important ones are point guesses that can be derived
from some context information:
%
\begin{lemma}[Context Guesses]\label{lemma_guesses_context}
\[
\begin{array}{l@{\quad\quad}l}
P(c) \Longrightarrow \GEP(K\ c,\ \lambda x.\ P(x))  \\
\neg P(c) \Longrightarrow \GUP(K\ c,\ \lambda x.\ P(x))
\end{array}
\]
\end{lemma}
%
\noindent
Moreover, generating guesses on the fly for constants is important to
implement lifting efficiently:
%
\begin{lemma}[Guesses for Constants]\label{lemma_guesses_const}
Given a term $c$ such that a variable $x$ does not occur in $c$, any term $i$ is a
valid existential and universal guess:
\[
\begin{array}{l@{\quad\quad}l}
\GE(i,\ \lambda x.\ c) & \GU(i,\ \lambda x.\ c)
\end{array}
\]
\end{lemma}


\section{Lifting Guesses}\label{sec_lifting_guesses}

In Sec.~\ref{sec_base_guesses} the base cases of the search for guesses have been presented.
It remains to discuss, how guesses are lifted over common operators.

\subsection{Negation}
Guesses are defined with negation in mind. Therefore, it is straightforward to lift
guesses over negation:
%
\begin{lemma}[Lifting Guesses over Negation]\label{lemma_guesses_lift_neg}
\[
\begin{array}{lll@{\quad}lll}
\GEP(i,\ \lambda x.\ P(x)) & \Rightarrow & \GUP(i,\ \lambda x.\ \neg P(x)) &
\GUP(i,\ \lambda x.\ P(x)) & \Rightarrow & \GEP(i,\ \lambda x.\ \neg P(x)) \\
\GE(i,\ \lambda x.\ P(x)) & \Rightarrow & \GU(i,\ \lambda x.\ \neg P(x)) &
\GU(i,\ \lambda x.\ P(x)) & \Rightarrow & \GE(i,\ \lambda x.\ \neg P(x)) \\
\GEG(i,\ \lambda x.\ P(x)) & \Rightarrow & \GUG(i,\ \lambda x.\ \neg P(x)) &
\GUG(i,\ \lambda x.\ P(x)) & \Rightarrow & \GEG(i,\ \lambda x.\ \neg P(x))
\end{array}
\]
\end{lemma}

\subsection{Disjunction}

Lifting guesses over a disjunction $P_1(x) \vee P_2(x)$ is a bit more
complicated. Point existential guesses are straightforward to lift. If we
have a point existential guess for either $P_1$ or $P_2$, it is also one for
the disjunction:
%
\begin{lemma}[Lifting Point Existential Guesses over Disjunction]\label{lemma_guesses_lift_disj_T}
\[
\begin{array}{l@{\quad}l@{\quad}l}
\GEP(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \vee P_2(x)) \\
\GEP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \vee P_2(x))
\end{array}
\]
\end{lemma}
%
In contrast, point universal guesses have to hold for both disjuncts:
\begin{lemma}[Lifting Point Universal Guesses over Disjunction]\label{lemma_guesses_lift_disj_F}
\[
\begin{array}{l@{\quad}l@{\quad}l}
\GUP(i,\ \lambda x.\ P_1(x)) \wedge \GUP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1(x) \vee P_2(x))
\end{array}
\]
\end{lemma}
%
For gap guesses, it is the other way round:
%
\begin{lemma}[Lifting Gap Existential Guesses over Disjunction]\label{lemma_guesses_lift_disj_SE}
\[
\begin{array}{l@{\quad}l@{\quad}l}
\GEG(i,\ \lambda x.\ P_1(x)) \wedge \GEG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1(x) \vee P_2(x))
\end{array}
\]
\end{lemma}
%
\begin{lemma}[Lifting Gap Universal Guesses over Disjunction]\label{lemma_guesses_lift_disj_SA}
\[
\begin{array}{l@{\quad}l@{\quad}l}
\GUG(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \vee P_2(x)) \\
\GUG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \vee P_2(x))
\end{array}
\]
\end{lemma}

For weak existential guesses, existential guesses for both subterms are needed. However,
Lemma~\ref{lemma_guesses_const} leads to a nice rule, provided the
variable does not occur in one of the operands.

\begin{lemma}[Lifting Existential Guesses over Disjunction]\label{lemma_guesses_lift_disj_E}
\[
\begin{array}{c@{\quad}c@{\quad}l}
\GE(i,\ \lambda x.\ P_1(x)) \wedge \GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \vee P_2(x)) \\
\GE(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \vee p_2) \\
\GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ p_1 \vee P_2(x))
\end{array}
\]
\end{lemma}

For universal guesses it is even more complicated, because the handling of free variables does not fit well.
The guess is not allowed to depend on any free variable (denoted by $K\ i_c$).
\begin{lemma}[Lifting Universal Guesses over Disjunction]\label{lemma_guesses_lift_disj_A}
\[
\begin{array}{c@{\quad}c@{\quad}l}
\begin{array}{cl}
\GU(K\ i_c,\ \lambda x.\ P_1(x)) & \wedge \\
\GU(K\ i_c,\ \lambda x.\ P_2(x))
\end{array} & \Longrightarrow & \GU(K\ i_c,\ \lambda x.\ P_1(x) \vee P_2(x)) \\[1em]
\GU(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ P_1(x) \vee p_2) \\
\GU(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ p_1 \vee P_2(x))
\end{array}
\]
\end{lemma}

So, for the strong types of guesses, one of the dual guesses behaves
nicely.  In contrast, none of the weak guesses does. As motivated
above, this is the main reason for introducing the stronger types of
guesses.


\subsection{Other Boolean Operations}

We have seen above how to handle negation and disjunction. Other Boolean operations can be expressed in terms of these.
Therefore, the above lemmata can also be used to lift guesses over other Boolean operations. However, for efficiency
reasons the implementation in HOL~4 uses special, derived rules. Here, some of these rules are listed without further explanation:

\begin{lemma}[Lifting Guesses over Conjunction]\label{lemma_guesses_lift_conj}
\[
\begin{array}{c@{\quad}c@{\quad}l}
\GEP(i,\ \lambda x.\ P_1(x)) \wedge \GEP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\
\GUP(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\
\GUP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\
\GEG(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\
\GEG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\
\GUG(i,\ \lambda x.\ P_1(x)) \wedge \GUG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\

\GE(K\ i_c,\ \lambda x.\ P_1(x)) \wedge \GE(K\ i_c,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(K\ i_c,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\
\GE(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \wedge p_2) \\
\GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ p_1 \wedge P_2(x)) \\

\GU(i,\ \lambda x.\ P_1(x)) \wedge \GU(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ P_1(x) \wedge P_2(x)) \\
\GU(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ P_1(x) \wedge p_2) \\
\GU(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ p_1 \wedge P_2(x))
\end{array}
\]
\end{lemma}

\begin{lemma}[Lifting Guesses over Implication]\label{lemma_guesses_lift_imp}
\[
\begin{array}{c@{\quad}c@{\quad}l}
\GEP(i,\ \lambda x.\ P_1(x)) \wedge \GUP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\
\GUP(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\
\GEP(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\

\GEG(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\
\GUG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\
\GUG(i,\ \lambda x.\ P_1(x)) \wedge \GEG(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\

\GU(i,\ \lambda x.\ P_1(x)) \wedge \GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\
\GU(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ P_1(x) \Rightarrow p_2) \\
\GE(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GE(i,\ \lambda x.\ p_1 \Rightarrow P_2(x)) \\

\GE(K\ i_c,\ \lambda x.\ P_1(x)) \wedge \GU(K\ i_c,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(K\ i_c,\ \lambda x.\ P_1(x) \Rightarrow P_2(x)) \\
\GE(i,\ \lambda x.\ P_1(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ P_1(x) \Rightarrow p_2) \\
\GU(i,\ \lambda x.\ P_2(x)) & \Longrightarrow & \GU(i,\ \lambda x.\ p_1 \Rightarrow P_2(x)) \\
\end{array}
\]
\end{lemma}


\subsection{Quantifiers}

It remains to lift guesses over quantifiers. Let's first consider universal quantification.
If the guess does depend on the quantified variables, it becomes a free variable of the guess:

\begin{lemma}[Lifting Guesses over Universal Quantification (1)]\label{lemma_guesses_lift_forall_1}
\[
\begin{array}{c}
(\forall y.\ \GEP(\lambda \fv.\ i(\fv, y),\ \lambda x.\ P(x, y)) \Longrightarrow \\
\GEP(\lambda \fv'.\ i(\textsf{FST}(\fv'), \textsf{SND}(\fv')),\ \lambda x.\ \forall y.\ P(x, y)) \\[1em]

(\forall y.\ \GU(\lambda \fv.\ i(\fv, y),\ \lambda x.\ P(x, y)) \Longrightarrow \\
\GU(\lambda \fv'.\ i(\textsf{FST}(\fv'), \textsf{SND}(\fv')),\ \lambda x.\ \forall y.\ P(x, y)) \\[1em]

(\forall y.\ \GUG(\lambda \fv.\ i(\fv, y),\ \lambda x.\ P(x, y)) \Longrightarrow \\
\GUG(\lambda \fv'.\ i(\textsf{FST}(\fv'), \textsf{SND}(\fv')),\ \lambda x.\ \forall y.\ P(x, y)) \\[1em]

(\forall y.\ \GEG(\lambda \fv.\ i(\fv, y),\ \lambda x.\ P(x, y)) \Longrightarrow \\
\GEG(\lambda \fv'.\ i(\textsf{FST}(\fv'), \textsf{SND}(\fv')),\ \lambda x.\ \forall y.\ P(x, y)) \\
\end{array}
\]
\end{lemma}
%
Notice however, that weak existential and point universal guesses can't be lifted that way. If a guess does not depend on the quantified variable,
it is possible, though:

\begin{lemma}[Lifting Guesses over Universal Quantification (2)]\label{lemma_guesses_lift_forall_2}
\[
\begin{array}{c@{\quad}c@{\quad}l}
(\forall y.\ \GEP(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GEP(i,\ \lambda x.\ \forall y.\ P(x, y)) \\
(\forall y.\ \GE(K\ i_c,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GE(K\ i_c,\ \lambda x.\ \forall y.\ P(x, y)) \\
(\forall y.\ \GEG(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GEG(i,\ \lambda x.\ \forall y.\ P(x, y)) \\
(\forall y.\ \GUP(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GUP(i,\ \lambda x.\ \forall y.\ P(x, y)) \\
(\forall y.\ \GU(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GU(i,\ \lambda x.\ \forall y.\ P(x, y)) \\
(\forall y.\ \GUG(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GUG(i,\ \lambda x.\ \forall y.\ P(x, y))
\end{array}
\]
\end{lemma}

Rules for lifting guesses over existential quantification are dual. However, unique existential quantification needs a bit
of attention:

\begin{lemma}[Lifting Guesses over Unique Existential Quantification]
\[
\begin{array}{c@{\quad}c@{\quad}l}
(\forall y.\ \GUP(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GUP(i,\ \lambda x.\ \exists! y.\ P(x, y)) \\
(\forall y.\ \GEG(i,\ \lambda x.\ P(x, y)) & \Longrightarrow & \GEG(i,\ \lambda x.\ \exists! y.\ P(x, y))
\end{array}
\]
\end{lemma}


\section{Related Techniques}\label{sec_other_techniques}

Above base guesses and lifting of guesses have been presented. This section now
briefly discusses other techniques that enhance guess search:

\subsection{Rewrites}\label{subsec_other_techniques_rewrites}

A very powerful, yet simple technique for teaching the guess search
about new constructs are rewrite rules. For example, the rules above
cannot generate guesses for the predicate $\textsf{IS\_SOME}$. By
rewriting $\textsf{IS\_SOME}(x)$ to $\exists x'.\ x =
\textsf{SOME}(x')$, however, the rules for equations and
quantification as well as the dichotomy rule for option types can be
used.

The HOL~4 implementation uses rewrites to add support for predicates
like $\textsf{IS\_SOME}$ or $\textsf{NULL}$ on lists. However, adding
rules like $\textsf{append}(l_1, l_2) = [\,] \Longleftrightarrow (l_1 =
[\,]\ \wedge\ l_2 = [\,])$ for list-append turned out to be beneficial
in practice as well.

\subsection{Strengthening and Weakening}\label{subsec_other_techniques_imp}

Rewrite rules are very useful. However, sometimes only implications instead of
equivalences are available. These can be exploited as well:

\begin{lemma}[Strengthening / Weakening Guesses]\label{lemma_guesses_strengthen_weaken}
\[
\left(\forall x.\ P_1(x) \Rightarrow P_2(x)\right) \Longrightarrow
\left(\begin{array}{@{}rcl}
\forall x.\ \GEP(i, P_1) & \Longrightarrow & \GEP(i,\ \lambda x.\ P_2) \qquad \wedge\\
\forall x.\ \GUG(i, P_1) & \Longrightarrow & \GUG(i,\ \lambda x.\ P_2) \qquad \wedge\\
\forall x.\ \GUP(i, P_2) & \Longrightarrow & \GUP(i,\ \lambda x.\ P_1) \qquad \wedge\\
\forall x.\ \GEG(i, P_2) & \Longrightarrow & \GEG(i,\ \lambda x.\ P_1)
\end{array}
\right)
\]
\end{lemma}


\subsection{Minimising Variable Occurrences}\label{subsec_varmin}

As for example Lemma~\ref{lemma_guesses_lift_disj_E} illustrates, it
is easier to find guesses for a variable if it occurs in fewer
positions. Therefore, the HOL~4 implementation preprocesses the term and tries to
minimise the number of occurrences. For example,
$\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f (x + 2))$ is
rewritten to $\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f (8 +
2))$ by this prepossessing step. This explains, why this example
can be handled, whereas apparently similar ones cannot (see Table~\ref{table_examples}).
The implementation for minimising variable occurrences is based
on simple rules like $(x = t) \wedge P(x)
\ \Longleftrightarrow\ (x = t) \wedge P(t)$ or $x \neq t \vee P(x)
\ \Longleftrightarrow\ x \neq t \vee P(t)$.


\section{Examples}\label{sec_examples}

In the last few sections, the method for searching guesses has been presented on an abstract level.
Let's now consider a few examples to see how this methods works in practice.

\subsection{Example 1}
Let's start with the example
$\exists x.\ (\forall y.\ Q(y)\ \wedge\ (x=7)) \
\wedge\ P(x)$. This example cannot be handled by
existing tools. However, the lemmata presented above allow to
derive a guess for this example:
%
\[\begin{array}{cc@{\qquad}l}
\GEG(K\ 7, \lambda x.\ x = 7) & \text{(1)} & \text{from Lemma~\ref{lemma_guesses_equation_top}} \\
\GEG(K\ 7, \lambda x.\ Q(y)\ \wedge\ (x=7)) & \text{(2)} & \text{from (1) and Lemma~\ref{lemma_guesses_lift_conj}} \\
\GEG(K\ 7, \lambda x.\ \forall y.\ Q(y)\ \wedge\ (x=7)) & \text{(3)} & \text{from (2) and Lemma~\ref{lemma_guesses_lift_forall_2}} \\
\GEG(K\ 7, \lambda x.\ (\forall y.\ Q(y)\ \wedge\ (x=7)) \wedge P(x)) & \text{(4)} & \text{from (3) and Lemma~\ref{lemma_guesses_lift_conj}}
\end{array}
\]
%
With Lemma~\ref{lemma_guesses_usage} we can therefore simplify
$\exists x.\ (\forall y.\ Q(y)\ \wedge\ (x=7)) \ \wedge\ P(x)$ to
$(\forall y.\ Q(y)\ \wedge\ (7=7)) \ \wedge\ P(7)$ and with some general infrastructure further to
$(\forall y.\ Q(y)) \ \wedge\ P(7)$.
Here, only the trace that succeeds is presented. The search actually produces more guesses.
For example, $\GEP(K\ 7, \lambda x.\ x = 7)$ is derived as well, but then fails to be lifted over
the conjunction.

\subsection{Example 2}\label{subsec_Example_2}
The example $\forall x.\ \textsf{IS\_NONE}(x) \vee P(x)$ illustrates partial instantiations for datatypes.
\[\begin{array}{cc@{\qquad}l}
\GUG(\lambda x'.\ \textsf{SOME}(x'), \lambda x.\ x = \textsf{NONE}) & \text{(1)} & \text{from Lemma~\ref{lemma_guesses_dichotomy}} \\
\GUG(\lambda x'.\ \textsf{SOME}(x'), \lambda x.\ \textsf{IS\_NONE}(x)) & \text{(2)} & \text{rewrite of (1)} \\
\GUG(\lambda x'.\ \textsf{SOME}(x'), \lambda x.\ \textsf{IS\_NONE}(x) \vee P(x)) & \text{(3)} & \text{from (2) and Lemma~\ref{lemma_guesses_lift_disj_SA}}
\end{array}
\]
Therefore,
$\forall x.\ \textsf{IS\_NONE}(x) \vee P(x)$ can be simplified to
$\forall x'.\ P(\textsf{SOME}(x'))$.

\subsection{Example 3}
Let's consider $\exists x.\ (f (8 + 2) = f (x + 2)) \wedge P (f (x + 2))$. The guess
\[\begin{array}{cc@{\quad}l}
\GEP(K\ 8, \lambda x.\ f (8 + 2) = f (x + 2)) & \text{(1)} & \text{from Lemma~\ref{lemma_guesses_equation_T}} \\
\end{array}
\]
can be easily derived. However, then we are stuck, because we cannot derive a point existential guess for the conjunct $P (f (x + 2))$.
So, we weaken the guess:
\[\begin{array}{cc@{\quad}l}
\GE(K\ 8, \lambda x.\ f (8 + 2) = f (x + 2)) & \text{(2)} & \text{from (1) and Lemma~\ref{lemma_guesses_strength}} \\
\end{array}
\]
Unluckily, we are still stuck, because $P (f (x + 2))$ depends on $x$. However, our tool can rewrite the overall term
such that this dependence disappears (see Sec.~\ref{subsec_varmin}).
\[\begin{array}{cc@{\quad}l}
\GE(K\ 8, \lambda x.\ (f (8 + 2) = f (x + 2)) \wedge P(f(8 + 2))) & \text{(3)} & \text{from (2), Lemma~\ref{lemma_guesses_lift_conj},
\ref{lemma_guesses_lift_neg}} \\
\GE(K\ 8, \lambda x.\ (f (8 + 2) = f (x + 2)) \wedge P(f(x + 2))) & \text{(4)} & \text{from (3) and rewrite}
\end{array}
\]
Thus, we found a guess and can instantiate the quantifier with 8.

\subsection{Example 4}
Finally, consider $\big((\forall x.\ P_1(x) \Rightarrow P_2(x)) \wedge P_1(2)\big) \Longrightarrow \exists x.\ P_2(x)$.
First, HOL~4's general infrastructure processes this and allows us to concentrate on
$\exists x.\ P_2(x)$, while using (1) $\forall x.\ P_1(x) \Rightarrow P_2(x)$ and (2)~$P_1(2)$ as lemmata.
Then guesses can be derived as follows:
\[\begin{array}{cc@{\qquad}l}
\GEP(K\ 2, \lambda x.\ P_1(x)) & \text{(3)} & \text{from (2), Lemma~\ref{lemma_guesses_context}} \\
\GEP(K\ 2, \lambda x.\ P_2(x)) & \text{(4)} & \text{from (1), (3), Lemma~\ref{lemma_guesses_strengthen_weaken}}
\end{array}
\]
Thus, we found a guess and can simplify the original goal first to
$\big((\forall x.\ P_1(x) \Rightarrow P_2(x)) \wedge P_1(2)\big) \Longrightarrow \textit{true}$ and then further to
\textit{true}.


\chapter{HOL~4 implementation}

\section{User Interface}\label{sec_interface}

The quantifier heuristics library can be found in the sub-directory
\texttt{src/quantHeuristics}.  The entry point to the framework is the
library \texttt{quantHeuristicsLib}.

\subsection{Conversions}
Usually the library is used for
converting a term containing quantifiers to an equivalent one. For this,
the following high level entry points exists:
\bigskip

\noindent
\begin{tabular}{@{}ll}
\texttt{QUANT\_INSTANTIATE\_CONV} & \texttt{: quant\_param list -> conv} \\
\texttt{QUANT\_INST\_ss} & \texttt{: quant\_param list -> ssfrag} \\
\texttt{QUANT\_INSTANTIATE\_TAC} & \texttt{: quant\_param list -> tactic} \\
\texttt{ASM\_QUANT\_INSTANTIATE\_TAC} & \texttt{: quant\_param list -> tactic}
\end{tabular}
\bigskip

All these functions get a list of \emph{quantifier heuristic parameters} as arguments. These
parameters essentially configure, which heuristics are used during the guess-search. If
an empty list is provided, the tools know about the standard Boolean combinators and equations.
\texttt{std\_qp} adds support for context and common datatypes like pairs or lists.
Quantifier heuristic parameters are explained in more detail in
Section~\ref{sec_qps}.

So, some simple usage of the quantifier heuristic library looks like:
{\scriptsize
\begin{verbatim}
> QUANT_INSTANTIATE_CONV [] ``?x. (!z. Q z /\ (x=7)) /\ P x``;
val it = |- (?x. (!z. Q z /\ (x = 7)) /\ P x) <=> (!z. Q z) /\ P 7: thm

> QUANT_INSTANTIATE_CONV [std_qp] ``!x. IS_SOME x ==> P x``
val it = |- (!x. IS_SOME x ==> P x) <=> !x_x'. P (SOME x_x'): thm
\end{verbatim}}

Usually, the quantifier heuristics library is used together with the
simplifier using \texttt{QUANT\_INST\_ss}. Besides interleaving
simplification and quantifier instantiation, this has the benefit of
being able to use context information collected by the simplifier:

{\scriptsize
\begin{verbatim}
> QUANT_INSTANTIATE_CONV [] ``P m ==> ?n. P n``
Exception- UNCHANGED raised

> SIMP_CONV (bool_ss ++ QUANT_INST_ss []) [] ``P m ==> ?n. P n``
val it = |- P m ==> (?n. P n) <=> T: thm
\end{verbatim}}

It's usually best to use \texttt{QUANT\_INST\_ss}
together with e.\,g.\ \texttt{SIMP\_TAC} when using the library with tactics.
However, if free variables of the goal should be instantiated, then
\texttt{ASM\_QUANT\_INSTANTIATE\_TAC} should be used:

{\scriptsize
\begin{verbatim}
P x
------------------------------------
  IS_SOME x
  : proof

> e (ASM\_QUANT_INSTANTIATE_TAC [std_qp])
P (SOME x_x') : proof
\end{verbatim}}

There is also \texttt{QUANT\_INSTANTIATE\_TAC} as a shortcut
for using \texttt{QUANT\_INSTANTIATE\_CONV} as a tactic. It does not
instantiate free variables or considers the assumptions.


\subsection{Unjustified Guesses}

Most heuristics justify the guesses they produce and therefore allow to
prove equivalences.
However, the implementation also supports unjustified guesses, which may be bogus.
Let's consider the example $\exists x.\ P(x) \Longrightarrow (x = 2)\ \wedge\ Q(x)$.
Because nothing is known about $P$ and $Q$, we can't find a safe instantiation for $x$ here.
However, $2$ looks tempting and is probably sensible in many situations. (Counterexample:
$P(2)$, $\neg Q(2)$ and $\neg P(3)$ hold)

\texttt{implication\_concl\_qp} is a quantifier parameter that looks for valid guesses in the conclusion of an implication.
Then, it assumes without justification that these guesses are probably sensible for the whole implication as well.
Because these guesses might be wrong, one can either use implications or
expansion theorems like $\exists x. P(x)\ \Leftrightarrow (\forall x.\ (x \neq c) \Rightarrow \neg P(x)) \Rightarrow P(c)$.

{\scriptsize
\begin{verbatim}
> QUANT_INSTANTIATE_CONV [implication_concl_qp] ``?x. P x ==> (x = 2) /\ Q x``
Exception- UNCHANGED raised

> QUANT_INSTANTIATE_CONSEQ_CONV [implication_concl_qp] CONSEQ_CONV_STRENGTHEN_direction
     ``?x. P x ==> (x = 2) /\ Q x``
val it =
   |- (P 2 ==> Q 2) ==> ?x. P x ==> (x = 2) /\ Q x: thm

> EXPAND_QUANT_INSTANTIATE_CONV [implication_concl_qp] ``?x. P x ==> (x = 2) /\ Q x``
val it = |- (?x. P x ==> (x = 2) /\ Q x) <=>
            (!x. x <> 2 ==> ~(P x ==> (x = 2) /\ Q 2)) ==> P 2 ==> Q 2: thm

> SIMP_CONV (std_ss++EXPAND_QUANT_INST_ss [implication_concl_qp]) [] ``?x. P x ==> (x = 2) /\ Q x``
val it =
   |- (?x. P x ==> (x = 2) /\ Q x) <=> (!x. x <> 2 ==> P x) ==> P 2 ==> Q 2: thm
\end{verbatim}}


The following entry points should be used to exploit unjustified guesses:
\bigskip

\noindent
\begin{tabular}{@{}ll}
\texttt{QUANT\_INSTANTIATE\_CONSEQ\_CONV} & \texttt{: quant\_param list -> directed\_conseq\_conv} \\
\texttt{EXPAND\_QUANT\_INSTANTIATE\_CONV} & \texttt{: quant\_param list -> conv} \\
\texttt{EXPAND\_QUANT\_INST\_ss} & \texttt{: quant\_param list -> ssfrag} \\
\texttt{QUANT\_INSTANTIATE\_CONSEQ\_TAC} & \texttt{: quant\_param list -> tactic}
\end{tabular}

\subsection{Debugging}

To debug the guess-search, it is possible to print tracing information.
This is done by setting the trace \texttt{QUANT\_INSTANTIATE\_HEURISTIC} to 1 or 2. For
the example in Sec.~\ref{subsec_Example_2} the debug output looks like:

{\scriptsize
\begin{verbatim}
val _ = set_trace "QUANT_INSTANTIATE_HEURISTIC" 1
val thm = QUANT_INSTANTIATE_CONV [std_qp] ``!x. IS_NONE x \/ P x``

searching guesses for ``x`` in ``~(IS_NONE x \/ P x)``
  searching guesses for ``x`` in ``IS_NONE x \/ P x``
    searching guesses for ``x`` in ``IS_NONE x``
      searching guesses for ``x`` in ``x = NONE``
      7 guesses found for ``x`` in ``x = NONE``
       - guess_exists_point (``NONE``, [], X)
       - guess_forall_point (``SOME x_x``, [x_x], X)
       - guess_forall (``SOME x_x``, [x_x], X)
       - guess_forall (``SOME x_x'``, [x_x'], X)
       - guess_exists (``NONE``, [], X)
       - guess_forall_gap (``SOME x_x'``, [x_x'], X)
       - guess_exists_gap (``NONE``, [], X)
    7 guesses found for ``x`` in ``IS_NONE x``
     - guess_exists_point (``NONE``, [], X)
     - guess_forall_point (``SOME x_x``, [x_x], X)
     - guess_forall (``SOME x_x``, [x_x], X)
     - guess_forall (``SOME x_x'``, [x_x'], X)
     - guess_exists (``NONE``, [], X)
     - guess_forall_gap (``SOME x_x'``, [x_x'], X)
     - guess_exists_gap (``NONE``, [], X)
    searching guesses for ``x`` in ``P x``
    no guesses found for ``x`` in ``P x``
  4 guesses found for ``x`` in ``IS_NONE x \/ P x``
   - guess_exists_point (``NONE``, [], X)
   - guess_forall (``SOME x_x'``, [x_x'], X)
   - guess_exists (``NONE``, [], X)
   - guess_forall_gap (``SOME x_x'``, [x_x'], X)
4 guesses found for ``x`` in ``~(IS_NONE x \/ P x)``
 - guess_forall_point (``NONE``, [], X)
 - guess_forall (``NONE``, [], X)
 - guess_exists (``SOME x_x'``, [x_x'], X)
 - guess_exists_gap (``SOME x_x'``, [x_x'], X)
searching guesses for ``x_x'`` in ``~P (SOME x_x')``
  searching guesses for ``x_x'`` in ``P (SOME x_x')``
  no guesses found for ``x_x'`` in ``P (SOME x_x')``
no guesses found for ``x_x'`` in ``~P (SOME x_x')``

val thm = |- (!x. IS_NONE x \/ P x) <=> !x_x'. P (SOME x_x'):  thm
\end{verbatim}}


\subsection{Interface Details}

The high level interface is mainly build around
an highly configurable conversion and a corresponding consequence conversion.
\texttt{EXTENSIBLE\_QUANT\_INSTANTIATE\_CONV} gets the following arguments:

\begin{description}
  \item[\texttt{cache\_ref\_opt\ :\ quant\_heuristic\_cache ref option}]
     a cache for guesses. If \texttt{NONE} is passed,
     a new cache is created on the fly. New caches can be created by \texttt{mk\_quant\_heuristic\_cache} and then
     used to cache results through multiple calls.
  \item[\texttt{re\ :\ bool}]  redescent into a term after some instantiation has been found?
     It determines, whether internally \texttt{DEPTH\_CONV} or \texttt{REDEPTH\_CONV} is used.

  \item[\texttt{min\_var\_occs\ :\ bool}]  add a preprocessing step to minimise the number of occurrences of
    a variable (see Sec.\ref{subsec_varmin}). Since this preprocessing might be slow, one might want to skip it.

  \item[\texttt{expand\ :\ bool}]  use expansion to exploit unjustified guesses?

  \item[\texttt{ctx\ :\ thm list}]  a list of theorems that come from the context (e.\,g.\ collected by the simplifier).

  \item[\texttt{base\_arg\ :\ quant\_param}]  a parameter that should always be used. This is by default
   \texttt{basic\_qp}, which can handle the standard Boolean connectives and equations. In special circumstances,
     it might be beneficial to use \texttt{empty\_qp}, though.

  \item[\texttt{args\ :\ quant\_param list}]  list of quantifier heuristic parameters to use.
\end{description}

The consequence conversion
\texttt{EXTENSIBLE\_QUANT\_INSTANTIATE\_CONSEQ\_CONV} gets the same
arguments, except \texttt{expand} and \texttt{ctx}. Since it can use
implications, expansion is not needed. Because
\texttt{DEPTH\_CONSEQ\_CONV} collects its own context and can't easily
be used with the simplifier anyhow, \texttt{ctx} is unnecessary.
\texttt{EXTENSIBLE\_QUANT\_INST\_ss} is a wrapper of the conversion that removes the arguments
\texttt{re} and \texttt{ctx}, because they are taken care of by the simplifier.

All other entry points, including the ones presented above are derived
form the conversion and consequence conversion. By default the argument
\texttt{cache\_ref\_opt} is set to \texttt{NONE}, \texttt{re} is false,
preprocessing turned on, expanding turned off, an empty context is used and
\texttt{basic\_qp} is always present. Versions of the high level entry points
containing \texttt{FAST} in their name, turn preprocessing off; \texttt{EXPAND} means that
expansion is turned on and \texttt{RE} that \texttt{re} is set to true.

\subsection{Explicit Instantiations}

A special (slightly degenerated) use of the framework, is turning guess search off completely and
providing instantiations explicitly. The tactic \texttt{QUANT\_TAC} allows this. This means that
it allows to partially instantiate quantifiers at subpositions
with explicitly given terms. As such, it can be seen as
a generalisation of \texttt{EXISTS\_TAC}.
%
{\scriptsize
\begin{verbatim}
val it = !x. (!z. P x z) ==> ?a b.    Q a        b z : proof

> e( QUANT_INST_TAC [("z", `0`, []), ("a", `SUC a'`, [`a'`])] )

val it = !x. (    P x 0) ==> ?  b a'. Q (SUC a') b z : proof
\end{verbatim}}
%
This tactic is implemented using oracle guesses. It normally
produces implications, which is fine when used as a tactic. There is
also a conversion called \texttt{INST\_QUANT\_CONV} with the same
functionality. For a conversion, implications are
problematic. Therefore, the simplifier and Metis are used to prove
the validity of the explicitly given instantiations. This succeeds
usually only for simple examples.


\subsection{Simple Quantifier Heuristics}\label{subsec_simple}

The full quantifier heuristics described above are powerful and very flexible.
However, they are sometimes slow.
The unwind library\footnote{see \texttt{src/simp/src/Unwind.sml}} on the other hand is limited, but fast.
The simple version of the quantifier heuristics fills the gap in the middle.
They just search for gap guesses without any free variables.
Moreover, slow operations like recombining or automatically looking up datatype information is omitted.
As a result, the conversion \texttt{SIMPLE\_QUANT\_INSTANTIATE\_CONV} (and corresponding \texttt{SIMPLE\_QUANT\_INST\_ss}) is nearly as fast as the corresponding unwind conversions.
However, it supports more complicated syntax. Moreover, there is support for quantifiers, pairs, list and much more.

\section{Quantifier Heuristic Parameters}\label{sec_qps}

Quantifier heuristic parameters play a similar role for the quantifier
instantiation library as simpsets do for the simplifier. They contain
theorems, ML code and general configuration parameters that allow to configure
guess-search. There are predefined parameters that handle
common constructs and the user can define own parameters.

\subsection{Quantifier Heuristic Parameters for Common Datatypes}

There are \texttt{option\_qp}, \texttt{list\_qp}, \texttt{num\_qp} and \texttt{sum\_qp} for option types, lists,
natural numbers and sum types respectively.
Some examples are displayed in the following table:
%
\[\begin{array}{r@{\quad \Longleftrightarrow \quad}l}
\forall x.\ \texttt{IS\_SOME}(x) \Rightarrow P(x) & \forall x'.\ P (\texttt{SOME}(x')) \\
\forall x.\ \texttt{IS\_NONE}(x)& \textit{false} \\
\forall l.\ l \neq [\,] \Rightarrow P(l)& \forall h, l'.\ P(h::l')  \\
\forall x.\ x = c + 3& \textit{false} \\
\forall x.\ x \neq 0 \Rightarrow P(x)& \forall x'.\ P(\texttt{SUC}(x'))
\end{array}\]

\subsection{Quantifier Heuristic Parameters for Tuples}

For tuples the situation is peculiar, because each quantifier over a variable of a product type
can be instantiated. The challenge is to decide which quantifiers should be instantiated and
which new variable names to use for the components of the pair.
There is a quantifier heuristic parameter called \texttt{pair\_default\_qp}. It first looks for
subterms of the form $(\lambda (x_1, \ldots, x_n).\ \ldots)\ x$. If such a term is found, $x$ is instantiated with
$(x_1, \ldots, x_n)$. Otherwise, subterms of the form $\texttt{FST}(x)$ and $\texttt{SND}(x)$ are searched. If such a term
is found, $x$ is instantiated as well. This parameter therefore allows simplifications like:
%
\[\begin{array}{r@{\quad \Longleftrightarrow \quad}l}
\forall p.\ (x = \texttt{SND}(p)) \Rightarrow P(p)& \forall p_1.\ P(p_1, x) \\
\exists p.\ (\lambda (p_a, p_b, p_c). P(p_a, p_b, p_c))\ p & \exists p_a, p_b, p_c.\ P(p_a, p_b, p_c)
\end{array}\]

\texttt{pair\_default\_qp} is implemented in terms of the more general
quantifier heuristic parameter \texttt{pair\_qp}, which allows the
user to provide a list of ML functions. These functions get the
variable and the term. If they return a tuple of variables, these
variables are used for the instantiation, otherwise the next function
in the list is called or - if there is no function left - the variable
is not instantiated. In the example of $\exists p.\ (\lambda (p_a,
p_b, p_c). P(p_a, p_b, p_c))\ p$ these functions are given the
variable $p$ and the term $(\lambda (p_a, p_b, p_c). P(p_a, p_b,
p_c))\ p$ and return $\texttt{SOME} (p_a, p_b, p_c)$.

\subsection{Quantifier Heuristic Parameter for Records}

Records are similar to pairs, because they can always be instantiated. Here, it is interesting that the necessary
monochotomy lemma comes from HOL~4's \texttt{Type\_Base} library. This means that \texttt{record\_qp} is stateful.
If a new record type is defined, the automatically proven monochotomy lemma is then automatically used
by \texttt{record\_qp}. In contrast to the pair parameter, the one for records gets only one function instead of a
list of functions to decide which variables to instantiate. However, this function is simpler, because it just needs
to return true or false. The names of the new variables are constructed from the field-names of the record.
The quantifier heuristic parameter \texttt{default\_record\_qp} expands all records.

\subsection{Stateful Quantifier Heuristic Parameters}

The parameter for records is stateful, as it uses knowledge from
\texttt{Type\_Base}. Such information is not only useful for records
but for general datatypes. The quantifier heuristic parameter
\texttt{TypeBase\_qp} uses automatically proven theorems about new
datatypes to exploit mono- and dichotomies. Moreover, there is also a
stateful \texttt{pure\_stateful\_qp} that allows the user to
explicitly add other parameters to it.  \texttt{stateful\_qp} is a
combination of \texttt{pure\_stateful\_qp} and \texttt{TypeBase\_qp}.

\subsection{Standard Quantifier Heuristic Parameter}

The standard quantifier heuristic parameter \texttt{std\_qp} combines
the parameters for lists, options, natural numbers, the default one
for pairs and the default one for records.


\section{User defined Quantifier Heuristic Parameters}\label{sec_qps_user}

The user is also able to define own parameters. There
is \texttt{empty\_qp}, which does not contain any information. Several
parameters can be combined using the function
\texttt{combine\_qps}. Together with the basic types of user defined
parameters that are explained below, these functions provide an
interface for user defined quantifier heuristic parameters.

\subsection{Rewrites / Conversions}

As discussed in Sec.~\ref{subsec_other_techniques_rewrites}, adding
rewrites is a very powerful technique. \texttt{rewrite\_qp} allows to provide rewrites in the form of rewrite theorems.
For the example of \texttt{IS\_SOME} discussed in Sec.~\label{subsec_other_techniques_rewrites} this
looks like:

{\scriptsize
\begin{verbatim}
> val thm = QUANT_INSTANTIATE_CONV [] ``!x. IS_SOME x ==> P x``
Exception- UNCHANGED raised

> val IS_SOME_EXISTS = prove (``IS_SOME x = (?x'. x = SOME x')``, Cases_on `x` THEN SIMP_TAC std_ss []);
val IS_SOME_EXISTS = |- IS_SOME x <=> ?x'. x = SOME x': thm

> val thm = QUANT_INSTANTIATE_CONV [rewrite_qp[IS_SOME_EXISTS]] ``!x. IS_SOME x ==> P x``
val thm = |- (!x. IS_SOME x ==> P x) <=> !x'. IS_SOME (SOME x') ==> P (SOME x'): thm
\end{verbatim}}

To clean up the result after instantiation, theorems used to rewrite the result after instantiation can be provided via
\texttt{final\_rewrite\_qp}.

{\scriptsize
\begin{verbatim}
> val thm = QUANT_INSTANTIATE_CONV [rewrite_qp[IS_SOME_EXISTS], final_rewrite_qp[option_CLAUSES]]
    ``!x. IS_SOME x ==> P x``
val thm = |- (!x. IS_SOME x ==> P x) <=> !x'. P (SOME x'): thm
\end{verbatim}}

If rewrites are not enough, \texttt{conv\_qp} can be used to add conversions:

{\scriptsize
\begin{verbatim}
> val thm = QUANT_INSTANTIATE_CONV [] ``?x. (\y. y = 2) x``
Exception- UNCHANGED raised

> val thm = QUANT_INSTANTIATE_CONV [convs_qp[BETA_CONV]] ``?x. (\y. y = 2) x``
val thm = |- (?x. (\y. y = 2) x) <=> T: thm
\end{verbatim}}

\subsection{Strengthening / Weakening}

In rare cases, equivalences that can be used for rewrites are unavailable. There might be just implications that
can be used for strengthening or weakening (see Sec.~\ref{subsec_other_techniques_imp}). The function
\texttt{imp\_qp} might be used to provide such implication.

{\scriptsize
\begin{verbatim}
> val thm = QUANT_INSTANTIATE_CONV [list_qp] ``!l. 0 < LENGTH l ==> P l``
Exception- UNCHANGED raised

> val LENGTH_LESS_IMP = prove (``!l n. n < LENGTH l ==> l <> []``, Cases_on `l` THEN SIMP_TAC list_ss []);
val LENGTH_LESS_IMP = |- !l n. n < LENGTH l ==> l <> []: thm

> val thm = QUANT_INSTANTIATE_CONV [imp_qp[LENGTH_LESS_IMP], list_qp] ``!l. 0 < LENGTH l ==> P l``
val thm =
   |- (!l. 0 < LENGTH l ==> P l) <=>
      !l_t l_h. 0 < LENGTH (l_h::l_t) ==> P (l_h::l_t): thm

> val thm = SIMP_CONV (list_ss ++ QUANT_INST_ss [imp_qp[LENGTH_LESS_IMP], list_qp]) []
              ``!l. SUC (SUC n) < LENGTH l ==> P l``
val thm =
   |- (!l. SUC (SUC n) < LENGTH l ==> P l) <=>
      !l_h l_t_h l_t_t_t l_t_t_h. n < SUC (LENGTH l_t_t_t) ==> P (l_h::l_t_h::l_t_t_h::l_t_t_t): thm
\end{verbatim}}


\subsection{Filtering}
Sometimes, one might want to avoid to instantiate certain quantifiers.
The function \texttt{filter\_qp} allows to add ML-functions that filter the handled
quantifiers. These functions are given a variable $x$ and a term $P(x)$.
The tool only tries to find instantiate $x$ in $P(x)$, if all filter functions
return \textit{true}.

{\scriptsize
\begin{verbatim}
> val thm = QUANT_INSTANTIATE_CONV [] ``?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x, y, z)``
val thm = |- (?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x,y,z)) <=> P (1,2,3): thm

> val thm = QUANT_INSTANTIATE_CONV [filter_qp [fn v => fn t => (v = ``y:num``)]]
   ``?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x, y, z)``
val thm = |- (?x y z. (x = 1) /\ (y = 2) /\ (z = 3) /\ P (x,y,z)) <=>
              ?x   z. (x = 1) /\            (z = 3) /\ P (x,2,z): thm
\end{verbatim}}

\subsection{Satisfying and Contradicting Instantiations}

As the satisfy library\footnote{see \texttt{src/simp/src/Satisfy.sml}} demonstrates, it is often
useful to use unification and explicitly given theorems to
find instantiations. In addition to satisfying instantiations, the quantifier heuristics framework
is also able to use contradicting ones. The theorems used for finding instantiations usually come from
the context. However, \texttt{instantiation\_qp} allows to add additional ones:

{\scriptsize
\begin{verbatim}
> val thm = SIMP_CONV (std_ss++QUANT_INST_ss[]) [] ``P n ==> ?m:num. n <= m /\ P m``
Exception- UNCHANGED raised

> val thm = SIMP_CONV (std_ss++QUANT_INST_ss[instantiation_qp[arithmeticTheory.LESS_EQ_REFL]]) []
               ``P n ==> ?m:num. n <= m /\ P m``
> val thm =
   |- P n ==> ?m:num. n <= m /\ P m = T : thm
\end{verbatim}}

\subsection{Di- and Monochotomies}

As discussed in Sec.~\ref{subsec_base_guesses_dichotomies}, dichotomies can be exploited for guess search.
\texttt{distinct\_qp} provides an interface to add theorems
of the form $\forall x.\ c_1(x) \neq c_2(x)$.
\texttt{cases\_qp} expects theorems of the form
$\forall x. \ (x = \exists \fv. c_1(\fv))\ \vee \ldots \vee (x = \exists \fv. c_n(\fv))$.
These theorems are for $n = 2$ used with Lemma~\ref{lemma_guesses_dichotomy} and
for $n=1$ with Lemma~\ref{lemma_guesses_monochotomy}. All other cases are currently ignored.

\subsection{Lifting Theorems}

In Section~\ref{sec_lifting_guesses} theorems have been presented that
allow lifting guesses. The function \texttt{inference\_qp} enables the
user to provide it's own lifting inference rules. Those rules have to
be theorems of the form $G_1 \wedge \ldots \wedge G_n \Longrightarrow
G$, where all $G_i$ are guesses that might be universally quantified
and $G$ is a guess. Examples for such inference rules can be found in
Section~\ref{sec_lifting_guesses}. Usually, inferences look like
Lemma~\ref{lemma_guesses_lift_conj}. However, also rules like
Lemma~\ref{lemma_guesses_lift_forall_1} or
\ref{lemma_guesses_lift_forall_2} are supported.

\begin{example}
When trying to add support for the Boolean operation of equivalence,
there are two choices.  One can use rewriting and replace every
occurrence of $P_1 \Leftrightarrow P_2$ with for example $(P_1 \wedge
P_2) \vee (\neg P_1 \wedge \neg P_2)$. However, this may lead to an
exponential blowup of the size of the original term, since both $P_1$
and $P_2$ occur twice in the result. Therefore, it is more efficient to
provide a new lifting inference for equivalences. Such a rule can easily be derived
using the existing rules for basic Boolean operations.
\end{example}

\subsection{Oracle Guesses}

Sometimes, the user does not want to justify guesses. The tactic
\texttt{QUANT\_TAC} is implemented using oracle guesses for example.
A simple interface to oracle guesses is provided by \texttt{oracle\_qp}.
It expects a ML function that given a variable and a term returns
an pair of an instantiation and the free variables in this instantiation.

As an example, lets define a parameter that states that every list is non-empty:
{\scriptsize
\begin{verbatim}
val dummy_list_qp = oracle_qp (fn v => fn t =>
  let
     val (v_name, v_list_ty) = dest_var v;
     val v_ty = listSyntax.dest_list_type v_list_ty;

     val x = mk_var (v_name ^ "_hd", v_ty);
     val xs = mk_var (v_name ^ "_tl", v_list_ty);
     val x_xs = listSyntax.mk_cons (x, xs)
  in
     SOME (x_xs, [x, xs])
  end)
\end{verbatim}}

\noindent
Notice, that an option type is returned and that the function is
allowed to throw \texttt{HOL\_ERR} exceptions.
With this definition, the call
\begin{verbatim}
NORE_QUANT_INSTANTIATE_CONSEQ_CONV [dummy_list_qp]
   CONSEQ_CONV_STRENGTHEN_direction ``?x:'a list y:'b. P (x, y)``
\end{verbatim}
results in
\verb+(?y x_hd x_tl. P (x_hd::x_tl,y)) ==> ?x y. P (x,y) : thm+.

\subsection{User defined Quantifier Heuristics}\label{subsec_user_defined_quantheu}

At the lowest level, our tool searches guesses using ML-functions
called \emph{quantifier heuristics}. Slightly simplified, such a
quantifier heuristic gets a variable and a term and returns a set of
guesses for this variable and term. Heuristics allow full
flexibility. However, to write your own heuristics a lot of knowledge
about the ML-datastructures and auxiliary functions is
required. Therefore, no details are discussed here. Please have a look
at the source code and contact Thomas Tuerk
(\url{tt291@cl.cam.ac.uk}), if you have questions.
\texttt{heuristics\_qp} and \texttt{top\_heuristics\_qp} provide
interfaces to add user defined heuristics to a quantifier heuristics
parameter.

\chapter{Conclusion}\label{sec_conclusion}

The quantifier heuristic is a powerful tool to instantiate quantifiers.
It subsumes the power of the existing unwind and satisfy libraries. More importantly though,
it is very flexible and easily extendable by the user. Moreover,
it can be used to instantiate quantifiers using unjustified guesses.

\bibliographystyle{plain}
\bibliography{paper}

\end{document}