doc-src/TutorialI/basics.tex
 author nipkow Wed, 19 Apr 2000 11:54:39 +0200 changeset 8743 3253c6046d57 child 8771 026f37a86ea7 permissions -rw-r--r--
I wonder if that's all?

\chapter{Basic Concepts}

\section{Introduction}

This is a tutorial on how to use Isabelle/HOL as a specification and
verification system. Isabelle is a generic system for implementing logical
formalisms, and Isabelle/HOL is the specialization of Isabelle for
HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
following the equation
$\mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}.$
We assume that the reader is familiar with the basic concepts of both fields.
For excellent introductions to functional programming consult the textbooks
by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although
this tutorial initially concentrates on functional programming, do not be
misled: HOL can express most mathematical concepts, and functional
programming is just one particularly simple and ubiquitous instance.

This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
which is an extension of Isabelle~\cite{paulson-isa-book} with structured
proofs.\footnote{Thus the full name of the system should be
Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
difference to classical Isabelle (which is the basis of another version of
this tutorial) is the replacement of the ML level by a dedicated language for
definitions and proofs.

A tutorial is by definition incomplete.  Currently the tutorial only
introduces the rudiments of Isar's proof language. To fully exploit the power
of Isar you need to consult the Isabelle/Isar Reference
Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
directly (for example for writing your own proof procedures) see the Isabelle
Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
index.

\section{Theories}
\label{sec:Basic:Theories}

Working with Isabelle means creating theories. Roughly speaking, a
\bfindex{theory} is a named collection of types, functions, and theorems,
much like a module in a programming language or a specification in a
specification language. In fact, theories in HOL can be either. The general
format of a theory \texttt{T} is
\begin{ttbox}
theory T = B$$@1$$ + $$\cdots$$ + B$$@n$$:
$$\textit{declarations, definitions, and proofs}$$
end
\end{ttbox}
where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
theories that \texttt{T} is based on and \texttt{\textit{declarations,
definitions, and proofs}} represents the newly introduced concepts
(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the
direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
Everything defined in the parent theories (and their parents \dots) is
automatically visible. To avoid name clashes, identifiers can be
\textbf{qualified} by theory names as in \texttt{T.f} and
\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
reside in a \indexbold{theory file} named \texttt{T.thy}.

This tutorial is concerned with introducing you to the different linguistic
constructs that can fill \textit{\texttt{declarations, definitions, and
proofs}} in the above theory template.  A complete grammar of the basic
constructs is found in the Isabelle/Isar Reference Manual.

HOL's theory library is available online at
\begin{center}\small
\url{http://isabelle.in.tum.de/library/}
\end{center}
and is recommended browsing.
\begin{warn}
HOL contains a theory \ttindexbold{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.\ (see the online
library).  Unless you know what you are doing, always include \texttt{Main}
as a direct or indirect parent theory of all your theories.
\end{warn}

\section{Interaction and interfaces}

Interaction with Isabelle can either occur at the shell level or through more
advanced interfaces. To keep the tutorial independent of the interface we
have phrased the description of the intraction in a neutral language. For
example, the phrase to cancel a proof'' means to type \texttt{oops} at the
shell level, which is explained the first time the phrase is used. Other
interfaces perform the same act by cursor movements and/or mouse clicks.
Although shell-based interaction is quite feasible for the kind of proof
scripts currently presented in this tutorial, the recommended interface for
Isabelle/Isar is the Emacs-based \bfindex{Proof
General}~\cite{Aspinall:TACAS:2000,proofgeneral}.

To improve readability some of the interfaces (including the shell level)
offer special fonts with mathematical symbols. Therefore the usual
mathematical symbols are used throughout the tutorial. Their
ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.

Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces, for example Proof General, require each command to be terminated by a semicolon, whereas others, for example the shell level, do not. But even at the shell level it is advisable to use semicolons to enforce that a command is executed immediately; otherwise Isabelle may wait for the next keyword before it knows that the command is complete. Note that for readibility reasons we often drop the final semicolon in the text. \section{Types, terms and formulae} \label{sec:TypesTermsForms} \indexbold{type} Embedded in the declarations of a theory are the types, terms and formulae of HOL. HOL is a typed logic whose type system resembles that of functional programming languages like ML or Haskell. Thus there are \begin{description} \item[base types,] in particular \ttindex{bool}, the type of truth values, and \ttindex{nat}, the type of natural numbers. \item[type constructors,] in particular \texttt{list}, the type of lists, and \texttt{set}, the type of sets. Type constructors are written postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are natural numbers. Parentheses around single arguments can be dropped (as in \texttt{nat list}), multiple arguments are separated by commas (as in \texttt{(bool,nat)foo}). \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
In HOL \isasymFun\ represents {\em total} functions only. As is customary,
\texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
\texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
\isasymFun~$\tau$}.
\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the
type of the identity function.
\end{description}
\begin{warn}
Types are extremely important because they prevent us from writing
nonsense.  Isabelle insists that all terms and formulae must be well-typed
and will print an error message if a type mismatch is encountered. To
reduce the amount of explicit type information that needs to be provided by
the user, Isabelle infers the type of all variables automatically (this is
called \bfindex{type inference}) and keeps quiet about it. Occasionally
this may lead to misunderstandings between you and the system. If anything
strange happens, we recommend to set the \rmindex{flag}
\ttindexbold{show_types} that tells Isabelle to display type information
that is usually suppressed: simply type
\begin{ttbox}
ML "set show_types"
\end{ttbox}

\noindent
This can be reversed by \texttt{ML "reset show_types"}. Various other flags
can be set and reset in the same manner.\bfindex{flag!(re)setting}
\end{warn}

\textbf{Terms}\indexbold{term} are formed as in functional programming by
applying functions to arguments. If \texttt{f} is a function of type
\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type
$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports
infix functions like \texttt{+} and some basic constructs from functional
programming:
\begin{description}
\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
means what you think it means and requires that
$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
is equivalent to $u$ where all occurrences of $x$ have been replaced by
$t$. For example,
\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
\indexbold{*case}
evaluates to $e@i$ if $e$ is of the form
$c@i$. See~\S\ref{sec:case-expressions} for details.
\end{description}

Terms may also contain
\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example, \texttt{\isasymlambda{}x.~x+1} is the function that takes an argument \texttt{x} and returns \texttt{x+1}. Instead of \texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$we can write \texttt{\isasymlambda{}x~y~z.}~$t$. \textbf{Formulae}\indexbold{formula} are terms of type \texttt{bool}. There are the basic constants \ttindexbold{True} and \ttindexbold{False} and the usual logical connectives (in decreasing order of priority): \indexboldpos{\isasymnot}{$HOL0not},
\indexboldpos{\isasymand}{$HOL0and}, \indexboldpos{\isasymor}{$HOL0or}, and
\indexboldpos{\isasymimp}{$HOL0imp}, all of which (except the unary \isasymnot) associate to the right. In particular \texttt{A \isasymimp~B \isasymimp~C} means \texttt{A \isasymimp~(B \isasymimp~C)} and is thus logically equivalent with \texttt{A \isasymand~B \isasymimp~C} (which is \texttt{(A \isasymand~B) \isasymimp~C}). Equality is available in the form of the infix function \texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a
\isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$
and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula
$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for
\texttt{\isasymnot($t@1$ = $t@2$)}.

The syntax for quantifiers is
\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and \texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}.  There is
even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which means that there exists exactly one \texttt{x} that satisfies$P$. Nested quantifications can be abbreviated: \texttt{\isasymforall{}x~y~z.}~$P$means \texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$. Despite type inference, it is sometimes necessary to attach explicit \bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly
and should therefore be enclosed in parentheses: \texttt{x < y::nat} is
ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason
for type constraints are overloaded functions like \texttt{+}, \texttt{*} and
\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
overloading.)

\begin{warn}
In general, HOL's concrete syntax tries to follow the conventions of
functional programming and mathematics. Below we list the main rules that you
should be familiar with to avoid certain syntactic traps. A particular
problem for novices can be the priority of operators. If you are unsure, use
more rather than fewer parentheses. In those cases where Isabelle echoes your
input, you can see which parentheses are dropped---they were superfluous. If
you are unsure how to interpret Isabelle's output because you don't know
where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}
\ttindexbold{show_brackets}:
\begin{ttbox}
ML "set show_brackets"; $$\dots$$; ML "reset show_brackets";
\end{ttbox}
\end{warn}

