doc-src/TutorialI/basics.tex
author nipkow
Wed Apr 19 11:54:39 2000 +0200 (2000-04-19)
changeset 8743 3253c6046d57
child 8771 026f37a86ea7
permissions -rw-r--r--
I wonder if that's all?
nipkow@8743
     1
\chapter{Basic Concepts}
nipkow@8743
     2
nipkow@8743
     3
\section{Introduction}
nipkow@8743
     4
nipkow@8743
     5
This is a tutorial on how to use Isabelle/HOL as a specification and
nipkow@8743
     6
verification system. Isabelle is a generic system for implementing logical
nipkow@8743
     7
formalisms, and Isabelle/HOL is the specialization of Isabelle for
nipkow@8743
     8
HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
nipkow@8743
     9
following the equation
nipkow@8743
    10
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
nipkow@8743
    11
We assume that the reader is familiar with the basic concepts of both fields.
nipkow@8743
    12
For excellent introductions to functional programming consult the textbooks
nipkow@8743
    13
by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although
nipkow@8743
    14
this tutorial initially concentrates on functional programming, do not be
nipkow@8743
    15
misled: HOL can express most mathematical concepts, and functional
nipkow@8743
    16
programming is just one particularly simple and ubiquitous instance.
nipkow@8743
    17
nipkow@8743
    18
This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
nipkow@8743
    19
which is an extension of Isabelle~\cite{paulson-isa-book} with structured
nipkow@8743
    20
