doc-src/Intro/advanced.tex
author aspinall
Sun Dec 31 15:34:21 2006 +0100 (2006-12-31)
changeset 21973 e7c9b0d3ce82
parent 14148 6580d374a509
child 42637 381fdcab0f36
permissions -rw-r--r--
Quote arguments in PGIP exceptions. Tune comment.
lcp@105
     1
%% $Id$
lcp@284
     2
\part{Advanced Methods}
lcp@105
     3
Before continuing, it might be wise to try some of your own examples in
lcp@105
     4
Isabelle, reinforcing your knowledge of the basic functions.
lcp@105
     5
wenzelm@3103
     6
Look through {\em Isabelle's Object-Logics\/} and try proving some
wenzelm@3103
     7
simple theorems.  You probably should begin with first-order logic
paulson@5205
     8
(\texttt{FOL} or~\texttt{LK}).  Try working some of the examples provided,
paulson@5205
     9
and others from the literature.  Set theory~(\texttt{ZF}) and
paulson@5205
    10
Constructive Type Theory~(\texttt{CTT}) form a richer world for
wenzelm@3103
    11
mathematical reasoning and, again, many examples are in the
paulson@5205
    12
literature.  Higher-order logic~(\texttt{HOL}) is Isabelle's most
paulson@3485
    13
elaborate logic.  Its types and functions are identified with those of
wenzelm@3103
    14
the meta-logic.
lcp@105
    15
lcp@105
    16
Choose a logic that you already understand.  Isabelle is a proof
lcp@105
    17
tool, not a teaching tool; if you do not know how to do a particular proof
lcp@105
    18
on paper, then you certainly will not be able to do it on the machine.
lcp@105
    19
Even experienced users plan large proofs on paper.
lcp@105
    20
lcp@105
    21
We have covered only the bare essentials of Isabelle, but enough to perform
lcp@105
    22
substantial proofs.  By occasionally dipping into the {\em Reference
lcp@105
    23
Manual}, you can learn additional tactics, subgoal commands and tacticals.
lcp@105
    24
lcp@105
    25
lcp@105
    26
\section{Deriving rules in Isabelle}
lcp@105
    27
\index{rules!derived}
lcp@105
    28
A mathematical development goes through a progression of stages.  Each
lcp@105
    29
stage defines some concepts and derives rules about them.  We shall see how
lcp@105
    30
to derive rules, perhaps involving definitions, using Isabelle.  The
lcp@310
    31
following section will explain how to declare types, constants, rules and
lcp@105
    32
definitions.
lcp@105
    33
lcp@105
    34
lcp@296
    35
\subsection{Deriving a rule using tactics and meta-level assumptions} 
lcp@296
    36
\label{deriving-example}
lcp@310
    37
\index{examples!of deriving rules}\index{assumptions!of main goal}
lcp@296
    38
lcp@307
    39
The subgoal module supports the derivation of rules, as discussed in
paulson@5205
    40
\S\ref{deriving}.  When the \ttindex{Goal} command is supplied a formula of
paulson@5205
    41
the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two
paulson@5205
    42
possibilities:
paulson@5205
    43
\begin{itemize}
paulson@5205
    44
\item If all of the premises $\theta@1$, \ldots, $\theta@k$ are simple
paulson@5205
    45
  formulae{} (they do not involve the meta-connectives $\Forall$ or
paulson@5205
    46
  $\Imp$) then the command sets the goal to be 
paulson@5205
    47
  $\List{\theta@1; \ldots; \theta@k} \Imp \phi$ and returns the empty list.
paulson@5205
    48
\item If one or more premises involves the meta-connectives $\Forall$ or
paulson@5205
    49
  $\Imp$, then the command sets the goal to be $\phi$ and returns a list
paulson@5205
    50
  consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$.
paulson@14148
    51
  These meta-level assumptions are also recorded internally, allowing
paulson@5205
    52
  \texttt{result} (which is called by \texttt{qed}) to discharge them in the
paulson@5205
    53
  original order.
paulson@5205
    54
\end{itemize}
paulson@5205
    55
Rules that discharge assumptions or introduce eigenvariables have complex
paulson@14148
    56
premises, and the second case applies.  In this section, many of the
paulson@14148
    57
theorems are subject to meta-level assumptions, so we make them visible by by setting the 
paulson@14148
    58
\ttindex{show_hyps} flag:
paulson@14148
    59
\begin{ttbox} 
paulson@14148
    60
set show_hyps;
paulson@14148
    61
{\out val it = true : bool}
paulson@14148
    62
\end{ttbox}
lcp@105
    63
paulson@14148
    64
Now, we are ready to derive $\conj$ elimination.  Until now, calling \texttt{Goal} has
paulson@5205
    65
returned an empty list, which we have ignored.  In this example, the list
paulson@5205
    66
contains the two premises of the rule, since one of them involves the $\Imp$
paulson@5205
    67
connective.  We bind them to the \ML\ identifiers \texttt{major} and {\tt
paulson@5205
    68
  minor}:\footnote{Some ML compilers will print a message such as {\em binding
paulson@5205
    69
    not exhaustive}.  This warns that \texttt{Goal} must return a 2-element
paulson@5205
    70
  list.  Otherwise, the pattern-match will fail; ML will raise exception
paulson@5205
    71
  \xdx{Match}.}
lcp@105
    72
\begin{ttbox}
paulson@5205
    73
val [major,minor] = Goal
lcp@105
    74
    "[| P&Q;  [| P; Q |] ==> R |] ==> R";
lcp@105
    75
{\out Level 0}
lcp@105
    76
{\out R}
lcp@105
    77
{\out  1. R}
lcp@105
    78
{\out val major = "P & Q  [P & Q]" : thm}
lcp@105
    79
{\out val minor = "[| P; Q |] ==> R  [[| P; Q |] ==> R]" : thm}
lcp@105
    80
\end{ttbox}
lcp@105
    81
Look at the minor premise, recalling that meta-level assumptions are
paulson@5205
    82
shown in brackets.  Using \texttt{minor}, we reduce $R$ to the subgoals
lcp@105
    83
$P$ and~$Q$:
lcp@105
    84
\begin{ttbox}
lcp@105
    85
by (resolve_tac [minor] 1);
lcp@105
    86
{\out Level 1}
lcp@105
    87
{\out R}
lcp@105
    88
{\out  1. P}
lcp@105
    89
{\out  2. Q}
lcp@105
    90
\end{ttbox}
lcp@105
    91
Deviating from~\S\ref{deriving}, we apply $({\conj}E1)$ forwards from the
lcp@105
    92
assumption $P\conj Q$ to obtain the theorem~$P\;[P\conj Q]$.
lcp@105
    93
\begin{ttbox}
lcp@105
    94
major RS conjunct1;
lcp@105
    95
{\out val it = "P  [P & Q]" : thm}
lcp@105
    96
\ttbreak
lcp@105
    97
by (resolve_tac [major RS conjunct1] 1);
lcp@105
    98
{\out Level 2}
lcp@105
    99
{\out R}
lcp@105
   100
{\out  1. Q}
lcp@105
   101
\end{ttbox}
lcp@105
   102
Similarly, we solve the subgoal involving~$Q$.
lcp@105
   103
\begin{ttbox}
lcp@105
   104
major RS conjunct2;
lcp@105
   105
{\out val it = "Q  [P & Q]" : thm}
lcp@105
   106
by (resolve_tac [major RS conjunct2] 1);
lcp@105
   107
{\out Level 3}
lcp@105
   108
{\out R}
lcp@105
   109
{\out No subgoals!}
lcp@105
   110
\end{ttbox}
lcp@105
   111
Calling \ttindex{topthm} returns the current proof state as a theorem.
wenzelm@3103
   112
Note that it contains assumptions.  Calling \ttindex{qed} discharges
wenzelm@3103
   113
the assumptions --- both occurrences of $P\conj Q$ are discharged as
wenzelm@3103
   114
one --- and makes the variables schematic.
lcp@105
   115
\begin{ttbox}
lcp@105
   116
topthm();
lcp@105
   117
{\out val it = "R  [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
wenzelm@3103
   118
qed "conjE";
lcp@105
   119
{\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
lcp@105
   120
\end{ttbox}
lcp@105
   121
lcp@105
   122
lcp@105
   123
\subsection{Definitions and derived rules} \label{definitions}
lcp@310
   124
\index{rules!derived}\index{definitions!and derived rules|(}
lcp@310
   125
lcp@105
   126
Definitions are expressed as meta-level equalities.  Let us define negation
lcp@105
   127
and the if-and-only-if connective:
lcp@105
   128
\begin{eqnarray*}
lcp@105
   129
  \neg \Var{P}          & \equiv & \Var{P}\imp\bot \\
lcp@105
   130
  \Var{P}\bimp \Var{Q}  & \equiv & 
lcp@105
   131
                (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
lcp@105
   132
\end{eqnarray*}
lcp@331
   133
\index{meta-rewriting}%
lcp@105
   134
Isabelle permits {\bf meta-level rewriting} using definitions such as
lcp@105
   135
these.  {\bf Unfolding} replaces every instance
lcp@331
   136
of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$.  For
lcp@105
   137
example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
lcp@105
   138
\[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.  \]
lcp@105
   139
{\bf Folding} a definition replaces occurrences of the right-hand side by
lcp@105
   140
the left.  The occurrences need not be free in the entire formula.
lcp@105
   141
lcp@105
   142
When you define new concepts, you should derive rules asserting their
lcp@105
   143
abstract properties, and then forget their definitions.  This supports
lcp@331
   144
modularity: if you later change the definitions without affecting their
lcp@105
   145
abstract properties, then most of your proofs will carry through without
lcp@105
   146
change.  Indiscriminate unfolding makes a subgoal grow exponentially,
lcp@105
   147
becoming unreadable.
lcp@105
   148
lcp@105
   149
Taking this point of view, Isabelle does not unfold definitions
lcp@105
   150
automatically during proofs.  Rewriting must be explicit and selective.
lcp@105
   151
Isabelle provides tactics and meta-rules for rewriting, and a version of
paulson@5205
   152
the \texttt{Goal} command that unfolds the conclusion and premises of the rule
lcp@105
   153
being derived.
lcp@105
   154
lcp@105
   155
For example, the intuitionistic definition of negation given above may seem
lcp@105
   156
peculiar.  Using Isabelle, we shall derive pleasanter negation rules:
lcp@105
   157
\[  \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}}   \qquad
lcp@105
   158
    \infer[({\neg}E)]{Q}{\neg P & P}  \]
lcp@296
   159
This requires proving the following meta-formulae:
wenzelm@3103
   160
$$ (P\Imp\bot)    \Imp \neg P   \eqno(\neg I) $$
wenzelm@3103
   161
$$ \List{\neg P; P} \Imp Q.       \eqno(\neg E) $$
lcp@105
   162
lcp@105
   163
lcp@296
   164
\subsection{Deriving the $\neg$ introduction rule}
paulson@5205
   165
To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula.
paulson@5205
   166
Again, the rule's premises involve a meta-connective, and \texttt{Goal}
paulson@5205
   167
returns one-element list.  We bind this list to the \ML\ identifier \texttt{prems}.
lcp@105
   168
\begin{ttbox}
paulson@5205
   169
val prems = Goal "(P ==> False) ==> ~P";
lcp@105
   170
{\out Level 0}
lcp@105
   171
{\out ~P}
lcp@105
   172
{\out  1. ~P}
lcp@105
   173
{\out val prems = ["P ==> False  [P ==> False]"] : thm list}
lcp@105
   174
\end{ttbox}
lcp@310
   175
Calling \ttindex{rewrite_goals_tac} with \tdx{not_def}, which is the
lcp@105
   176
definition of negation, unfolds that definition in the subgoals.  It leaves
lcp@105
   177
the main goal alone.
lcp@105
   178
\begin{ttbox}
lcp@105
   179
not_def;
lcp@105
   180
{\out val it = "~?P == ?P --> False" : thm}
lcp@105
   181
by (rewrite_goals_tac [not_def]);
lcp@105
   182
{\out Level 1}
lcp@105
   183
{\out ~P}
lcp@105
   184
{\out  1. P --> False}
lcp@105
   185
\end{ttbox}
lcp@310
   186
Using \tdx{impI} and the premise, we reduce subgoal~1 to a triviality:
lcp@105
   187
\begin{ttbox}
lcp@105
   188
by (resolve_tac [impI] 1);
lcp@105
   189
{\out Level 2}
lcp@105
   190
{\out ~P}
lcp@105
   191
{\out  1. P ==> False}
lcp@105
   192
\ttbreak
lcp@105
   193
by (resolve_tac prems 1);
lcp@105
   194
{\out Level 3}
lcp@105
   195
{\out ~P}
lcp@105
   196
{\out  1. P ==> P}
lcp@105
   197
\end{ttbox}
lcp@296
   198
The rest of the proof is routine.  Note the form of the final result.
lcp@105
   199
\begin{ttbox}
lcp@105
   200
by (assume_tac 1);
lcp@105
   201
{\out Level 4}
lcp@105
   202
{\out ~P}
lcp@105
   203
{\out No subgoals!}
lcp@296
   204
\ttbreak
wenzelm@3103
   205
qed "notI";
lcp@105
   206
{\out val notI = "(?P ==> False) ==> ~?P" : thm}
lcp@105
   207
\end{ttbox}
lcp@310
   208
\indexbold{*notI theorem}
lcp@105
   209
paulson@5205
   210
There is a simpler way of conducting this proof.  The \ttindex{Goalw}
paulson@5205
   211
command starts a backward proof, as does \texttt{Goal}, but it also
lcp@296
   212
unfolds definitions.  Thus there is no need to call
lcp@296
   213
\ttindex{rewrite_goals_tac}:
lcp@105
   214
\begin{ttbox}
paulson@5205
   215
val prems = Goalw [not_def]
lcp@105
   216
    "(P ==> False) ==> ~P";
lcp@105
   217
{\out Level 0}
lcp@105
   218
{\out ~P}
lcp@105
   219
{\out  1. P --> False}
lcp@105
   220
{\out val prems = ["P ==> False  [P ==> False]"] : thm list}
lcp@105
   221
\end{ttbox}
lcp@105
   222
lcp@105
   223
lcp@296
   224
\subsection{Deriving the $\neg$ elimination rule}
paulson@5205
   225
Let us derive the rule $(\neg E)$.  The proof follows that of~\texttt{conjE}
lcp@296
   226
above, with an additional step to unfold negation in the major premise.
paulson@5205
   227
The \texttt{Goalw} command is best for this: it unfolds definitions not only
paulson@5205
   228
in the conclusion but the premises.
lcp@105
   229
\begin{ttbox}
paulson@5205
   230
Goalw [not_def] "[| ~P;  P |] ==> R";
lcp@105
   231
{\out Level 0}
paulson@5205
   232
{\out [| ~ P; P |] ==> R}
paulson@5205
   233
{\out  1. [| P --> False; P |] ==> R}
paulson@5205
   234
\end{ttbox}
paulson@5205
   235
As the first step, we apply \tdx{FalseE}:
paulson@5205
   236
\begin{ttbox}
lcp@105
   237
by (resolve_tac [FalseE] 1);
lcp@105
   238
{\out Level 1}
paulson@5205
   239
{\out [| ~ P; P |] ==> R}
paulson@5205
   240
{\out  1. [| P --> False; P |] ==> False}
lcp@284
   241
\end{ttbox}
paulson@5205
   242
%
lcp@284
   243
Everything follows from falsity.  And we can prove falsity using the
lcp@284
   244
premises and Modus Ponens:
lcp@284
   245
\begin{ttbox}
paulson@5205
   246
by (eresolve_tac [mp] 1);
lcp@105
   247
{\out Level 2}
paulson@5205
   248
{\out [| ~ P; P |] ==> R}
paulson@5205
   249
{\out  1. P ==> P}
paulson@5205
   250
\ttbreak
paulson@5205
   251
by (assume_tac 1);
lcp@105
   252
{\out Level 3}
paulson@5205
   253
{\out [| ~ P; P |] ==> R}
lcp@105
   254
{\out No subgoals!}
paulson@5205
   255
\ttbreak
wenzelm@3103
   256
qed "notE";
lcp@105
   257
{\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
lcp@105
   258
\end{ttbox}
paulson@5205
   259
lcp@105
   260
lcp@105
   261
\medskip
paulson@5205
   262
\texttt{Goalw} unfolds definitions in the premises even when it has to return
paulson@5205
   263
them as a list.  Another way of unfolding definitions in a theorem is by
paulson@5205
   264
applying the function \ttindex{rewrite_rule}.
lcp@105
   265
paulson@5205
   266
\index{definitions!and derived rules|)}
lcp@105
   267
lcp@105
   268
lcp@284
   269
\section{Defining theories}\label{sec:defining-theories}
lcp@105
   270
\index{theories!defining|(}
lcp@310
   271
wenzelm@3103
   272
Isabelle makes no distinction between simple extensions of a logic ---
wenzelm@3103
   273
like specifying a type~$bool$ with constants~$true$ and~$false$ ---
wenzelm@3103
   274
and defining an entire logic.  A theory definition has a form like
lcp@105
   275
\begin{ttbox}
lcp@105
   276
\(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
lcp@105
   277
classes      {\it class declarations}
lcp@105
   278
default      {\it sort}
lcp@331
   279
types        {\it type declarations and synonyms}
wenzelm@3103
   280
arities      {\it type arity declarations}
lcp@105
   281
consts       {\it constant declarations}
wenzelm@3103
   282
syntax       {\it syntactic constant declarations}
wenzelm@3103
   283
translations {\it ast translation rules}
wenzelm@3103
   284
defs         {\it meta-logical definitions}
lcp@105
   285
rules        {\it rule declarations}
lcp@105
   286
end
lcp@105
   287
ML           {\it ML code}
lcp@105
   288
\end{ttbox}
lcp@105
   289
This declares the theory $T$ to extend the existing theories
wenzelm@3103
   290
$S@1$,~\ldots,~$S@n$.  It may introduce new classes, types, arities
wenzelm@3103
   291
(of existing types), constants and rules; it can specify the default
wenzelm@3103
   292
sort for type variables.  A constant declaration can specify an
wenzelm@3103
   293
associated concrete syntax.  The translations section specifies
wenzelm@3103
   294
rewrite rules on abstract syntax trees, handling notations and
paulson@5205
   295
abbreviations.  \index{*ML section} The \texttt{ML} section may contain
wenzelm@3103
   296
code to perform arbitrary syntactic transformations.  The main
wenzelm@3212
   297
declaration forms are discussed below.  There are some more sections
wenzelm@3212
   298
not presented here, the full syntax can be found in
wenzelm@3212
   299
\iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
wenzelm@3212
   300
    Manual}}{App.\ts\ref{app:TheorySyntax}}.  Also note that
wenzelm@3212
   301
object-logics may add further theory sections, for example
wenzelm@9695
   302
\texttt{typedef}, \texttt{datatype} in HOL.
lcp@105
   303
wenzelm@3103
   304
All the declaration parts can be omitted or repeated and may appear in
wenzelm@3103
   305
any order, except that the {\ML} section must be last (after the {\tt
wenzelm@3103
   306
  end} keyword).  In the simplest case, $T$ is just the union of
wenzelm@3103
   307
$S@1$,~\ldots,~$S@n$.  New theories always extend one or more other
wenzelm@3103
   308
theories, inheriting their types, constants, syntax, etc.  The theory
paulson@3485
   309
\thydx{Pure} contains nothing but Isabelle's meta-logic.  The variant
wenzelm@3103
   310
\thydx{CPure} offers the more usual higher-order function application
wenzelm@9695
   311
syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in Pure.
lcp@105
   312
wenzelm@3103
   313
Each theory definition must reside in a separate file, whose name is
wenzelm@3103
   314
the theory's with {\tt.thy} appended.  Calling
wenzelm@3103
   315
\ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it
wenzelm@3103
   316
  T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it
wenzelm@3103
   317
    T}.thy.ML}, reads the latter file, and deletes it if no errors
wenzelm@3103
   318
occurred.  This declares the {\ML} structure~$T$, which contains a
paulson@5205
   319
component \texttt{thy} denoting the new theory, a component for each
wenzelm@3103
   320
rule, and everything declared in {\it ML code}.
lcp@105
   321
wenzelm@3103
   322
Errors may arise during the translation to {\ML} (say, a misspelled
wenzelm@3103
   323
keyword) or during creation of the new theory (say, a type error in a
paulson@5205
   324
rule).  But if all goes well, \texttt{use_thy} will finally read the file
wenzelm@3103
   325
{\it T}{\tt.ML} (if it exists).  This file typically contains proofs
paulson@3485
   326
that refer to the components of~$T$.  The structure is automatically
wenzelm@3103
   327
opened, so its components may be referred to by unqualified names,
paulson@5205
   328
e.g.\ just \texttt{thy} instead of $T$\texttt{.thy}.
lcp@105
   329
wenzelm@3103
   330
\ttindexbold{use_thy} automatically loads a theory's parents before
wenzelm@3103
   331
loading the theory itself.  When a theory file is modified, many
wenzelm@3103
   332
theories may have to be reloaded.  Isabelle records the modification
wenzelm@3103
   333
times and dependencies of theory files.  See
lcp@331
   334
\iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
lcp@331
   335
                 {\S\ref{sec:reloading-theories}}
lcp@296
   336
for more details.
lcp@296
   337
lcp@105
   338
lcp@1084
   339
\subsection{Declaring constants, definitions and rules}
lcp@310
   340
\indexbold{constants!declaring}\index{rules!declaring}
lcp@310
   341
lcp@1084
   342
Most theories simply declare constants, definitions and rules.  The {\bf
lcp@1084
   343
  constant declaration part} has the form
lcp@105
   344
\begin{ttbox}
clasohm@1387
   345
consts  \(c@1\) :: \(\tau@1\)
lcp@105
   346
        \vdots
clasohm@1387
   347
        \(c@n\) :: \(\tau@n\)
lcp@105
   348
\end{ttbox}
lcp@105
   349
where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
clasohm@1387
   350
types.  The types must be enclosed in quotation marks if they contain
paulson@5205
   351
user-declared infix type constructors like \texttt{*}.  Each
lcp@105
   352
constant must be enclosed in quotation marks unless it is a valid
lcp@105
   353
identifier.  To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
lcp@105
   354
the $n$ declarations may be abbreviated to a single line:
lcp@105
   355
\begin{ttbox}
clasohm@1387
   356
        \(c@1\), \ldots, \(c@n\) :: \(\tau\)
lcp@105
   357
\end{ttbox}
lcp@105
   358
The {\bf rule declaration part} has the form
lcp@105
   359
\begin{ttbox}
lcp@105
   360
rules   \(id@1\) "\(rule@1\)"
lcp@105
   361
        \vdots
lcp@105
   362
        \(id@n\) "\(rule@n\)"
lcp@105
   363
\end{ttbox}
lcp@105
   364
where $id@1$, \ldots, $id@n$ are \ML{} identifiers and $rule@1$, \ldots,
lcp@284
   365
$rule@n$ are expressions of type~$prop$.  Each rule {\em must\/} be
paulson@14148
   366
enclosed in quotation marks.  Rules are simply axioms; they are 
paulson@14148
   367
called \emph{rules} because they are mainly used to specify the inference
paulson@14148
   368
rules when defining a new logic.
lcp@284
   369
wenzelm@3103
   370
\indexbold{definitions} The {\bf definition part} is similar, but with
paulson@5205
   371
the keyword \texttt{defs} instead of \texttt{rules}.  {\bf Definitions} are
wenzelm@3103
   372
rules of the form $s \equiv t$, and should serve only as
paulson@3485
   373
abbreviations.  The simplest form of a definition is $f \equiv t$,
paulson@3485
   374
where $f$ is a constant.  Also allowed are $\eta$-equivalent forms of
wenzelm@3106
   375
this, where the arguments of~$f$ appear applied on the left-hand side
wenzelm@3106
   376
of the equation instead of abstracted on the right-hand side.
lcp@1084
   377
wenzelm@3103
   378
Isabelle checks for common errors in definitions, such as extra
paulson@14148
   379
variables on the right-hand side and cyclic dependencies, that could
paulson@14148
   380
least to inconsistency.  It is still essential to take care:
paulson@14148
   381
theorems proved on the basis of incorrect definitions are useless,
paulson@14148
   382
your system can be consistent and yet still wrong.
wenzelm@3103
   383
wenzelm@3103
   384
\index{examples!of theories} This example theory extends first-order
wenzelm@3103
   385
logic by declaring and defining two constants, {\em nand} and {\em
wenzelm@3103
   386
  xor}:
lcp@284
   387
\begin{ttbox}
lcp@105
   388
Gate = FOL +
clasohm@1387
   389
consts  nand,xor :: [o,o] => o
lcp@1084
   390
defs    nand_def "nand(P,Q) == ~(P & Q)"
lcp@105
   391
        xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
lcp@105
   392
end
lcp@105
   393
\end{ttbox}
lcp@105
   394
nipkow@1649
   395
Declaring and defining constants can be combined:
nipkow@1649
   396
\begin{ttbox}
nipkow@1649
   397
Gate = FOL +
nipkow@1649
   398
constdefs  nand :: [o,o] => o
nipkow@1649
   399
           "nand(P,Q) == ~(P & Q)"
nipkow@1649
   400
           xor  :: [o,o] => o
nipkow@1649
   401
           "xor(P,Q)  == P & ~Q | ~P & Q"
nipkow@1649
   402
end
nipkow@1649
   403
\end{ttbox}
paulson@5205
   404
\texttt{constdefs} generates the names \texttt{nand_def} and \texttt{xor_def}
paulson@3485
   405
automatically, which is why it is restricted to alphanumeric identifiers.  In
nipkow@1649
   406
general it has the form
nipkow@1649
   407
\begin{ttbox}
nipkow@1649
   408
constdefs  \(id@1\) :: \(\tau@1\)
nipkow@1649
   409
           "\(id@1 \equiv \dots\)"
nipkow@1649
   410
           \vdots
nipkow@1649
   411
           \(id@n\) :: \(\tau@n\)
nipkow@1649
   412
           "\(id@n \equiv \dots\)"
nipkow@1649
   413
\end{ttbox}
nipkow@1649
   414
nipkow@1649
   415
nipkow@1366
   416
\begin{warn}
nipkow@1366
   417
A common mistake when writing definitions is to introduce extra free variables
nipkow@1468
   418
on the right-hand side as in the following fictitious definition:
nipkow@1366
   419
\begin{ttbox}
nipkow@1366
   420
defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
nipkow@1366
   421
\end{ttbox}
paulson@5205
   422
Isabelle rejects this ``definition'' because of the extra \texttt{m} on the
paulson@3485
   423
right-hand side, which would introduce an inconsistency.  What you should have
nipkow@1366
   424
written is
nipkow@1366
   425
\begin{ttbox}
nipkow@1366
   426
defs  prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"
nipkow@1366
   427
\end{ttbox}
nipkow@1366
   428
\end{warn}
lcp@105
   429
lcp@105
   430
\subsection{Declaring type constructors}
nipkow@303
   431
\indexbold{types!declaring}\indexbold{arities!declaring}
lcp@284
   432
%
lcp@105
   433
Types are composed of type variables and {\bf type constructors}.  Each
lcp@284
   434
type constructor takes a fixed number of arguments.  They are declared
lcp@284
   435
with an \ML-like syntax.  If $list$ takes one type argument, $tree$ takes
lcp@284
   436
two arguments and $nat$ takes no arguments, then these type constructors
lcp@284
   437
can be declared by
lcp@105
   438
\begin{ttbox}
lcp@284
   439
types 'a list
lcp@284
   440
      ('a,'b) tree
lcp@284
   441
      nat
lcp@105
   442
\end{ttbox}
lcp@284
   443
lcp@284
   444
The {\bf type declaration part} has the general form
lcp@284
   445
\begin{ttbox}
lcp@284
   446
types   \(tids@1\) \(id@1\)
lcp@284
   447
        \vdots
wenzelm@841
   448
        \(tids@n\) \(id@n\)
lcp@284
   449
\end{ttbox}
lcp@284
   450
where $id@1$, \ldots, $id@n$ are identifiers and $tids@1$, \ldots, $tids@n$
lcp@284
   451
are type argument lists as shown in the example above.  It declares each
lcp@284
   452
$id@i$ as a type constructor with the specified number of argument places.
lcp@105
   453
lcp@105
   454
The {\bf arity declaration part} has the form
lcp@105
   455
\begin{ttbox}
lcp@105
   456
arities \(tycon@1\) :: \(arity@1\)
lcp@105
   457
        \vdots
lcp@105
   458
        \(tycon@n\) :: \(arity@n\)
lcp@105
   459
\end{ttbox}
lcp@105
   460
where $tycon@1$, \ldots, $tycon@n$ are identifiers and $arity@1$, \ldots,
lcp@105
   461
$arity@n$ are arities.  Arity declarations add arities to existing
lcp@296
   462
types; they do not declare the types themselves.
lcp@105
   463
In the simplest case, for an 0-place type constructor, an arity is simply
lcp@105
   464
the type's class.  Let us declare a type~$bool$ of class $term$, with
lcp@284
   465
constants $tt$ and~$ff$.  (In first-order logic, booleans are
lcp@284
   466
distinct from formulae, which have type $o::logic$.)
lcp@105
   467
\index{examples!of theories}
lcp@284
   468
\begin{ttbox}
lcp@105
   469
Bool = FOL +
lcp@284
   470
types   bool
lcp@105
   471
arities bool    :: term
clasohm@1387
   472
consts  tt,ff   :: bool
lcp@105
   473
end
lcp@105
   474
\end{ttbox}
lcp@296
   475
A $k$-place type constructor may have arities of the form
lcp@296
   476
$(s@1,\ldots,s@k)c$, where $s@1,\ldots,s@n$ are sorts and $c$ is a class.
lcp@296
   477
Each sort specifies a type argument; it has the form $\{c@1,\ldots,c@m\}$,
lcp@296
   478
where $c@1$, \dots,~$c@m$ are classes.  Mostly we deal with singleton
lcp@296
   479
sorts, and may abbreviate them by dropping the braces.  The arity
lcp@296
   480
$(term)term$ is short for $(\{term\})term$.  Recall the discussion in
lcp@296
   481
\S\ref{polymorphic}.
lcp@105
   482
lcp@105
   483
A type constructor may be overloaded (subject to certain conditions) by
lcp@296
   484
appearing in several arity declarations.  For instance, the function type
lcp@331
   485
constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
lcp@105
   486
logic, it is declared also to have arity $(term,term)term$.
lcp@105
   487
paulson@5205
   488
Theory \texttt{List} declares the 1-place type constructor $list$, gives
paulson@5205
   489
it the arity $(term)term$, and declares constants $Nil$ and $Cons$ with
lcp@296
   490
polymorphic types:%
paulson@5205
   491
\footnote{In the \texttt{consts} part, type variable {\tt'a} has the default
paulson@5205
   492
  sort, which is \texttt{term}.  See the {\em Reference Manual\/}
lcp@296
   493
\iflabelundefined{sec:ref-defining-theories}{}%
lcp@296
   494
{(\S\ref{sec:ref-defining-theories})} for more information.}
lcp@105
   495
\index{examples!of theories}
lcp@284
   496
\begin{ttbox}
lcp@105
   497
List = FOL +
lcp@284
   498
types   'a list
lcp@105
   499
arities list    :: (term)term
clasohm@1387
   500
consts  Nil     :: 'a list
clasohm@1387
   501
        Cons    :: ['a, 'a list] => 'a list
lcp@105
   502
end
lcp@105
   503
\end{ttbox}
lcp@284
   504
Multiple arity declarations may be abbreviated to a single line:
lcp@105
   505
\begin{ttbox}
lcp@105
   506
arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
lcp@105
   507
\end{ttbox}
lcp@105
   508
wenzelm@3103
   509
%\begin{warn}
wenzelm@3103
   510
%Arity declarations resemble constant declarations, but there are {\it no\/}
wenzelm@3103
   511
%quotation marks!  Types and rules must be quoted because the theory
wenzelm@3103
   512
%translator passes them verbatim to the {\ML} output file.
wenzelm@3103
   513
%\end{warn}
lcp@105
   514
lcp@331
   515
\subsection{Type synonyms}\indexbold{type synonyms}
nipkow@303
   516
Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
lcp@307
   517
to those found in \ML.  Such synonyms are defined in the type declaration part
nipkow@303
   518
and are fairly self explanatory:
nipkow@303
   519
\begin{ttbox}
clasohm@1387
   520
types gate       = [o,o] => o
clasohm@1387
   521
      'a pred    = 'a => o
clasohm@1387
   522
      ('a,'b)nuf = 'b => 'a
nipkow@303
   523
\end{ttbox}
nipkow@303
   524
Type declarations and synonyms can be mixed arbitrarily:
nipkow@303
   525
\begin{ttbox}
nipkow@303
   526
types nat
clasohm@1387
   527
      'a stream = nat => 'a
clasohm@1387
   528
      signal    = nat stream
nipkow@303
   529
      'a list
nipkow@303
   530
\end{ttbox}
wenzelm@3103
   531
A synonym is merely an abbreviation for some existing type expression.
wenzelm@3103
   532
Hence synonyms may not be recursive!  Internally all synonyms are
wenzelm@3103
   533
fully expanded.  As a consequence Isabelle output never contains
wenzelm@3103
   534
synonyms.  Their main purpose is to improve the readability of theory
wenzelm@3103
   535
definitions.  Synonyms can be used just like any other type:
nipkow@303
   536
\begin{ttbox}
clasohm@1387
   537
consts and,or :: gate
clasohm@1387
   538
       negate :: signal => signal
nipkow@303
   539
\end{ttbox}
nipkow@303
   540
lcp@348
   541
\subsection{Infix and mixfix operators}
lcp@310
   542
\index{infixes}\index{examples!of theories}
lcp@310
   543
lcp@310
   544
Infix or mixfix syntax may be attached to constants.  Consider the
lcp@310
   545
following theory:
lcp@284
   546
\begin{ttbox}
lcp@105
   547
Gate2 = FOL +
clasohm@1387
   548
consts  "~&"     :: [o,o] => o         (infixl 35)
clasohm@1387
   549
        "#"      :: [o,o] => o         (infixl 30)
lcp@1084
   550
defs    nand_def "P ~& Q == ~(P & Q)"    
lcp@105
   551
        xor_def  "P # Q  == P & ~Q | ~P & Q"
lcp@105
   552
end
lcp@105
   553
\end{ttbox}
lcp@310
   554
The constant declaration part declares two left-associating infix operators
lcp@310
   555
with their priorities, or precedences; they are $\nand$ of priority~35 and
lcp@310
   556
$\xor$ of priority~30.  Hence $P \xor Q \xor R$ is parsed as $(P\xor Q)
lcp@310
   557
\xor R$ and $P \xor Q \nand R$ as $P \xor (Q \nand R)$.  Note the quotation
lcp@310
   558
marks in \verb|"~&"| and \verb|"#"|.
lcp@105
   559
lcp@105
   560
The constants \hbox{\verb|op ~&|} and \hbox{\verb|op #|} are declared
lcp@105
   561
automatically, just as in \ML.  Hence you may write propositions like
lcp@105
   562
\verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
lcp@105
   563
Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
lcp@105
   564
wenzelm@3212
   565
\medskip Infix syntax and constant names may be also specified
paulson@3485
   566
independently.  For example, consider this version of $\nand$:
wenzelm@3212
   567
\begin{ttbox}
wenzelm@3212
   568
consts  nand     :: [o,o] => o         (infixl "~&" 35)
wenzelm@3212
   569
\end{ttbox}
wenzelm@3212
   570
lcp@310
   571
\bigskip\index{mixfix declarations}
lcp@310
   572
{\bf Mixfix} operators may have arbitrary context-free syntaxes.  Let us
lcp@310
   573
add a line to the constant declaration part:
lcp@284
   574
\begin{ttbox}
clasohm@1387
   575
        If :: [o,o,o] => o       ("if _ then _ else _")
lcp@105
   576
\end{ttbox}
lcp@310
   577
This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
paulson@5205
   578
  if~$P$ then~$Q$ else~$R$} as well as \texttt{If($P$,$Q$,$R$)}.  Underscores
lcp@310
   579
denote argument positions.  
lcp@105
   580
paulson@5205
   581
The declaration above does not allow the \texttt{if}-\texttt{then}-{\tt
wenzelm@3103
   582
  else} construct to be printed split across several lines, even if it
wenzelm@3103
   583
is too long to fit on one line.  Pretty-printing information can be
wenzelm@3103
   584
added to specify the layout of mixfix operators.  For details, see
lcp@310
   585
\iflabelundefined{Defining-Logics}%
lcp@310
   586
    {the {\it Reference Manual}, chapter `Defining Logics'}%
lcp@310
   587
    {Chap.\ts\ref{Defining-Logics}}.
lcp@310
   588
lcp@310
   589
Mixfix declarations can be annotated with priorities, just like
lcp@105
   590
infixes.  The example above is just a shorthand for
lcp@284
   591
\begin{ttbox}
clasohm@1387
   592
        If :: [o,o,o] => o       ("if _ then _ else _" [0,0,0] 1000)
lcp@105
   593
\end{ttbox}
lcp@310
   594
The numeric components determine priorities.  The list of integers
lcp@310
   595
defines, for each argument position, the minimal priority an expression
lcp@310
   596
at that position must have.  The final integer is the priority of the
lcp@105
   597
construct itself.  In the example above, any argument expression is
lcp@310
   598
acceptable because priorities are non-negative, and conditionals may
lcp@310
   599
appear everywhere because 1000 is the highest priority.  On the other
lcp@310
   600
hand, the declaration
lcp@284
   601
\begin{ttbox}
clasohm@1387
   602
        If :: [o,o,o] => o       ("if _ then _ else _" [100,0,0] 99)
lcp@105
   603
\end{ttbox}
lcp@284
   604
defines concrete syntax for a conditional whose first argument cannot have
paulson@5205
   605
the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority
lcp@310
   606
of at least~100.  We may of course write
lcp@284
   607
\begin{quote}\tt
lcp@284
   608
if (if $P$ then $Q$ else $R$) then $S$ else $T$
lcp@156
   609
\end{quote}
lcp@310
   610
because expressions in parentheses have maximal priority.  
lcp@105
   611
lcp@105
   612
Binary type constructors, like products and sums, may also be declared as
lcp@105
   613
infixes.  The type declaration below introduces a type constructor~$*$ with
lcp@105
   614
infix notation $\alpha*\beta$, together with the mixfix notation
lcp@1084
   615
${<}\_,\_{>}$ for pairs.  We also see a rule declaration part.
lcp@310
   616
\index{examples!of theories}\index{mixfix declarations}
lcp@105
   617
\begin{ttbox}
lcp@105
   618
Prod = FOL +
lcp@284
   619
types   ('a,'b) "*"                           (infixl 20)
lcp@105
   620
arities "*"     :: (term,term)term
lcp@105
   621
consts  fst     :: "'a * 'b => 'a"
lcp@105
   622
        snd     :: "'a * 'b => 'b"
lcp@105
   623
        Pair    :: "['a,'b] => 'a * 'b"       ("(1<_,/_>)")
lcp@105
   624
rules   fst     "fst(<a,b>) = a"
lcp@105
   625
        snd     "snd(<a,b>) = b"
lcp@105
   626
end
lcp@105
   627
\end{ttbox}
lcp@105
   628
lcp@105
   629
\begin{warn}
paulson@5205
   630
  The name of the type constructor is~\texttt{*} and not \texttt{op~*}, as
wenzelm@3103
   631
  it would be in the case of an infix constant.  Only infix type
paulson@5205
   632
  constructors can have symbolic names like~\texttt{*}.  General mixfix
paulson@5205
   633
  syntax for types may be introduced via appropriate \texttt{syntax}
wenzelm@3103
   634
  declarations.
lcp@105
   635
\end{warn}
lcp@105
   636
lcp@105
   637
lcp@105
   638
\subsection{Overloading}
lcp@105
   639
\index{overloading}\index{examples!of theories}
lcp@105
   640
The {\bf class declaration part} has the form
lcp@105
   641
\begin{ttbox}
lcp@105
   642
classes \(id@1\) < \(c@1\)
lcp@105
   643
        \vdots
lcp@105
   644
        \(id@n\) < \(c@n\)
lcp@105
   645
\end{ttbox}
lcp@105
   646
where $id@1$, \ldots, $id@n$ are identifiers and $c@1$, \ldots, $c@n$ are
lcp@105
   647
existing classes.  It declares each $id@i$ as a new class, a subclass
lcp@105
   648
of~$c@i$.  In the general case, an identifier may be declared to be a
lcp@105
   649
subclass of $k$ existing classes:
lcp@105
   650
\begin{ttbox}
lcp@105
   651
        \(id\) < \(c@1\), \ldots, \(c@k\)
lcp@105
   652
\end{ttbox}
lcp@296
   653
Type classes allow constants to be overloaded.  As suggested in
lcp@307
   654
\S\ref{polymorphic}, let us define the class $arith$ of arithmetic
lcp@296
   655
types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
lcp@296
   656
\alpha$, for $\alpha{::}arith$.  We introduce $arith$ as a subclass of
lcp@296
   657
$term$ and add the three polymorphic constants of this class.
lcp@310
   658
\index{examples!of theories}\index{constants!overloaded}
lcp@105
   659
\begin{ttbox}
lcp@105
   660
Arith = FOL +
lcp@105
   661
classes arith < term
clasohm@1387
   662
consts  "0"     :: 'a::arith                  ("0")
clasohm@1387
   663
        "1"     :: 'a::arith                  ("1")
clasohm@1387
   664
        "+"     :: ['a::arith,'a] => 'a       (infixl 60)
lcp@105
   665
end
lcp@105
   666
\end{ttbox}
lcp@105
   667
No rules are declared for these constants: we merely introduce their
lcp@105
   668
names without specifying properties.  On the other hand, classes
lcp@105
   669
with rules make it possible to prove {\bf generic} theorems.  Such
lcp@105
   670
theorems hold for all instances, all types in that class.
lcp@105
   671
lcp@105
   672
We can now obtain distinct versions of the constants of $arith$ by
lcp@105
   673
declaring certain types to be of class $arith$.  For example, let us
lcp@105
   674
declare the 0-place type constructors $bool$ and $nat$:
lcp@105
   675
\index{examples!of theories}
lcp@105
   676
\begin{ttbox}
lcp@105
   677
BoolNat = Arith +
lcp@348
   678
types   bool  nat
lcp@348
   679
arities bool, nat   :: arith
clasohm@1387
   680
consts  Suc         :: nat=>nat
lcp@284
   681
\ttbreak
lcp@105
   682
rules   add0        "0 + n = n::nat"
lcp@105
   683
        addS        "Suc(m)+n = Suc(m+n)"
lcp@105
   684
        nat1        "1 = Suc(0)"
lcp@105
   685
        or0l        "0 + x = x::bool"
lcp@105
   686
        or0r        "x + 0 = x::bool"
lcp@105
   687
        or1l        "1 + x = 1::bool"
lcp@105
   688
        or1r        "x + 1 = 1::bool"
lcp@105
   689
end
lcp@105
   690
\end{ttbox}
lcp@105
   691
Because $nat$ and $bool$ have class $arith$, we can use $0$, $1$ and $+$ at
lcp@105
   692
either type.  The type constraints in the axioms are vital.  Without
paulson@14148
   693
constraints, the $x$ in $1+x = 1$ (axiom \texttt{or1l})
paulson@14148
   694
would have type $\alpha{::}arith$
lcp@105
   695
and the axiom would hold for any type of class $arith$.  This would
lcp@284
   696
collapse $nat$ to a trivial type:
lcp@105
   697
\[ Suc(1) = Suc(0+1) = Suc(0)+1 = 1+1 = 1! \]
lcp@296
   698
lcp@105
   699
lcp@296
   700
\section{Theory example: the natural numbers}
lcp@296
   701
lcp@296
   702
We shall now work through a small example of formalized mathematics
lcp@105
   703
demonstrating many of the theory extension features.
lcp@105
   704
lcp@105
   705
lcp@105
   706
\subsection{Extending first-order logic with the natural numbers}
lcp@105
   707
\index{examples!of theories}
lcp@105
   708
lcp@284
   709
Section\ts\ref{sec:logical-syntax} has formalized a first-order logic,
lcp@284
   710
including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
lcp@284
   711
Let us introduce the Peano axioms for mathematical induction and the
lcp@310
   712
freeness of $0$ and~$Suc$:\index{axioms!Peano}
lcp@307
   713
\[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
lcp@105
   714
 \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
lcp@105
   715
\]
lcp@105
   716
\[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad
lcp@105
   717
   \infer[(Suc\_neq\_0)]{R}{Suc(m)=0}
lcp@105
   718
\]
lcp@105
   719
Mathematical induction asserts that $P(n)$ is true, for any $n::nat$,
lcp@105
   720
provided $P(0)$ holds and that $P(x)$ implies $P(Suc(x))$ for all~$x$.
lcp@105
   721
Some authors express the induction step as $\forall x. P(x)\imp P(Suc(x))$.
lcp@105
   722
To avoid making induction require the presence of other connectives, we
lcp@105
   723
formalize mathematical induction as
lcp@105
   724
$$ \List{P(0); \Forall x. P(x)\Imp P(Suc(x))} \Imp P(n). \eqno(induct) $$
lcp@105
   725
lcp@105
   726
\noindent
lcp@105
   727
Similarly, to avoid expressing the other rules using~$\forall$, $\imp$
lcp@105
   728
and~$\neg$, we take advantage of the meta-logic;\footnote
lcp@105
   729
{On the other hand, the axioms $Suc(m)=Suc(n) \bimp m=n$
lcp@105
   730
and $\neg(Suc(m)=0)$ are logically equivalent to those given, and work
lcp@105
   731
better with Isabelle's simplifier.} 
lcp@105
   732
$(Suc\_neq\_0)$ is
lcp@105
   733
an elimination rule for $Suc(m)=0$:
lcp@105
   734
$$ Suc(m)=Suc(n) \Imp m=n  \eqno(Suc\_inject) $$
lcp@105
   735
$$ Suc(m)=0      \Imp R    \eqno(Suc\_neq\_0) $$
lcp@105
   736
lcp@105
   737
\noindent
lcp@105
   738
We shall also define a primitive recursion operator, $rec$.  Traditionally,
lcp@105
   739
primitive recursion takes a natural number~$a$ and a 2-place function~$f$,
lcp@105
   740
and obeys the equations
lcp@105
   741
\begin{eqnarray*}
lcp@105
   742
  rec(0,a,f)            & = & a \\
lcp@105
   743
  rec(Suc(m),a,f)       & = & f(m, rec(m,a,f))
lcp@105
   744
\end{eqnarray*}
lcp@105
   745
Addition, defined by $m+n \equiv rec(m,n,\lambda x\,y.Suc(y))$,
lcp@105
   746
should satisfy
lcp@105
   747
\begin{eqnarray*}
lcp@105
   748
  0+n      & = & n \\
lcp@105
   749
  Suc(m)+n & = & Suc(m+n)
lcp@105
   750
\end{eqnarray*}
lcp@296
   751
Primitive recursion appears to pose difficulties: first-order logic has no
lcp@296
   752
function-valued expressions.  We again take advantage of the meta-logic,
lcp@296
   753
which does have functions.  We also generalise primitive recursion to be
lcp@105
   754
polymorphic over any type of class~$term$, and declare the addition
lcp@105
   755
function:
lcp@105
   756
\begin{eqnarray*}
lcp@105
   757
  rec   & :: & [nat, \alpha{::}term, [nat,\alpha]\To\alpha] \To\alpha \\
lcp@105
   758
  +     & :: & [nat,nat]\To nat 
lcp@105
   759
\end{eqnarray*}
lcp@105
   760
lcp@105
   761
lcp@105
   762
\subsection{Declaring the theory to Isabelle}
lcp@105
   763
\index{examples!of theories}
lcp@310
   764
Let us create the theory \thydx{Nat} starting from theory~\verb$FOL$,
lcp@105
   765
which contains only classical logic with no natural numbers.  We declare
lcp@307
   766
the 0-place type constructor $nat$ and the associated constants.  Note that
lcp@307
   767
the constant~0 requires a mixfix annotation because~0 is not a legal
lcp@307
   768
identifier, and could not otherwise be written in terms:
lcp@310
   769
\begin{ttbox}\index{mixfix declarations}
lcp@105
   770
Nat = FOL +
lcp@284
   771
types   nat
lcp@105
   772
arities nat         :: term
clasohm@1387
   773
consts  "0"         :: nat                              ("0")
clasohm@1387
   774
        Suc         :: nat=>nat
clasohm@1387
   775
        rec         :: [nat, 'a, [nat,'a]=>'a] => 'a
clasohm@1387
   776
        "+"         :: [nat, nat] => nat                (infixl 60)
lcp@296
   777
rules   Suc_inject  "Suc(m)=Suc(n) ==> m=n"
lcp@105
   778
        Suc_neq_0   "Suc(m)=0      ==> R"
lcp@296
   779
        induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
lcp@105
   780
        rec_0       "rec(0,a,f) = a"
lcp@105
   781
        rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
lcp@296
   782
        add_def     "m+n == rec(m, n, \%x y. Suc(y))"
lcp@105
   783
end
lcp@105
   784
\end{ttbox}
paulson@5205
   785
In axiom \texttt{add_def}, recall that \verb|%| stands for~$\lambda$.
paulson@5205
   786
Loading this theory file creates the \ML\ structure \texttt{Nat}, which
wenzelm@3103
   787
contains the theory and axioms.
lcp@296
   788
lcp@296
   789
\subsection{Proving some recursion equations}
paulson@5205
   790
Theory \texttt{FOL/ex/Nat} contains proofs involving this theory of the
lcp@105
   791
natural numbers.  As a trivial example, let us derive recursion equations
lcp@105
   792
for \verb$+$.  Here is the zero case:
lcp@284
   793
\begin{ttbox}
paulson@5205
   794
Goalw [add_def] "0+n = n";
lcp@105
   795
{\out Level 0}
lcp@105
   796
{\out 0 + n = n}
lcp@284
   797
{\out  1. rec(0,n,\%x y. Suc(y)) = n}
lcp@105
   798
\ttbreak
lcp@105
   799
by (resolve_tac [rec_0] 1);
lcp@105
   800
{\out Level 1}
lcp@105
   801
{\out 0 + n = n}
lcp@105
   802
{\out No subgoals!}
wenzelm@3103
   803
qed "add_0";
lcp@284
   804
\end{ttbox}
lcp@105
   805
And here is the successor case:
lcp@284
   806
\begin{ttbox}
paulson@5205
   807
Goalw [add_def] "Suc(m)+n = Suc(m+n)";
lcp@105
   808
{\out Level 0}
lcp@105
   809
{\out Suc(m) + n = Suc(m + n)}
lcp@284
   810
{\out  1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))}
lcp@105
   811
\ttbreak
lcp@105
   812
by (resolve_tac [rec_Suc] 1);
lcp@105
   813
{\out Level 1}
lcp@105
   814
{\out Suc(m) + n = Suc(m + n)}
lcp@105
   815
{\out No subgoals!}
wenzelm@3103
   816
qed "add_Suc";
lcp@284
   817
\end{ttbox}
lcp@105
   818
The induction rule raises some complications, which are discussed next.
lcp@105
   819
\index{theories!defining|)}
lcp@105
   820
lcp@105
   821
lcp@105
   822
\section{Refinement with explicit instantiation}
lcp@310
   823
\index{resolution!with instantiation}
lcp@310
   824
\index{instantiation|(}
lcp@310
   825
lcp@105
   826
In order to employ mathematical induction, we need to refine a subgoal by
lcp@105
   827
the rule~$(induct)$.  The conclusion of this rule is $\Var{P}(\Var{n})$,
lcp@105
   828
which is highly ambiguous in higher-order unification.  It matches every
lcp@105
   829
way that a formula can be regarded as depending on a subterm of type~$nat$.
lcp@105
   830
To get round this problem, we could make the induction rule conclude
lcp@105
   831
$\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires
lcp@105
   832
refinement by~$(\forall E)$, which is equally hard!
lcp@105
   833
paulson@5205
   834
The tactic \texttt{res_inst_tac}, like \texttt{resolve_tac}, refines a subgoal by
lcp@105
   835
a rule.  But it also accepts explicit instantiations for the rule's
lcp@105
   836
schematic variables.  
lcp@105
   837
\begin{description}
lcp@310
   838
\item[\ttindex{res_inst_tac} {\it insts} {\it thm} {\it i}]
lcp@105
   839
instantiates the rule {\it thm} with the instantiations {\it insts}, and
lcp@105
   840
then performs resolution on subgoal~$i$.
lcp@105
   841
lcp@310
   842
\item[\ttindex{eres_inst_tac}] 
lcp@310
   843
and \ttindex{dres_inst_tac} are similar, but perform elim-resolution
lcp@105
   844
and destruct-resolution, respectively.
lcp@105
   845
\end{description}
lcp@105
   846
The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
lcp@105
   847
where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
lcp@307
   848
with no leading question marks! --- and $e@1$, \ldots, $e@n$ are
lcp@105
   849
expressions giving their instantiations.  The expressions are type-checked
lcp@105
   850
in the context of a particular subgoal: free variables receive the same
lcp@105
   851
types as they have in the subgoal, and parameters may appear.  Type
lcp@105
   852
variable instantiations may appear in~{\it insts}, but they are seldom
paulson@5205
   853
required: \texttt{res_inst_tac} instantiates type variables automatically
lcp@105
   854
whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$.
lcp@105
   855
lcp@105
   856
\subsection{A simple proof by induction}
lcp@310
   857
\index{examples!of induction}
lcp@105
   858
Let us prove that no natural number~$k$ equals its own successor.  To
lcp@105
   859
use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good
lcp@105
   860
instantiation for~$\Var{P}$.
lcp@284
   861
\begin{ttbox}
paulson@5205
   862
Goal "~ (Suc(k) = k)";
lcp@105
   863
{\out Level 0}
lcp@459
   864
{\out Suc(k) ~= k}
lcp@459
   865
{\out  1. Suc(k) ~= k}
lcp@105
   866
\ttbreak
lcp@105
   867
by (res_inst_tac [("n","k")] induct 1);
lcp@105
   868
{\out Level 1}
lcp@459
   869
{\out Suc(k) ~= k}
lcp@459
   870
{\out  1. Suc(0) ~= 0}
lcp@459
   871
{\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
lcp@284
   872
\end{ttbox}
lcp@105
   873
We should check that Isabelle has correctly applied induction.  Subgoal~1
lcp@105
   874
is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
lcp@105
   875
with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$.
lcp@310
   876
The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the
paulson@5205
   877
other rules of theory \texttt{Nat}.  The base case holds by~\ttindex{Suc_neq_0}:
lcp@284
   878
\begin{ttbox}
lcp@105
   879
by (resolve_tac [notI] 1);
lcp@105
   880
{\out Level 2}
lcp@459
   881
{\out Suc(k) ~= k}
lcp@105
   882
{\out  1. Suc(0) = 0 ==> False}
lcp@459
   883
{\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
lcp@105
   884
\ttbreak
lcp@105
   885
by (eresolve_tac [Suc_neq_0] 1);
lcp@105
   886
{\out Level 3}
lcp@459
   887
{\out Suc(k) ~= k}
lcp@459
   888
{\out  1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
lcp@284
   889
\end{ttbox}
lcp@105
   890
The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
lcp@284
   891
Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
lcp@284
   892
$Suc(Suc(x)) = Suc(x)$:
lcp@284
   893
\begin{ttbox}
lcp@105
   894
by (resolve_tac [notI] 1);
lcp@105
   895
{\out Level 4}
lcp@459
   896
{\out Suc(k) ~= k}
lcp@459
   897
{\out  1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
lcp@105
   898
\ttbreak
lcp@105
   899
by (eresolve_tac [notE] 1);
lcp@105
   900
{\out Level 5}
lcp@459
   901
{\out Suc(k) ~= k}
lcp@105
   902
{\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
lcp@105
   903
\ttbreak
lcp@105
   904
by (eresolve_tac [Suc_inject] 1);
lcp@105
   905
{\out Level 6}
lcp@459
   906
{\out Suc(k) ~= k}
lcp@105
   907
{\out No subgoals!}
lcp@284
   908
\end{ttbox}
lcp@105
   909
lcp@105
   910
paulson@5205
   911
\subsection{An example of ambiguity in \texttt{resolve_tac}}
lcp@105
   912
\index{examples!of induction}\index{unification!higher-order}
paulson@5205
   913
If you try the example above, you may observe that \texttt{res_inst_tac} is
lcp@105
   914
not actually needed.  Almost by chance, \ttindex{resolve_tac} finds the right
lcp@105
   915
instantiation for~$(induct)$ to yield the desired next state.  With more
lcp@105
   916
complex formulae, our luck fails.  
lcp@284
   917
\begin{ttbox}
paulson@5205
   918
Goal "(k+m)+n = k+(m+n)";
lcp@105
   919
{\out Level 0}
lcp@105
   920
{\out k + m + n = k + (m + n)}
lcp@105
   921
{\out  1. k + m + n = k + (m + n)}
lcp@105
   922
\ttbreak
lcp@105
   923
by (resolve_tac [induct] 1);
lcp@105
   924
{\out Level 1}
lcp@105
   925
{\out k + m + n = k + (m + n)}
lcp@105
   926
{\out  1. k + m + n = 0}
lcp@105
   927
{\out  2. !!x. k + m + n = x ==> k + m + n = Suc(x)}
lcp@284
   928
\end{ttbox}
lcp@284
   929
This proof requires induction on~$k$.  The occurrence of~0 in subgoal~1
lcp@284
   930
indicates that induction has been applied to the term~$k+(m+n)$; this
lcp@284
   931
application is sound but will not lead to a proof here.  Fortunately,
lcp@284
   932
Isabelle can (lazily!) generate all the valid applications of induction.
lcp@284
   933
The \ttindex{back} command causes backtracking to an alternative outcome of
lcp@284
   934
the tactic.
lcp@284
   935
\begin{ttbox}
lcp@105
   936
back();
lcp@105
   937
{\out Level 1}
lcp@105
   938
{\out k + m + n = k + (m + n)}
lcp@105
   939
{\out  1. k + m + n = k + 0}
lcp@105
   940
{\out  2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)}
lcp@284
   941
\end{ttbox}
lcp@284
   942
Now induction has been applied to~$m+n$.  This is equally useless.  Let us
lcp@284
   943
call \ttindex{back} again.
lcp@284
   944
\begin{ttbox}
lcp@105
   945
back();
lcp@105
   946
{\out Level 1}
lcp@105
   947
{\out k + m + n = k + (m + n)}
lcp@105
   948
{\out  1. k + m + 0 = k + (m + 0)}
lcp@284
   949
{\out  2. !!x. k + m + x = k + (m + x) ==>}
lcp@284
   950
{\out          k + m + Suc(x) = k + (m + Suc(x))}
lcp@284
   951
\end{ttbox}
lcp@105
   952
Now induction has been applied to~$n$.  What is the next alternative?
lcp@284
   953
\begin{ttbox}
lcp@105
   954
back();
lcp@105
   955
{\out Level 1}
lcp@105
   956
{\out k + m + n = k + (m + n)}
lcp@105
   957
{\out  1. k + m + n = k + (m + 0)}
lcp@105
   958
{\out  2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))}
lcp@284
   959
\end{ttbox}
lcp@105
   960
Inspecting subgoal~1 reveals that induction has been applied to just the
lcp@105
   961
second occurrence of~$n$.  This perfectly legitimate induction is useless
lcp@310
   962
here.  
lcp@310
   963
lcp@310
   964
The main goal admits fourteen different applications of induction.  The
lcp@310
   965
number is exponential in the size of the formula.
lcp@105
   966
lcp@105
   967
\subsection{Proving that addition is associative}
lcp@331
   968
Let us invoke the induction rule properly, using~{\tt
lcp@310
   969
  res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
lcp@310
   970
simplification tactics, which are described in 
lcp@310
   971
\iflabelundefined{simp-chap}%
lcp@310
   972
    {the {\em Reference Manual}}{Chap.\ts\ref{simp-chap}}.
lcp@284
   973
lcp@310
   974
\index{simplification}\index{examples!of simplification} 
lcp@310
   975
wenzelm@9695
   976
Isabelle's simplification tactics repeatedly apply equations to a subgoal,
wenzelm@9695
   977
perhaps proving it.  For efficiency, the rewrite rules must be packaged into a
wenzelm@9695
   978
{\bf simplification set},\index{simplification sets} or {\bf simpset}.  We
wenzelm@9695
   979
augment the implicit simpset of FOL with the equations proved in the previous
wenzelm@9695
   980
section, namely $0+n=n$ and $\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$:
lcp@284
   981
\begin{ttbox}
wenzelm@3114
   982
Addsimps [add_0, add_Suc];
lcp@284
   983
\end{ttbox}
lcp@105
   984
We state the goal for associativity of addition, and
lcp@105
   985
use \ttindex{res_inst_tac} to invoke induction on~$k$:
lcp@284
   986
\begin{ttbox}
paulson@5205
   987
Goal "(k+m)+n = k+(m+n)";
lcp@105
   988
{\out Level 0}
lcp@105
   989
{\out k + m + n = k + (m + n)}
lcp@105
   990
{\out  1. k + m + n = k + (m + n)}
lcp@105
   991
\ttbreak
lcp@105
   992
by (res_inst_tac [("n","k")] induct 1);
lcp@105
   993
{\out Level 1}
lcp@105
   994
{\out k + m + n = k + (m + n)}
lcp@105
   995
{\out  1. 0 + m + n = 0 + (m + n)}
lcp@284
   996
{\out  2. !!x. x + m + n = x + (m + n) ==>}
lcp@284
   997
{\out          Suc(x) + m + n = Suc(x) + (m + n)}
lcp@284
   998
\end{ttbox}
lcp@105
   999
The base case holds easily; both sides reduce to $m+n$.  The
wenzelm@3114
  1000
tactic~\ttindex{Simp_tac} rewrites with respect to the current
wenzelm@3114
  1001
simplification set, applying the rewrite rules for addition:
lcp@284
  1002
\begin{ttbox}
wenzelm@3114
  1003
by (Simp_tac 1);
lcp@105
  1004
{\out Level 2}
lcp@105
  1005
{\out k + m + n = k + (m + n)}
lcp@284
  1006
{\out  1. !!x. x + m + n = x + (m + n) ==>}
lcp@284
  1007
{\out          Suc(x) + m + n = Suc(x) + (m + n)}
lcp@284
  1008
\end{ttbox}
lcp@331
  1009
The inductive step requires rewriting by the equations for addition
paulson@14148
  1010
and with the induction hypothesis, which is also an equation.  The
wenzelm@3114
  1011
tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
wenzelm@3114
  1012
simplification set and any useful assumptions:
lcp@284
  1013
\begin{ttbox}
wenzelm@3114
  1014
by (Asm_simp_tac 1);
lcp@105
  1015
{\out Level 3}
lcp@105
  1016
{\out k + m + n = k + (m + n)}
lcp@105
  1017
{\out No subgoals!}
lcp@284
  1018
\end{ttbox}
lcp@310
  1019
\index{instantiation|)}
lcp@105
  1020
lcp@105
  1021
lcp@284
  1022
\section{A Prolog interpreter}
lcp@105
  1023
\index{Prolog interpreter|bold}
lcp@284
  1024
To demonstrate the power of tacticals, let us construct a Prolog
lcp@105
  1025
interpreter and execute programs involving lists.\footnote{To run these
paulson@5205
  1026
examples, see the file \texttt{FOL/ex/Prolog.ML}.} The Prolog program
lcp@105
  1027
consists of a theory.  We declare a type constructor for lists, with an
lcp@105
  1028
arity declaration to say that $(\tau)list$ is of class~$term$
lcp@105
  1029
provided~$\tau$ is:
lcp@105
  1030
\begin{eqnarray*}
lcp@105
  1031
  list  & :: & (term)term
lcp@105
  1032
\end{eqnarray*}
lcp@105
  1033
We declare four constants: the empty list~$Nil$; the infix list
lcp@105
  1034
constructor~{:}; the list concatenation predicate~$app$; the list reverse
lcp@284
  1035
predicate~$rev$.  (In Prolog, functions on lists are expressed as
lcp@105
  1036
predicates.)
lcp@105
  1037
\begin{eqnarray*}
lcp@105
  1038
    Nil         & :: & \alpha list \\
lcp@105
  1039
    {:}         & :: & [\alpha,\alpha list] \To \alpha list \\
lcp@105
  1040
    app & :: & [\alpha list,\alpha list,\alpha list] \To o \\
lcp@105
  1041
    rev & :: & [\alpha list,\alpha list] \To o 
lcp@105
  1042
\end{eqnarray*}
lcp@284
  1043
The predicate $app$ should satisfy the Prolog-style rules
lcp@105
  1044
\[ {app(Nil,ys,ys)} \qquad
lcp@105
  1045
   {app(xs,ys,zs) \over app(x:xs, ys, x:zs)} \]
lcp@105
  1046
We define the naive version of $rev$, which calls~$app$:
lcp@105
  1047
\[ {rev(Nil,Nil)} \qquad
lcp@105
  1048
   {rev(xs,ys)\quad  app(ys, x:Nil, zs) \over
lcp@105
  1049
    rev(x:xs, zs)} 
lcp@105
  1050
\]
lcp@105
  1051
lcp@105
  1052
\index{examples!of theories}
lcp@310
  1053
Theory \thydx{Prolog} extends first-order logic in order to make use
lcp@105
  1054
of the class~$term$ and the type~$o$.  The interpreter does not use the
paulson@5205
  1055
rules of~\texttt{FOL}.
lcp@105
  1056
\begin{ttbox}
lcp@105
  1057
Prolog = FOL +
lcp@296
  1058
types   'a list
lcp@105
  1059
arities list    :: (term)term
clasohm@1387
  1060
consts  Nil     :: 'a list
clasohm@1387
  1061
        ":"     :: ['a, 'a list]=> 'a list            (infixr 60)
clasohm@1387
  1062
        app     :: ['a list, 'a list, 'a list] => o
clasohm@1387
  1063
        rev     :: ['a list, 'a list] => o
lcp@105
  1064
rules   appNil  "app(Nil,ys,ys)"
lcp@105
  1065
        appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
lcp@105
  1066
        revNil  "rev(Nil,Nil)"
lcp@105
  1067
        revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"
lcp@105
  1068
end
lcp@105
  1069
\end{ttbox}
lcp@105
  1070
\subsection{Simple executions}
lcp@284
  1071
Repeated application of the rules solves Prolog goals.  Let us
lcp@105
  1072
append the lists $[a,b,c]$ and~$[d,e]$.  As the rules are applied, the
paulson@5205
  1073
answer builds up in~\texttt{?x}.
lcp@105
  1074
\begin{ttbox}
paulson@5205
  1075
Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
lcp@105
  1076
{\out Level 0}
lcp@105
  1077
{\out app(a : b : c : Nil, d : e : Nil, ?x)}
lcp@105
  1078
{\out  1. app(a : b : c : Nil, d : e : Nil, ?x)}
lcp@105
  1079
\ttbreak
lcp@105
  1080
by (resolve_tac [appNil,appCons] 1);
lcp@105
  1081
{\out Level 1}
lcp@105
  1082
{\out app(a : b : c : Nil, d : e : Nil, a : ?zs1)}
lcp@105
  1083
{\out  1. app(b : c : Nil, d : e : Nil, ?zs1)}
lcp@105
  1084
\ttbreak
lcp@105
  1085
by (resolve_tac [appNil,appCons] 1);
lcp@105
  1086
{\out Level 2}
lcp@105
  1087
{\out app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)}
lcp@105
  1088
{\out  1. app(c : Nil, d : e : Nil, ?zs2)}
lcp@105
  1089
\end{ttbox}
lcp@105
  1090
At this point, the first two elements of the result are~$a$ and~$b$.
lcp@105
  1091
\begin{ttbox}
lcp@105
  1092
by (resolve_tac [appNil,appCons] 1);
lcp@105
  1093
{\out Level 3}
lcp@105
  1094
{\out app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)}
lcp@105
  1095
{\out  1. app(Nil, d : e : Nil, ?zs3)}
lcp@105
  1096
\ttbreak
lcp@105
  1097
by (resolve_tac [appNil,appCons] 1);
lcp@105
  1098
{\out Level 4}
lcp@105
  1099
{\out app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)}
lcp@105
  1100
{\out No subgoals!}
lcp@105
  1101
\end{ttbox}
lcp@105
  1102
lcp@284
  1103
Prolog can run functions backwards.  Which list can be appended
lcp@105
  1104
with $[c,d]$ to produce $[a,b,c,d]$?
lcp@105
  1105
Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$:
lcp@105
  1106
\begin{ttbox}
paulson@5205
  1107
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
lcp@105
  1108
{\out Level 0}
lcp@105
  1109
{\out app(?x, c : d : Nil, a : b : c : d : Nil)}
lcp@105
  1110
{\out  1. app(?x, c : d : Nil, a : b : c : d : Nil)}
lcp@105
  1111
\ttbreak
lcp@105
  1112
by (REPEAT (resolve_tac [appNil,appCons] 1));
lcp@105
  1113
{\out Level 1}
lcp@105
  1114
{\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
lcp@105
  1115
{\out No subgoals!}
lcp@105
  1116
\end{ttbox}
lcp@105
  1117
lcp@105
  1118
lcp@310
  1119
\subsection{Backtracking}\index{backtracking!Prolog style}
lcp@296
  1120
Prolog backtracking can answer questions that have multiple solutions.
lcp@296
  1121
Which lists $x$ and $y$ can be appended to form the list $[a,b,c,d]$?  This
lcp@296
  1122
question has five solutions.  Using \ttindex{REPEAT} to apply the rules, we
lcp@296
  1123
quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$:
lcp@105
  1124
\begin{ttbox}
paulson@5205
  1125
Goal "app(?x, ?y, a:b:c:d:Nil)";
lcp@105
  1126
{\out Level 0}
lcp@105
  1127
{\out app(?x, ?y, a : b : c : d : Nil)}
lcp@105
  1128
{\out  1. app(?x, ?y, a : b : c : d : Nil)}
lcp@105
  1129
\ttbreak
lcp@105
  1130
by (REPEAT (resolve_tac [appNil,appCons] 1));
lcp@105
  1131
{\out Level 1}
lcp@105
  1132
{\out app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)}
lcp@105
  1133
{\out No subgoals!}
lcp@105
  1134
\end{ttbox}
lcp@284
  1135
Isabelle can lazily generate all the possibilities.  The \ttindex{back}
lcp@284
  1136
command returns the tactic's next outcome, namely $x=[a]$ and $y=[b,c,d]$:
lcp@105
  1137
\begin{ttbox}
lcp@105
  1138
back();
lcp@105
  1139
{\out Level 1}
lcp@105
  1140
{\out app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)}
lcp@105
  1141
{\out No subgoals!}
lcp@105
  1142
\end{ttbox}
lcp@105
  1143
The other solutions are generated similarly.
lcp@105
  1144
\begin{ttbox}
lcp@105
  1145
back();
lcp@105
  1146
{\out Level 1}
lcp@105
  1147
{\out app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)}
lcp@105
  1148
{\out No subgoals!}
lcp@105
  1149
\ttbreak
lcp@105
  1150
back();
lcp@105
  1151
{\out Level 1}
lcp@105
  1152
{\out app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)}
lcp@105
  1153
{\out No subgoals!}
lcp@105
  1154
\ttbreak
lcp@105
  1155
back();
lcp@105
  1156
{\out Level 1}
lcp@105
  1157
{\out app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)}
lcp@105
  1158
{\out No subgoals!}
lcp@105
  1159
\end{ttbox}
lcp@105
  1160
lcp@105
  1161
lcp@105
  1162
\subsection{Depth-first search}
lcp@105
  1163
\index{search!depth-first}
lcp@105
  1164
Now let us try $rev$, reversing a list.
paulson@5205
  1165
Bundle the rules together as the \ML{} identifier \texttt{rules}.  Naive
lcp@105
  1166
reverse requires 120 inferences for this 14-element list, but the tactic
lcp@105
  1167
terminates in a few seconds.
lcp@105
  1168
\begin{ttbox}
paulson@5205
  1169
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
lcp@105
  1170
{\out Level 0}
lcp@105
  1171
{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)}
lcp@284
  1172
{\out  1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
lcp@284
  1173
{\out         ?w)}
lcp@284
  1174
\ttbreak
lcp@105
  1175
val rules = [appNil,appCons,revNil,revCons];
lcp@105
  1176
\ttbreak
lcp@105
  1177
by (REPEAT (resolve_tac rules 1));
lcp@105
  1178
{\out Level 1}
lcp@105
  1179
{\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,}
lcp@105
  1180
{\out     n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)}
lcp@105
  1181
{\out No subgoals!}
lcp@105
  1182
\end{ttbox}
lcp@105
  1183
We may execute $rev$ backwards.  This, too, should reverse a list.  What
lcp@105
  1184
is the reverse of $[a,b,c]$?
lcp@105
  1185
\begin{ttbox}
paulson@5205
  1186
Goal "rev(?x, a:b:c:Nil)";
lcp@105
  1187
{\out Level 0}
lcp@105
  1188
{\out rev(?x, a : b : c : Nil)}
lcp@105
  1189
{\out  1. rev(?x, a : b : c : Nil)}
lcp@105
  1190
\ttbreak
lcp@105
  1191
by (REPEAT (resolve_tac rules 1));
lcp@105
  1192
{\out Level 1}
lcp@105
  1193
{\out rev(?x1 : Nil, a : b : c : Nil)}
lcp@105
  1194
{\out  1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
lcp@105
  1195
\end{ttbox}
lcp@105
  1196
The tactic has failed to find a solution!  It reached a dead end at
lcp@331
  1197
subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$
lcp@105
  1198
equals~$[a,b,c]$.  Backtracking explores other outcomes.
lcp@105
  1199
\begin{ttbox}
lcp@105
  1200
back();
lcp@105
  1201
{\out Level 1}
lcp@105
  1202
{\out rev(?x1 : a : Nil, a : b : c : Nil)}
lcp@105
  1203
{\out  1. app(Nil, ?x1 : Nil, b : c : Nil)}
lcp@105
  1204
\end{ttbox}
lcp@105
  1205
This too is a dead end, but the next outcome is successful.
lcp@105
  1206
\begin{ttbox}
lcp@105
  1207
back();
lcp@105
  1208
{\out Level 1}
lcp@105
  1209
{\out rev(c : b : a : Nil, a : b : c : Nil)}
lcp@105
  1210
{\out No subgoals!}
lcp@105
  1211
\end{ttbox}
lcp@310
  1212
\ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a
paulson@5205
  1213
search tactical.  \texttt{REPEAT} stops when it cannot continue, regardless of
lcp@310
  1214
which state is reached.  The tactical \ttindex{DEPTH_FIRST} searches for a
lcp@310
  1215
satisfactory state, as specified by an \ML{} predicate.  Below,
lcp@105
  1216
\ttindex{has_fewer_prems} specifies that the proof state should have no
lcp@310
  1217
subgoals.
lcp@105
  1218
\begin{ttbox}
lcp@105
  1219
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) 
lcp@105
  1220
                             (resolve_tac rules 1);
lcp@105
  1221
\end{ttbox}
lcp@284
  1222
Since Prolog uses depth-first search, this tactic is a (slow!) 
lcp@296
  1223
Prolog interpreter.  We return to the start of the proof using
paulson@5205
  1224
\ttindex{choplev}, and apply \texttt{prolog_tac}:
lcp@105
  1225
\begin{ttbox}
lcp@105
  1226
choplev 0;
lcp@105
  1227
{\out Level 0}
lcp@105
  1228
{\out rev(?x, a : b : c : Nil)}
lcp@105
  1229
{\out  1. rev(?x, a : b : c : Nil)}
lcp@105
  1230
\ttbreak
paulson@14148
  1231
by prolog_tac;
lcp@105
  1232
{\out Level 1}
lcp@105
  1233
{\out rev(c : b : a : Nil, a : b : c : Nil)}
lcp@105
  1234
{\out No subgoals!}
lcp@105
  1235
\end{ttbox}
paulson@5205
  1236
Let us try \texttt{prolog_tac} on one more example, containing four unknowns:
lcp@105
  1237
\begin{ttbox}
paulson@5205
  1238
Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
lcp@105
  1239
{\out Level 0}
lcp@105
  1240
{\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
lcp@105
  1241
{\out  1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}
lcp@105
  1242
\ttbreak
lcp@105
  1243
by prolog_tac;
lcp@105
  1244
{\out Level 1}
lcp@105
  1245
{\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}
lcp@105
  1246
{\out No subgoals!}
lcp@105
  1247
\end{ttbox}
lcp@284
  1248
Although Isabelle is much slower than a Prolog system, Isabelle
lcp@156
  1249
tactics can exploit logic programming techniques.  
lcp@156
  1250