doc-src/Intro/getting.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 5205 602354039306
child 14148 6580d374a509
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
lcp@105
     1
%% $Id$
lcp@296
     2
\part{Getting Started with Isabelle}\label{chap:getting}
wenzelm@3103
     3
Let us consider how to perform simple proofs using Isabelle.  At
wenzelm@3103
     4
present, Isabelle's user interface is \ML.  Proofs are conducted by
wenzelm@3103
     5
applying certain \ML{} functions, which update a stored proof state.
wenzelm@3103
     6
Basically, all syntax must be expressed using plain {\sc ascii}
paulson@3485
     7
characters.  There are also mechanisms built into Isabelle that support
wenzelm@3103
     8
alternative syntaxes, for example using mathematical symbols from a
paulson@3485
     9
special screen font.  The meta-logic and major object-logics already
wenzelm@3103
    10
provide such fancy output as an option.
lcp@105
    11
wenzelm@3103
    12
Object-logics are built upon Pure Isabelle, which implements the
wenzelm@3103
    13
meta-logic and provides certain fundamental data structures: types,
wenzelm@3103
    14
terms, signatures, theorems and theories, tactics and tacticals.
paulson@5205
    15
These data structures have the corresponding \ML{} types \texttt{typ},
paulson@5205
    16
\texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic};
paulson@5205
    17
tacticals have function types such as \texttt{tactic->tactic}.  Isabelle
wenzelm@3103
    18
users can operate on these data structures by writing \ML{} programs.
lcp@105
    19
paulson@4802
    20
lcp@311
    21
\section{Forward proof}\label{sec:forward} \index{forward proof|(}
lcp@105
    22
This section describes the concrete syntax for types, terms and theorems,
paulson@4802
    23
and demonstrates forward proof.  The examples are set in first-order logic.
paulson@4802
    24
The command to start Isabelle running first-order logic is
paulson@4802
    25
\begin{ttbox}
paulson@4802
    26
isabelle FOL
paulson@4802
    27
\end{ttbox}
paulson@4802
    28
Note that just typing \texttt{isabelle} usually brings up higher-order logic
wenzelm@9695
    29
(HOL) by default.
paulson@4802
    30
lcp@105
    31
lcp@105
    32
\subsection{Lexical matters}
lcp@311
    33
\index{identifiers}\index{reserved words} 
lcp@105
    34
An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|)
lcp@105
    35