proofs.\footnote{Thus the full name of the system should be
nipkow@8743
    21
  Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
nipkow@8743
    22
difference to classical Isabelle (which is the basis of another version of
nipkow@8743
    23
this tutorial) is the replacement of the ML level by a dedicated language for
nipkow@8743
    24
definitions and proofs.
nipkow@8743
    25
nipkow@8743
    26
A tutorial is by definition incomplete.  Currently the tutorial only
nipkow@8743
    27
introduces the rudiments of Isar's proof language. To fully exploit the power
nipkow@8743
    28
of Isar you need to consult the Isabelle/Isar Reference
nipkow@8743
    29
Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
nipkow@8743
    30
directly (for example for writing your own proof procedures) see the Isabelle
nipkow@8743
    31
Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
nipkow@8743
    32
Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
nipkow@8743
    33
index.
nipkow@8743
    34
nipkow@8743
    35
\section{Theories}
nipkow@8743
    36
\label{sec:Basic:Theories}
nipkow@8743
    37
nipkow@8743
    38
Working with Isabelle means creating theories. Roughly speaking, a
nipkow@8743
    39
\bfindex{theory} is a named collection of types, functions, and theorems,
nipkow@8743
    40
much like a module in a programming language or a specification in a
nipkow@8743
    41
specification language. In fact, theories in HOL can be either. The general
nipkow@8743
    42
format of a theory \texttt{T} is
nipkow@8743
    43
\begin{ttbox}
nipkow@8743
    44
theory T = B\(@1\) + \(\cdots\) + B\(@n\):
nipkow@8743
    45
\(\textit{declarations, definitions, and proofs}\)
nipkow@8743
    46
end
nipkow@8743
    47
\end{ttbox}
nipkow@8743
    48
where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
nipkow@8743
    49
theories that \texttt{T} is based on and \texttt{\textit{declarations,
nipkow@8743
    50
    definitions, and proofs}} represents the newly introduced concepts
nipkow@8743
    51
(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the
nipkow@8743
    52
direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
nipkow@8743
    53
Everything defined in the parent theories (and their parents \dots) is
nipkow@8743
    54
automatically visible. To avoid name clashes, identifiers can be
nipkow@8743
    55
\textbf{qualified} by theory names as in \texttt{T.f} and
nipkow@8743
    56
\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
nipkow@8743
    57
reside in a \indexbold{theory file} named \texttt{T.thy}.
nipkow@8743
    58
nipkow@8743
    59
This tutorial is concerned with introducing you to the different linguistic
nipkow@8743
    60
constructs that can fill \textit{\texttt{declarations, definitions, and
nipkow@8743
    61
    proofs}} in the above theory template.  A complete grammar of the basic
nipkow@8743
    62
constructs is found in the Isabelle/Isar Reference Manual.
nipkow@8743
    63
nipkow@8743
    64
HOL's theory library is available online at
nipkow@8743
    65
\begin{center}\small
nipkow@8743
    66
    \url{http://isabelle.in.tum.de/library/}
nipkow@8743
    67
\end{center}
nipkow@8743
    68
and is recommended browsing.
nipkow@8743
    69
\begin{warn}
nipkow@8743
    70
  HOL contains a theory \ttindexbold{Main}, the union of all the basic
nipkow@8743
    71
  predefined theories like arithmetic, lists, sets, etc.\ (see the online
nipkow@8743
    72
  library).  Unless you know what you are doing, always include \texttt{Main}
nipkow@8743
    73
  as a direct or indirect parent theory of all your theories.
nipkow@8743
    74
\end{warn}
nipkow@8743
    75
nipkow@8743
    76
nipkow@8743
    77
\section{Interaction and interfaces}
nipkow@8743
    78
nipkow@8743
    79
Interaction with Isabelle can either occur at the shell level or through more
nipkow@8743
    80
advanced interfaces. To keep the tutorial independent of the interface we
nipkow@8743
    81
have phrased the description of the intraction in a neutral language. For
nipkow@8743
    82
example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the
nipkow@8743
    83
shell level, which is explained the first time the phrase is used. Other
nipkow@8743
    84
interfaces perform the same act by cursor movements and/or mouse clicks.
nipkow@8743
    85
Although shell-based interaction is quite feasible for the kind of proof
nipkow@8743
    86
scripts currently presented in this tutorial, the recommended interface for
nipkow@8743
    87
Isabelle/Isar is the Emacs-based \bfindex{Proof
nipkow@8743
    88
  General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
nipkow@8743
    89
nipkow@8743
    90
To improve readability some of the interfaces (including the shell level)
nipkow@8743
    91
offer special fonts with mathematical symbols. Therefore the usual
nipkow@8743
    92
mathematical symbols are used throughout the tutorial. Their
nipkow@8743
    93
ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.
nipkow@8743
    94
nipkow@8743
    95
Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
nipkow@8743
    96
for example Proof General, require each command to be terminated by a
nipkow@8743
    97
semicolon, whereas others, for example the shell level, do not. But even at
nipkow@8743
    98
the shell level it is advisable to use semicolons to enforce that a command
nipkow@8743
    99
is executed immediately; otherwise Isabelle may wait for the next keyword
nipkow@8743
   100
before it knows that the command is complete. Note that for readibility
nipkow@8743
   101
reasons we often drop the final semicolon in the text.
nipkow@8743
   102
nipkow@8743
   103
nipkow@8743
   104
\section{Types, terms and formulae}
nipkow@8743
   105
\label{sec:TypesTermsForms}
nipkow@8743
   106
\indexbold{type}
nipkow@8743
   107
nipkow@8743
   108
Embedded in the declarations of a theory are the types, terms and formulae of
nipkow@8743
   109
HOL. HOL is a typed logic whose type system resembles that of functional
nipkow@8743
   110
programming languages like ML or Haskell. Thus there are
nipkow@8743
   111
\begin{description}
nipkow@8743
   112
\item[base types,] in particular \ttindex{bool}, the type of truth values,
nipkow@8743
   113
and \ttindex{nat}, the type of natural numbers.
nipkow@8743
   114
\item[type constructors,] in particular \texttt{list}, the type of
nipkow@8743
   115
lists, and \texttt{set}, the type of sets. Type constructors are written
nipkow@8743
   116
postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
nipkow@8743
   117
natural numbers. Parentheses around single arguments can be dropped (as in
nipkow@8743
   118
\texttt{nat list}), multiple arguments are separated by commas (as in
nipkow@8743
   119
\texttt{(bool,nat)foo}).
nipkow@8743
   120
\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
nipkow@8743
   121
  In HOL \isasymFun\ represents {\em total} functions only. As is customary,
nipkow@8743
   122
  \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
nipkow@8743
   123
  \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
nipkow@8743
   124
  supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
nipkow@8743
   125
  which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
nipkow@8743
   126
    \isasymFun~$\tau$}.
nipkow@8743
   127
\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
nipkow@8743
   128
ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the
nipkow@8743
   129
type of the identity function.
nipkow@8743
   130
\end{description}
nipkow@8743
   131
\begin{warn}
nipkow@8743
   132
  Types are extremely important because they prevent us from writing
nipkow@8743
   133
  nonsense.  Isabelle insists that all terms and formulae must be well-typed
nipkow@8743
   134
  and will print an error message if a type mismatch is encountered. To
nipkow@8743
   135
  reduce the amount of explicit type information that needs to be provided by
nipkow@8743
   136
  the user, Isabelle infers the type of all variables automatically (this is
nipkow@8743
   137
  called \bfindex{type inference}) and keeps quiet about it. Occasionally
nipkow@8743
   138
  this may lead to misunderstandings between you and the system. If anything
nipkow@8743
   139
  strange happens, we recommend to set the \rmindex{flag}
nipkow@8743
   140
  \ttindexbold{show_types} that tells Isabelle to display type information
nipkow@8743
   141
  that is usually suppressed: simply type
nipkow@8743
   142
\begin{ttbox}
nipkow@8743
   143
ML "set show_types"
nipkow@8743
   144
\end{ttbox}
nipkow@8743
   145
nipkow@8743
   146
\noindent
nipkow@8743
   147
This can be reversed by \texttt{ML "reset show_types"}. Various other flags
nipkow@8743
   148
can be set and reset in the same manner.\bfindex{flag!(re)setting}
nipkow@8743
   149
\end{warn}
nipkow@8743
   150
nipkow@8743
   151
nipkow@8743
   152
\textbf{Terms}\indexbold{term} are formed as in functional programming by
nipkow@8743
   153
applying functions to arguments. If \texttt{f} is a function of type
nipkow@8743
   154
\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type
nipkow@8743
   155
$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports
nipkow@8743
   156
infix functions like \texttt{+} and some basic constructs from functional
nipkow@8743
   157
programming:
nipkow@8743
   158
\begin{description}
nipkow@8743
   159
\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
nipkow@8743
   160
means what you think it means and requires that
nipkow@8743
   161
$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
nipkow@8743
   162
\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
nipkow@8743
   163
is equivalent to $u$ where all occurrences of $x$ have been replaced by
nipkow@8743
   164
$t$. For example,
nipkow@8743
   165
\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
nipkow@8743
   166
by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
nipkow@8743
   167
\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
nipkow@8743
   168
\indexbold{*case}
nipkow@8743
   169
evaluates to $e@i$ if $e$ is of the form
nipkow@8743
   170
$c@i$. See~\S\ref{sec:case-expressions} for details.
nipkow@8743
   171
\end{description}
nipkow@8743
   172
nipkow@8743
   173
Terms may also contain
nipkow@8743
   174
\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
nipkow@8743
   175
\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument
nipkow@8743
   176
\texttt{x} and returns \texttt{x+1}. Instead of
nipkow@8743
   177
\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write
nipkow@8743
   178
\texttt{\isasymlambda{}x~y~z.}~$t$.
nipkow@8743
   179
nipkow@8743
   180
\textbf{Formulae}\indexbold{formula}
nipkow@8743
   181
are terms of type \texttt{bool}. There are the basic
nipkow@8743
   182
constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
nipkow@8743
   183
connectives (in decreasing order of priority):
nipkow@8743
   184
\indexboldpos{\isasymnot}{$HOL0not},
nipkow@8743
   185
\indexboldpos{\isasymand}{$HOL0and},
nipkow@8743
   186
\indexboldpos{\isasymor}{$HOL0or}, and
nipkow@8743
   187
\indexboldpos{\isasymimp}{$HOL0imp},
nipkow@8743
   188
all of which (except the unary \isasymnot) associate to the right. In
nipkow@8743
   189
particular \texttt{A \isasymimp~B \isasymimp~C} means
nipkow@8743
   190
\texttt{A \isasymimp~(B \isasymimp~C)} and is thus
nipkow@8743
   191
logically equivalent with \texttt{A \isasymand~B \isasymimp~C}
nipkow@8743
   192
(which is \texttt{(A \isasymand~B) \isasymimp~C}).
nipkow@8743
   193
nipkow@8743
   194
Equality is available in the form of the infix function
nipkow@8743
   195
\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a
nipkow@8743
   196
  \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$
nipkow@8743
   197
and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
nipkow@8743
   198
\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula
nipkow@8743
   199
$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for
nipkow@8743
   200
\texttt{\isasymnot($t@1$ = $t@2$)}.
nipkow@8743
   201
nipkow@8743
   202
The syntax for quantifiers is
nipkow@8743
   203
\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and
nipkow@8743
   204
\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}.  There is
nipkow@8743
   205
even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which
nipkow@8743
   206
means that there exists exactly one \texttt{x} that satisfies $P$.
nipkow@8743
   207
Nested quantifications can be abbreviated:
nipkow@8743
   208
\texttt{\isasymforall{}x~y~z.}~$P$ means
nipkow@8743
   209
\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.
nipkow@8743
   210
nipkow@8743
   211
Despite type inference, it is sometimes necessary to attach explicit
nipkow@8743
   212
\bfindex{type constraints} to a term.  The syntax is \texttt{$t$::$\tau$} as
nipkow@8743
   213
in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly
nipkow@8743
   214
and should therefore be enclosed in parentheses: \texttt{x < y::nat} is
nipkow@8743
   215
ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason
nipkow@8743
   216
for type constraints are overloaded functions like \texttt{+}, \texttt{*} and
nipkow@8743
   217
\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
nipkow@8743
   218
overloading.)
nipkow@8743
   219
nipkow@8743
   220
\begin{warn}
nipkow@8743
   221
In general, HOL's concrete syntax tries to follow the conventions of
nipkow@8743
   222
functional programming and mathematics. Below we list the main rules that you
nipkow@8743
   223
should be familiar with to avoid certain syntactic traps. A particular
nipkow@8743
   224
problem for novices can be the priority of operators. If you are unsure, use
nipkow@8743
   225
more rather than fewer parentheses. In those cases where Isabelle echoes your
nipkow@8743
   226
input, you can see which parentheses are dropped---they were superfluous. If
nipkow@8743
   227
you are unsure how to interpret Isabelle's output because you don't know
nipkow@8743
   228
where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}
nipkow@8743
   229
