doc-src/Intro/getting.tex

revisions to first Springer draft

%% $Id$
\part{Getting Started with Isabelle}\label{chap:getting}
We now consider how to perform simple proofs using Isabelle.  As of this
writing, Isabelle's user interface is \ML.  Proofs are conducted by
applying certain \ML{} functions, which update a stored proof state.  All
syntax must be expressed using {\sc ascii} characters.  Menu-driven
graphical interfaces are under construction, but Isabelle users will always
need to know some \ML, at least to use tacticals.

Object-logics are built upon Pure Isabelle, which implements the meta-logic
and provides certain fundamental data structures: types, terms, signatures,
theorems and theories, tactics and tacticals.  These data structures have
the corresponding \ML{} types {\tt typ}, {\tt term}, {\tt Sign.sg}, {\tt thm},
{\tt theory} and {\tt tactic}; tacticals have function types such as {\tt
tactic->tactic}.  Isabelle users can operate on these data structures by
writing \ML{} programs.

\section{Forward proof}
\index{Isabelle!getting started}\index{ML}
This section describes the concrete syntax for types, terms and theorems,
and demonstrates forward proof.

\subsection{Lexical matters}
\index{identifiers|bold}\index{reserved words|bold} 
An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|)
and single quotes~({\tt'}), beginning with a letter.  Single quotes are
regarded as primes; for instance {\tt x'} is read as~$x'$.  Identifiers are
separated by white space and special characters.  {\bf Reserved words} are
identifiers that appear in Isabelle syntax definitions.

An Isabelle theory can declare symbols composed of special characters, such
as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}.  (The latter three are part of
the syntax of the meta-logic.)  Such symbols may be run together; thus if
\verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is
valid notation for a set of sets --- but only if \verb|}}| and \verb|{{|
have not been declared as symbols!  The parser resolves any ambiguity by
taking the longest possible symbol that has been declared.  Thus the string
{\tt==>} is read as a single symbol.  But \hbox{\tt= =>} is read as two
symbols.

Identifiers that are not reserved words may serve as free variables or
constants.  A type identifier consists of an identifier prefixed by a
prime, for example {\tt'a} and \hbox{\tt'hello}.  An unknown (or type
unknown) consists of a question mark, an identifier (or type identifier),
and a subscript.  The subscript, a non-negative integer, allows the
renaming of unknowns prior to unification.%
%
\footnote{The subscript may appear after the identifier, separated by a
  dot; this prevents ambiguity when the identifier ends with a digit.  Thus
  {\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5}
  has identifier {\tt"a0"} and subscript~5.  If the identifier does not
  end with a digit, then no dot appears and a subscript of~0 is omitted;
  for example, {\tt?hello} has identifier {\tt"hello"} and subscript
  zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6.  The same
  conventions apply to type unknowns.  The question mark is {\it not\/}
  part of the identifier!}


\subsection{Syntax of types and terms}
\index{Isabelle!syntax of}
\index{classes!built-in|bold}
Classes are denoted by identifiers; the built-in class \ttindex{logic}
contains the `logical' types.  Sorts are lists of classes enclosed in
braces~\} and \{; singleton sorts may be abbreviated by dropping the braces.

\index{types!syntax|bold}
Types are written with a syntax like \ML's.  The built-in type \ttindex{prop}
is the type of propositions.  Type variables can be constrained to particular
classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\{ord,arith\}}.
\[\dquotes
\begin{array}{lll}
    \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
  t "::" C              & t :: C        & \hbox{class constraint} \\
  t "::" "\{"   C@1 "," \ldots "," C@n "\}" &
     t :: \{C@1,\dots,C@n\}             & \hbox{sort constraint} \\
  \sigma"=>"\tau        & \sigma\To\tau & \hbox{function type} \\
  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
     [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\
  "(" \tau@1"," \ldots "," \tau@n ")" tycon & 
     (\tau@1, \ldots, \tau@n)tycon      & \hbox{type construction}
\end{array} 
\]
Terms are those of the typed $\lambda$-calculus.
\index{terms!syntax|bold}
\[\dquotes
\begin{array}{lll}
    \multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
  t "::" \sigma         & t :: \sigma   & \hbox{type constraint} \\
  "\%" x "." t          & \lambda x.t   & \hbox{abstraction} \\
  "\%" x@1\ldots x@n "." t  & \lambda x@1\ldots x@n.t & 
     \hbox{curried abstraction} \\
  t "(" u@1"," \ldots "," u@n ")" & 
  t (u@1, \ldots, u@n) & \hbox{curried application}
\end{array}  
\]
The theorems and rules of an object-logic are represented by theorems in
the meta-logic, which are expressed using meta-formulae.  Since the
meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}
are just terms of type~\ttindex{prop}.  
\index{meta-formulae!syntax|bold}
\[\dquotes
  \begin{array}{l@{\quad}l@{\quad}l}
    \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline
  a " == " b    & a\equiv b &   \hbox{meta-equality} \\
  a " =?= " b   & a\qeq b &     \hbox{flex-flex constraint} \\
  \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\
  "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & 
  \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\
  "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\
  "!!" x@1\ldots x@n "." \phi & 
  \Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification}
  \end{array}
\]
Flex-flex constraints are meta-equalities arising from unification; they
require special treatment.  See~\S\ref{flexflex}.
\index{flex-flex equations}

Most logics define the implicit coercion $Trueprop$ from object-formulae to
propositions.  
\index{Trueprop@{$Trueprop$}}
This could cause an ambiguity: in $P\Imp Q$, do the variables $P$ and $Q$
stand for meta-formulae or object-formulae?  If the latter, $P\Imp Q$
really abbreviates $Trueprop(P)\Imp Trueprop(Q)$.  To prevent such
ambiguities, Isabelle's syntax does not allow a meta-formula to consist of
a variable.  Variables of type~\ttindex{prop} are seldom useful, but you
can make a variable stand for a meta-formula by prefixing it with the
keyword \ttindex{PROP}:
\begin{ttbox} 
PROP ?psi ==> PROP ?theta 
\end{ttbox}

Symbols of object-logics also must be rendered into {\sc ascii}, typically
as follows:
\[ \begin{tabular}{l@{\quad}l@{\quad}l}
      \tt True          & $\top$        & true \\
      \tt False         & $\bot$        & false \\
      \tt $P$ \& $Q$    & $P\conj Q$    & conjunction \\
      \tt $P$ | $Q$     & $P\disj Q$    & disjunction \\
      \verb'~' $P$      & $\neg P$      & negation \\
      \tt $P$ --> $Q$   & $P\imp Q$     & implication \\
      \tt $P$ <-> $Q$   & $P\bimp Q$    & bi-implication \\
      \tt ALL $x\,y\,z$ .\ $P$  & $\forall x\,y\,z.P$   & for all \\
      \tt EX  $x\,y\,z$ .\ $P$  & $\exists x\,y\,z.P$   & there exists
   \end{tabular}
\]
To illustrate the notation, consider two axioms for first-order logic:
$$ \List{P; Q} \Imp P\conj Q                 \eqno(\conj I) $$
$$ \List{\exists x.P(x);  \Forall x. P(x)\imp Q} \Imp Q  \eqno(\exists E) $$
Using the {\tt [|\ldots|]} shorthand, $({\conj}I)$ translates into
{\sc ascii} characters as
\begin{ttbox}
[| ?P; ?Q |] ==> ?P & ?Q
\end{ttbox}
The schematic variables let unification instantiate the rule.  To avoid
cluttering logic definitions with question marks, Isabelle converts any
free variables in a rule to schematic variables; we normally declare
$({\conj}I)$ as
\begin{ttbox}
[| P; Q |] ==> P & Q
\end{ttbox}
This variables convention agrees with the treatment of variables in goals.
Free variables in a goal remain fixed throughout the proof.  After the
proof is finished, Isabelle converts them to scheme variables in the
resulting theorem.  Scheme variables in a goal may be replaced by terms
during the proof, supporting answer extraction, program synthesis, and so
forth.

For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as
\begin{ttbox}
[| EX x.P(x);  !!x. P(x) ==> Q |] ==> Q
\end{ttbox}


\subsection{Basic operations on theorems}
\index{theorems!basic operations on|bold}
\index{LCF}
Meta-level theorems have type \ttindex{thm} and represent the theorems and
inference rules of object-logics.  Isabelle's meta-logic is implemented
using the {\sc lcf} approach: each meta-level inference rule is represented by
a function from theorems to theorems.  Object-level rules are taken as
axioms.

The main theorem printing commands are {\tt prth}, {\tt prths} and~{\tt
  prthq}.  Of the other operations on theorems, most useful are {\tt RS}
and {\tt RSN}, which perform resolution.

\index{printing commands|bold}
\begin{description}
\item[\ttindexbold{prth} {\it thm}]  pretty-prints {\it thm\/} at the terminal.

\item[\ttindexbold{prths} {\it thms}]  pretty-prints {\it thms}, a list of
theorems.

\item[\ttindexbold{prthq} {\it thmq}]  pretty-prints {\it thmq}, a sequence of
theorems; this is useful for inspecting the output of a tactic.

\item[\tt$thm1$ RS $thm2$] \indexbold{*RS} resolves the conclusion of $thm1$
with the first premise of~$thm2$.

\item[\tt$thm1$ RSN $(i,thm2)$] \indexbold{*RSN} resolves the conclusion of $thm1$
with the $i$th premise of~$thm2$.

\item[\ttindexbold{standard} $thm$]  puts $thm$ into a standard
format.  It also renames schematic variables to have subscript zero,
improving readability and reducing subscript growth.
\end{description}
\index{ML}
The rules of a theory are normally bound to \ML\ identifiers.  Suppose we
are running an Isabelle session containing natural deduction first-order
logic.  Let us try an example given in~\S\ref{joining}.  We first print
\ttindex{mp}, which is the rule~$({\imp}E)$, then resolve it with itself.
\begin{ttbox} 
prth mp; 
{\out [| ?P --> ?Q; ?P |] ==> ?Q}
{\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm}
prth (mp RS mp);
{\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}
{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
\end{ttbox}
User input appears in {\tt typewriter characters}, and output appears in
{\sltt slanted typewriter characters}.  \ML's response {\out val }~\ldots{}
is compiler-dependent and will sometimes be suppressed.  This session
illustrates two formats for the display of theorems.  Isabelle's top-level
displays theorems as ML values, enclosed in quotes.\footnote{This works
  under both Poly/ML and Standard ML of New Jersey.}  Printing commands
like {\tt prth} omit the quotes and the surrounding {\tt val \ldots :\ 
  thm}.  Ignoring their side-effects, the commands are identity functions.

To contrast {\tt RS} with {\tt RSN}, we resolve
\ttindex{conjunct1}, which stands for~$(\conj E1)$, with~\ttindex{mp}.
\begin{ttbox} 
conjunct1 RS mp;
{\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm}
conjunct1 RSN (2,mp);
{\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm}
\end{ttbox}
These correspond to the following proofs:
\[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P}
   \qquad
   \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}} 
\]
%
Rules can be derived by pasting other rules together.  Let us join
\ttindex{spec}, which stands for~$(\forall E)$, with {\tt mp} and {\tt
  conjunct1}.  In \ML{}, the identifier~{\tt it} denotes the value just
printed.
\begin{ttbox} 
spec;
{\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}
it RS mp;
{\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==>}
{\out           ?Q2(?x1)" : thm}
it RS conjunct1;
{\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>}
{\out           ?P6(?x2)" : thm}
standard it;
{\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>}
{\out           ?Pa(?x)" : thm}
\end{ttbox}
By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have
derived a destruction rule for formulae of the form $\forall x.
P(x)\imp(Q(x)\conj R(x))$.  Used with destruct-resolution, such specialized
rules provide a way of referring to particular assumptions.

\subsection{*Flex-flex equations} \label{flexflex}
\index{flex-flex equations|bold}\index{unknowns!of function type}
In higher-order unification, {\bf flex-flex} equations are those where both
sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$.
They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and
$\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown.  They
admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$
and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$.  Huet's
procedure does not enumerate the unifiers; instead, it retains flex-flex
equations as constraints on future unifications.  Flex-flex constraints
occasionally become attached to a proof state; more frequently, they appear
during use of {\tt RS} and~{\tt RSN}:
\begin{ttbox} 
refl;
{\out val it = "?a = ?a" : thm}
exI;
{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}
refl RS exI;
{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm}
\end{ttbox}

\noindent
Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with
the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$.  Instances
satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and
$\exists x.x=\Var{u}$.  Calling \ttindex{flexflex_rule} removes all
constraints by applying the trivial unifier:\index{*prthq}
\begin{ttbox} 
prthq (flexflex_rule it);
{\out EX x. ?a4 = ?a4}
\end{ttbox} 
Isabelle simplifies flex-flex equations to eliminate redundant bound
variables.  In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$,
there is no bound occurrence of~$x$ on the right side; thus, there will be
none on the left in a common instance of these terms.  Choosing a new
variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$,
simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$.  Dropping $x$
from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda
y.\Var{g}(y)$.  By $\eta$-conversion, this simplifies to the assignment
$\Var{g}\equiv\lambda y.?h(k(y))$.

\begin{warn}
\ttindex{RS} and \ttindex{RSN} fail (by raising exception {\tt THM}) unless
the resolution delivers {\bf exactly one} resolvent.  For multiple results,
use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists.  The
following example uses \ttindex{read_instantiate} to create an instance
of \ttindex{refl} containing no schematic variables.
\begin{ttbox} 
val reflk = read_instantiate [("a","k")] refl;
{\out val reflk = "k = k" : thm}
\end{ttbox}

\noindent
A flex-flex constraint is no longer possible; resolution does not find a
unique unifier:
\begin{ttbox} 
reflk RS exI;
{\out uncaught exception THM}
\end{ttbox}
Using \ttindex{RL} this time, we discover that there are four unifiers, and
four resolvents:
\begin{ttbox} 
[reflk] RL [exI];
{\out val it = ["EX x. x = x", "EX x. k = x",}
{\out           "EX x. x = k", "EX x. k = k"] : thm list}
\end{ttbox} 
\end{warn}


\section{Backward proof}
Although {\tt RS} and {\tt RSN} are fine for simple forward reasoning,
large proofs require tactics.  Isabelle provides a suite of commands for
conducting a backward proof using tactics.

\subsection{The basic tactics}
\index{tactics!basic|bold}
The tactics {\tt assume_tac}, {\tt
resolve_tac}, {\tt eresolve_tac}, and {\tt dresolve_tac} suffice for most
single-step proofs.  Although {\tt eresolve_tac} and {\tt dresolve_tac} are
not strictly necessary, they simplify proofs involving elimination and
destruction rules.  All the tactics act on a subgoal designated by a
positive integer~$i$, failing if~$i$ is out of range.  The resolution
tactics try their list of theorems in left-to-right order.

\begin{description}
\item[\ttindexbold{assume_tac} {\it i}] is the tactic that attempts to solve
subgoal~$i$ by assumption.  Proof by assumption is not a trivial step; it
can falsify other subgoals by instantiating shared variables.  There may be
several ways of solving the subgoal by assumption.

\item[\ttindexbold{resolve_tac} {\it thms} {\it i}]
is the basic resolution tactic, used for most proof steps.  The $thms$
represent object-rules, which are resolved against subgoal~$i$ of the proof
state.  For each rule, resolution forms next states by unifying the
conclusion with the subgoal and inserting instantiated premises in its
place.  A rule can admit many higher-order unifiers.  The tactic fails if
none of the rules generates next states.

\item[\ttindexbold{eresolve_tac} {\it thms} {\it i}] 
performs elim-resolution.  Like
\hbox{\tt resolve_tac {\it thms} {\it i}} followed by \hbox{\tt assume_tac
{\it i}}, it applies a rule then solves its first premise by assumption.
But {\tt eresolve_tac} additionally deletes that assumption from any
subgoals arising from the resolution.


\item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
performs destruct-resolution with the~$thms$, as described
in~\S\ref{destruct}.  It is useful for forward reasoning from the
assumptions.
\end{description}

\subsection{Commands for backward proof}
\index{proof!commands for|bold}
Tactics are normally applied using the subgoal module, which maintains a
proof state and manages the proof construction.  It allows interactive
backtracking through the proof space, going away to prove lemmas, etc.; of
its many commands, most important are the following:
\begin{description}
\item[\ttindexbold{goal} {\it theory} {\it formula}; ] 
begins a new proof, where $theory$ is usually an \ML\ identifier
and the {\it formula\/} is written as an \ML\ string.

\item[\ttindexbold{by} {\it tactic}; ] 
applies the {\it tactic\/} to the current proof
state, raising an exception if the tactic fails.

\item[\ttindexbold{undo}(); ] 
  reverts to the previous proof state.  Undo can be repeated but cannot be
  undone.  Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely
  causes \ML\ to echo the value of that function.

\item[\ttindexbold{result}()] 
returns the theorem just proved, in a standard format.  It fails if
unproved subgoals are left, etc.
\end{description}
The commands and tactics given above are cumbersome for interactive use.
Although our examples will use the full commands, you may prefer Isabelle's
shortcuts:
\begin{center} \tt
\indexbold{*br} \indexbold{*be} \indexbold{*bd} \indexbold{*ba}
\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l}
    ba {\it i};           & by (assume_tac {\it i}); \\

    br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\

    be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\

    bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i}); 
\end{tabular}
\end{center}

\subsection{A trivial example in propositional logic}
\index{examples!propositional}

Directory {\tt FOL} of the Isabelle distribution defines the theory of
first-order logic.  Let us try the example from \S\ref{prop-proof},
entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these
  examples, see the file {\tt FOL/ex/intro.ML}.  The files {\tt README} and
  {\tt Makefile} on the directories {\tt Pure} and {\tt FOL} explain how to
  build first-order logic.}
\begin{ttbox}
goal FOL.thy "P|P --> P"; 
{\out Level 0} 
{\out P | P --> P} 
{\out 1. P | P --> P} 
\end{ttbox}
Isabelle responds by printing the initial proof state, which has $P\disj
P\imp P$ as the main goal and the only subgoal.  The \bfindex{level} of the
state is the number of {\tt by} commands that have been applied to reach
it.  We now use \ttindex{resolve_tac} to apply the rule \ttindex{impI},
or~$({\imp}I)$, to subgoal~1:
\begin{ttbox}
by (resolve_tac [impI] 1); 
{\out Level 1} 
{\out P | P --> P} 
{\out 1. P | P ==> P}
\end{ttbox}
In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$.
(The meta-implication {\tt==>} indicates assumptions.)  We apply
\ttindex{disjE}, or~(${\disj}E)$, to that subgoal:
\begin{ttbox}
by (resolve_tac [disjE] 1); 
{\out Level 2} 
{\out P | P --> P} 
{\out 1. P | P ==> ?P1 | ?Q1} 
{\out 2. [| P | P; ?P1 |] ==> P} 
{\out 3. [| P | P; ?Q1 |] ==> P}
\end{ttbox}
At Level~2 there are three subgoals, each provable by assumption.  We
deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using
\ttindex{assume_tac}.  This affects subgoal~1, updating {\tt?Q1} to~{\tt
  P}.
\begin{ttbox}
by (assume_tac 3); 
{\out Level 3} 
{\out P | P --> P} 
{\out 1. P | P ==> ?P1 | P} 
{\out 2. [| P | P; ?P1 |] ==> P}
\end{ttbox}
Next we tackle subgoal~2, instantiating {\tt?P1} to~{\tt P} in subgoal~1.
\begin{ttbox}
by (assume_tac 2); 
{\out Level 4} 
{\out P | P --> P} 
{\out 1. P | P ==> P | P}
\end{ttbox}
Lastly we prove the remaining subgoal by assumption:
\begin{ttbox}
by (assume_tac 1); 
{\out Level 5} 
{\out P | P --> P} 
{\out No subgoals!}
\end{ttbox}
Isabelle tells us that there are no longer any subgoals: the proof is
complete.  Calling \ttindex{result} returns the theorem.
\begin{ttbox}
val mythm = result(); 
{\out val mythm = "?P | ?P --> ?P" : thm} 
\end{ttbox}
Isabelle has replaced the free variable~{\tt P} by the scheme
variable~{\tt?P}\@.  Free variables in the proof state remain fixed
throughout the proof.  Isabelle finally converts them to scheme variables
so that the resulting theorem can be instantiated with any formula.

As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how
instantiations affect the proof state.


\subsection{Part of a distributive law}
\index{examples!propositional}
To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac}
and the tactical \ttindex{REPEAT}, let us prove part of the distributive
law 
\[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \]
We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it:
\begin{ttbox}
goal FOL.thy "(P & Q) | R  --> (P | R)";
{\out Level 0}
{\out P & Q | R --> P | R}
{\out  1. P & Q | R --> P | R}
\ttbreak
by (resolve_tac [impI] 1);
{\out Level 1}
{\out P & Q | R --> P | R}
{\out  1. P & Q | R ==> P | R}
\end{ttbox}
Previously we applied~(${\disj}E)$ using {\tt resolve_tac}, but 
\ttindex{eresolve_tac} deletes the assumption after use.  The resulting proof
state is simpler.
\begin{ttbox}
by (eresolve_tac [disjE] 1);
{\out Level 2}
{\out P & Q | R --> P | R}
{\out  1. P & Q ==> P | R}
{\out  2. R ==> P | R}
\end{ttbox}
Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1,
replacing the assumption $P\conj Q$ by~$P$.  Normally we should apply the
rule~(${\conj}E)$, given in~\S\ref{destruct}.  That is an elimination rule
and requires {\tt eresolve_tac}; it would replace $P\conj Q$ by the two
assumptions~$P$ and~$Q$.  Because the present example does not need~$Q$, we
may try out {\tt dresolve_tac}.
\begin{ttbox}
by (dresolve_tac [conjunct1] 1);
{\out Level 3}
{\out P & Q | R --> P | R}
{\out  1. P ==> P | R}
{\out  2. R ==> P | R}
\end{ttbox}
The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner.
\begin{ttbox}
by (resolve_tac [disjI1] 1);
{\out Level 4}
{\out P & Q | R --> P | R}
{\out  1. P ==> P}
{\out  2. R ==> P | R}
\ttbreak
by (resolve_tac [disjI2] 2);
{\out Level 5}
{\out P & Q | R --> P | R}
{\out  1. P ==> P}
{\out  2. R ==> R}
\end{ttbox}
Two calls of~\ttindex{assume_tac} can finish the proof.  The
tactical~\ttindex{REPEAT} expresses a tactic that calls {\tt assume_tac~1}
as many times as possible.  We can restrict attention to subgoal~1 because
the other subgoals move up after subgoal~1 disappears.
\begin{ttbox}
by (REPEAT (assume_tac 1));
{\out Level 6}
{\out P & Q | R --> P | R}
{\out No subgoals!}
\end{ttbox}


\section{Quantifier reasoning}
\index{quantifiers!reasoning about}\index{parameters}\index{unknowns}
This section illustrates how Isabelle enforces quantifier provisos.
Quantifier rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a
function unknown and $x$ and~$z$ are parameters.  This may be replaced by
any term, possibly containing free occurrences of $x$ and~$z$.

\subsection{Two quantifier proofs: a success and a failure}
\index{examples!with quantifiers}
Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an
attempted proof of the non-theorem $\exists y.\forall x.x=y$.  The former
proof succeeds, and the latter fails, because of the scope of quantified
variables~\cite{paulson89}.  Unification helps even in these trivial
proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$,
but we need never say so. This choice is forced by the reflexive law for
equality, and happens automatically.

\paragraph{The successful proof.}
The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules
$(\forall I)$ and~$(\exists I)$.  We state the goal and apply $(\forall I)$:
\begin{ttbox}
goal FOL.thy "ALL x. EX y. x=y";
{\out Level 0}
{\out ALL x. EX y. x = y}
{\out  1. ALL x. EX y. x = y}
\ttbreak
by (resolve_tac [allI] 1);
{\out Level 1}
{\out ALL x. EX y. x = y}
{\out  1. !!x. EX y. x = y}
\end{ttbox}
The variable~{\tt x} is no longer universally quantified, but is a
parameter in the subgoal; thus, it is universally quantified at the
meta-level.  The subgoal must be proved for all possible values of~{\tt x}.

To remove the existential quantifier, we apply the rule $(\exists I)$:
\begin{ttbox}
by (resolve_tac [exI] 1);
{\out Level 2}
{\out ALL x. EX y. x = y}
{\out  1. !!x. x = ?y1(x)}
\end{ttbox}
The bound variable {\tt y} has become {\tt?y1(x)}.  This term consists of
the function unknown~{\tt?y1} applied to the parameter~{\tt x}.
Instances of {\tt?y1(x)} may or may not contain~{\tt x}.  We resolve the
subgoal with the reflexivity axiom.
\begin{ttbox}
by (resolve_tac [refl] 1);
{\out Level 3}
{\out ALL x. EX y. x = y}
{\out No subgoals!}
\end{ttbox}
Let us consider what has happened in detail.  The reflexivity axiom is
lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is
unified with $\Forall x.x=\Var{y@1}(x)$.  The function unknowns $\Var{f}$
and~$\Var{y@1}$ are both instantiated to the identity function, and
$x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction.

\paragraph{The unsuccessful proof.}
We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and
try~$(\exists I)$:
\begin{ttbox}
goal FOL.thy "EX y. ALL x. x=y";
{\out Level 0}
{\out EX y. ALL x. x = y}
{\out  1. EX y. ALL x. x = y}
\ttbreak
by (resolve_tac [exI] 1);
{\out Level 1}
{\out EX y. ALL x. x = y}
{\out  1. ALL x. x = ?y}
\end{ttbox}
The unknown {\tt ?y} may be replaced by any term, but this can never
introduce another bound occurrence of~{\tt x}.  We now apply~$(\forall I)$:
\begin{ttbox}
by (resolve_tac [allI] 1);
{\out Level 2}
{\out EX y. ALL x. x = y}
{\out  1. !!x. x = ?y}
\end{ttbox}
Compare our position with the previous Level~2.  Instead of {\tt?y1(x)} we
have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}.
The reflexivity axiom does not unify with subgoal~1.
\begin{ttbox}
by (resolve_tac [refl] 1);
{\out by: tactic returned no results}
\end{ttbox}
There can be no proof of $\exists y.\forall x.x=y$ by the soundness of
first-order logic.  I have elsewhere proved the faithfulness of Isabelle's
encoding of first-order logic~\cite{paulson89}; there could, of course, be
faults in the implementation.


\subsection{Nested quantifiers}
\index{examples!with quantifiers}
Multiple quantifiers create complex terms.  Proving 
\[ (\forall x\,y.P(x,y)) \imp (\forall z\,w.P(w,z)) \] 
will demonstrate how parameters and unknowns develop.  If they appear in
the wrong order, the proof will fail.

This section concludes with a demonstration of {\tt REPEAT}
and~{\tt ORELSE}.  
\begin{ttbox}
goal FOL.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
{\out Level 0}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
\ttbreak
by (resolve_tac [impI] 1);
{\out Level 1}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
\end{ttbox}

\paragraph{The wrong approach.}
Using \ttindex{dresolve_tac}, we apply the rule $(\forall E)$, bound to the
\ML\ identifier \ttindex{spec}.  Then we apply $(\forall I)$.
\begin{ttbox}
by (dresolve_tac [spec] 1);
{\out Level 2}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)}
\ttbreak
by (resolve_tac [allI] 1);
{\out Level 3}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)}
\end{ttbox}
The unknown {\tt ?u} and the parameter {\tt z} have appeared.  We again
apply $(\forall E)$ and~$(\forall I)$.
\begin{ttbox}
by (dresolve_tac [spec] 1);
{\out Level 4}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)}
\ttbreak
by (resolve_tac [allI] 1);
{\out Level 5}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. !!z w. P(?x1,?y3(z)) ==> P(w,z)}
\end{ttbox}
The unknown {\tt ?y3} and the parameter {\tt w} have appeared.  Each
unknown is applied to the parameters existing at the time of its creation;
instances of {\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances
of {\tt?y3(z)} can only contain~{\tt z}.  Because of these restrictions,
proof by assumption will fail.
\begin{ttbox}
by (assume_tac 1);
{\out by: tactic returned no results}
{\out uncaught exception ERROR}
\end{ttbox}

\paragraph{The right approach.}
To do this proof, the rules must be applied in the correct order.
Eigenvariables should be created before unknowns.  The
\ttindex{choplev} command returns to an earlier stage of the proof;
let us return to the result of applying~$({\imp}I)$:
\begin{ttbox}
choplev 1;
{\out Level 1}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
\end{ttbox}
Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$.
\begin{ttbox}
by (resolve_tac [allI] 1);
{\out Level 2}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)}
\ttbreak
by (resolve_tac [allI] 1);
{\out Level 3}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. !!z w. ALL x y. P(x,y) ==> P(w,z)}
\end{ttbox}
The parameters {\tt z} and~{\tt w} have appeared.  We now create the
unknowns:
\begin{ttbox}
by (dresolve_tac [spec] 1);
{\out Level 4}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)}
\ttbreak
by (dresolve_tac [spec] 1);
{\out Level 5}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)}
\end{ttbox}
Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt
z} and~{\tt w}:
\begin{ttbox}
by (assume_tac 1);
{\out Level 6}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out No subgoals!}
\end{ttbox}

\paragraph{A one-step proof using tacticals.}
\index{tacticals} \index{examples!of tacticals} 

Repeated application of rules can be effective, but the rules should be
attempted in an order that delays the creation of unknowns.  Let us return
to the original goal using \ttindex{choplev}:
\begin{ttbox}
choplev 0;
{\out Level 0}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
\end{ttbox}
As we have just seen, \ttindex{allI} should be attempted
before~\ttindex{spec}, while \ttindex{assume_tac} generally can be
attempted first.  Such priorities can easily be expressed
using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}.
\begin{ttbox}
by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1
     ORELSE dresolve_tac [spec] 1));
{\out Level 1}
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
{\out No subgoals!}
\end{ttbox}


\subsection{A realistic quantifier proof}
\index{examples!with quantifiers}
To see the practical use of parameters and unknowns, let us prove half of
the equivalence 
\[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \]
We state the left-to-right half to Isabelle in the normal way.
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we
use \ttindex{REPEAT}:
\begin{ttbox}
goal FOL.thy "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q";
{\out Level 0}
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
{\out  1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
\ttbreak
by (REPEAT (resolve_tac [impI] 1));
{\out Level 1}
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
{\out  1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q}
\end{ttbox}
We can eliminate the universal or the existential quantifier.  The
existential quantifier should be eliminated first, since this creates a
parameter.  The rule~$(\exists E)$ is bound to the
identifier~\ttindex{exE}.
\begin{ttbox}
by (eresolve_tac [exE] 1);
{\out Level 2}
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
{\out  1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q}
\end{ttbox}
The only possibility now is $(\forall E)$, a destruction rule.  We use 
\ttindex{dresolve_tac}, which discards the quantified assumption; it is
only needed once.
\begin{ttbox}
by (dresolve_tac [spec] 1);
{\out Level 3}
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
{\out  1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q}
\end{ttbox}
Because we applied $(\exists E)$ before $(\forall E)$, the unknown
term~{\tt?x3(x)} may depend upon the parameter~{\tt x}.

Although $({\imp}E)$ is a destruction rule, it works with 
\ttindex{eresolve_tac} to perform backward chaining.  This technique is
frequently useful.  
\begin{ttbox}
by (eresolve_tac [mp] 1);
{\out Level 4}
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
{\out  1. !!x. P(x) ==> P(?x3(x))}
\end{ttbox}
The tactic has reduced~{\tt Q} to~{\tt P(?x3(x))}, deleting the
implication.  The final step is trivial, thanks to the occurrence of~{\tt x}.
\begin{ttbox}
by (assume_tac 1);
{\out Level 5}
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
{\out No subgoals!}
\end{ttbox}


\subsection{The classical reasoning package}
\index{classical reasoning package}
Although Isabelle cannot compete with fully automatic theorem provers, it
provides enough automation to tackle substantial examples.  The classical
reasoning package can be set up for any classical natural deduction logic
--- see the {\em Reference Manual}.

Rules are packaged into bundles called \bfindex{classical sets}.  The package
provides several tactics, which apply rules using naive algorithms, using
unification to handle quantifiers.  The most useful tactic
is~\ttindex{fast_tac}.  

Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The
backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape
sequence, to break the long string over two lines.)
\begin{ttbox}
goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \ttback
\ttback       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
{\out Level 0}
{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
{\out  1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
{\out     ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
\end{ttbox}
The rules of classical logic are bundled as {\tt FOL_cs}.  We may solve
subgoal~1 at a stroke, using~\ttindex{fast_tac}.
\begin{ttbox}
by (fast_tac FOL_cs 1);
{\out Level 1}
{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
{\out No subgoals!}
\end{ttbox}
Sceptics may examine the proof by calling the package's single-step
tactics, such as~{\tt step_tac}.  This would take up much space, however,
so let us proceed to the next example:
\begin{ttbox}
goal FOL.thy "ALL x. P(x,f(x)) <-> \ttback
\ttback       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
{\out Level 0}
{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
{\out  1. ALL x. P(x,f(x)) <->}
{\out     (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
\end{ttbox}
Again, subgoal~1 succumbs immediately.
\begin{ttbox}
by (fast_tac FOL_cs 1);
{\out Level 1}
{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
{\out No subgoals!}
\end{ttbox}
The classical reasoning package is not restricted to the usual logical
connectives.  The natural deduction rules for unions and intersections in
set theory resemble those for disjunction and conjunction, and in the
infinitary case, for quantifiers.  The package is valuable for reasoning in
set theory.


% Local Variables: 
% mode: latex
% TeX-master: t
% End: