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