doc-src/Tutorial/fp.tex
author wenzelm
Fri, 16 Jul 1999 22:24:42 +0200
changeset 7024 44bd3c094fd6
parent 6691 8a1b5f9d8420
child 7569 1d9263172b54
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     1
\chapter{Functional Programming in HOL}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     2
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     3
Although on the surface this chapter is mainly concerned with how to write
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     4
functional programs in HOL and how to verify them, most of the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     5
constructs and proof procedures introduced are general purpose and recur in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     6
any specification or verification task.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     7
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     8
The dedicated functional programmer should be warned: HOL offers only what
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
     9
could be called {\em total functional programming} --- all functions in HOL
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    10
must be total; lazy data structures are not directly available. On the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    11
positive side, functions in HOL need not be computable: HOL is a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    12
specification language that goes well beyond what can be expressed as a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    13
program. However, for the time being we concentrate on the computable.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    14
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    15
\section{An introductory theory}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    16
\label{sec:intro-theory}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    17
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    18
Functional programming needs datatypes and functions. Both of them can be
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    19
defined in a theory with a syntax reminiscent of languages like ML or
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    20
Haskell. As an example consider the theory in Fig.~\ref{fig:ToyList}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    21
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    22
\begin{figure}[htbp]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    23
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    24
\input{ToyList/ToyList.thy}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    25
\caption{A theory of lists}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    26
\label{fig:ToyList}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    27
\end{figure}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    28
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    29
HOL already has a predefined theory of lists called \texttt{List} ---
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    30
\texttt{ToyList} is merely a small fragment of it chosen as an example. In
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    31
contrast to what is recommended in \S\ref{sec:Basic:Theories},
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    32
\texttt{ToyList} is not based on \texttt{Main} but on \texttt{Datatype}, a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    33
theory that contains everything required for datatype definitions but does
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    34
not have \texttt{List} as a parent, thus avoiding ambiguities caused by
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    35
defining lists twice.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    36
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    37
The \ttindexbold{datatype} \texttt{list} introduces two constructors
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    38
\texttt{Nil} and \texttt{Cons}, the empty list and the operator that adds an
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    39
element to the front of a list. For example, the term \texttt{Cons True (Cons
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    40
  False Nil)} is a value of type \texttt{bool~list}, namely the list with the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    41
