doc-src/Intro/getting.tex

remove FIXME;

%% $Id$
\part{Getting Started with Isabelle}\label{chap:getting}
Let us consider how to perform simple proofs using Isabelle.  At
present, Isabelle's user interface is \ML.  Proofs are conducted by
applying certain \ML{} functions, which update a stored proof state.
Basically, all syntax must be expressed using plain {\sc ascii}
characters. There are also mechanisms built into Isabelle that support
alternative syntaxes, for example using mathematical symbols from a
special screen font. The meta-logic and major object-logics already
provide such fancy output as an option.

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}\label{sec:forward} \index{forward proof|(}
This section describes the concrete syntax for types, terms and theorems,
and demonstrates forward proof.

\subsection{Lexical matters}
\index{identifiers}\index{reserved words} 
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 {\bf type identifier} consists of an identifier prefixed by a
prime, for example {\tt'a} and \hbox{\tt'hello}.  Type identifiers stand
for (free) type variables, which remain fixed during a proof.
\index{type identifiers}

An {\bf unknown}\index{unknowns} (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{classes!built-in|bold}\index{syntax!of types and terms}

Classes are denoted by identifiers; the built-in class \cldx{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 of|bold}\index{sort constraints} Types are written
with a syntax like \ML's.  The built-in type \tydx{prop} is the type
of propositions.  Type variables can be constrained to particular
classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\ttlbrace
  ord, arith\ttrbrace}.
\[\dquotes
\index{*:: symbol}\index{*=> symbol}
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
\index{*[ symbol}\index{*] symbol}
\begin{array}{lll}
    \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
  \alpha "::" C              & \alpha :: C        & \hbox{class constraint} \\
  \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
     \alpha :: \{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 of|bold}\index{type constraints}
\[\dquotes
\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions}
\index{*:: symbol}
\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~{\tt prop}.  
\index{meta-implication}
\index{meta-quantifiers}\index{meta-equality}
\index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol}
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
\[\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 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 constraints}

\index{*Trueprop constant}
Most logics define the implicit coercion $Trueprop$ from object-formulae to
propositions.  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~\tydx{prop} are seldom
useful, but you can make a variable stand for a meta-formula by prefixing
it with the symbol {\tt PROP}:\index{*PROP symbol}
\begin{ttbox} 
PROP ?psi ==> PROP ?theta 
\end{ttbox}

Symbols of object-logics are typically rendered into {\sc ascii} 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) $$
$({\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 system}
Meta-level theorems have the \ML{} type \mltydx{thm}.  They 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{theorems!printing of}
\begin{ttdescription}
\item[\ttindex{prth} {\it thm};]
  pretty-prints {\it thm\/} at the terminal.

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

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

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

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

\item[\ttindex{standard} $thm$]  
  puts $thm$ into a standard format.  It also renames schematic variables
  to have subscript zero, improving readability and reducing subscript
  growth.
\end{ttdescription}
The rules of a theory are normally bound to \ML\ identifiers.  Suppose we
are running an Isabelle session containing theory~\FOL, natural deduction
first-order logic.\footnote{For a listing of the \FOL{} rules and their
  \ML{} names, turn to
\iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
           {page~\pageref{fol-rules}}.}
Let us try an example given in~\S\ref{joining}.  We
first print \tdx{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 {\footnotesize\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.  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
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{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
\tdx{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.
\index{assumptions!use of}

\subsection{*Flex-flex constraints} \label{flexflex}
\index{flex-flex constraints|bold}\index{unknowns!function}
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 \tdx{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}

\index{forward proof|)}

\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}
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{ttdescription}
\item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption}
  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[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution}
  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[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution}
  performs elim-resolution.  Like {\tt resolve_tac~{\it thms}~{\it i\/}}
  followed by {\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[\ttindex{dresolve_tac} {\it thms} {\it i}]
  \index{forward proof}\index{destruct-resolution}
  performs destruct-resolution with the~$thms$, as described
  in~\S\ref{destruct}.  It is useful for forward reasoning from the
  assumptions.
\end{ttdescription}

\subsection{Commands for backward proof}
\index{proofs!commands for}
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{ttdescription}
\item[\ttindex{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[\ttindex{by} {\it tactic}; ] 
applies the {\it tactic\/} to the current proof
state, raising an exception if the tactic fails.

\item[\ttindex{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[\ttindex{result}();]
returns the theorem just proved, in a standard format.  It fails if
unproved subgoals are left, etc.

\item[\ttindex{qed} {\it name};] is the usual way of ending a proof.
  It gets the theorem using {\tt result}, stores it in Isabelle's
  theorem database and binds it to an \ML{} identifier.

\end{ttdescription}
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
\index{*br} \index{*be} \index{*bd} \index{*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}\index{level of a proof}
Isabelle responds by printing the initial proof state, which has $P\disj
P\imp P$ as the main goal and the only subgoal.  The {\bf 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 \tdx{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
\tdx{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 {\tt qed} stores the theorem.
\begin{ttbox}
qed "mythm";
{\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 {\tt 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 {\tt assume_tac} can finish the proof.  The
tactical~\ttindex{REPEAT} here 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}\index{parameters}\index{unknowns}\index{unknowns!function}
This section illustrates how Isabelle enforces quantifier provisos.
Suppose that $x$, $y$ and~$z$ are parameters of a subgoal.  Quantifier
rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function
unknown.  Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of
replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free
occurrences of~$x$ and~$z$.  On the other hand, no instantiation
of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free
occurrences of~$y$, since parameters are bound variables.

\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{paulson-found}.  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 failed}
\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{paulson-found}; 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 {\tt dresolve_tac}, we apply the rule $(\forall E)$, bound to the
\ML\ identifier \tdx{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 ?x1} 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}.  Due to the restriction on~{\tt ?x1},
proof by assumption will fail.
\begin{ttbox}
by (assume_tac 1);
{\out by: tactic failed}
{\out uncaught exception ERROR}
\end{ttbox}

\paragraph{The right approach.}
To do this proof, the rules must be applied in the correct order.
Parameters 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 the correct order.  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, \tdx{allI} should be attempted
before~\tdx{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 {\tt 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~\tdx{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 reasoner}
\index{classical reasoner}
Although Isabelle cannot compete with fully automatic theorem provers, it
provides enough automation to tackle substantial examples.  The classical
reasoner can be set up for any classical natural deduction logic;
see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
        {Chap.\ts\ref{chap:classical}}. 

Rules are packaged into {\bf classical sets}.  The classical reasoner
provides several tactics, which apply rules using naive algorithms.
Unification handles quantifiers as shown above.  The most useful tactic
is~\ttindex{Blast_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}
\ttindex{Blast_tac} proves subgoal~1 at a stroke.
\begin{ttbox}
by (Blast_tac 1);
{\out Depth = 0}
{\out Depth = 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 (Blast_tac 1);
{\out Depth = 0}
{\out Depth = 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 reasoner is not restricted to the usual logical connectives.
The natural deduction rules for unions and intersections resemble those for
disjunction and conjunction.  The rules for infinite unions and
intersections resemble those for quantifiers.  Given such rules, the classical
reasoner is effective for reasoning in set theory.