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