\ttindexbold{show_brackets}:
nipkow@8743
   230
\begin{ttbox}
nipkow@8743
   231
ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
nipkow@8743
   232
\end{ttbox}
nipkow@8743
   233
\end{warn}
nipkow@8743
   234
nipkow@8743
   235
\begin{itemize}
nipkow@8743
   236
\item
nipkow@8743
   237
Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
nipkow@8743
   238
\item
nipkow@8743
   239
Isabelle allows infix functions like \texttt{+}. The prefix form of function
nipkow@8743
   240
application binds more strongly than anything else and hence \texttt{f~x + y}
nipkow@8743
   241
means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
nipkow@8743
   242
\item Remember that in HOL if-and-only-if is expressed using equality.  But
nipkow@8743
   243
  equality has a high priority, as befitting a relation, while if-and-only-if
nipkow@8743
   244
  typically has the lowest priority.  Thus, \texttt{\isasymnot~\isasymnot~P =
nipkow@8743
   245
    P} means \texttt{\isasymnot\isasymnot(P = P)} and not
nipkow@8743
   246
  \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean
nipkow@8743
   247
  logical equivalence, enclose both operands in parentheses, as in \texttt{(A
nipkow@8743
   248
    \isasymand~B) = (B \isasymand~A)}.
nipkow@8743
   249