\begin{itemize}
\item
Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
\item
Isabelle allows infix functions like \texttt{+}. The prefix form of function
application binds more strongly than anything else and hence \texttt{f~x + y}
means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
\item Remember that in HOL if-and-only-if is expressed using equality.  But
equality has a high priority, as befitting a relation, while if-and-only-if
typically has the lowest priority.  Thus, \texttt{\isasymnot~\isasymnot~P =
P} means \texttt{\isasymnot\isasymnot(P = P)} and not
\texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean
logical equivalence, enclose both operands in parentheses, as in \texttt{(A
\isasymand~B) = (B \isasymand~A)}.
\item
Constructs with an opening but without a closing delimiter bind very weakly
and should therefore be enclosed in parentheses if they appear in subterms, as
in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},
\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.
\item
Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}
because \texttt{x.x} is always read as a single qualified identifier that
refers to an item \texttt{x} in theory \texttt{x}. Write
\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.
\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.
\end{itemize}

Remember that ASCII-equivalents of all mathematical symbols are
given in figure~\ref{fig:ascii} in the appendix.

\section{Variables}
\label{sec:variables}
\indexbold{variable}

Isabelle distinguishes free and bound variables just as is customary. Bound
variables are automatically renamed to avoid clashes with free variables. In
addition, Isabelle has a third kind of variable, called a \bfindex{schematic
variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
with a \texttt{?}.  Logically, an unknown is a free variable. But it may be
instantiated by another term during the proof process. For example, the
mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},
which means that Isabelle can instantiate it arbitrarily. This is in contrast
to ordinary variables, which remain fixed. The programming language Prolog
calls unknowns {\em logical\/} variables.

Most of the time you can and should ignore unknowns and work with ordinary
variables. Just don't be surprised that after you have finished the proof of
a theorem, Isabelle will turn your free variables into unknowns: it merely
indicates that Isabelle will automatically instantiate those unknowns
suitably when the theorem is used in some other proof.
\begin{warn}
If you use \texttt{?}\index{\$HOL0Ex@\texttt{?}} as an existential
quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is
interpreted as a schematic variable.
\end{warn}

\section{Getting started}

Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
-I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
starts the default logic, which usually is already \texttt{HOL}.  This is
controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
System Manual} for more details.} This presents you with Isabelle's most
basic ASCII interface.  In addition you need to open an editor window to
create theory files.  While you are developing a theory, we recommend to
type each command into the file first and then enter it into Isabelle by
copy-and-paste, thus ensuring that you have a complete record of your theory.
As mentioned earlier, Proof General offers a much superior interface.