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