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