\item
nipkow@8743
   250
Constructs with an opening but without a closing delimiter bind very weakly
nipkow@8743
   251
and should therefore be enclosed in parentheses if they appear in subterms, as
nipkow@8743
   252
in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},
nipkow@8743
   253
\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.
nipkow@8743
   254
\item
nipkow@8743
   255
Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}
nipkow@8743
   256
because \texttt{x.x} is always read as a single qualified identifier that
nipkow@8743
   257
refers to an item \texttt{x} in theory \texttt{x}. Write
nipkow@8743
   258
\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.
nipkow@8743
   259
\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.
nipkow@8743
   260
\end{itemize}
nipkow@8743
   261
nipkow@8743
   262
Remember that ASCII-equivalents of all mathematical symbols are
nipkow@8743
   263
given in figure~\ref{fig:ascii} in the appendix.
nipkow@8743
   264
nipkow@8743
   265
\section{Variables}
nipkow@8743
   266
\label{sec:variables}
nipkow@8743
   267
\indexbold{variable}
nipkow@8743
   268
nipkow@8743
   269
Isabelle distinguishes free and bound variables just as is customary. Bound
nipkow@8743
   270
variables are automatically renamed to avoid clashes with free variables. In
nipkow@8743
   271
addition, Isabelle has a third kind of variable, called a \bfindex{schematic
nipkow@8743
   272
  variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
nipkow@8743
   273
with a \texttt{?}.  Logically, an unknown is a free variable. But it may be
nipkow@8743
   274
instantiated by another term during the proof process. For example, the
nipkow@8743
   275
mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},
nipkow@8743
   276