and single quotes~({\tt'}), beginning with a letter.  Single quotes are
paulson@5205
    36
regarded as primes; for instance \texttt{x'} is read as~$x'$.  Identifiers are
lcp@105
    37
separated by white space and special characters.  {\bf Reserved words} are
lcp@105
    38
identifiers that appear in Isabelle syntax definitions.
lcp@105
    39
lcp@105
    40
An Isabelle theory can declare symbols composed of special characters, such
lcp@105
    41
as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}.  (The latter three are part of
lcp@105
    42
the syntax of the meta-logic.)  Such symbols may be run together; thus if
lcp@105
    43
\verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is
lcp@105
    44
valid notation for a set of sets --- but only if \verb|}}| and \verb|{{|
lcp@105
    45
have not been declared as symbols!  The parser resolves any ambiguity by
lcp@105
    46
taking the longest possible symbol that has been declared.  Thus the string
lcp@105
    47
{\tt==>} is read as a single symbol.  But \hbox{\tt= =>} is read as two
lcp@296
    48
symbols.
lcp@105
    49
lcp@105
    50
Identifiers that are not reserved words may serve as free variables or
lcp@331
    51
constants.  A {\bf type identifier} consists of an identifier prefixed by a
lcp@331
    52
prime, for example {\tt'a} and \hbox{\tt'hello}.  Type identifiers stand
lcp@331
    53
for (free) type variables, which remain fixed during a proof.
lcp@331
    54
\index{type identifiers}
lcp@331
    55
lcp@331
    56
An {\bf unknown}\index{unknowns} (or type unknown) consists of a question
lcp@331
    57
mark, an identifier (or type identifier), and a subscript.  The subscript,
lcp@331
    58
a non-negative integer,
lcp@331
    59
allows the renaming of unknowns prior to unification.%
lcp@296
    60
\footnote{The subscript may appear after the identifier, separated by a
lcp@296
    61
  dot; this prevents ambiguity when the identifier ends with a digit.  Thus
lcp@296
    62
  {\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5}
lcp@296
    63
  has identifier {\tt"a0"} and subscript~5.  If the identifier does not
lcp@296
    64
  end with a digit, then no dot appears and a subscript of~0 is omitted;
lcp@296
    65
  for example, {\tt?hello} has identifier {\tt"hello"} and subscript
lcp@296
    66
  zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6.  The same
lcp@296
    67
  conventions apply to type unknowns.  The question mark is {\it not\/}
lcp@296
    68
  part of the identifier!}
lcp@105
    69
lcp@105
    70
lcp@105
    71
\subsection{Syntax of types and terms}
lcp@311
    72
\index{classes!built-in|bold}\index{syntax!of types and terms}
lcp@311
    73
lcp@311
    74
Classes are denoted by identifiers; the built-in class \cldx{logic}
lcp@105
    75
contains the `logical' types.  Sorts are lists of classes enclosed in
lcp@296
    76
braces~\} and \{; singleton sorts may be abbreviated by dropping the braces.
lcp@105
    77
wenzelm@3103
    78
\index{types!syntax of|bold}\index{sort constraints} Types are written
wenzelm@3103
    79
with a syntax like \ML's.  The built-in type \tydx{prop} is the type
wenzelm@3103
    80
of propositions.  Type variables can be constrained to particular
paulson@5205
    81
classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace
wenzelm@3103
    82
  ord, arith\ttrbrace}.
lcp@105
    83
\[\dquotes
lcp@311
    84
\index{*:: symbol}\index{*=> symbol}
lcp@311
    85
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
lcp@311
    86
\index{*[ symbol}\index{*] symbol}
paulson@4802
    87
\begin{array}{ll}
paulson@4802
    88
    \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline
paulson@4802
    89
  \alpha "::" C              & \hbox{class constraint} \\
wenzelm@3103
    90
  \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
paulson@4802
    91
        \hbox{sort constraint} \\
paulson@4802
    92
  \sigma " => " \tau        & \hbox{function type } \sigma\To\tau \\
paulson@4802
    93
  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau 
paulson@4802
    94
       & \hbox{$n$-argument function type} \\
paulson@4802
    95
  "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction}
lcp@105
    96
\end{array} 
lcp@105
    97
\]
lcp@105
    98
Terms are those of the typed $\lambda$-calculus.
lcp@331
    99
\index{terms!syntax of|bold}\index{type constraints}
lcp@105
   100
\[\dquotes
lcp@311
   101
\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions}
lcp@311
   102
\index{*:: symbol}
paulson@4802
   103
\begin{array}{ll}
paulson@4802
   104
    \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
paulson@4802
   105
  t "::" \sigma         & \hbox{type constraint} \\
paulson@4802
   106
  "\%" x "." t          & \hbox{abstraction } \lambda x.t \\
paulson@4802
   107
  "\%" x@1\ldots x@n "." t  & \hbox{abstraction over several arguments} \\
paulson@4802
   108
  t "(" u@1"," \ldots "," u@n ")" &
paulson@4802
   109
     \hbox{application to several arguments (FOL and ZF)} \\
paulson@4802
   110
  t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}
lcp@105
   111
\end{array}  
lcp@105
   112
\]
wenzelm@9695
   113
Note that HOL uses its traditional ``higher-order'' syntax for application,
wenzelm@9695
   114
which differs from that used in FOL.
paulson@4802
   115
lcp@105
   116
The theorems and rules of an object-logic are represented by theorems in
lcp@105
   117
the meta-logic, which are expressed using meta-formulae.  Since the
lcp@105
   118
meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}
paulson@5205
   119
are just terms of type~\texttt{prop}.  
lcp@311
   120
\index{meta-implication}
lcp@311
   121
\index{meta-quantifiers}\index{meta-equality}
lcp@311
   122
\index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol}
lcp@311
   123
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
lcp@105
   124
\[\dquotes
lcp@105
   125
  \begin{array}{l@{\quad}l@{\quad}l}
lcp@105
   126
    \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline
lcp@105
   127
  a " == " b    & a\equiv b &   \hbox{meta-equality} \\
lcp@105
   128
  a " =?= " b   & a\qeq b &     \hbox{flex-flex constraint} \\
lcp@105
   129
  \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\
lcp@105
   130
  "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & 
lcp@105
   131
  \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\
lcp@105
   132
  "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\
lcp@105
   133
  "!!" x@1\ldots x@n "." \phi & 
wenzelm@3103
   134
  \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification}
lcp@105
   135
  \end{array}
lcp@105
   136
\]
lcp@105
   137
Flex-flex constraints are meta-equalities arising from unification; they
lcp@105
   138
require special treatment.  See~\S\ref{flexflex}.
lcp@311
   139
\index{flex-flex constraints}
lcp@105
   140
lcp@311
   141
\index{*Trueprop constant}
lcp@105
   142
Most logics define the implicit coercion $Trueprop$ from object-formulae to
lcp@311
   143
propositions.  This could cause an ambiguity: in $P\Imp Q$, do the
lcp@311
   144
variables $P$ and $Q$ stand for meta-formulae or object-formulae?  If the
lcp@311
   145
latter, $P\Imp Q$ really abbreviates $Trueprop(P)\Imp Trueprop(Q)$.  To
lcp@311
   146
prevent such ambiguities, Isabelle's syntax does not allow a meta-formula
lcp@311
   147
to consist of a variable.  Variables of type~\tydx{prop} are seldom
lcp@311
   148
useful, but you can make a variable stand for a meta-formula by prefixing
paulson@5205
   149
it with the symbol \texttt{PROP}:\index{*PROP symbol}
lcp@105
   150
\begin{ttbox} 
lcp@105
   151
PROP ?psi ==> PROP ?theta 
lcp@105
   152
\end{ttbox}
lcp@105
   153
wenzelm@3103
   154
Symbols of object-logics are typically rendered into {\sc ascii} as
wenzelm@3103
   155
follows:
lcp@105
   156
\[ \begin{tabular}{l@{\quad}l@{\quad}l}
lcp@105
   157
      \tt True          & $\top$        & true \\
lcp@105
   158
      \tt False         & $\bot$        & false \\
lcp@105
   159
      \tt $P$ \& $Q$    & $P\conj Q$    & conjunction \\
lcp@105
   160
      \tt $P$ | $Q$     & $P\disj Q$    & disjunction \\
lcp@105
   161
      \verb'~' $P$      & $\neg P$      & negation \\
lcp@105
   162
      \tt $P$ --> $Q$   & $P\imp Q$     & implication \\
lcp@105
   163
      \tt $P$ <-> $Q$   & $P\bimp Q$    & bi-implication \\
lcp@105
   164
      \tt ALL $x\,y\,z$ .\ $P$  & $\forall x\,y\,z.P$   & for all \\
lcp@105
   165
      \tt EX  $x\,y\,z$ .\ $P$  & $\exists x\,y\,z.P$   & there exists
lcp@105
   166
   \end{tabular}
lcp@105
   167
\]
lcp@105
   168
To illustrate the notation, consider two axioms for first-order logic:
lcp@105
   169
$$ \List{P; Q} \Imp P\conj Q                 \eqno(\conj I) $$
wenzelm@3103
   170
$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
wenzelm@3103
   171
$({\conj}I)$ translates into {\sc ascii} characters as
lcp@105
   172
\begin{ttbox}
lcp@105
   173
[| ?P; ?Q |] ==> ?P & ?Q
lcp@105
   174
\end{ttbox}
lcp@296
   175
The schematic variables let unification instantiate the rule.  To avoid
lcp@296
   176
cluttering logic definitions with question marks, Isabelle converts any
lcp@296
   177
free variables in a rule to schematic variables; we normally declare
lcp@296
   178
$({\conj}I)$ as
lcp@105
   179
\begin{ttbox}
lcp@105
   180
[| P; Q |] ==> P & Q
lcp@105
   181
\end{ttbox}
lcp@105
   182
This variables convention agrees with the treatment of variables in goals.
lcp@105
   183
Free variables in a goal remain fixed throughout the proof.  After the
lcp@105
   184
proof is finished, Isabelle converts them to scheme variables in the
lcp@105
   185
resulting theorem.  Scheme variables in a goal may be replaced by terms
lcp@105
   186
during the proof, supporting answer extraction, program synthesis, and so
lcp@105
   187
forth.
lcp@105
   188
lcp@105
   189
For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as
lcp@105
   190
\begin{ttbox}
lcp@105
   191
[| EX x.P(x);  !!x. P(x) ==> Q |] ==> Q
lcp@105
   192
\end{ttbox}
lcp@105
   193
lcp@105
   194
lcp@105
   195
\subsection{Basic operations on theorems}
lcp@105
   196
\index{theorems!basic operations on|bold}
lcp@311
   197
\index{LCF system}
lcp@331
   198
Meta-level theorems have the \ML{} type \mltydx{thm}.  They represent the
lcp@331
   199
theorems and inference rules of object-logics.  Isabelle's meta-logic is
lcp@331
   200
implemented using the {\sc lcf} approach: each meta-level inference rule is
lcp@331
   201
represented by a function from theorems to theorems.  Object-level rules
lcp@331
   202
are taken as axioms.
lcp@105
   203
paulson@5205
   204
The main theorem printing commands are \texttt{prth}, \texttt{prths} and~{\tt
paulson@5205
   205
  prthq}.  Of the other operations on theorems, most useful are \texttt{RS}
paulson@5205
   206
and \texttt{RSN}, which perform resolution.
lcp@105
   207
lcp@311
   208
\index{theorems!printing of}
lcp@311
   209
\begin{ttdescription}
lcp@311
   210
\item[\ttindex{prth} {\it thm};]
lcp@311
   211
  pretty-prints {\it thm\/} at the terminal.
lcp@105
   212
lcp@311
   213
\item[\ttindex{prths} {\it thms};]
lcp@311
   214
  pretty-prints {\it thms}, a list of theorems.
lcp@105
   215
lcp@311
   216
\item[\ttindex{prthq} {\it thmq};]
lcp@311
   217
  pretty-prints {\it thmq}, a sequence of theorems; this is useful for
lcp@311
   218
  inspecting the output of a tactic.
lcp@105
   219
lcp@311
   220
\item[$thm1$ RS $thm2$] \index{*RS} 
lcp@311
   221
  resolves the conclusion of $thm1$ with the first premise of~$thm2$.
lcp@105
   222
lcp@311
   223
\item[$thm1$ RSN $(i,thm2)$] \index{*RSN} 
lcp@311
   224
  resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$.
lcp@105
   225
lcp@311
   226
\item[\ttindex{standard} $thm$]  
lcp@311
   227
  puts $thm$ into a standard format.  It also renames schematic variables
lcp@311
   228
  to have subscript zero, improving readability and reducing subscript
lcp@311
   229
  growth.
lcp@311
   230
\end{ttdescription}
wenzelm@9695
   231
The rules of a theory are normally bound to \ML\ identifiers.  Suppose we are
wenzelm@9695
   232
running an Isabelle session containing theory~FOL, natural deduction
wenzelm@9695
   233
first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
wenzelm@9695
   234
  names, turn to
lcp@331
   235
\iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
lcp@331
   236
           {page~\pageref{fol-rules}}.}
lcp@331
   237
Let us try an example given in~\S\ref{joining}.  We
lcp@331
   238
first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with
lcp@331
   239
itself.
lcp@105
   240
\begin{ttbox} 
lcp@105
   241
prth mp; 
lcp@105
   242
{\out [| ?P --> ?Q; ?P |] ==> ?Q}
lcp@105
   243
{\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm}
lcp@105
   244
prth (mp RS mp);
lcp@105
   245
{\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}
lcp@105
   246
{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
lcp@105
   247
\end{ttbox}
lcp@331
   248
User input appears in {\footnotesize\tt typewriter characters}, and output
paulson@4244
   249
appears in{\out slanted typewriter characters}.  \ML's response {\out val
lcp@331
   250
  }~\ldots{} is compiler-dependent and will sometimes be suppressed.  This
lcp@331
   251
session illustrates two formats for the display of theorems.  Isabelle's
lcp@331
   252
top-level displays theorems as \ML{} values, enclosed in quotes.  Printing
paulson@5205
   253
commands like \texttt{prth} omit the quotes and the surrounding \texttt{val
lcp@331
   254
  \ldots :\ thm}.  Ignoring their side-effects, the commands are identity
lcp@331
   255
functions.
lcp@105
   256
paulson@5205
   257
To contrast \texttt{RS} with \texttt{RSN}, we resolve
lcp@311
   258
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}.
lcp@105
   259
\begin{ttbox} 
lcp@105
   260
conjunct1 RS mp;
lcp@105
   261
{\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm}
lcp@105
   262
conjunct1 RSN (2,mp);
lcp@105
   263
{\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm}
lcp@105
   264
\end{ttbox}
lcp@105
   265
These correspond to the following proofs:
lcp@105
   266
\[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P}
lcp@105
   267
   \qquad
lcp@105
   268
   \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}} 
lcp@105
   269
\]
lcp@296
   270
%
lcp@296
   271
Rules can be derived by pasting other rules together.  Let us join
paulson@5205
   272
\tdx{spec}, which stands for~$(\forall E)$, with \texttt{mp} and {\tt
paulson@5205
   273
  conjunct1}.  In \ML{}, the identifier~\texttt{it} denotes the value just
lcp@296
   274
printed.
lcp@105
   275
\begin{ttbox} 
lcp@105
   276
spec;
lcp@105
   277
{\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm}
lcp@105
   278
it RS mp;
lcp@296
   279
{\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==>}
lcp@296
   280
{\out           ?Q2(?x1)" : thm}
lcp@105
   281
it RS conjunct1;
lcp@296
   282
{\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>}
lcp@296
   283
{\out           ?P6(?x2)" : thm}
lcp@105
   284
standard it;
lcp@296
   285
{\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>}
lcp@296
   286
{\out           ?Pa(?x)" : thm}
lcp@105
   287
\end{ttbox}
lcp@105
   288
By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have
lcp@105
   289
derived a destruction rule for formulae of the form $\forall x.
lcp@105
   290
P(x)\imp(Q(x)\conj R(x))$.  Used with destruct-resolution, such specialized
lcp@105
   291
rules provide a way of referring to particular assumptions.
lcp@311
   292
\index{assumptions!use of}
lcp@105
   293
lcp@311
   294
\subsection{*Flex-flex constraints} \label{flexflex}
lcp@311
   295
\index{flex-flex constraints|bold}\index{unknowns!function}
lcp@105
   296
In higher-order unification, {\bf flex-flex} equations are those where both
lcp@105
   297
sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$.
lcp@105
   298
They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and
lcp@105
   299
$\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown.  They
lcp@105
   300
admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$
lcp@105
   301
and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$.  Huet's
lcp@105
   302
procedure does not enumerate the unifiers; instead, it retains flex-flex
lcp@105
   303
equations as constraints on future unifications.  Flex-flex constraints
lcp@105
   304
occasionally become attached to a proof state; more frequently, they appear
paulson@5205
   305
during use of \texttt{RS} and~\texttt{RSN}:
lcp@105
   306
\begin{ttbox} 
lcp@105
   307
refl;
lcp@105
   308
{\out val it = "?a = ?a" : thm}
lcp@105
   309
exI;
lcp@105
   310
{\out val it = "?P(?x) ==> EX x. ?P(x)" : thm}
lcp@105
   311
refl RS exI;
lcp@105
   312
{\out val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm}
lcp@105
   313
\end{ttbox}
lcp@105
   314
lcp@105
   315
\noindent
lcp@105
   316
Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with
lcp@105
   317
the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$.  Instances
lcp@105
   318
satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and
lcp@105
   319
$\exists x.x=\Var{u}$.  Calling \ttindex{flexflex_rule} removes all
lcp@105
   320
constraints by applying the trivial unifier:\index{*prthq}
lcp@105
   321
\begin{ttbox} 
lcp@105
   322
prthq (flexflex_rule it);
lcp@105
   323
{\out EX x. ?a4 = ?a4}
lcp@105
   324
\end{ttbox} 
lcp@105
   325
Isabelle simplifies flex-flex equations to eliminate redundant bound
lcp@105
   326
variables.  In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$,
lcp@105
   327
there is no bound occurrence of~$x$ on the right side; thus, there will be
lcp@296
   328
none on the left in a common instance of these terms.  Choosing a new
lcp@105
   329
variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$,
lcp@105
   330
simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$.  Dropping $x$
lcp@105
   331
from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda
lcp@105
   332
y.\Var{g}(y)$.  By $\eta$-conversion, this simplifies to the assignment
lcp@105
   333
$\Var{g}\equiv\lambda y.?h(k(y))$.
lcp@105
   334
lcp@105
   335
\begin{warn}
paulson@5205
   336
\ttindex{RS} and \ttindex{RSN} fail (by raising exception \texttt{THM}) unless
lcp@105
   337
the resolution delivers {\bf exactly one} resolvent.  For multiple results,
lcp@105
   338
use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists.  The
lcp@105
   339
following example uses \ttindex{read_instantiate} to create an instance
lcp@311
   340
of \tdx{refl} containing no schematic variables.
lcp@105
   341
\begin{ttbox} 
lcp@105
   342
val reflk = read_instantiate [("a","k")] refl;
lcp@105
   343
{\out val reflk = "k = k" : thm}
lcp@105
   344
\end{ttbox}
lcp@105
   345
lcp@105
   346
\noindent
lcp@105
   347
A flex-flex constraint is no longer possible; resolution does not find a
lcp@105
   348
unique unifier:
lcp@105
   349
\begin{ttbox} 
lcp@105
   350
reflk RS exI;
lcp@105
   351
{\out uncaught exception THM}
lcp@105
   352
\end{ttbox}
lcp@105
   353
Using \ttindex{RL} this time, we discover that there are four unifiers, and
lcp@105
   354
four resolvents:
lcp@105
   355
\begin{ttbox} 
lcp@105
   356
[reflk] RL [exI];
lcp@105
   357
{\out val it = ["EX x. x = x", "EX x. k = x",}
lcp@105
   358
{\out           "EX x. x = k", "EX x. k = k"] : thm list}
lcp@105
   359
\end{ttbox} 
lcp@105
   360
\end{warn}
lcp@105
   361
lcp@311
   362
\index{forward proof|)}
lcp@105
   363
lcp@105
   364
\section{Backward proof}
paulson@5205
   365
Although \texttt{RS} and \texttt{RSN} are fine for simple forward reasoning,
lcp@105
   366
large proofs require tactics.  Isabelle provides a suite of commands for
lcp@105
   367
conducting a backward proof using tactics.
lcp@105
   368
lcp@105
   369
\subsection{The basic tactics}
paulson@5205
   370
The tactics \texttt{assume_tac}, {\tt
paulson@5205
   371
resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most
paulson@5205
   372
single-step proofs.  Although \texttt{eresolve_tac} and \texttt{dresolve_tac} are
lcp@105
   373
not strictly necessary, they simplify proofs involving elimination and
lcp@105
   374
destruction rules.  All the tactics act on a subgoal designated by a
lcp@105
   375
positive integer~$i$, failing if~$i$ is out of range.  The resolution
lcp@105
   376
tactics try their list of theorems in left-to-right order.
lcp@105
   377
lcp@311
   378
\begin{ttdescription}
lcp@311
   379
\item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption}
lcp@311
   380
  is the tactic that attempts to solve subgoal~$i$ by assumption.  Proof by
lcp@311
   381
  assumption is not a trivial step; it can falsify other subgoals by
lcp@311
   382
  instantiating shared variables.  There may be several ways of solving the
lcp@311
   383
  subgoal by assumption.
lcp@105
   384
lcp@311
   385
\item[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution}
lcp@311
   386
  is the basic resolution tactic, used for most proof steps.  The $thms$
lcp@311
   387
  represent object-rules, which are resolved against subgoal~$i$ of the
lcp@311
   388
  proof state.  For each rule, resolution forms next states by unifying the
lcp@311
   389
  conclusion with the subgoal and inserting instantiated premises in its
lcp@311
   390
  place.  A rule can admit many higher-order unifiers.  The tactic fails if
lcp@311
   391
  none of the rules generates next states.
lcp@105
   392
lcp@311
   393
\item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution}
paulson@5205
   394
  performs elim-resolution.  Like \texttt{resolve_tac~{\it thms}~{\it i\/}}
paulson@5205
   395
  followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its
paulson@5205
   396
  first premise by assumption.  But \texttt{eresolve_tac} additionally deletes
lcp@311
   397
  that assumption from any subgoals arising from the resolution.
lcp@105
   398
lcp@311
   399
\item[\ttindex{dresolve_tac} {\it thms} {\it i}]
lcp@311
   400
  \index{forward proof}\index{destruct-resolution}
lcp@311
   401
  performs destruct-resolution with the~$thms$, as described
lcp@311
   402
  in~\S\ref{destruct}.  It is useful for forward reasoning from the
lcp@311
   403
  assumptions.
lcp@311
   404
\end{ttdescription}
lcp@105
   405
lcp@105
   406
\subsection{Commands for backward proof}
lcp@311
   407
\index{proofs!commands for}
lcp@105
   408
Tactics are normally applied using the subgoal module, which maintains a
lcp@105
   409
proof state and manages the proof construction.  It allows interactive
lcp@105
   410
backtracking through the proof space, going away to prove lemmas, etc.; of
lcp@105
   411
its many commands, most important are the following:
lcp@311
   412
\begin{ttdescription}
paulson@5205
   413
\item[\ttindex{Goal} {\it formula}; ] 
lcp@105
   414
begins a new proof, where $theory$ is usually an \ML\ identifier
lcp@105
   415
and the {\it formula\/} is written as an \ML\ string.
lcp@105
   416
lcp@311
   417
\item[\ttindex{by} {\it tactic}; ] 
lcp@105
   418
applies the {\it tactic\/} to the current proof
lcp@105
   419
state, raising an exception if the tactic fails.
lcp@105
   420
wenzelm@3103
   421
\item[\ttindex{undo}(); ]
lcp@296
   422
  reverts to the previous proof state.  Undo can be repeated but cannot be
lcp@296
   423
  undone.  Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely
lcp@296
   424
  causes \ML\ to echo the value of that function.
lcp@105
   425
wenzelm@3103
   426
\item[\ttindex{result}();]
lcp@105
   427
returns the theorem just proved, in a standard format.  It fails if
lcp@296
   428
unproved subgoals are left, etc.
wenzelm@3103
   429
wenzelm@3103
   430
\item[\ttindex{qed} {\it name};] is the usual way of ending a proof.
paulson@5205
   431
  It gets the theorem using \texttt{result}, stores it in Isabelle's
wenzelm@3103
   432
  theorem database and binds it to an \ML{} identifier.
wenzelm@3103
   433
lcp@311
   434
\end{ttdescription}
lcp@105
   435
The commands and tactics given above are cumbersome for interactive use.
lcp@105
   436
Although our examples will use the full commands, you may prefer Isabelle's
lcp@105
   437
shortcuts:
lcp@105
   438
\begin{center} \tt
lcp@311
   439
\index{*br} \index{*be} \index{*bd} \index{*ba}
lcp@105
   440
\begin{tabular}{l@{\qquad\rm abbreviates\qquad}l}
lcp@105
   441
    ba {\it i};           & by (assume_tac {\it i}); \\
lcp@105
   442
lcp@105
   443
    br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\
lcp@105
   444
lcp@105
   445
    be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\
lcp@105
   446
lcp@105
   447
    bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i}); 
lcp@105
   448
\end{tabular}
lcp@105
   449
\end{center}
lcp@105
   450
lcp@105
   451
\subsection{A trivial example in propositional logic}
lcp@105
   452
\index{examples!propositional}
lcp@296
   453
paulson@5205
   454
Directory \texttt{FOL} of the Isabelle distribution defines the theory of
lcp@296
   455
first-order logic.  Let us try the example from \S\ref{prop-proof},
lcp@296
   456
entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these
paulson@5205
   457
  examples, see the file \texttt{FOL/ex/intro.ML}.}
lcp@105
   458
\begin{ttbox}
paulson@5205
   459
Goal "P|P --> P"; 
lcp@105
   460
{\out Level 0} 
lcp@105
   461
{\out P | P --> P} 
lcp@105
   462
{\out 1. P | P --> P} 
lcp@311
   463
\end{ttbox}\index{level of a proof}
lcp@105
   464
Isabelle responds by printing the initial proof state, which has $P\disj
lcp@311
   465
P\imp P$ as the main goal and the only subgoal.  The {\bf level} of the
paulson@5205
   466
state is the number of \texttt{by} commands that have been applied to reach
lcp@311
   467
it.  We now use \ttindex{resolve_tac} to apply the rule \tdx{impI},
lcp@105
   468
or~$({\imp}I)$, to subgoal~1:
lcp@105
   469
\begin{ttbox}
lcp@105
   470
by (resolve_tac [impI] 1); 
lcp@105
   471
{\out Level 1} 
lcp@105
   472
{\out P | P --> P} 
lcp@105
   473
{\out 1. P | P ==> P}
lcp@105
   474
\end{ttbox}
lcp@105
   475
In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$.
lcp@105
   476
(The meta-implication {\tt==>} indicates assumptions.)  We apply
lcp@311
   477
\tdx{disjE}, or~(${\disj}E)$, to that subgoal:
lcp@105
   478
\begin{ttbox}
lcp@105
   479
by (resolve_tac [disjE] 1); 
lcp@105
   480
{\out Level 2} 
lcp@105
   481
{\out P | P --> P} 
lcp@105
   482
{\out 1. P | P ==> ?P1 | ?Q1} 
lcp@105
   483
{\out 2. [| P | P; ?P1 |] ==> P} 
lcp@105
   484
{\out 3. [| P | P; ?Q1 |] ==> P}
lcp@105
   485
\end{ttbox}
lcp@296
   486
At Level~2 there are three subgoals, each provable by assumption.  We
lcp@296
   487
deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using
lcp@296
   488
\ttindex{assume_tac}.  This affects subgoal~1, updating {\tt?Q1} to~{\tt
lcp@296
   489
  P}.
lcp@105
   490
\begin{ttbox}
lcp@105
   491
by (assume_tac 3); 
lcp@105
   492
{\out Level 3} 
lcp@105
   493
{\out P | P --> P} 
lcp@105
   494
{\out 1. P | P ==> ?P1 | P} 
lcp@105
   495
{\out 2. [| P | P; ?P1 |] ==> P}
lcp@105
   496
\end{ttbox}
paulson@5205
   497
Next we tackle subgoal~2, instantiating {\tt?P1} to~\texttt{P} in subgoal~1.
lcp@105
   498
\begin{ttbox}
lcp@105
   499
by (assume_tac 2); 
lcp@105
   500
{\out Level 4} 
lcp@105
   501
{\out P | P --> P} 
lcp@105
   502
{\out 1. P | P ==> P | P}
lcp@105
   503
\end{ttbox}
lcp@105
   504
Lastly we prove the remaining subgoal by assumption:
lcp@105
   505
\begin{ttbox}
lcp@105
   506
by (assume_tac 1); 
lcp@105
   507
{\out Level 5} 
lcp@105
   508
{\out P | P --> P} 
lcp@105
   509
{\out No subgoals!}
lcp@105
   510
\end{ttbox}
lcp@105
   511
Isabelle tells us that there are no longer any subgoals: the proof is
paulson@5205
   512
complete.  Calling \texttt{qed} stores the theorem.
lcp@105
   513
\begin{ttbox}
wenzelm@3103
   514
qed "mythm";
lcp@105
   515
{\out val mythm = "?P | ?P --> ?P" : thm} 
lcp@105
   516
\end{ttbox}
paulson@5205
   517
Isabelle has replaced the free variable~\texttt{P} by the scheme
lcp@105
   518
variable~{\tt?P}\@.  Free variables in the proof state remain fixed
lcp@105
   519
throughout the proof.  Isabelle finally converts them to scheme variables
lcp@105
   520
so that the resulting theorem can be instantiated with any formula.
lcp@105
   521
lcp@296
   522
As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how
lcp@296
   523
instantiations affect the proof state.
lcp@105
   524
lcp@296
   525
lcp@296
   526
\subsection{Part of a distributive law}
lcp@105
   527
\index{examples!propositional}
lcp@105
   528
To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac}
paulson@5205
   529
and the tactical \texttt{REPEAT}, let us prove part of the distributive
lcp@296
   530
law 
lcp@296
   531
\[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \]
lcp@105
   532
We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it:
lcp@105
   533
\begin{ttbox}
paulson@5205
   534
Goal "(P & Q) | R  --> (P | R)";
lcp@105
   535
{\out Level 0}
lcp@105
   536
{\out P & Q | R --> P | R}
lcp@105
   537
{\out  1. P & Q | R --> P | R}
lcp@296
   538
\ttbreak
lcp@105
   539
by (resolve_tac [impI] 1);
lcp@105
   540
{\out Level 1}
lcp@105
   541
{\out P & Q | R --> P | R}
lcp@105
   542
{\out  1. P & Q | R ==> P | R}
lcp@105
   543
\end{ttbox}
paulson@5205
   544
Previously we applied~(${\disj}E)$ using \texttt{resolve_tac}, but 
lcp@105
   545
\ttindex{eresolve_tac} deletes the assumption after use.  The resulting proof
lcp@105
   546
state is simpler.
lcp@105
   547
\begin{ttbox}
lcp@105
   548
by (eresolve_tac [disjE] 1);
lcp@105
   549
{\out Level 2}
lcp@105
   550
{\out P & Q | R --> P | R}
lcp@105
   551
{\out  1. P & Q ==> P | R}
lcp@105
   552
{\out  2. R ==> P | R}
lcp@105
   553
\end{ttbox}
lcp@105
   554
Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1,
lcp@105
   555
replacing the assumption $P\conj Q$ by~$P$.  Normally we should apply the
lcp@105
   556
rule~(${\conj}E)$, given in~\S\ref{destruct}.  That is an elimination rule
paulson@5205
   557
and requires \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two
lcp@296
   558
assumptions~$P$ and~$Q$.  Because the present example does not need~$Q$, we
paulson@5205
   559
may try out \texttt{dresolve_tac}.
lcp@105
   560
\begin{ttbox}
lcp@105
   561
by (dresolve_tac [conjunct1] 1);
lcp@105
   562
{\out Level 3}
lcp@105
   563
{\out P & Q | R --> P | R}
lcp@105
   564
{\out  1. P ==> P | R}
lcp@105
   565
{\out  2. R ==> P | R}
lcp@105
   566
\end{ttbox}
lcp@105
   567
The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner.
lcp@105
   568
\begin{ttbox}
lcp@105
   569
by (resolve_tac [disjI1] 1);
lcp@105
   570
{\out Level 4}
lcp@105
   571
{\out P & Q | R --> P | R}
lcp@105
   572
{\out  1. P ==> P}
lcp@105
   573
{\out  2. R ==> P | R}
lcp@105
   574
\ttbreak
lcp@105
   575
by (resolve_tac [disjI2] 2);
lcp@105
   576
{\out Level 5}
lcp@105
   577
{\out P & Q | R --> P | R}
lcp@105
   578
{\out  1. P ==> P}
lcp@105
   579
{\out  2. R ==> R}
lcp@105
   580
\end{ttbox}
paulson@5205
   581
Two calls of \texttt{assume_tac} can finish the proof.  The
paulson@5205
   582
tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{assume_tac~1}
lcp@105
   583
as many times as possible.  We can restrict attention to subgoal~1 because
lcp@105
   584
the other subgoals move up after subgoal~1 disappears.
lcp@105
   585
\begin{ttbox}
lcp@105
   586
by (REPEAT (assume_tac 1));
lcp@105
   587
{\out Level 6}
lcp@105
   588
{\out P & Q | R --> P | R}
lcp@105
   589
{\out No subgoals!}
lcp@105
   590
\end{ttbox}
lcp@105
   591
lcp@105
   592
lcp@105
   593
\section{Quantifier reasoning}
lcp@331
   594
\index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function}
lcp@105
   595
This section illustrates how Isabelle enforces quantifier provisos.
lcp@331
   596
Suppose that $x$, $y$ and~$z$ are parameters of a subgoal.  Quantifier
lcp@331
   597
rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function
lcp@331
   598
unknown.  Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of
lcp@331
   599
replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free
lcp@331
   600
occurrences of~$x$ and~$z$.  On the other hand, no instantiation
lcp@331
   601
of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free
lcp@331
   602
occurrences of~$y$, since parameters are bound variables.
lcp@105
   603
lcp@296
   604
\subsection{Two quantifier proofs: a success and a failure}
lcp@105
   605
\index{examples!with quantifiers}
lcp@105
   606
Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an
lcp@105
   607
attempted proof of the non-theorem $\exists y.\forall x.x=y$.  The former
lcp@105
   608
proof succeeds, and the latter fails, because of the scope of quantified
paulson@1878
   609
variables~\cite{paulson-found}.  Unification helps even in these trivial
paulson@3485
   610
proofs.  In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$,
paulson@3485
   611
but we need never say so.  This choice is forced by the reflexive law for
lcp@105
   612
equality, and happens automatically.
lcp@105
   613
lcp@296
   614
\paragraph{The successful proof.}
lcp@105
   615
The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules
lcp@105
   616
$(\forall I)$ and~$(\exists I)$.  We state the goal and apply $(\forall I)$:
lcp@105
   617
\begin{ttbox}
paulson@5205
   618
Goal "ALL x. EX y. x=y";
lcp@105
   619
{\out Level 0}
lcp@105
   620
{\out ALL x. EX y. x = y}
lcp@105
   621
{\out  1. ALL x. EX y. x = y}
lcp@105
   622
\ttbreak
lcp@105
   623
by (resolve_tac [allI] 1);
lcp@105
   624
{\out Level 1}
lcp@105
   625
{\out ALL x. EX y. x = y}
lcp@105
   626
{\out  1. !!x. EX y. x = y}
lcp@105
   627
\end{ttbox}
paulson@5205
   628
The variable~\texttt{x} is no longer universally quantified, but is a
lcp@105
   629
parameter in the subgoal; thus, it is universally quantified at the
paulson@5205
   630
meta-level.  The subgoal must be proved for all possible values of~\texttt{x}.
lcp@296
   631
lcp@296
   632
To remove the existential quantifier, we apply the rule $(\exists I)$:
lcp@105
   633
\begin{ttbox}
lcp@105
   634
by (resolve_tac [exI] 1);
lcp@105
   635
{\out Level 2}
lcp@105
   636
{\out ALL x. EX y. x = y}
lcp@105
   637
{\out  1. !!x. x = ?y1(x)}
lcp@105
   638
\end{ttbox}
paulson@5205
   639
The bound variable \texttt{y} has become {\tt?y1(x)}.  This term consists of
paulson@5205
   640
the function unknown~{\tt?y1} applied to the parameter~\texttt{x}.
paulson@5205
   641
Instances of {\tt?y1(x)} may or may not contain~\texttt{x}.  We resolve the
lcp@105
   642
subgoal with the reflexivity axiom.
lcp@105
   643
\begin{ttbox}
lcp@105
   644
by (resolve_tac [refl] 1);
lcp@105
   645
{\out Level 3}
lcp@105
   646
{\out ALL x. EX y. x = y}
lcp@105
   647
{\out No subgoals!}
lcp@105
   648
\end{ttbox}
lcp@105
   649
Let us consider what has happened in detail.  The reflexivity axiom is
lcp@105
   650
lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is
lcp@105
   651
unified with $\Forall x.x=\Var{y@1}(x)$.  The function unknowns $\Var{f}$
lcp@105
   652
and~$\Var{y@1}$ are both instantiated to the identity function, and
lcp@105
   653
$x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction.
lcp@105
   654
lcp@296
   655
\paragraph{The unsuccessful proof.}
lcp@296
   656
We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and
lcp@105
   657
try~$(\exists I)$:
lcp@105
   658
\begin{ttbox}
paulson@5205
   659
Goal "EX y. ALL x. x=y";
lcp@105
   660
{\out Level 0}
lcp@105
   661
{\out EX y. ALL x. x = y}
lcp@105
   662
{\out  1. EX y. ALL x. x = y}
lcp@105
   663
\ttbreak
lcp@105
   664
by (resolve_tac [exI] 1);
lcp@105
   665
{\out Level 1}
lcp@105
   666
{\out EX y. ALL x. x = y}
lcp@105
   667
{\out  1. ALL x. x = ?y}
lcp@105
   668
\end{ttbox}
paulson@5205
   669
The unknown \texttt{?y} may be replaced by any term, but this can never
paulson@5205
   670
introduce another bound occurrence of~\texttt{x}.  We now apply~$(\forall I)$:
lcp@105
   671
\begin{ttbox}
lcp@105
   672
by (resolve_tac [allI] 1);
lcp@105
   673
{\out Level 2}
lcp@105
   674
{\out EX y. ALL x. x = y}
lcp@105
   675
{\out  1. !!x. x = ?y}
lcp@105
   676
\end{ttbox}
lcp@105
   677
Compare our position with the previous Level~2.  Instead of {\tt?y1(x)} we
paulson@5205
   678
have~{\tt?y}, whose instances may not contain the bound variable~\texttt{x}.
lcp@105
   679
The reflexivity axiom does not unify with subgoal~1.
lcp@105
   680
\begin{ttbox}
lcp@105
   681
by (resolve_tac [refl] 1);
wenzelm@3103
   682
{\out by: tactic failed}
lcp@105
   683
\end{ttbox}
lcp@296
   684
There can be no proof of $\exists y.\forall x.x=y$ by the soundness of
lcp@296
   685
first-order logic.  I have elsewhere proved the faithfulness of Isabelle's
paulson@1878
   686
encoding of first-order logic~\cite{paulson-found}; there could, of course, be
lcp@296
   687
faults in the implementation.
lcp@105
   688
lcp@105
   689
lcp@105
   690
\subsection{Nested quantifiers}
lcp@105
   691
\index{examples!with quantifiers}
lcp@296
   692
Multiple quantifiers create complex terms.  Proving 
lcp@296
   693
\[ (\forall x\,y.P(x,y)) \imp (\forall z\,w.P(w,z)) \] 
lcp@296
   694
will demonstrate how parameters and unknowns develop.  If they appear in
lcp@296
   695
the wrong order, the proof will fail.
lcp@296
   696
paulson@5205
   697
This section concludes with a demonstration of \texttt{REPEAT}
paulson@5205
   698
and~\texttt{ORELSE}.  
lcp@105
   699
\begin{ttbox}
paulson@5205
   700
Goal "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
lcp@105
   701
{\out Level 0}
lcp@105
   702
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   703
{\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   704
\ttbreak
lcp@105
   705
by (resolve_tac [impI] 1);
lcp@105
   706
{\out Level 1}
lcp@105
   707
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   708
{\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
lcp@105
   709
\end{ttbox}
lcp@105
   710
lcp@296
   711
\paragraph{The wrong approach.}
paulson@5205
   712
Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the
lcp@311
   713
\ML\ identifier \tdx{spec}.  Then we apply $(\forall I)$.
lcp@105
   714
\begin{ttbox}
lcp@105
   715
by (dresolve_tac [spec] 1);
lcp@105
   716
{\out Level 2}
lcp@105
   717
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   718
{\out  1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)}
lcp@105
   719
\ttbreak
lcp@105
   720
by (resolve_tac [allI] 1);
lcp@105
   721
{\out Level 3}
lcp@105
   722
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   723
{\out  1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)}
lcp@105
   724
\end{ttbox}
paulson@5205
   725
The unknown \texttt{?x1} and the parameter \texttt{z} have appeared.  We again
lcp@296
   726
apply $(\forall E)$ and~$(\forall I)$.
lcp@105
   727
\begin{ttbox}
lcp@105
   728
by (dresolve_tac [spec] 1);
lcp@105
   729
{\out Level 4}
lcp@105
   730
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   731
{\out  1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)}
lcp@105
   732
\ttbreak
lcp@105
   733
by (resolve_tac [allI] 1);
lcp@105
   734
{\out Level 5}
lcp@105
   735
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   736
{\out  1. !!z w. P(?x1,?y3(z)) ==> P(w,z)}
lcp@105
   737
\end{ttbox}
paulson@5205
   738
The unknown \texttt{?y3} and the parameter \texttt{w} have appeared.  Each
lcp@105
   739
unknown is applied to the parameters existing at the time of its creation;
paulson@5205
   740
instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances
paulson@5205
   741
of {\tt?y3(z)} can only contain~\texttt{z}.  Due to the restriction on~\texttt{?x1},
lcp@105
   742
proof by assumption will fail.
lcp@105
   743
\begin{ttbox}
lcp@105
   744
by (assume_tac 1);
wenzelm@3103
   745
{\out by: tactic failed}
lcp@105
   746
{\out uncaught exception ERROR}
lcp@105
   747
\end{ttbox}
lcp@105
   748
lcp@296
   749
\paragraph{The right approach.}
lcp@105
   750
To do this proof, the rules must be applied in the correct order.
lcp@331
   751
Parameters should be created before unknowns.  The
lcp@105
   752
\ttindex{choplev} command returns to an earlier stage of the proof;
lcp@105
   753
let us return to the result of applying~$({\imp}I)$:
lcp@105
   754
\begin{ttbox}
lcp@105
   755
choplev 1;
lcp@105
   756
{\out Level 1}
lcp@105
   757
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   758
{\out  1. ALL x y. P(x,y) ==> ALL z w. P(w,z)}
lcp@105
   759
\end{ttbox}
lcp@296
   760
Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$.
lcp@105
   761
\begin{ttbox}
lcp@105
   762
by (resolve_tac [allI] 1);
lcp@105
   763
{\out Level 2}
lcp@105
   764
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   765
{\out  1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)}
lcp@105
   766
\ttbreak
lcp@105
   767
by (resolve_tac [allI] 1);
lcp@105
   768
{\out Level 3}
lcp@105
   769
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   770
{\out  1. !!z w. ALL x y. P(x,y) ==> P(w,z)}
lcp@105
   771
\end{ttbox}
paulson@5205
   772
The parameters \texttt{z} and~\texttt{w} have appeared.  We now create the
lcp@105
   773
unknowns:
lcp@105
   774
\begin{ttbox}
lcp@105
   775
by (dresolve_tac [spec] 1);
lcp@105
   776
{\out Level 4}
lcp@105
   777
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   778
{\out  1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)}
lcp@105
   779
\ttbreak
lcp@105
   780
by (dresolve_tac [spec] 1);
lcp@105
   781
{\out Level 5}
lcp@105
   782
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   783
{\out  1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)}
lcp@105
   784
\end{ttbox}
lcp@105
   785
Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt
paulson@5205
   786
z} and~\texttt{w}:
lcp@105
   787
\begin{ttbox}
lcp@105
   788
by (assume_tac 1);
lcp@105
   789
{\out Level 6}
lcp@105
   790
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   791
{\out No subgoals!}
lcp@105
   792
\end{ttbox}
lcp@105
   793
lcp@296
   794
\paragraph{A one-step proof using tacticals.}
lcp@296
   795
\index{tacticals} \index{examples!of tacticals} 
lcp@296
   796
lcp@296
   797
Repeated application of rules can be effective, but the rules should be
lcp@331
   798
attempted in the correct order.  Let us return to the original goal using
lcp@331
   799
\ttindex{choplev}:
lcp@105
   800
\begin{ttbox}
lcp@105
   801
choplev 0;
lcp@105
   802
{\out Level 0}
lcp@105
   803
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   804
{\out  1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   805
\end{ttbox}
lcp@311
   806
As we have just seen, \tdx{allI} should be attempted
lcp@311
   807
before~\tdx{spec}, while \ttindex{assume_tac} generally can be
lcp@296
   808
attempted first.  Such priorities can easily be expressed
lcp@296
   809
using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}.
lcp@105
   810
\begin{ttbox}
lcp@296
   811
by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1
lcp@105
   812
     ORELSE dresolve_tac [spec] 1));
lcp@105
   813
{\out Level 1}
lcp@105
   814
{\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))}
lcp@105
   815
{\out No subgoals!}
lcp@105
   816
\end{ttbox}
lcp@105
   817
lcp@105
   818
lcp@105
   819
\subsection{A realistic quantifier proof}
lcp@105
   820
\index{examples!with quantifiers}
lcp@296
   821
To see the practical use of parameters and unknowns, let us prove half of
lcp@296
   822
the equivalence 
lcp@296
   823
\[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \]
lcp@296
   824
We state the left-to-right half to Isabelle in the normal way.
lcp@105
   825
Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we
paulson@5205
   826
use \texttt{REPEAT}:
lcp@105
   827
\begin{ttbox}
paulson@5205
   828
Goal "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q";
lcp@105
   829
{\out Level 0}
lcp@105
   830
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
lcp@105
   831
{\out  1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
lcp@105
   832
\ttbreak
lcp@105
   833
by (REPEAT (resolve_tac [impI] 1));
lcp@105
   834
{\out Level 1}
lcp@105
   835
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
lcp@105
   836
{\out  1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q}
lcp@105
   837
\end{ttbox}
lcp@105
   838
We can eliminate the universal or the existential quantifier.  The
lcp@105
   839
existential quantifier should be eliminated first, since this creates a
lcp@105
   840
parameter.  The rule~$(\exists E)$ is bound to the
lcp@311
   841
identifier~\tdx{exE}.
lcp@105
   842
\begin{ttbox}
lcp@105
   843
by (eresolve_tac [exE] 1);
lcp@105
   844
{\out Level 2}
lcp@105
   845
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
lcp@105
   846
{\out  1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q}
lcp@105
   847
\end{ttbox}
lcp@105
   848
The only possibility now is $(\forall E)$, a destruction rule.  We use 
lcp@105
   849
\ttindex{dresolve_tac}, which discards the quantified assumption; it is
lcp@105
   850
only needed once.
lcp@105
   851
\begin{ttbox}
lcp@105
   852
by (dresolve_tac [spec] 1);
lcp@105
   853
{\out Level 3}
lcp@105
   854
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
lcp@105
   855
{\out  1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q}
lcp@105
   856
\end{ttbox}
lcp@296
   857
Because we applied $(\exists E)$ before $(\forall E)$, the unknown
paulson@5205
   858
term~{\tt?x3(x)} may depend upon the parameter~\texttt{x}.
lcp@105
   859
lcp@105
   860
Although $({\imp}E)$ is a destruction rule, it works with 
lcp@105
   861
\ttindex{eresolve_tac} to perform backward chaining.  This technique is
lcp@105
   862
frequently useful.  
lcp@105
   863
\begin{ttbox}
lcp@105
   864
by (eresolve_tac [mp] 1);
lcp@105
   865
{\out Level 4}
lcp@105
   866
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
lcp@105
   867
{\out  1. !!x. P(x) ==> P(?x3(x))}
lcp@105
   868
\end{ttbox}
paulson@5205
   869
The tactic has reduced~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the
paulson@5205
   870
implication.  The final step is trivial, thanks to the occurrence of~\texttt{x}.
lcp@105
   871
\begin{ttbox}
lcp@105
   872
by (assume_tac 1);
lcp@105
   873
{\out Level 5}
lcp@105
   874
{\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q}
lcp@105
   875
{\out No subgoals!}
lcp@105
   876
\end{ttbox}
lcp@105
   877
lcp@105
   878
lcp@311
   879
\subsection{The classical reasoner}
lcp@311
   880
\index{classical reasoner}
lcp@105
   881
Although Isabelle cannot compete with fully automatic theorem provers, it
lcp@105
   882
provides enough automation to tackle substantial examples.  The classical
lcp@331
   883
reasoner can be set up for any classical natural deduction logic;
lcp@331
   884
see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
lcp@331
   885
        {Chap.\ts\ref{chap:classical}}. 
lcp@105
   886
lcp@331
   887
Rules are packaged into {\bf classical sets}.  The classical reasoner
lcp@331
   888
provides several tactics, which apply rules using naive algorithms.
lcp@331
   889
Unification handles quantifiers as shown above.  The most useful tactic
paulson@3127
   890
is~\ttindex{Blast_tac}.  
lcp@105
   891
lcp@105
   892
Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The
lcp@105
   893
backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape
lcp@105
   894
sequence, to break the long string over two lines.)
lcp@105
   895
\begin{ttbox}
paulson@5205
   896
Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \ttback
lcp@105
   897
\ttback       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
lcp@105
   898
{\out Level 0}
lcp@105
   899
{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
lcp@105
   900
{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
lcp@105
   901
{\out  1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
lcp@105
   902
{\out     ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
lcp@105
   903
\end{ttbox}
paulson@3127
   904
\ttindex{Blast_tac} proves subgoal~1 at a stroke.
lcp@105
   905
\begin{ttbox}
paulson@3127
   906
by (Blast_tac 1);
paulson@3127
   907
{\out Depth = 0}
paulson@3127
   908
{\out Depth = 1}
lcp@105
   909
{\out Level 1}
lcp@105
   910
{\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->}
lcp@105
   911
{\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))}
lcp@105
   912
{\out No subgoals!}
lcp@105
   913
\end{ttbox}
lcp@105
   914
Sceptics may examine the proof by calling the package's single-step
paulson@5205
   915
tactics, such as~\texttt{step_tac}.  This would take up much space, however,
lcp@105
   916
so let us proceed to the next example:
lcp@105
   917
\begin{ttbox}
paulson@5205
   918
Goal "ALL x. P(x,f(x)) <-> \ttback
lcp@105
   919
\ttback       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
lcp@105
   920
{\out Level 0}
lcp@105
   921
{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
lcp@296
   922
{\out  1. ALL x. P(x,f(x)) <->}
lcp@296
   923
{\out     (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
lcp@105
   924
\end{ttbox}
lcp@105
   925
Again, subgoal~1 succumbs immediately.
lcp@105
   926
\begin{ttbox}
paulson@3127
   927
by (Blast_tac 1);
paulson@3127
   928
{\out Depth = 0}
paulson@3127
   929
{\out Depth = 1}
lcp@105
   930
{\out Level 1}
lcp@105
   931
{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
lcp@105
   932
{\out No subgoals!}
lcp@105
   933
\end{ttbox}
lcp@331
   934
The classical reasoner is not restricted to the usual logical connectives.
lcp@331
   935
The natural deduction rules for unions and intersections resemble those for
lcp@331
   936
disjunction and conjunction.  The rules for infinite unions and
lcp@331
   937
intersections resemble those for quantifiers.  Given such rules, the classical
lcp@331
   938
reasoner is effective for reasoning in set theory.
lcp@331
   939