res_quan/Manual/description.tex

% Document Type: LaTeX

\chapter{The \resquan\ Library}

The \resquan\ library provides some basic facilities for working with
restricted quantifications. It consists of a single theory \verb|res_quan.th|,
which contains a number of theorems about the properties of some
restricted quantifiers, and a set of ML functions for dealing with
these quantifiers. It also contains some conditional
rewriting tools which can be loaded as a separate library part.

The description in this chapter begins with a brief introduction to
the syntax for restricted quantification. This is followed by an
overview of the ML functions available in the library and a
description of the theory \verb|res_quan.th|. A complete reference
manual for all ML functions appears in Chapter~2. The last chapter
lists all theorems in the \verb|res_quan.th|.

\section{Syntax for restricted quantification}

Since Version 2.0, \HOL\ provides parser and pretty printer support
for restricted quantification. This notation allows terms of the form
\[
\con{Q}\,x ::P.\, t[x],
\]
where \con{Q} is a quantifier and
if $x:\alpha$ then $P$ can be any term of type $\alpha\fun\bool$; this
denotes the quantification of $x$ over those values satisfying $P$.
The qualifier {\small\verb|::|} can be used with {\small\verb|\|} and any
binder, including user defined ones. The appropriate meanings are
predefined for {\small\verb|\|} and the built-in binders
{\small\verb|!|}, {\small\verb|?|} and {\small\verb|@|}.
This syntax automatically translates as follows:

\begin{hol}
{\small\verb%   \%}$v${\small\verb%::%}$P${\small\verb%.%}$tm${\small\verb%    <---->   %}\con{RES\_ABSTRACT}\ $P${\small\verb% (\%}$v${\small\verb%.%}$tm${\small\verb%)%}\\
{\small\verb%   !%}$v${\small\verb%::%}$P${\small\verb%.%}$tm${\small\verb%    <---->   %}\con{RES\_FORALL}\ \ \ $P${\small\verb% (\%}$v${\small\verb%.%}$tm${\small\verb%)%}\\
{\small\verb%   ?%}$v${\small\verb%::%}$P${\small\verb%.%}$tm${\small\verb%    <---->   %}\con{RES\_EXISTS}\ \ \ $P${\small\verb% (\%}$v${\small\verb%.%}$tm${\small\verb%)%}\\
{\small\verb%   @%}$v${\small\verb%::%}$P${\small\verb%.%}$tm${\small\verb%    <---->   %}\con{RES\_SELECT}\ \ \ $P${\small\verb% (\%}$v${\small\verb%.%}$tm${\small\verb%)%}
\end{hol}

The constants \con{RES\_ABSTRACT}, \con{RES\_FORALL}, \con{RES\_EXISTS} and
\con{RES\_SELECT} are defined in the theory \ml{bool} to provide
semantics for these restricted quantifiers as follows:

\begin{hol}\begin{verbatim}
   RES_ABSTRACT P tm  =  \x:*. (P x => tm x | ARB:**)

   RES_FORALL   P tm  =  !x:*. P x ==> tm x

   RES_EXISTS   P tm  =  ?x:*. P x /\ tm x

   RES_SELECT   P tm  =  @x:*. P x /\ tm x
\end{verbatim}\end{hol}

\noindent where the constant \con{ARB} is defined in the theory \ml{bool} by:

\begin{hol}\begin{verbatim}
   ARB  =  @x:*. T
\end{verbatim}\end{hol}

User-defined binders can also have restricted forms, which are set up
with the function:

