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