elements \texttt{True} and \texttt{False}. Because this notation becomes
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    42
unwieldy very quickly, the datatype declaration is annotated with an
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    43
alternative syntax: instead of \texttt{Nil} and \texttt{Cons}~$x$~$xs$ we can
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    44
write \index{#@{\tt[]}|bold}\texttt{[]} and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    45
\texttt{$x$~\#~$xs$}\index{#@{\tt\#}|bold}. In fact, this alternative syntax
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    46
is the standard syntax. Thus the list \texttt{Cons True (Cons False Nil)}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    47
becomes \texttt{True \# False \# []}. The annotation \ttindexbold{infixr}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    48
means that \texttt{\#} associates to the right, i.e.\ the term \texttt{$x$ \#
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    49
  $y$ \# $z$} is read as \texttt{$x$ \# ($y$ \# $z$)} and not as \texttt{($x$
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    50
  \# $y$) \# $z$}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    51
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    52
\begin{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    53
  Syntax annotations are a powerful but completely optional feature. You
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    54
  could drop them from theory \texttt{ToyList} and go back to the identifiers
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    55
  \texttt{Nil} and \texttt{Cons}. However, lists are such a central datatype
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    56
  that their syntax is highly customized. We recommend that novices should
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    57
  not use syntax annotations in their own theories.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    58
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    59
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    60
Next, the functions \texttt{app} and \texttt{rev} are declared. In contrast
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    61
to ML, Isabelle insists on explicit declarations of all functions (keyword
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    62
\ttindexbold{consts}).  (Apart from the declaration-before-use restriction,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    63
the order of items in a theory file is unconstrained.) Function \texttt{app}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    64
is annotated with concrete syntax too. Instead of the prefix syntax
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    65
\texttt{app}~$xs$~$ys$ the infix $xs$~\texttt{\at}~$ys$ becomes the preferred
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    66
form.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    67
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    68
Both functions are defined recursively. The equations for \texttt{app} and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    69
\texttt{rev} hardly need comments: \texttt{app} appends two lists and
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
    70
\texttt{rev} reverses a list.  The keyword \ttindex{primrec} indicates that
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    71
the recursion is of a particularly primitive kind where each recursive call
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    72
peels off a datatype constructor from one of the arguments (see
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    73
\S\ref{sec:datatype}).  Thus the recursion always terminates, i.e.\ the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    74
function is \bfindex{total}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    75
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    76
The termination requirement is absolutely essential in HOL, a logic of total
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    77
functions. If we were to drop it, inconsistencies could quickly arise: the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    78
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    79
$f(n)$ on both sides.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    80
% However, this is a subtle issue that we cannot discuss here further.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    81
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    82
\begin{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    83
  As we have indicated, the desire for total functions is not a gratuitously
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    84
  imposed restriction but an essential characteristic of HOL. It is only
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    85
  because of totality that reasoning in HOL is comparatively easy.  More
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    86
  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    87
  function definitions whose totality has not been proved) because they
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    88
  quickly lead to inconsistencies. Instead, fixed constructs for introducing
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    89
  types and functions are offered (such as \texttt{datatype} and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    90
  \texttt{primrec}) which are guaranteed to preserve consistency.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    91
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    92
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    93
A remark about syntax.  The textual definition of a theory follows a fixed
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    94
syntax with keywords like \texttt{datatype} and \texttt{end} (see
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    95
Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    96
Embedded in this syntax are the types and formulae of HOL, whose syntax is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    97
extensible, e.g.\ by new user-defined infix operators
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    98
(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
    99
HOL-specific should be enclosed in \texttt{"}\dots\texttt{"}. The same holds
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   100
for identifiers that happen to be keywords, as in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   101
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   102
consts "end" :: 'a list => 'a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   103
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   104
To lessen this burden, quotation marks around types can be dropped,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   105
provided their syntax does not go beyond what is described in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   106
\S\ref{sec:TypesTermsForms}. Types containing further operators, e.g.\
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
   107
\label{startype} \texttt{*} for Cartesian products, need quotation marks.
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   108
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   109
When Isabelle prints a syntax error message, it refers to the HOL syntax as
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   110
the \bfindex{inner syntax}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   111
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   112
\section{An introductory proof}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   113
\label{sec:intro-proof}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   114
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   115
Having defined \texttt{ToyList}, we load it with the ML command
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   116
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   117
use_thy "ToyList";
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   118
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   119
and are ready to prove a few simple theorems. This will illustrate not just
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   120
the basic proof commands but also the typical proof process.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   121
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   122
\subsubsection*{Main goal: \texttt{rev(rev xs) = xs}}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   123
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   124
Our goal is to show that reversing a list twice produces the original
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   125
list. Typing
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   126
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   127
\input{ToyList/thm}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   128
establishes a new goal to be proved in the context of the current theory,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   129
which is the one we just loaded. Isabelle's response is to print the current proof state:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   130
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   131
{\out Level 0}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   132
{\out rev (rev xs) = xs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   133
{\out  1. rev (rev xs) = xs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   134
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   135
Until we have finished a proof, the proof state always looks like this:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   136
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   137
{\out Level \(i\)}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   138
{\out \(G\)}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   139
{\out  1. \(G@1\)}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   140
{\out  \(\vdots\)}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   141
{\out  \(n\). \(G@n\)}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   142
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   143
where \texttt{Level}~$i$ indicates that we are $i$ steps into the proof, $G$
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   144
is the overall goal that we are trying to prove, and the numbered lines
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   145
contain the subgoals $G@1$, \dots, $G@n$ that we need to prove to establish
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   146
$G$. At \texttt{Level 0} there is only one subgoal, which is identical with
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   147
the overall goal.  Normally $G$ is constant and only serves as a reminder.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   148
Hence we rarely show it in this tutorial.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   149
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   150
Let us now get back to \texttt{rev(rev xs) = xs}. Properties of recursively
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   151
defined functions are best established by induction. In this case there is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   152
not much choice except to induct on \texttt{xs}:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   153
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   154
\input{ToyList/inductxs}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   155
This tells Isabelle to perform induction on variable \texttt{xs} in subgoal
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   156
1. The new proof state contains two subgoals, namely the base case
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   157
(\texttt{Nil}) and the induction step (\texttt{Cons}):
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   158
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   159
{\out 1. rev (rev []) = []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   160
{\out 2. !!a list. rev (rev list) = list ==> rev (rev (a # list)) = a # list}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   161
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   162
The induction step is an example of the general format of a subgoal:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   163
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   164
{\out  \(i\). !!\(x@1 \dots x@n\). {\it assumptions} ==> {\it conclusion}}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   165
\end{ttbox}\index{==>@{\tt==>}|bold}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   166
The prefix of bound variables \texttt{!!\(x@1 \dots x@n\)} can be ignored
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   167
most of the time, or simply treated as a list of variables local to this
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   168
subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.  The
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   169
{\it assumptions} are the local assumptions for this subgoal and {\it
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   170
  conclusion} is the actual proposition to be proved. Typical proof steps
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   171
that add new assumptions are induction or case distinction. In our example
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   172
the only assumption is the induction hypothesis \texttt{rev (rev list) =
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   173
  list}, where \texttt{list} is a variable name chosen by Isabelle. If there
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   174
are multiple assumptions, they are enclosed in the bracket pair
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   175
\texttt{[|}\index{==>@\ttlbr|bold} and \texttt{|]}\index{==>@\ttrbr|bold}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   176
and separated by semicolons.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   177
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   178
Let us try to solve both goals automatically:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   179
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   180
\input{ToyList/autotac}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   181
This command tells Isabelle to apply a proof strategy called
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   182
\texttt{Auto_tac} to all subgoals. Essentially, \texttt{Auto_tac} tries to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   183
`simplify' the subgoals.  In our case, subgoal~1 is solved completely (thanks
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   184
to the equation \texttt{rev [] = []}) and disappears; the simplified version
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   185
of subgoal~2 becomes the new subgoal~1:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   186
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   187
{\out 1. !!a list. rev(rev list) = list ==> rev(rev list @ a # []) = a # list}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   188
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   189
In order to simplify this subgoal further, a lemma suggests itself.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   190
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   191
\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   192
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   193
We start the proof as usual:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   194
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   195
\input{ToyList/lemma1}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   196
There are two variables that we could induct on: \texttt{xs} and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   197
\texttt{ys}. Because \texttt{\at} is defined by recursion on
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   198
the first argument, \texttt{xs} is the correct one:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   199
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   200
\input{ToyList/inductxs}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   201
This time not even the base case is solved automatically:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   202
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   203
by(Auto_tac);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   204
{\out 1. rev ys = rev ys @ []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   205
{\out 2. \dots}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   206
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   207
We need another lemma.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   208
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   209
\subsubsection*{Second lemma: \texttt{xs \at~[] = xs}}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   210
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   211
This time the canonical proof procedure
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   212
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   213
\input{ToyList/lemma2}\input{ToyList/inductxs}\input{ToyList/autotac}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   214
leads to the desired message \texttt{No subgoals!}:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   215
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   216
{\out Level 2}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   217
{\out xs @ [] = xs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   218
{\out No subgoals!}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   219
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   220
Now we can give the lemma just proved a suitable name
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   221
\begin{ttbox}
6691
8a1b5f9d8420 qed indexed.
nipkow
parents: 6628
diff changeset
   222
\input{ToyList/qed2}\end{ttbox}\index{*qed}
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   223
and tell Isabelle to use this lemma in all future proofs by simplification:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   224
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   225
\input{ToyList/addsimps2}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   226
Note that in the theorem \texttt{app_Nil2} the free variable \texttt{xs} has
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   227
been replaced by the unknown \texttt{?xs}, just as explained in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   228
\S\ref{sec:variables}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   229
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   230
Going back to the proof of the first lemma
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   231
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   232
\input{ToyList/lemma1}\input{ToyList/inductxs}\input{ToyList/autotac}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   233
we find that this time \texttt{Auto_tac} solves the base case, but the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   234
induction step merely simplifies to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   235
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   236
{\out 1. !!a list.}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   237
{\out       rev (list @ ys) = rev ys @ rev list}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   238
{\out       ==> (rev ys @ rev list) @ a # [] = rev ys @ rev list @ a # []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   239
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   240
Now we need to remember that \texttt{\at} associates to the right, and that
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   241
\texttt{\#} and \texttt{\at} have the same priority (namely the \texttt{65}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   242
in the definition of \texttt{ToyList}). Thus the conclusion really is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   243
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   244
{\out     ==> (rev ys @ rev list) @ (a # []) = rev ys @ (rev list @ (a # []))}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   245
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   246
and the missing lemma is associativity of \texttt{\at}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   247
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   248
\subsubsection*{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   249
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   250
This time the canonical proof procedure
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   251
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   252
\input{ToyList/lemma3}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   253
succeeds without further ado. Again we name the lemma and add it to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   254
the set of lemmas used during simplification:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   255
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   256
\input{ToyList/qed3}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   257
Now we can go back and prove the first lemma
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   258
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   259
\input{ToyList/lemma1}\input{ToyList/inductxs}\input{ToyList/autotac}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   260
add it to the simplification lemmas
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   261
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   262
\input{ToyList/qed1}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   263
and then solve our main theorem:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   264
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   265
\input{ToyList/thm}\input{ToyList/inductxs}\input{ToyList/autotac}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   266
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   267
\subsubsection*{Review}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   268
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   269
This is the end of our toy proof. It should have familiarized you with
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   270
\begin{itemize}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   271
\item the standard theorem proving procedure:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   272
state a goal; proceed with proof until a new lemma is required; prove that
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   273
lemma; come back to the original goal.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   274
\item a specific procedure that works well for functional programs:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   275
induction followed by all-out simplification via \texttt{Auto_tac}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   276
\item a basic repertoire of proof commands.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   277
\end{itemize}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   278
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   279
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   280
\section{Some helpful commands}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   281
\label{sec:commands-and-hints}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   282
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   283
This section discusses a few basic commands for manipulating the proof state
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   284
and can be skipped by casual readers.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   285
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   286
There are two kinds of commands used during a proof: the actual proof
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   287
commands and auxiliary commands for examining the proof state and controlling
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   288
the display. Proof commands are always of the form
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   289
\texttt{by(\textit{tactic});}\indexbold{tactic} where \textbf{tactic} is a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   290
synonym for ``theorem proving function''. Typical examples are
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   291
\texttt{induct_tac} and \texttt{Auto_tac} --- the suffix \texttt{_tac} is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   292
merely a mnemonic. Further tactics are introduced throughout the tutorial.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   293
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   294
%Tactics can also be modified. For example,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   295
%\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   296
%by(ALLGOALS Asm_simp_tac);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   297
%\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   298
%tells Isabelle to apply \texttt{Asm_simp_tac} to all subgoals. For more on
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   299
%tactics and how to combine them see~\S\ref{sec:Tactics}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   300
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   301
The most useful auxiliary commands are:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   302
\begin{description}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   303
\item[Printing the current state]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   304
Type \texttt{pr();} to redisplay the current proof state, for example when it
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   305
has disappeared off the screen.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   306
\item[Limiting the number of subgoals]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   307
Typing \texttt{prlim $k$;} tells Isabelle to print only the first $k$
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   308
subgoals from now on and redisplays the current proof state. This is helpful
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   309
when there are many subgoals.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   310
\item[Undoing] Typing \texttt{undo();} undoes the effect of the last
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   311
tactic.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   312
\item[Context switch] Every proof happens in the context of a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   313
  \bfindex{current theory}. By default, this is the last theory loaded. If
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   314
  you want to prove a theorem in the context of a different theory
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   315
  \texttt{T}, you need to type \texttt{context T.thy;}\index{*context|bold}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   316
  first. Of course you need to change the context again if you want to go
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   317
  back to your original theory.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   318
\item[Displaying types] We have already mentioned the flag
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   319
  \ttindex{show_types} above. It can also be useful for detecting typos in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   320
  formulae early on. For example, if \texttt{show_types} is set and the goal
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   321
  \texttt{rev(rev xs) = xs} is started, Isabelle prints the additional output
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   322
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   323
{\out Variables:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   324
{\out   xs :: 'a list}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   325
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   326
which tells us that Isabelle has correctly inferred that
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   327
\texttt{xs} is a variable of list type. On the other hand, had we
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   328
made a typo as in \texttt{rev(re xs) = xs}, the response
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   329
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   330
Variables:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   331
  re :: 'a list => 'a list
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   332
  xs :: 'a list
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   333
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   334
would have alerted us because of the unexpected variable \texttt{re}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   335
\item[(Re)loading theories]\index{loading theories}\index{reloading theories}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   336
Initially you load theory \texttt{T} by typing \ttindex{use_thy}~\texttt{"T";},
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   337
which loads all parent theories of \texttt{T} automatically, if they are not
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   338
loaded already. If you modify \texttt{T.thy} or \texttt{T.ML}, you can
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   339
reload it by typing \texttt{use_thy~"T";} again. This time, however, only
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   340
\texttt{T} is reloaded. If some of \texttt{T}'s parents have changed as well,
6577
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   341
type \ttindexbold{update_thy}~\texttt{"T";} to reload \texttt{T} and all of
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   342
its parents that have changed (or have changed parents).
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   343
\end{description}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   344
Further commands are found in the Reference Manual.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   345
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   346
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   347
\section{Datatypes}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   348
\label{sec:datatype}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   349
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   350
Inductive datatypes are part of almost every non-trivial application of HOL.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   351
First we take another look at a very important example, the datatype of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   352
lists, before we turn to datatypes in general. The section closes with a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   353
case study.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   354
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   355
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   356
\subsection{Lists}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   357
6148
d97a944c6ea3 isabelle.in.tum.de;
wenzelm
parents: 6099
diff changeset
   358
Lists are one of the essential datatypes in computing. Readers of this
d97a944c6ea3 isabelle.in.tum.de;
wenzelm
parents: 6099
diff changeset
   359
tutorial and users of HOL need to be familiar with their basic operations.
d97a944c6ea3 isabelle.in.tum.de;
wenzelm
parents: 6099
diff changeset
   360
Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory
6628
12ed4f748f7c pdf setup;
wenzelm
parents: 6606
diff changeset
   361
\texttt{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   362
The latter contains many further operations. For example, the functions
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   363
\ttindexbold{hd} (`head') and \ttindexbold{tl} (`tail') return the first
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   364
element and the remainder of a list. (However, pattern-matching is usually
6148
d97a944c6ea3 isabelle.in.tum.de;
wenzelm
parents: 6099
diff changeset
   365
preferable to \texttt{hd} and \texttt{tl}.)  Theory \texttt{List} also
d97a944c6ea3 isabelle.in.tum.de;
wenzelm
parents: 6099
diff changeset
   366
contains more syntactic sugar:
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   367
\texttt{[}$x@1$\texttt{,}\dots\texttt{,}$x@n$\texttt{]} abbreviates
6148
d97a944c6ea3 isabelle.in.tum.de;
wenzelm
parents: 6099
diff changeset
   368
$x@1$\texttt{\#}\dots\texttt{\#}$x@n$\texttt{\#[]}.  In the rest of the
d97a944c6ea3 isabelle.in.tum.de;
wenzelm
parents: 6099
diff changeset
   369
tutorial we always use HOL's predefined lists.
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   370
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   371
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   372
\subsection{The general format}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   373
\label{sec:general-datatype}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   374
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   375
The general HOL \texttt{datatype} definition is of the form
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   376
\[
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   377
\mathtt{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   378
C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   379
C@m~\tau@{m1}~\dots~\tau@{mk@m}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   380
\]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   381
where $\alpha@i$ are type variables (the parameters), $C@i$ are distinct
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   382
constructor names and $\tau@{ij}$ are types; it is customary to capitalize
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   383
the first letter in constructor names. There are a number of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   384
restrictions (such as the type should not be empty) detailed
6606
nipkow
parents: 6577
diff changeset
   385
elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   386
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   387
Laws about datatypes, such as \verb$[] ~= x#xs$ and \texttt{(x\#xs = y\#ys) =
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   388
  (x=y \& xs=ys)}, are used automatically during proofs by simplification.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   389
The same is true for the equations in primitive recursive function
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   390
definitions.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   391
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   392
\subsection{Primitive recursion}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   393
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   394
Functions on datatypes are usually defined by recursion. In fact, most of the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   395
time they are defined by what is called \bfindex{primitive recursion}.
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
   396
The keyword \ttindexbold{primrec} is followed by a list of equations
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   397
\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   398
such that $C$ is a constructor of the datatype $t$ and all recursive calls of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   399
$f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   400
Isabelle immediately sees that $f$ terminates because one (fixed!) argument
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   401
becomes smaller with every recursive call. There must be exactly one equation
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   402
for each constructor.  Their order is immaterial.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   403
A more general method for defining total recursive functions is explained in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   404
\S\ref{sec:recdef}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   405
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   406
\begin{exercise}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   407
Given the datatype of binary trees
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   408
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   409
\input{Misc/tree}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   410
define a function \texttt{mirror} that mirrors the structure of a binary tree
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   411
by swapping subtrees (recursively). Prove \texttt{mirror(mirror(t)) = t}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   412
\end{exercise}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   413
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   414
\subsection{\texttt{case}-expressions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   415
\label{sec:case-expressions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   416
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   417
HOL also features \ttindexbold{case}-expressions for analyzing elements of a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   418
datatype. For example,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   419
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   420
case xs of [] => 0 | y#ys => y
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   421
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   422
evaluates to \texttt{0} if \texttt{xs} is \texttt{[]} and to \texttt{y} if 
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   423
\texttt{xs} is \texttt{y\#ys}. (Since the result in both branches must be of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   424
the same type, it follows that \texttt{y::nat} and hence
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   425
\texttt{xs::(nat)list}.)
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   426
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   427
In general, if $e$ is a term of the datatype $t$ defined in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   428
\S\ref{sec:general-datatype} above, the corresponding
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   429
\texttt{case}-expression analyzing $e$ is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   430
\[
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   431
\begin{array}{rrcl}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   432
\mbox{\tt case}~e~\mbox{\tt of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   433
                           \vdots \\
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   434
                           \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   435
\end{array}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   436
\]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   437
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   438
\begin{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   439
{\em All} constructors must be present, their order is fixed, and nested
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   440
patterns are not supported.  Violating these restrictions results in strange
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   441
error messages.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   442
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   443
\noindent
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   444
Nested patterns can be simulated by nested \texttt{case}-expressions: instead
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   445
of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   446
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   447
case xs of [] => 0 | [x] => x | x#(y#zs) => y
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   448
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   449
write
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   450
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   451
case xs of [] => 0 | x#ys => (case ys of [] => x | y#zs => y)
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   452
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   453
Note that \texttt{case}-expressions should be enclosed in parentheses to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   454
indicate their scope.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   455
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   456
\subsection{Structural induction}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   457
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   458
Almost all the basic laws about a datatype are applied automatically during
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   459
simplification. Only induction is invoked by hand via \texttt{induct_tac},
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   460
which works for any datatype. In some cases, induction is overkill and a case
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   461
distinction over all constructors of the datatype suffices. This is performed
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   462
by \ttindexbold{exhaust_tac}. A trivial example:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   463
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   464
\input{Misc/exhaust.ML}{\out1. xs = [] ==> (case xs of [] => [] | y # ys => xs) = xs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   465
{\out2. !!a list. xs = a # list ==> (case xs of [] => [] | y # ys => xs) = xs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   466
\input{Misc/autotac.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   467
Note that this particular case distinction could have been automated
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   468
completely. See~\S\ref{sec:SimpFeatures}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   469
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   470
\begin{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   471
  Induction is only allowed on a free variable that should not occur among
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   472
  the assumptions of the subgoal.  Exhaustion works for arbitrary terms.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   473
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   474
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   475
\subsection{Case study: boolean expressions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   476
\label{sec:boolex}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   477
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   478
The aim of this case study is twofold: it shows how to model boolean
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   479
expressions and some algorithms for manipulating them, and it demonstrates
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   480
the constructs introduced above.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   481
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   482
\subsubsection{How can we model boolean expressions?}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   483
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   484
We want to represent boolean expressions built up from variables and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   485
constants by negation and conjunction. The following datatype serves exactly
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   486
that purpose:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   487
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   488
\input{Ifexpr/boolex}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   489
The two constants are represented by the terms \texttt{Const~True} and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   490
\texttt{Const~False}. Variables are represented by terms of the form
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   491
\texttt{Var}~$n$, where $n$ is a natural number (type \texttt{nat}).
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   492
For example, the formula $P@0 \land \neg P@1$ is represented by the term
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   493
\texttt{And~(Var~0)~(Neg(Var~1))}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   494
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   495
\subsubsection{What is the value of boolean expressions?}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   496
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   497
The value of a boolean expressions depends on the value of its variables.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   498
Hence the function \texttt{value} takes an additional parameter, an {\em
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   499
  environment} of type \texttt{nat~=>~bool}, which maps variables to their
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   500
values:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   501
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   502
\input{Ifexpr/value}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   503
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   504
\subsubsection{If-expressions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   505
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   506
An alternative and often more efficient (because in a certain sense
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   507
canonical) representation are so-called \textit{If-expressions\/} built up
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   508
from constants (\texttt{CIF}), variables (\texttt{VIF}) and conditionals
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   509
(\texttt{IF}):
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   510
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   511
\input{Ifexpr/ifex}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   512
The evaluation if If-expressions proceeds as for \texttt{boolex}:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   513
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   514
\input{Ifexpr/valif}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   515
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   516
\subsubsection{Transformation into and of If-expressions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   517
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   518
The type \texttt{boolex} is close to the customary representation of logical
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   519
formulae, whereas \texttt{ifex} is designed for efficiency. Thus we need to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   520
translate from \texttt{boolex} into \texttt{ifex}:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   521
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   522
\input{Ifexpr/bool2if}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   523
At last, we have something we can verify: that \texttt{bool2if} preserves the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   524
value of its argument.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   525
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   526
\input{Ifexpr/bool2if.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   527
The proof is canonical:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   528
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   529
\input{Ifexpr/proof.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   530
In fact, all proofs in this case study look exactly like this. Hence we do
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   531
not show them below.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   532
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   533
More interesting is the transformation of If-expressions into a normal form
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   534
where the first argument of \texttt{IF} cannot be another \texttt{IF} but
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   535
must be a constant or variable. Such a normal form can be computed by
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   536
repeatedly replacing a subterm of the form \texttt{IF~(IF~b~x~y)~z~u} by
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   537
\texttt{IF b (IF x z u) (IF y z u)}, which has the same value. The following
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   538
primitive recursive functions perform this task:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   539
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   540
\input{Ifexpr/normif}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   541
\input{Ifexpr/norm}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   542
Their interplay is a bit tricky, and we leave it to the reader to develop an
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   543
intuitive understanding. Fortunately, Isabelle can help us to verify that the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   544
transformation preserves the value of the expression:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   545
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   546
\input{Ifexpr/norm.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   547
The proof is canonical, provided we first show the following lemma (which
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   548
also helps to understand what \texttt{normif} does) and make it available
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   549
for simplification via \texttt{Addsimps}:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   550
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   551
\input{Ifexpr/normif.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   552
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   553
But how can we be sure that \texttt{norm} really produces a normal form in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   554
the above sense? We have to prove
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   555
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   556
\input{Ifexpr/normal_norm.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   557
where \texttt{normal} expresses that an If-expression is in normal form:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   558
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   559
\input{Ifexpr/normal}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   560
Of course, this requires a lemma about normality of \texttt{normif}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   561
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   562
\input{Ifexpr/normal_normif.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   563
that has to be made available for simplification via \texttt{Addsimps}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   564
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   565
How does one come up with the required lemmas? Try to prove the main theorems
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   566
without them and study carefully what \texttt{Auto_tac} leaves unproved. This
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   567
has to provide the clue.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   568
The necessity of universal quantification (\texttt{!t e}) in the two lemmas
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   569
is explained in \S\ref{sec:InductionHeuristics}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   570
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   571
\begin{exercise}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   572
  We strengthen the definition of a {\em normal\/} If-expression as follows:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   573
  the first argument of all \texttt{IF}s must be a variable. Adapt the above
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   574
  development to this changed requirement. (Hint: you may need to formulate
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   575
  some of the goals as implications (\texttt{-->}) rather than equalities
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   576
  (\texttt{=}).)
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   577
\end{exercise}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   578
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   579
\section{Some basic types}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   580
6577
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   581
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   582
\subsection{Natural numbers}
6577
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   583
\index{arithmetic|(}
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   584
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   585
The type \ttindexbold{nat} of natural numbers is predefined and behaves like
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   586
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   587
datatype nat = 0 | Suc nat
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   588
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   589
In particular, there are \texttt{case}-expressions, for example
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   590
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   591
case n of 0 => 0 | Suc m => m
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   592
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   593
primitive recursion, for example
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   594
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   595
\input{Misc/natsum}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   596
and induction, for example
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   597
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   598
\input{Misc/NatSum.ML}\ttbreak
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   599
{\out sum n + sum n = n * Suc n}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   600
{\out No subgoals!}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   601
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   602
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   603
The usual arithmetic operations \ttindexbold{+}, \ttindexbold{-},
6577
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   604
\ttindexbold{*}, \ttindexbold{div}, \ttindexbold{mod}, \ttindexbold{min} and
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   605
\ttindexbold{max} are predefined, as are the relations \ttindexbold{<=} and
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   606
\ttindexbold{<}. There is even a least number operation \ttindexbold{LEAST}.
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   607
For example, \texttt{(LEAST n.$\,$1 < n) = 2} (HOL does not prove this
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   608
completely automatically).
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   609
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   610
\begin{warn}
6577
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   611
  The operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{*},
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   612
  \ttindexbold{min}, \ttindexbold{max}, \ttindexbold{<=} and \ttindexbold{<}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   613
  are overloaded, i.e.\ they are available not just for natural numbers but
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   614
  at other types as well (see \S\ref{sec:TypeClasses}). For example, given
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   615
  the goal \texttt{x+y = y+x}, there is nothing to indicate that you are
6577
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   616
  talking about natural numbers.  Hence Isabelle can only infer that
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   617
  \texttt{x} and \texttt{y} are of some arbitrary type where \texttt{+} is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   618
  declared. As a consequence, you will be unable to prove the goal (although
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   619
  it may take you some time to realize what has happened if
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   620
  \texttt{show_types} is not set).  In this particular example, you need to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   621
  include an explicit type constraint, for example \texttt{x+y = y+(x::nat)}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   622
  If there is enough contextual information this may not be necessary:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   623
  \texttt{x+0 = x} automatically implies \texttt{x::nat}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   624
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   625
6577
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   626
Simple arithmetic goals are proved automatically by both \texttt{Auto_tac}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   627
and the simplification tactics introduced in \S\ref{sec:Simplification}.  For
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   628
example, the goal
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   629
\begin{ttbox}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   630
\input{Misc/arith1.ML}\end{ttbox}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   631
is proved automatically. The main restriction is that only addition is taken
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   632
into account; other arithmetic operations and quantified formulae are ignored.
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   633
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   634
For more complex goals, there is the special tactic \ttindexbold{arith_tac}. It
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   635
proves arithmetic goals involving the usual logical connectives (\verb$~$,
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   636
\verb$&$, \verb$|$, \verb$-->$), the relations \texttt{<=} and \texttt{<},
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   637
and the operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{min} and
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   638
\ttindexbold{max}. For example, it can prove
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   639
\begin{ttbox}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   640
\input{Misc/arith2.ML}\end{ttbox}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   641
because \texttt{k*k} can be treated as atomic.
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   642
In contrast, $n*n = n \Longrightarrow n=0 \lor n=1$ is not
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   643
even proved by \texttt{arith_tac} because the proof relies essentially on
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   644
properties of multiplication.
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   645
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   646
\begin{warn}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   647
  The running time of \texttt{arith_tac} is exponential in the number of
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   648
  occurrences of \ttindexbold{-}, \ttindexbold{min} and \ttindexbold{max}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   649
  because they are first eliminated by case distinctions.
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   650
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   651
  \texttt{arith_tac} is incomplete even for the restricted class of formulae
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   652
  described above (known as ``linear arithmetic''). If divisibility plays a
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   653
  role, it may fail to prove a valid formula, for example $m+m \neq n+n+1$.
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   654
  Fortunately, such examples are rare in practice.
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   655
\end{warn}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   656
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   657
\index{arithmetic|)}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
   658
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   659
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   660
\subsection{Products}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   661
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   662
HOL also has pairs: \texttt{($a@1$,$a@2$)} is of type \texttt{$\tau@1$ *
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   663
$\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   664
are extracted by \texttt{fst} and \texttt{snd}:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   665
\texttt{fst($x$,$y$) = $x$} and \texttt{snd($x$,$y$) = $y$}. Tuples
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   666
are simulated by pairs nested to the right: 
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   667
\texttt{($a@1$,$a@2$,$a@3$)} and \texttt{$\tau@1$ * $\tau@2$ * $\tau@3$}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   668
stand for \texttt{($a@1$,($a@2$,$a@3$))} and \texttt{$\tau@1$ * ($\tau@2$ *
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   669
$\tau@3$)}. Therefore \texttt{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   670
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   671
It is possible to use (nested) tuples as patterns in abstractions, for
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   672
example \texttt{\%(x,y,z).x+y+z} and \texttt{\%((x,y),z).x+y+z}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   673
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   674
In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   675
most variable binding constructs. Typical examples are
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   676
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   677
let (x,y) = f z in (y,x)
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   678
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   679
case xs of [] => 0 | (x,y)\#zs => x+y
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   680
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   681
Further important examples are quantifiers and sets.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   682
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   683
\begin{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   684
Abstraction over pairs and tuples is merely a convenient shorthand for a more
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   685
complex internal representation.  Thus the internal and external form of a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   686
term may differ, which can affect proofs. If you want to avoid this
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   687
complication, use \texttt{fst} and \texttt{snd}, i.e.\ write
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   688
\texttt{\%p.~fst p + snd p} instead of \texttt{\%(x,y).~x + y}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   689
See~\S\ref{} for theorem proving with tuple patterns.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   690
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   691
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   692
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   693
\section{Definitions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   694
\label{sec:Definitions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   695
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   696
A definition is simply an abbreviation, i.e.\ a new name for an existing
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   697
construction. In particular, definitions cannot be recursive. Isabelle offers
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   698
definitions on the level of types and terms. Those on the type level are
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   699
called type synonyms, those on the term level are called (constant)
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   700
definitions.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   701
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   702
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   703
\subsection{Type synonyms}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   704
\indexbold{type synonyms}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   705
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   706
Type synonyms are similar to those found in ML. Their syntax is fairly self
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   707
explanatory:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   708
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   709
\input{Misc/types}\end{ttbox}\indexbold{*types}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   710
The synonym \texttt{alist} shows that in general the type on the right-hand
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   711
side needs to be enclosed in double quotation marks
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   712
(see the end of~\S\ref{sec:intro-theory}).
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   713
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   714
Internally all synonyms are fully expanded.  As a consequence Isabelle's
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   715
output never contains synonyms.  Their main purpose is to improve the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   716
readability of theory definitions.  Synonyms can be used just like any other
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   717
type:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   718
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   719
\input{Misc/consts}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   720
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   721
\subsection{Constant definitions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   722
\label{sec:ConstDefinitions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   723
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   724
The above constants \texttt{nand} and \texttt{exor} are non-recursive and can
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   725
therefore be defined directly by
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   726
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   727
\input{Misc/defs}\end{ttbox}\indexbold{*defs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   728
where \texttt{defs} is a keyword and \texttt{nand_def} and \texttt{exor_def}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   729
are arbitrary user-supplied names.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   730
The symbol \texttt{==}\index{==>@{\tt==}|bold} is a special form of equality
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   731
that should only be used in constant definitions.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   732
Declarations and definitions can also be merged
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   733
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   734
\input{Misc/constdefs}\end{ttbox}\indexbold{*constdefs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   735
in which case the default name of each definition is $f$\texttt{_def}, where
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   736
$f$ is the name of the defined constant.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   737
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   738
Note that pattern-matching is not allowed, i.e.\ each definition must be of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   739
the form $f\,x@1\,\dots\,x@n$\texttt{~==~}$t$.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   740
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   741
Section~\S\ref{sec:Simplification} explains how definitions are used
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   742
in proofs.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   743
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   744
\begin{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   745
A common mistake when writing definitions is to introduce extra free variables
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   746
on the right-hand side as in the following fictitious definition:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   747
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   748
defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   749
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   750
Isabelle rejects this `definition' because of the extra {\tt m} on the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   751
right-hand side, which would introduce an inconsistency.  What you should have
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   752
written is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   753
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   754
defs  prime_def "prime(p) == !m. (m divides p) --> (m=1 | m=p)"
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   755
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   756
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   757
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   758
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   759
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   760
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   761
\chapter{More Functional Programming}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   762
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   763
The purpose of this chapter is to deepen the reader's understanding of the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   764
concepts encountered so far and to introduce an advanced method for defining
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   765
recursive functions. The first two sections give a structured presentation of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   766
theorem proving by simplification (\S\ref{sec:Simplification}) and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   767
discuss important heuristics for induction (\S\ref{sec:InductionHeuristics}). They
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   768
can be skipped by readers less interested in proofs. They are followed by a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   769
case study, a compiler for expressions (\S\ref{sec:ExprCompiler}).
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   770
Finally we present a very general method for defining recursive functions
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   771
that goes well beyond what \texttt{primrec} allows (\S\ref{sec:recdef}).
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   772
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   773
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   774
\section{Simplification}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   775
\label{sec:Simplification}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   776
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   777
So far we have proved our theorems by \texttt{Auto_tac}, which
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   778
`simplifies' all subgoals. In fact, \texttt{Auto_tac} can do much more than
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   779
that, except that it did not need to so far. However, when you go beyond toy
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   780
examples, you need to understand the ingredients of \texttt{Auto_tac}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   781
This section covers the tactic that \texttt{Auto_tac} always applies first,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   782
namely simplification.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   783
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   784
Simplification is one of the central theorem proving tools in Isabelle and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   785
many other systems. The tool itself is called the \bfindex{simplifier}. The
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   786
purpose of this section is twofold: to introduce the many features of the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   787
simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   788
simplifier works (\S\ref{sec:SimpHow}).  Anybody intending to use HOL should
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   789
read \S\ref{sec:SimpFeatures}, and the serious student should read
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   790
\S\ref{sec:SimpHow} as well in order to understand what happened in case
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   791
things do not simplify as expected.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   792
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   793
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   794
\subsection{Using the simplifier}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   795
\label{sec:SimpFeatures}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   796
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   797
In its most basic form, simplification means repeated application of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   798
equations from left to right. For example, taking the rules for \texttt{\at}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   799
and applying them to the term \texttt{[0,1] \at\ []} results in a sequence of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   800
simplification steps:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   801
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   802
(0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   803
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   804
This is also known as {\em term rewriting} and the equations are referred
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   805
to as {\em rewrite rules}. This is more honest than `simplification' because
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   806
the terms do not necessarily become simpler in the process.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   807
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   808
\subsubsection{Simpsets}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   809
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   810
To facilitate simplification, each theory has an associated set of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   811
simplification rules, known as a \bfindex{simpset}. Within a theory,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   812
proofs by simplification refer to the associated simpset by default.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   813
The simpset of a theory is built up as follows: starting with the union of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   814
the simpsets of the parent theories, each occurrence of a \texttt{datatype}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   815
or \texttt{primrec} construct augments the simpset. Explicit definitions are
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   816
not added automatically. Users can add new theorems via \texttt{Addsimps} and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   817
delete them again later by \texttt{Delsimps}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   818
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   819
You may augment a simpset not just by equations but by pretty much any
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   820
theorem. The simplifier will try to make sense of it.  For example, a theorem
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   821
\verb$~$$P$ is automatically turned into \texttt{$P$ = False}. The details are
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   822
explained in \S\ref{sec:SimpHow}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   823
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   824
As a rule of thumb, rewrite rules that really simplify a term (like
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   825
\texttt{xs \at\ [] = xs} and \texttt{rev(rev xs) = xs}) should be added to the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   826
current simpset right after they have been proved.  Those of a more specific
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   827
nature (e.g.\ distributivity laws, which alter the structure of terms
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   828
considerably) should only be added for specific proofs and deleted again
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   829
afterwards.  Conversely, it may also happen that a generally useful rule
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   830
needs to be removed for a certain proof and is added again afterwards.  The
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   831
need of frequent temporary additions or deletions may indicate a badly
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   832
designed simpset.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   833
\begin{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   834
  Simplification may not terminate, for example if both $f(x) = g(x)$ and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   835
  $g(x) = f(x)$ are in the simpset. It is the user's responsibility not to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   836
  include rules that can lead to nontermination, either on their own or in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   837
  combination with other rules.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   838
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   839
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   840
\subsubsection{Simplification tactics}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   841
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   842
There are four main simplification tactics:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   843
\begin{ttdescription}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   844
\item[\ttindexbold{Simp_tac} $i$] simplifies the conclusion of subgoal~$i$
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   845
  using the theory's simpset.  It may solve the subgoal completely if it has
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   846
  become trivial. For example:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   847
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   848
{\out 1. [] @ [] = []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   849
by(Simp_tac 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   850
{\out No subgoals!}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   851
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   852
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   853
\item[\ttindexbold{Asm_simp_tac}]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   854
  is like \verb$Simp_tac$, but extracts additional rewrite rules from
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   855
  the assumptions of the subgoal. For example, it solves
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   856
\begin{ttbox}\makeatother
6691
8a1b5f9d8420 qed indexed.
nipkow
parents: 6628
diff changeset
   857
{\out 1. xs = [] ==> xs @ ys = ys @ xs}
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   858
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   859
which \texttt{Simp_tac} does not do.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   860
  
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   861
\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   862
  simplifies the assumptions (without using the assumptions to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   863
  simplify each other or the actual goal).
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   864
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   865
\item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   866
  but also simplifies the assumptions. In particular, assumptions can
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   867
  simplify each other. For example:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   868
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   869
\out{ 1. [| xs @ zs = ys @ xs; [] @ xs = [] @ [] |] ==> ys = zs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   870
by(Asm_full_simp_tac 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   871
{\out No subgoals!}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   872
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   873
The second assumption simplifies to \texttt{xs = []}, which in turn
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   874
simplifies the first assumption to \texttt{zs = ys}, thus reducing the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   875
conclusion to \texttt{ys = ys} and hence to \texttt{True}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   876
(See also the paragraph on tracing below.)
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   877
\end{ttdescription}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   878
\texttt{Asm_full_simp_tac} is the most powerful of this quartet of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   879
tactics. In fact, \texttt{Auto_tac} starts by applying
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   880
\texttt{Asm_full_simp_tac} to all subgoals. The only reason for the existence
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   881
of the other three tactics is that sometimes one wants to limit the amount of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   882
simplification, for example to avoid nontermination:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   883
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   884
{\out  1. ! x. f x = g (f (g x)) ==> f [] = f [] @ []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   885
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   886
is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   887
\texttt{Asm_full_simp_tac} loop because the rewrite rule \texttt{f x = g(f(g
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   888
x))} extracted from the assumption does not terminate.  Isabelle notices
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   889
certain simple forms of nontermination, but not this one.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   890
 
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   891
\subsubsection{Modifying simpsets locally}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   892
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   893
If a certain theorem is merely needed in one proof by simplification, the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   894
pattern
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   895
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   896
Addsimps [\(rare_theorem\)];
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   897
by(Simp_tac 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   898
Delsimps [\(rare_theorem\)];
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   899
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   900
is awkward. Therefore there are lower-case versions of the simplification
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   901
tactics (\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   902
\ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}) and of the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   903
simpset modifiers (\ttindexbold{addsimps}, \ttindexbold{delsimps})
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   904
that do not access or modify the implicit simpset but explicitly take a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   905
simpset as an argument. For example, the above three lines become
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   906
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   907
by(simp_tac (simpset() addsimps [\(rare_theorem\)]) 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   908
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   909
where the result of the function call \texttt{simpset()} is the simpset of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   910
the current theory and \texttt{addsimps} is an infix function. The implicit
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   911
simpset is read once but not modified.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   912
This is far preferable to pairs of \texttt{Addsimps} and \texttt{Delsimps}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   913
Local modifications can be stacked as in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   914
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   915
by(simp_tac (simpset() addsimps [\(rare_theorem\)] delsimps [\(some_thm\)]) 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   916
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   917
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   918
\subsubsection{Rewriting with definitions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   919
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   920
Constant definitions (\S\ref{sec:ConstDefinitions}) are not automatically
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   921
included in the simpset of a theory. Hence such definitions are not expanded
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   922
automatically either, just as it should be: definitions are introduced for
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   923
the purpose of abbreviating complex concepts. Of course we need to expand the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   924
definitions initially to derive enough lemmas that characterize the concept
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   925
sufficiently for us to forget the original definition completely. For
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   926
example, given the theory
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   927
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   928
\input{Misc/Exor.thy}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   929
we may want to prove \verb$exor A (~A)$. Instead of \texttt{Goal} we use
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   930
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   931
\input{Misc/exorgoal.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   932
which tells Isabelle to expand the definition of \texttt{exor}---the first
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   933
argument of \texttt{Goalw} can be a list of definitions---in the initial goal:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   934
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   935
{\out exor A (~ A)}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   936
{\out  1. A & ~ ~ A | ~ A & ~ A}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   937
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   938
In this simple example, the goal is proved by \texttt{Simp_tac}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   939
Of course the resulting theorem is insufficient to characterize \texttt{exor}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   940
completely.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   941
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   942
In case we want to expand a definition in the middle of a proof, we can
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   943
simply add the definition locally to the simpset:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   944
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   945
\input{Misc/exorproof.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   946
You should normally not add the definition permanently to the simpset
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   947
using \texttt{Addsimps} because this defeats the whole purpose of an
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   948
abbreviation.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   949
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   950
\begin{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   951
If you have defined $f\,x\,y$\texttt{~==~}$t$ then you can only expand
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   952
occurrences of $f$ with at least two arguments. Thus it is safer to define
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   953
$f$\texttt{~==~\%$x\,y$.}$\;t$.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   954
\end{warn}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   955
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   956
\subsubsection{Simplifying \texttt{let}-expressions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   957
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   958
Proving a goal containing \ttindex{let}-expressions invariably requires the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   959
\texttt{let}-constructs to be expanded at some point. Since
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   960
\texttt{let}-\texttt{in} is just syntactic sugar for a defined constant
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   961
(called \texttt{Let}), expanding \texttt{let}-constructs means rewriting with
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   962
\texttt{Let_def}:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   963
%context List.thy;
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   964
%Goal "(let xs = [] in xs@xs) = ys";
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   965
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   966
{\out  1. (let xs = [] in xs @ xs) = ys}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   967
by(simp_tac (simpset() addsimps [Let_def]) 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   968
{\out  1. [] = ys}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   969
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   970
If, in a particular context, there is no danger of a combinatorial explosion
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   971
of nested \texttt{let}s one could even add \texttt{Let_def} permanently via
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   972
\texttt{Addsimps}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   973
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   974
\subsubsection{Conditional equations}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   975
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   976
So far all examples of rewrite rules were equations. The simplifier also
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   977
accepts {\em conditional\/} equations, for example
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   978
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   979
xs ~= []  ==>  hd xs # tl xs = xs \hfill \((*)\)
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   980
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   981
(which is proved by \texttt{exhaust_tac} on \texttt{xs} followed by
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   982
\texttt{Asm_full_simp_tac} twice). Assuming that this theorem together with
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   983
%\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   984
\texttt{(rev xs = []) = (xs = [])}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   985
%\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   986
are part of the simpset, the subgoal
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   987
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   988
{\out 1. xs ~= [] ==> hd(rev xs) # tl(rev xs) = rev xs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   989
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   990
is proved by simplification:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   991
the conditional equation $(*)$ above
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   992
can simplify \texttt{hd(rev~xs)~\#~tl(rev~xs)} to \texttt{rev xs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   993
because the corresponding precondition \verb$rev xs ~= []$ simplifies to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   994
\verb$xs ~= []$, which is exactly the local assumption of the subgoal.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   995
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   996
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   997
\subsubsection{Automatic case splits}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   998
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
   999
Goals containing \ttindex{if}-expressions are usually proved by case
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1000
distinction on the condition of the \texttt{if}. For example the goal
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1001
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1002
{\out 1. ! xs. if xs = [] then rev xs = [] else rev xs ~= []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1003
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1004
can be split into
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1005
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1006
{\out 1. ! xs. (xs = [] --> rev xs = []) \& (xs ~= [] --> rev xs ~= [])}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1007
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1008
by typing
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1009
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1010
\input{Misc/splitif.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1011
Because this is almost always the right proof strategy, the simplifier
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1012
performs case-splitting on \texttt{if}s automatically. Try \texttt{Simp_tac}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1013
on the initial goal above.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1014
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1015
This splitting idea generalizes from \texttt{if} to \ttindex{case}:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1016
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1017
{\out 1. (case xs of [] => zs | y#ys => y#(ys@zs)) = xs@zs}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1018
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1019
becomes
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1020
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1021
{\out 1. (xs = [] --> zs = xs @ zs) &}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1022
{\out    (! a list. xs = a # list --> a # list @ zs = xs @ zs)}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1023
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1024
by typing
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1025
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1026
\input{Misc/splitlist.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1027
In contrast to \texttt{if}-expressions, the simplifier does not split
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1028
\texttt{case}-expressions by default because this can lead to nontermination
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1029
in case of recursive datatypes.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1030
Nevertheless the simplifier can be instructed to perform \texttt{case}-splits
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1031
by adding the appropriate rule to the simpset:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1032
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1033
by(simp_tac (simpset() addsplits [split_list_case]) 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1034
\end{ttbox}\indexbold{*addsplits}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1035
solves the initial goal outright, which \texttt{Simp_tac} alone will not do.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1036
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1037
In general, every datatype $t$ comes with a rule
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1038
\texttt{$t$.split} that can be added to the simpset either
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1039
locally via \texttt{addsplits} (see above), or permanently via
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1040
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1041
Addsplits [\(t\).split];
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1042
\end{ttbox}\indexbold{*Addsplits}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1043
Split-rules can be removed globally via \ttindexbold{Delsplits} and locally
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1044
via \ttindexbold{delsplits} as, for example, in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1045
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1046
by(simp_tac (simpset() addsimps [\(\dots\)] delsplits [split_if]) 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1047
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1048
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1049
6577
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1050
\subsubsection{Arithmetic}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1051
\index{arithmetic}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1052
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1053
The simplifier routinely solves a small class of linear arithmetic formulae
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1054
(over types \texttt{nat} and \texttt{int}): it only takes into account
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1055
assumptions and conclusions that are (possibly negated) (in)equalities
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1056
(\texttt{=}, \texttt{<=}, \texttt{<}) and it only knows about addition. Thus
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1057
\begin{ttbox}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1058
\input{Misc/arith1.ML}\end{ttbox}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1059
is proved by simplification, whereas the only slightly more complex
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1060
\begin{ttbox}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1061
\input{Misc/arith3.ML}\end{ttbox}
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1062
is not proved by simplification and requires \texttt{arith_tac}.
a2b5c84d590a Arithmetic.
nipkow
parents: 6148
diff changeset
  1063
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1064
\subsubsection{Permutative rewrite rules}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1065
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1066
A rewrite rule is {\bf permutative} if the left-hand side and right-hand side
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1067
are the same up to renaming of variables.  The most common permutative rule
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1068
is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.  Such
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1069
rules are problematic because once they apply, they can be used forever.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1070
The simplifier is aware of this danger and treats permutative rules
6606
nipkow
parents: 6577
diff changeset
  1071
separately. For details see~\cite{isabelle-ref}.
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1072
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1073
\subsubsection{Tracing}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1074
\indexbold{tracing the simplifier}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1075
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1076
Using the simplifier effectively may take a bit of experimentation.  Set the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1077
\verb$trace_simp$ flag to get a better idea of what is going on:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1078
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1079
{\out  1. rev [x] = []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1080
\ttbreak
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1081
set trace_simp;
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1082
by(Simp_tac 1);
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1083
\ttbreak\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1084
{\out Applying instance of rewrite rule:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1085
{\out rev (?x # ?xs) == rev ?xs @ [?x]}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1086
{\out Rewriting:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1087
{\out rev [x] == rev [] @ [x]}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1088
\ttbreak
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1089
{\out Applying instance of rewrite rule:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1090
{\out rev [] == []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1091
{\out Rewriting:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1092
{\out rev [] == []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1093
\ttbreak\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1094
{\out Applying instance of rewrite rule:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1095
{\out [] @ ?y == ?y}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1096
{\out Rewriting:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1097
{\out [] @ [x] == [x]}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1098
\ttbreak
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1099
{\out Applying instance of rewrite rule:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1100
{\out ?x # ?t = ?t == False}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1101
{\out Rewriting:}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1102
{\out [x] = [] == False}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1103
\ttbreak
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1104
{\out Level 1}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1105
{\out rev [x] = []}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1106
{\out  1. False}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1107
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1108
In more complicated cases, the trace can be enormous, especially since
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1109
invocations of the simplifier are often nested (e.g.\ when solving conditions
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1110
of rewrite rules).
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1111
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1112
\subsection{How it works}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1113
\label{sec:SimpHow}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1114
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1115
\subsubsection{Higher-order patterns}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1116
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1117
\subsubsection{Local assumptions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1118
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1119
\subsubsection{The preprocessor}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1120
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1121
\section{Induction heuristics}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1122
\label{sec:InductionHeuristics}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1123
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1124
The purpose of this section is to illustrate some simple heuristics for
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1125
inductive proofs. The first one we have already mentioned in our initial
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1126
example:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1127
\begin{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1128
{\em 1. Theorems about recursive functions are proved by induction.}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1129
\end{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1130
In case the function has more than one argument
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1131
\begin{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1132
{\em 2. Do induction on argument number $i$ if the function is defined by
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1133
recursion in argument number $i$.}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1134
\end{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1135
When we look at the proof of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1136
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1137
(xs @ ys) @ zs = xs @ (ys @ zs)
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1138
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1139
in \S\ref{sec:intro-proof} we find (a) \texttt{\at} is recursive in the first
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1140
argument, (b) \texttt{xs} occurs only as the first argument of \texttt{\at},
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1141
and (c) both \texttt{ys} and \texttt{zs} occur at least once as the second
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1142
argument of \texttt{\at}. Hence it is natural to perform induction on
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1143
\texttt{xs}.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1144
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1145
The key heuristic, and the main point of this section, is to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1146
generalize the goal before induction. The reason is simple: if the goal is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1147
too specific, the induction hypothesis is too weak to allow the induction
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1148
step to go through. Let us now illustrate the idea with an example.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1149
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1150
We define a tail-recursive version of list-reversal,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1151
i.e.\ one that can be compiled into a loop:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1152
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1153
\input{Misc/Itrev.thy}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1154
The behaviour of \texttt{itrev} is simple: it reverses its first argument by
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1155
stacking its elements onto the second argument, and returning that second
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1156
argument when the first one becomes empty.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1157
We need to show that \texttt{itrev} does indeed reverse its first argument
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1158
provided the second one is empty:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1159
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1160
\input{Misc/itrev1.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1161
There is no choice as to the induction variable, and we immediately simplify:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1162
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1163
\input{Misc/induct_auto.ML}\ttbreak\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1164
{\out1. !!a list. itrev list [] = rev list\(\;\)==> itrev list [a] = rev list @ [a]}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1165
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1166
Just as predicted above, the overall goal, and hence the induction
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1167
hypothesis, is too weak to solve the induction step because of the fixed
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1168
\texttt{[]}. The corresponding heuristic:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1169
\begin{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1170
{\em 3. Generalize goals for induction by replacing constants by variables.}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1171
\end{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1172
Of course one cannot do this na\"{\i}vely: \texttt{itrev xs ys = rev xs} is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1173
just not true --- the correct generalization is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1174
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1175
\input{Misc/itrev2.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1176
If \texttt{ys} is replaced by \texttt{[]}, the right-hand side simplifies to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1177
\texttt{rev xs}, just as required.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1178
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1179
In this particular instance it is easy to guess the right generalization,
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1180
but in more complex situations a good deal of creativity is needed. This is
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1181
the main source of complications in inductive proofs.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1182
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1183
Although we now have two variables, only \texttt{xs} is suitable for
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1184
induction, and we repeat our above proof attempt. Unfortunately, we are still
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1185
not there:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1186
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1187
{\out 1. !!a list.}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1188
{\out       itrev list ys = rev list @ ys}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1189
{\out       ==> itrev list (a # ys) = rev list @ a # ys}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1190
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1191
The induction hypothesis is still too weak, but this time it takes no
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1192
intuition to generalize: the problem is that \texttt{ys} is fixed throughout
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1193
the subgoal, but the induction hypothesis needs to be applied with
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1194
\texttt{a \# ys} instead of \texttt{ys}. Hence we prove the theorem
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1195
for all \texttt{ys} instead of a fixed one:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1196
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1197
\input{Misc/itrev3.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1198
This time induction on \texttt{xs} followed by simplification succeeds. This
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1199
leads to another heuristic for generalization:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1200
\begin{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1201
{\em 4. Generalize goals for induction by universally quantifying all free
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1202
variables {\em(except the induction variable itself!)}.}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1203
\end{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1204
This prevents trivial failures like the above and does not change the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1205
provability of the goal. Because it is not always required, and may even
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1206
complicate matters in some cases, this heuristic is often not
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1207
applied blindly.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1208
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1209
A final point worth mentioning is the orientation of the equation we just
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1210
proved: the more complex notion (\texttt{itrev}) is on the left-hand
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1211
side, the simpler \texttt{rev} on the right-hand side. This constitutes
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1212
another, albeit weak heuristic that is not restricted to induction:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1213
\begin{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1214
  {\em 5. The right-hand side of an equation should (in some sense) be
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1215
    simpler than the left-hand side.}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1216
\end{quote}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1217
The heuristic is tricky to apply because it is not obvious that
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1218
\texttt{rev xs \at\ ys} is simpler than \texttt{itrev xs ys}. But see what
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1219
happens if you try to prove the symmetric equation!
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1220
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1221
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1222
\section{Case study: compiling expressions}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1223
\label{sec:ExprCompiler}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1224
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1225
The task is to develop a compiler from a generic type of expressions (built
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1226
up from variables, constants and binary operations) to a stack machine.  This
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1227
generic type of expressions is a generalization of the boolean expressions in
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1228
\S\ref{sec:boolex}.  This time we do not commit ourselves to a particular
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1229
type of variables or values but make them type parameters.  Neither is there
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1230
a fixed set of binary operations: instead the expression contains the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1231
appropriate function itself.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1232
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1233
\input{CodeGen/expr}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1234
The three constructors represent constants, variables and the combination of
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1235
two subexpressions with a binary operation.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1236
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1237
The value of an expression w.r.t.\ an environment that maps variables to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1238
values is easily defined:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1239
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1240
\input{CodeGen/value}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1241
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1242
The stack machine has three instructions: load a constant value onto the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1243
stack, load the contents of a certain address onto the stack, and apply a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1244
binary operation to the two topmost elements of the stack, replacing them by
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1245
the result. As for \texttt{expr}, addresses and values are type parameters:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1246
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1247
\input{CodeGen/instr}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1248
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1249
The execution of the stack machine is modelled by a function \texttt{exec}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1250
that takes a store (modelled as a function from addresses to values, just
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1251
like the environment for evaluating expressions), a stack (modelled as a
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1252
list) of values and a list of instructions and returns the stack at the end
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1253
of the execution --- the store remains unchanged:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1254
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1255
\input{CodeGen/exec}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1256
Recall that \texttt{hd} and \texttt{tl}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1257
return the first element and the remainder of a list.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1258
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1259
Because all functions are total, \texttt{hd} is defined even for the empty
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1260
list, although we do not know what the result is. Thus our model of the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1261
machine always terminates properly, although the above definition does not
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1262
tell us much about the result in situations where \texttt{Apply} was executed
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1263
with fewer than two elements on the stack.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1264
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1265
The compiler is a function from expressions to a list of instructions. Its
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1266
definition is pretty much obvious:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1267
\begin{ttbox}\makeatother
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1268
\input{CodeGen/comp}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1269
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1270
Now we have to prove the correctness of the compiler, i.e.\ that the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1271
execution of a compiled expression results in the value of the expression:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1272
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1273
exec s [] (comp e) = [value s e]
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1274
\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1275
This is generalized to
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1276
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1277
\input{CodeGen/goal2.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1278
and proved by induction on \texttt{e} followed by simplification, once we
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1279
have the following lemma about executing the concatenation of two instruction
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1280
sequences:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1281
\begin{ttbox}\makeatother
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1282
\input{CodeGen/goal1.ML}\end{ttbox}
5375
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1283
This requires induction on \texttt{xs} and ordinary simplification for the
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1284
base cases. In the induction step, simplification leaves us with a formula
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1285
that contains two \texttt{case}-expressions over instructions. Thus we add
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1286
automatic case splitting as well, which finishes the proof:
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1287
\begin{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1288
\input{CodeGen/simpsplit.ML}\end{ttbox}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1289
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1290
We could now go back and prove \texttt{exec s [] (comp e) = [value s e]}
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1291
merely by simplification with the generalized version we just proved.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1292
However, this is unnecessary because the generalized version fully subsumes
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1293
its instance.
1463e182c533 The HOL tutorial.
nipkow
parents:
diff changeset
  1294
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1295
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1296
\section{Advanced datatypes}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1297
\index{*datatype|(}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1298
\index{*primrec|(}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1299
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1300
This section presents advanced forms of \texttt{datatype}s and (in the near
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1301
future!) records.
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1302
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1303
\subsection{Mutual recursion}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1304
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1305
Sometimes it is necessary to define two datatypes that depend on each
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1306
other. This is called \textbf{mutual recursion}. As an example consider a
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1307
language of arithmetic and boolean expressions where
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1308
\begin{itemize}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1309
\item arithmetic expressions contain boolean expressions because there are
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1310
  conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1311
  and
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1312
\item boolean expressions contain arithmetic expressions because of
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1313
  comparisons like ``$m<n$''.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1314
\end{itemize}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1315
In Isabelle this becomes
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1316
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1317
\input{Datatype/abdata}\end{ttbox}\indexbold{*and}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1318
Type \texttt{aexp} is similar to \texttt{expr} in \S\ref{sec:ExprCompiler},
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1319
except that we have fixed the values to be of type \texttt{nat} and that we
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1320
have fixed the two binary operations \texttt{Sum} and \texttt{Diff}. Boolean
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1321
expressions can be arithmetic comparisons, conjunctions and negations.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1322
The semantics is fixed via two evaluation functions
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1323
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1324
\input{Datatype/abconstseval}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1325
that take an environment (a mapping from variables \texttt{'a} to values
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1326
\texttt{nat}) and an expression and return its arithmetic/boolean
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1327
value. Since the datatypes are mutually recursive, so are functions that
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1328
operate on them. Hence they need to be defined in a single \texttt{primrec}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1329
section:
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1330
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1331
\input{Datatype/abevala}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1332
\input{Datatype/abevalb}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1333
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1334
%In general, given $n$ mutually recursive datatypes, whenever you define a
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1335
%\texttt{primrec} function on one of them, Isabelle expects you to define $n$
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1336
%(possibly mutually recursive) functions simultaneously.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1337
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1338
In the same fashion we also define two functions that perform substitution:
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1339
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1340
\input{Datatype/abconstssubst}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1341
The first argument is a function mapping variables to expressions, the
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1342
substitution. It is applied to all variables in the second argument. As a
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1343
result, the type of variables in the expression may change from \texttt{'a}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1344
to \texttt{'b}. Note that there are only arithmetic and no boolean variables.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1345
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1346
\input{Datatype/absubsta}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1347
\input{Datatype/absubstb}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1348
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1349
Now we can prove a fundamental theorem about the interaction between
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1350
evaluation and substitution: applying a substitution $s$ to an expression $a$
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1351
and evaluating the result in an environment $env$ yields the same result as
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1352
evaluation $a$ in the environment that maps every variable $x$ to the value
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1353
of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1354
boolean expressions (by induction), you find that you always need the other
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1355
theorem in the induction step. Therefore you need to state and prove both
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1356
theorems simultaneously:
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1357
\begin{quote}\small
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1358
\verbatiminput{Datatype/abgoalind.ML}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1359
\end{quote}\indexbold{*mutual_induct_tac}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1360
The resulting 8 goals (one for each constructor) are proved in one fell swoop
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1361
\texttt{by Auto_tac;}.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1362
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1363
In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1364
Isabelle expects an inductive proof to start with a goal of the form
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1365
\[ P@1(x@1)\ \texttt{\&}\ \dots\ \texttt{\&}\ P@n(x@n) \]
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1366
where each variable $x@i$ is of type $\tau@i$. Induction is started by
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1367
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1368
by(mutual_induct_tac ["\(x@1\)",\(\dots\),"\(x@n\)"] \(k\));
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1369
\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1370
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1371
\begin{exercise}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1372
  Define a function \texttt{norma} of type \texttt{'a aexp => 'a aexp} that
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1373
  replaces \texttt{IF}s with complex boolean conditions by nested
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1374
  \texttt{IF}s where each condition is a \texttt{Less} --- \texttt{And} and
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1375
  \texttt{Neg} should be eliminated completely. Prove that \texttt{norma}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1376
  preserves the value of an expression and that the result of \texttt{norma}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1377
  is really normal, i.e.\ no more \texttt{And}s and \texttt{Neg}s occur in
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1378
  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1379
\end{exercise}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1380
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1381
\subsection{Nested recursion}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1382
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1383
So far, all datatypes had the property that on the right-hand side of their
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1384
definition they occurred only at the top-level, i.e.\ directly below a
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1385
constructor. This is not the case any longer for the following model of terms
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1386
where function symbols can be applied to a list of arguments:
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1387
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1388
\input{Datatype/tdata}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1389
Parameter \texttt{'a} is the type of variables and \texttt{'b} the type of
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1390
function symbols.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1391
A mathematical term like $f(x,g(y))$ becomes \texttt{App f [Var x, App g
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1392
  [Var y]]}, where \texttt{f}, \texttt{g}, \texttt{x}, \texttt{y} are
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1393
suitable values, e.g.\ numbers or strings.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1394
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1395
What complicates the definition of \texttt{term} is the nested occurrence of
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1396
\texttt{term} inside \texttt{list} on the right-hand side. In principle,
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1397
nested recursion can be eliminated in favour of mutual recursion by unfolding
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1398
the offending datatypes, here \texttt{list}. The result for \texttt{term}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1399
would be something like
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1400
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1401
\input{Datatype/tunfoldeddata}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1402
Although we do not recommend this unfolding to the user, this is how Isabelle
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1403
deals with nested recursion internally. Strictly speaking, this information
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1404
is irrelevant at the user level (and might change in the future), but it
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1405
motivates why \texttt{primrec} and induction work for nested types the way
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1406
they do. We now return to the initial definition of \texttt{term} using
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1407
nested recursion.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1408
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1409
Let us define a substitution function on terms. Because terms involve term
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1410
lists, we need to define two substitution functions simultaneously:
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1411
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1412
\input{Datatype/tconstssubst}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1413
\input{Datatype/tsubst}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1414
\input{Datatype/tsubsts}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1415
Similarly, when proving a statement about terms inductively, we need
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1416
to prove a related statement about term lists simultaneously. For example,
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1417
the fact that the identity substitution does not change a term needs to be
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1418
strengthened and proved as follows:
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1419
\begin{quote}\small
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1420
\verbatiminput{Datatype/tidproof.ML}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1421
\end{quote}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1422
Note that \texttt{Var} is the identity substitution because by definition it
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1423
leaves variables unchanged: \texttt{subst Var (Var $x$) = Var $x$}. Note also
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1424
that the type annotations are necessary because otherwise there is nothing in
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1425
the goal to enforce that both halves of the goal talk about the same type
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1426
parameters \texttt{('a,'b)}. As a result, induction would fail
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1427
because the two halves of the goal would be unrelated.
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1428
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1429
\begin{exercise}
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1430
The fact that substitution distributes over composition can be expressed
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1431
roughly as follows:
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1432
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1433
subst (f o g) t = subst f (subst g t)
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1434
\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1435
Correct this statement (you will find that it does not type-check),
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1436
strengthen it and prove it. (Note: \texttt{o} is function composition; its
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1437
definition is found in the theorem \texttt{o_def}).
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1438
\end{exercise}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1439
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1440
If you feel that the \texttt{App}-equation in the definition of substitution
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1441
is overly complicated, you are right: the simpler
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1442
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1443
\input{Datatype/appmap}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1444
would have done the job. Unfortunately, Isabelle insists on the more verbose
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1445
equation given above. Nevertheless, we can easily {\em prove} that the
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1446
\texttt{map}-equation holds: simply by induction on \texttt{ts} followed by
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1447
\texttt{Auto_tac}.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1448
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1449
%FIXME: forward pointer to section where better induction principles are
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1450
%derived?
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1451
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1452
\begin{exercise}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1453
  Define a function \texttt{rev_term} of type \texttt{term -> term} that
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1454
  recursively reverses the order of arguments of all function symbols in a
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1455
  term. Prove that \texttt{rev_term(rev_term t) = t}.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1456
\end{exercise}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1457
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1458
Of course, you may also combine mutual and nested recursion as in the
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1459
following example
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1460
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1461
\input{Datatype/mutnested}\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1462
taken from an operational semantics of applied lambda terms. Note that double
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1463
quotes are required around the type involving \texttt{*}, as explained on
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1464
page~\pageref{startype}.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1465
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1466
\subsection{The limits of nested recursion}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1467
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1468
How far can we push nested recursion? By the unfolding argument above, we can
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1469
reduce nested to mutual recursion provided the nested recursion only involves
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1470
previously defined datatypes. Isabelle is a bit more generous and also permits
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1471
products as in the \texttt{data} example above.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1472
However, functions are most emphatically not allowed:
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1473
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1474
datatype t = C (t => bool)
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1475
\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1476
is a real can of worms: in HOL it must be ruled out because it requires a
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1477
type \texttt{t} such that \texttt{t} and its power set \texttt{t => bool}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1478
have the same cardinality---an impossibility.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1479
In theory, we could allow limited forms of recursion involving function
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1480
spaces. For example
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1481
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1482
datatype t = C (nat => t) | D
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1483
\end{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1484
is unproblematic. However, Isabelle does not support recursion involving
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1485
\texttt{=>} at all at the moment.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1486
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1487
For a theoretical analysis of what kinds of datatypes are feasible in HOL
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1488
see, for example,~\cite{Gunter-HOL92}. There are alternatives to pure HOL:
6606
nipkow
parents: 6577
diff changeset
  1489
LCF~\cite{paulson87} is a logic where types like
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1490
\begin{ttbox}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1491
datatype t = C (t -> t)
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1492
\end{ttbox}
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
  1493
do indeed make sense (note the intentionally different arrow \texttt{->}!).
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1494
There is even a version of LCF on top of HOL, called
6606
nipkow
parents: 6577
diff changeset
  1495
HOLCF~\cite{MuellerNvOS99}.
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1496
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1497
\index{*primrec|)}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1498
\index{*datatype|)}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1499
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1500
\subsection{Case study: Tries}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1501
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1502
Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1503
indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1504
trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1505
``cat''.  When searching a string in a trie, the letters of the string are
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1506
examined sequentially. Each letter determines which subtrie to search next.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1507
In this case study we model tries as a datatype, define a lookup and an
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1508
update function, and prove that they behave as expected.
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1509
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1510
\begin{figure}[htbp]
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1511
\begin{center}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1512
\unitlength1mm
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1513
\begin{picture}(60,30)
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1514
\put( 5, 0){\makebox(0,0)[b]{l}}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1515
\put(25, 0){\makebox(0,0)[b]{e}}
9712294e60b9 *** empty log message ***
nipkow
parents: 5375
diff changeset
  1516
\put(35, 0){\makebox(0,0)[b]{n}}