\begin{holboxed}\index{associate_restriction@\ml{associate\_restriction}}
\begin{verbatim}
   associate_restriction : (string # string) -> *
\end{verbatim}\end{holboxed}


\noindent If \m{B} is the name
of a binder and \ml{RES\_}$B$ is the name of a suitable constant (which
must be explicitly defined), then executing:

\begin{hol}
{\small\verb%   associate_restriction(`%}\m{B}{\small\verb%`, `RES_%}\m{B}{\small\verb%`)%}
\end{hol}

\noindent will cause the parser and pretty-printer to support:

\begin{hol}
{\small\verb%   %}$B$ $v${\small\verb%::%}$P${\small\verb%. %}$tm${\small\verb%    <---->   RES_%}$B$ $P${\small\verb% (\%}$v${\small\verb%. %}$tm${\small\verb%)%}
\end{hol}

\noindent Note that associations between user defined binders and their
restrictions are not stored in theory files, so they have to be set up
for each \HOL\ session (e.g. with a {\small\verb%hol-init.ml%} initialization file).

The flag \ml{print\_restrict} has default \ml{true}, but if set to
\ml{false} will
disable the pretty printing. This is useful for seeing what the
semantics of particular restricted abstractions are.
Here is an example session:

\setcounter{sessioncount}{1}
\begin{session}\begin{verbatim}
#"!x y::P. x<y";;
"!x y :: P. x < y" : term

#set_flag(`print_restrict`, false);;
true : bool

#"!x y::P. x<y";;
"RES_FORALL P(\x. RES_FORALL P(\y. x < y))" : term

#"?(x,y) p::(\(m,n).m<n). p=(x,y)";;
"RES_EXISTS
 (\(m,n). m < n)
 (\(x,y). RES_EXISTS(\(m,n). m < n)(\p. p = x,y))"
: term

#"\x y z::P.[0;x;y;z]";;
"RES_ABSTRACT P(\x. RES_ABSTRACT P(\y. RES_ABSTRACT P(\z. [0;x;y;z])))"
: term
\end{verbatim}\end{session}

The syntax for restricted quantification provides a method of
simulating subtypes and dependent types; the qualifying predicate $P$ can be
an arbitrary term containing parameters. For example:
{\small\verb|!|}$w${\small\verb|::|}$\con{Word}(n)${\small\verb|. |}$t[w]$,
for a suitable constant \con{Word}, simulates a quantification over the
`type' of $n$-bit words.\footnote{This approach is used in the library
{\tt word} to model bit vectors.}

\section{The theory {\tt res\_quan.{}th}}

This theory contains a small number of theorems about the restricted
universal quantifier and restricted existential quantifier.
The following four theorems state the distributivity property of these
quantifiers across conjunction and disjunction.
\begin{verbatim}
 RESQ_FORALL_CONJ_DIST
  |- !P Q R.
     (!(i:*) :: P. (Q i /\ R i)) = (!i :: P. Q i) /\ (!i :: P. R i)

 RESQ_FORALL_DISJ_DIST
  |- !P Q R.
     (!(i:*) :: \i. P i \/ Q i. R i) = (!i :: P. R i) /\ (!i :: Q. R i)

 RESQ_EXISTS_DISJ_DIST
  |- !P Q R.
     (?(i:*) :: P. (Q i \/ R i)) = (?i :: P. Q i) \/ (?i :: P. R i)

 RESQ_DISJ_EXISTS_DIST
  |- !P Q R.
     (?(i:*) :: \i. P i \/ Q i. R i) = (?i :: P. R i) \/ (?i :: Q. R i)
\end{verbatim}

The theorems \ml{RESQ\_FORALL\_REORDER} and \ml{RESQ\_EXISTS\_REORDER}
state the reordering property of these quantifiers.
\begin{verbatim}
 RESQ_FORALL_REORDER
  |- !(P:*->bool) (Q:**->bool) (R:*->**->bool).
      (!i :: P. !j :: Q. R i j) = (!j :: Q. !i :: P. R i j)

 RESQ_EXISTS_REORDER
  |- !(P:*->bool) (Q:**->bool) (R:*->**->bool).
      (?i :: P. ?j :: Q. R i j) = (?j :: Q. ?i :: P. R i j)
\end{verbatim}
The theorem \ml{RESQ\_FORALL\_FORALL} states the reordering property of
the restricted universal quantifier and the ordinary universal
quantifier.
\begin{verbatim}
 RESQ_FORALL_FORALL
  |- !(P:*->bool) (R:*->**->bool) x.
      (!x. !i :: P. R i x) = (!i :: P. !x. R i x)
\end{verbatim}

\section{ML functions}

The ML functions available when this library is loaded can be divided
into six groups: conditional rewriting tools, syntax functions,
derived rules, conversions, tactics, and constant definitions. They
will be described in separate subsections.

\subsection{Conditional rewriting tools}

The conditional rewriting tools are not specific for restricted
quantifiers. They are available as a separate part of the library
which can be loaded into \HOL\ without loading other functions in this
library. This is done by the command
\begin{verbatim}
 load_library `res_quan:cond_rewrite`;;
\end{verbatim}

The conditional rewriting tools consists of a simple tactic which is
for use in goal-directed proof and a simple conversion which is
usually used in forward proof.

\subsubsection{Conditional theorems}

Both the conditional rewriting tactic and conversion require a theorem
to do the rewriting. This theorem should be an implication whose
consequence is an equation, i.e., it should be of the following form:
\begin{equation}
   A \vdash \forall\,x_1 \ldots x_n\DOT P_1 \IMP \ldots P_m \IMP
 (Q[x_1,\ldots,x_n] = R[x_1,\ldots,x_n]) \label{eq-cond-thm}
\end{equation}
where $x_1, \ldots, x_n$ are the only variables that occur free in the
left-hand side of the conclusion of the theorem but do not occur free
in the assumptions. Futhermore, none of the antecedents
$P_1,\ldots,P_n$ should be
conjunctions. The idea of  conditional rewriting is that the
antecedents of this input theorem are treated as conditions which have
to be satisfied before the equation $Q[x_1,\ldots,x_n] = R[x_1,\ldots,x_n]$
can be used to rewrite a term.

The ML function \ml{COND\_REWR\_CANON} transforms a theorem
into the canonical form in~\ref{eq-cond-thm}. The antecedents of the
input theorem to \ml{COND\_REWR\_CANON} may contain conjunctions and
quantification. For example, suppose that {\tt th} is the theorem
\begin{equation}
   A \vdash \forall\,x\DOT P_1\,x \IMP  \forall y\,z.(P_2\,y \AND P_3\,z) \IMP
 (\forall t. Q[x,y,z,t] = R[x,y,z,t]) \label{eq-cond-thm2}
\end{equation}
then \verb|COND_REWR_CANON th| returns the theorem
\[
   A \vdash \forall\,x\,y\,z\,t\DOT P_1\,x \IMP P_2\,y \IMP P_3\,z \IMP
 (Q[x,y,z,t] = R[x,y,z,t])
\]
That is all universal quantifications are moved to the outer most level
and conjunctions in the antecedents are converted to implication.

\subsubsection{Conditional rewriting tactic}

The basic conditional rewriting tactic is
\begin{holboxed}
\begin{verbatim}
   COND_REWRITE1_TAC : thm_tactic
\end{verbatim}
\end{holboxed}
Suppose {\tt th} is the theorem in~\ref{eq-cond-thm2},
the effects of applying the tactic $\ml{COND\_REWRITE1\_TAC}\;th$ to the
goal $(asm,gl)$ is that
\begin{itemize}
\item  all instances of $Q$ in the goal $gl$ are
	replaced by corresponding instances of $R$, and
\item the instances of the antecedents $P_i$ which do not appear in
	the assumption $asm$ become new subgoals.
\end{itemize}

This tactic is implemented using a lower level tactic \ml{COND\_REWR\_TAC}.
The theorem $th$ supplied to \ml{COND\_REWRITE1\_TAC} is processed by
\ml{COND\_REWR\_CANON} first. The resulting theorem is passed to the low
level conditional rewriting tactic \ml{COND\_REWR\_TAC} together with a
search function \ml{search\_top\_down}. This function determines how to
find the instantiations. By calling \ml{COND\_REWR\_TAC} with different
search function, other conditional rewriting strategy can be
implemented. The details of the tactics and search functions can be
found in the reference entries in Chapter~2.
Note that the {\tt 1} in the name of the tactic indicates that it
takes only a single theorem as its argument.

\subsubsection{Conditional rewriting conversion}

The basic conditional rewriting conversion is
\begin{holboxed}
\begin{verbatim}
   COND_REWRITE1_CONV : (thm list -> thm -> conv)
\end{verbatim}
\end{holboxed}
which performs conversion in a way similar to the conditional
rewriting tactics. The difference is that the instances of the
antecedents are added to the list of assumptions of the resulting theorem. The
extra argument to this conversion is a list of theorems which are
used to eliminate instances of the antecedents from the assumptions.

\subsection{Syntax functions}

There are term constructors, term destructors and term testers for the
four built-in restricted quantifiers. There are also iterative
constructors and destructors for the restricted universal and
existential quantifiers. Their names and types are:
\begin{holboxed}
\begin{verbatim}
mk_resq_forall = - : ((term # term # term) -> term)
mk_resq_exists = - : ((term # term # term) -> term)
mk_resq_select = - : ((term # term # term) -> term)
mk_resq_abstract = - : ((term # term # term) -> term)
list_mk_resq_forall = - : (((term # term) list # term) -> term)
list_mk_resq_exists = - : (((term # term) list # term) -> term)

dest_resq_forall = - : (term -> (term # term # term))
dest_resq_exists = - : (term -> (term # term # term))
dest_resq_select = - : (term -> (term # term # term))
dest_resq_abstract = - : (term -> (term # term # term))
strip_resq_forall = - : (term -> ((term # term) list # term))
strip_resq_exists = - : (term -> ((term # term) list # term))

is_resq_forall = - : (term -> bool)
is_resq_exists = - : (term -> bool)
is_resq_select = - : (term -> bool)
is_resq_abstract = - : (term -> bool)
\end{verbatim}
\end{holboxed}

\subsection{Derived rules}

The introduction and elimination rules for the restricted universal
quantifier are \ml{RESQ\_SPEC} and \ml{RESQ\_GEN} which are in analogy
to the rules for the universal quantifier. The specification of these
rules are:
\[
\frac{\Gamma \THM \forall x :: P. t[x]}{\Gamma,P\,x'\THM t[x'/x]}
\quad\mbox{{\tt RESQ\_SPEC "x'"}}
\]
\[
\frac{\Gamma,P\,x\THM t[x]}{\Gamma \THM \forall x :: P. t[x]}
\quad\mbox{{\tt RESQ\_GEN "x" "P"}}
\]
There is an extra rule \ml{RESQ\_HALF\_SPEC} which transform a
restricted universal quantification into its underlying semantic
representation, namely an implication.
\[
\frac{\Gamma \THM \forall x :: P. t[x]}{\Gamma \THM\forall x. P\,x\IMP t[x]}
\quad\mbox{{\tt RESQ\_HALF\_SPEC}}
\]

There are iterative versions of the introduction and elimination rules:
\begin{holboxed}
\begin{verbatim}
RESQ_SPECL = - : (term list -> thm -> thm)
RESQ_SPEC_ALL = - : (thm -> thm)

RESQ_GENL = - : (term list -> thm -> thm)
RESQ_GEN_ALL = - : (thm -> thm)
\end{verbatim}
\end{holboxed}

Since instantiation of a theorem is a very common operation, for
convenience, the following ML functions are provided to instantiate a
theorem with a mixture of ordinary and restricted universal quantifiers:
\begin{holboxed}
\begin{verbatim}
GQSPEC = - : tm -> thm -> thm
GQSPECL : term list -> thm -> thm
GQSPEC_ALL : thm -> thm
\end{verbatim}
\end{holboxed}

The rule for eliminating restricted existential quantification is
\ml{RESQ\_HALF\_EXISTS} whose specification is:
\[
\frac{\Gamma \THM \exists x:: P. t[x]}{\Gamma \THM \exists x. P\,x
\AND t[x]}\quad\mbox{{\tt RESQ\_HALF\_EXISTS}}
\]
This function only transforms the restricted existential quantifier to
an ordinary existential quantifier.

The function \ml{RESQ\_MATCH\_MP} eliminates a restricted universal
quantifier using an instance of the condition. Its specification is:
\[
\frac{\Gamma_1 \THM \forall x::P. t[x]\qquad\Gamma_2\THM P\,x'}
{\Gamma_1 \cup \Gamma_2 \THM t[x'/x]}\quad\mbox{{\tt RESQ\_MATCH\_MP}}
\]

\subsection{Conversions}

There are a number of conversions for manipulating restricted
universal quantification. The conversion \ml{RESQ\_FORALL\_CONV}
converts a restricted universal quantification to its underlying
semantic representation, namely an implication. For example,
evaluating the ML expression
\verb|RESQ_FORALL_CONV "!x :: P. t[x]"| returns the following theorem:
\[
\THM \forall x :: P. t[x] = \forall x. P x \IMP t[x]
\]
The ML function
\ml{IMP\_RESQ\_FORALL\_CONV} performs the reverse conversion. The ML
function \ml{LIST\_RESQ\_FORALL\_CONV} is an iterative version of
\ml{RESQ\_FORALL\_CONV} which converts a term having multiple
restricted universal quantifiers at the outer level.

The conversions \ml{RESQ\_FORALL\_AND\_CONV} and
\ml{AND\_RESQ\_FORALL\_CONV} move the restricted universal
quantification in and out of a conjunction, respectively.
The conversion \linebreak\ml{RESQ\_FORALL\_SWAP\_CONV} changes the order of two
restricted universal quantifications. For instance, evaluating the
following ML expression
\begin{verbatim}
   RESQ_FORALL_SWAP_CONV "!i :: P. !j :: Q. R"
\end{verbatim}
returns the theorem:
\[
\THM (\forall i :: P. \forall j :: Q. R) = (\forall j :: Q. \forall i :: P. R)
\]
providing that $i$ does not occur free in $Q$ and $j$ does not occur
free in $P$.

The conversion \ml{RESQ\_EXISTS\_CONV} transforms a restricted
existential quantification to its underlying semantic representation.
For instance, \verb|RESQ_EXISTS_CONV "?x::P. t"| returns the theorem
\[
\THM \exists x::P. t = \exists x. P x \AND t[x]
\]

A rewriting conversion \ml{RESQ\_REWRITE1\_CONV} uses a restricted
universal quantified equation to rewrite a term. For instance, if {\tt
th} is a theorem of the following form:
\[
\THM \forall x::P. u[x] = v[x]
\]
and {\tt tm} is a term containing some instances of $u$,
then \verb|RESQ_REWRITE1_CONV ths th tm| will return the theorem
\[
\Gamma \THM tm = tm'
\]
where $tm'$ is obtained by replacing all instances of $u$ by
corresponding instances of $v$ and $\Gamma$ contains instances of $P$
which cannot be eliminated by the theorems in the list {\tt ths}. This
conversion is implemented using the conditional rewriting conversion
\ml{COND\_REWRITE1\_CONV}.

\subsection{Tactics}

The simple tactics \ml{RESQ\_GEN\_TAC} and \ml{RESQ\_EXISTS\_TAC} are
provided for stripping of a restricted universal or existential
quantifier, respectively. They reduce a restricted quantified goal to
a goal in the underlying semantic representation. They are in analogy
to \ml{GEN\_TAC} and \ml{EXISTS\_TAC}.

The resolution tactics and tactical listed below are in analogy to
\ml{RES\_TAC}, \ml{IMP\_RES\_TAC}, \ml{RES\_THEN} and
\ml{IMP\_RES\_THEN}.
\begin{holboxed}
\begin{verbatim}
RESQ_RES_THEN : (thm_tactic -> tactic)
RESQ_IMP_RES_THEN : thm_tactical
RESQ_RES_TAC : tactic
RESQ_IMP_RES_TAC : thm_tactic
\end{verbatim}
\end{holboxed}
The theorem-tactic \ml{RESQ\_IMP\_RES\_TAC} uses a restricted universally
quantified theorem as if it is an implication to perform resolution.
Similarly, the tactic \ml{RESQ\_RES\_TAC} uses a restricted universally
quantified assumption as if it is an implication to
perform resolution against other assumptions.

The theorem-tactic \ml{RESQ\_REWRITE1\_TAC} uses a restricted universally
quantified theorem to perform conditional rewriting.
For instance, if {\tt th} is the following theorem
\[
\THM \forall x::P. u[x] = v[x]
\]
then applying the tactic \verb|RESQ_REWRITE1_TAC th| to a goal {\tt
gl} will reduce it to one or more subgoals {\tt gl0}, \ldots, {\tt
gln}. The main subgoal {\tt gl0} is obtained by replacing instances of
$u$ in {\tt gl} with corresponding instances of $v$. The new subgoals
are the instances of $P$ which do not occur in the assumption of $gl$.


\subsection{Constant definitions}


This library provides support for defining constants whose arguments
can be restricted quantified variables. For example, one can defined a constant
\con{C} by the following equation:
\begin{eqnarray*}
\lefteqn{\forall x_1::P_1. \ldots \forall x_n::P_n.} \\
 & &  \mbox{{\sf C}}\, y\, x_1 \ldots x_n\, z = t[y,x_1,\ldots,x_n,z]
\end{eqnarray*}
The constant \con{C} may be an ordinary constant, or it may have
either `infix' or `binder' status. The ML functions for defining
restricted quantified constants are:
\begin{holboxed}
\begin{verbatim}
new_resq_definition        : (string # term) -> thm
new_infix_resq_definition  : (string # term) -> thm
new_binder_resq_definition : (string # term) -> thm
\end{verbatim}
\end{holboxed}
Suppose {\tt tm} is the term shown above, evaluating the ML expression
\begin{verbatim}
   new_resq_definition(`C_DEF`,tm)
\end{verbatim}
will store the definition under
the name \verb|C_DEF| in the current theory. The definition is
returned as the value of the expression.