%% $Id$

\part{Using Isabelle from the ML Top-Level}\label{chap:getting}

Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however.  

Proofs are conducted by

applying certain \ML{} functions, which update a stored proof state.

All syntax can be expressed using plain {\sc ascii}

characters, but Isabelle can support

alternative syntaxes, for example using mathematical symbols from a

special screen font.  The meta-logic and main 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 \texttt{typ},

\texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic};

tacticals have function types such as \texttt{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.  The examples are set in first-order logic.

The command to start Isabelle running first-order logic is

\begin{ttbox}

isabelle FOL

\end{ttbox}

Note that just typing \texttt{isabelle} usually brings up higher-order logic

(HOL) by default.

\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 \texttt{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 \texttt{'a::term} and \texttt{?'b::\ttlbrace

  ord, arith\ttrbrace}.

\[\dquotes

\index{*:: symbol}\index{*=> symbol}

\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}

\index{*[ symbol}\index{*] symbol}

\begin{array}{ll}

    \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline

  \alpha "::" C              & \hbox{class constraint} \\

  \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &

        \hbox{sort constraint} \\

  \sigma " => " \tau        & \hbox{function type } \sigma\To\tau \\

  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau 

       & \hbox{$n$-argument function type} \\

  "(" \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}{ll}

    \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline

  t "::" \sigma         & \hbox{type constraint} \\

  "\%" x "." t          & \hbox{abstraction } \lambda x.t \\

  "\%" x@1\ldots x@n "." t  & \hbox{abstraction over several arguments} \\

  t "(" u@1"," \ldots "," u@n ")" &

     \hbox{application to several arguments (FOL and ZF)} \\

  t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}

\end{array}  

\]

Note that HOL uses its traditional ``higher-order'' syntax for application,

which differs from that used in FOL.

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~\texttt{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 \texttt{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 \texttt{prth}, \texttt{prths} and~{\tt

  prthq}.  Of the other operations on theorems, most useful are \texttt{RS}

and \texttt{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{\out 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 \texttt{prth} omit the quotes and the surrounding \texttt{val

  \ldots :\ thm}.  Ignoring their side-effects, the printing commands are 

identity functions.

To contrast \texttt{RS} with \texttt{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 \texttt{mp} and {\tt

  conjunct1}.  In \ML{}, the identifier~\texttt{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 \texttt{RS} and~\texttt{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 = "EX x. ?a3(x) = ?a2(x)"  [.] : thm}

\end{ttbox}

%

The mysterious symbol \texttt{[.]} indicates that the result is subject to 

a meta-level hypothesis. We can make all such hypotheses visible by setting the 

\ttindexbold{show_hyps} flag:

\begin{ttbox} 

set show_hyps;

{\out val it = true : bool}

refl RS exI;

{\out val it = "EX x. ?a3(x) = ?a2(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 \texttt{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}

{\out    THM ("RSN: multiple unifiers", 1,}

{\out         ["k = k", "?P(?x) ==> EX x. ?P(x)"])}

\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 \texttt{RS} and \texttt{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 \texttt{assume_tac}, {\tt

resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most

single-step proofs.  Although \texttt{eresolve_tac} and \texttt{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 \texttt{resolve_tac~{\it thms}~{\it i\/}}

  followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its

  first premise by assumption.  But \texttt{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 formula}; ] 

begins a new proof, where 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 \texttt{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 \texttt{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 \texttt{FOL/ex/intro.ML}.}

\begin{ttbox}

Goal "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 \texttt{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~\texttt{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 \texttt{qed} stores the theorem.

\begin{ttbox}

qed "mythm";

{\out val mythm = "?P | ?P --> ?P" : thm} 

\end{ttbox}

Isabelle has replaced the free variable~\texttt{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 \texttt{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 "(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 \texttt{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 \texttt{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 \texttt{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 \texttt{assume_tac} can finish the proof.  The

tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{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 "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~\texttt{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~\texttt{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 \texttt{y} has become {\tt?y1(x)}.  This term consists of

the function unknown~{\tt?y1} applied to the parameter~\texttt{x}.

Instances of {\tt?y1(x)} may or may not contain~\texttt{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 "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 \texttt{?y} may be replaced by any term, but this can never

introduce another bound occurrence of~\texttt{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~\texttt{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 \texttt{REPEAT}

and~\texttt{ORELSE}.  

\begin{ttbox}

Goal "(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 \texttt{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 \texttt{?x1} and the parameter \texttt{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 \texttt{?y3} and the parameter \texttt{w} have appeared.  Each

unknown is applied to the parameters existing at the time of its creation;

instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances

of {\tt?y3(z)} can only contain~\texttt{z}.  Due to the restriction on~\texttt{?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 \texttt{z} and~\texttt{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~\texttt{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 \texttt{REPEAT}:

\begin{ttbox}

Goal "(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~\texttt{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~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the

implication.  The final step is trivial, thanks to the occurrence of~\texttt{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}

Isabelle 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}}. 

It cannot compete with fully automatic theorem provers, but it is 

competitive with tools found in other interactive provers.

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 "(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~\texttt{step_tac}.  This would take up much space, however,

so let us proceed to the next example:

\begin{ttbox}

Goal "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.