which means that Isabelle can instantiate it arbitrarily. This is in contrast
nipkow@8743
   277
to ordinary variables, which remain fixed. The programming language Prolog
nipkow@8743
   278
calls unknowns {\em logical\/} variables.
nipkow@8743
   279
nipkow@8743
   280
Most of the time you can and should ignore unknowns and work with ordinary
nipkow@8743
   281
variables. Just don't be surprised that after you have finished the proof of
nipkow@8743
   282
a theorem, Isabelle will turn your free variables into unknowns: it merely
nipkow@8743
   283
indicates that Isabelle will automatically instantiate those unknowns
nipkow@8743
   284
suitably when the theorem is used in some other proof.
nipkow@8743
   285
\begin{warn}
nipkow@8743
   286
  If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential
nipkow@8743
   287
  quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is
nipkow@8743
   288
  interpreted as a schematic variable.
nipkow@8743
   289
\end{warn}
nipkow@8743
   290
nipkow@8743
   291
\section{Getting started}
nipkow@8743
   292
nipkow@8743
   293
Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
nipkow@8743
   294
  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
nipkow@8743
   295
  starts the default logic, which usually is already \texttt{HOL}.  This is
nipkow@8743
   296
  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
nipkow@8743
   297
    System Manual} for more details.} This presents you with Isabelle's most
nipkow@8743
   298
basic ASCII interface.  In addition you need to open an editor window to
nipkow@8743
   299
create theory files.  While you are developing a theory, we recommend to
nipkow@8743
   300
type each command into the file first and then enter it into Isabelle by
nipkow@8743
   301
copy-and-paste, thus ensuring that you have a complete record of your theory.
nipkow@8743
   302
As mentioned earlier, Proof General offers a much superior interface.