8743

1 
\chapter{Basic Concepts}


2 


3 
\section{Introduction}


4 


5 
This is a tutorial on how to use Isabelle/HOL as a specification and


6 
verification system. Isabelle is a generic system for implementing logical


7 
formalisms, and Isabelle/HOL is the specialization of Isabelle for


8 
HOL, which abbreviates HigherOrder Logic. We introduce HOL step by step


9 
following the equation


10 
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]


11 
We assume that the reader is familiar with the basic concepts of both fields.


12 
For excellent introductions to functional programming consult the textbooks


13 
by Bird and Wadler~\cite{BirdWadler} or Paulson~\cite{paulsonml2}. Although


14 
this tutorial initially concentrates on functional programming, do not be


15 
misled: HOL can express most mathematical concepts, and functional


16 
programming is just one particularly simple and ubiquitous instance.


17 


18 
This tutorial introduces HOL via Isabelle/Isar~\cite{isabelleisarref},


19 
which is an extension of Isabelle~\cite{paulsonisabook} with structured


20 
proofs.\footnote{Thus the full name of the system should be


21 
Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable


22 
difference to classical Isabelle (which is the basis of another version of


23 
this tutorial) is the replacement of the ML level by a dedicated language for


24 
definitions and proofs.


25 


26 
A tutorial is by definition incomplete. Currently the tutorial only


27 
introduces the rudiments of Isar's proof language. To fully exploit the power


28 
of Isar you need to consult the Isabelle/Isar Reference


29 
Manual~\cite{isabelleisarref}. If you want to use Isabelle's ML level


30 
directly (for example for writing your own proof procedures) see the Isabelle


31 
Reference Manual~\cite{isabelleref}; for details relating to HOL see the


32 
Isabelle/HOL manual~\cite{isabelleHOL}. All manuals have a comprehensive


33 
index.


34 


35 
\section{Theories}


36 
\label{sec:Basic:Theories}


37 


38 
Working with Isabelle means creating theories. Roughly speaking, a


39 
\bfindex{theory} is a named collection of types, functions, and theorems,


40 
much like a module in a programming language or a specification in a


41 
specification language. In fact, theories in HOL can be either. The general


42 
format of a theory \texttt{T} is


43 
\begin{ttbox}


44 
theory T = B\(@1\) + \(\cdots\) + B\(@n\):


45 
\(\textit{declarations, definitions, and proofs}\)


46 
end


47 
\end{ttbox}


48 
where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing


49 
theories that \texttt{T} is based on and \texttt{\textit{declarations,


50 
definitions, and proofs}} represents the newly introduced concepts


51 
(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the


52 
direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.


53 
Everything defined in the parent theories (and their parents \dots) is


54 
automatically visible. To avoid name clashes, identifiers can be


55 
\textbf{qualified} by theory names as in \texttt{T.f} and


56 
\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must


57 
reside in a \indexbold{theory file} named \texttt{T.thy}.


58 


59 
This tutorial is concerned with introducing you to the different linguistic


60 
constructs that can fill \textit{\texttt{declarations, definitions, and


61 
proofs}} in the above theory template. A complete grammar of the basic


62 
constructs is found in the Isabelle/Isar Reference Manual.


63 


64 
HOL's theory library is available online at


65 
\begin{center}\small


66 
\url{http://isabelle.in.tum.de/library/}


67 
\end{center}


68 
and is recommended browsing.


69 
\begin{warn}


70 
HOL contains a theory \ttindexbold{Main}, the union of all the basic


71 
predefined theories like arithmetic, lists, sets, etc.\ (see the online


72 
library). Unless you know what you are doing, always include \texttt{Main}


73 
as a direct or indirect parent theory of all your theories.


74 
\end{warn}


75 


76 


77 
\section{Interaction and interfaces}


78 


79 
Interaction with Isabelle can either occur at the shell level or through more


80 
advanced interfaces. To keep the tutorial independent of the interface we


81 
have phrased the description of the intraction in a neutral language. For


82 
example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the


83 
shell level, which is explained the first time the phrase is used. Other


84 
interfaces perform the same act by cursor movements and/or mouse clicks.


85 
Although shellbased interaction is quite feasible for the kind of proof


86 
scripts currently presented in this tutorial, the recommended interface for


87 
Isabelle/Isar is the Emacsbased \bfindex{Proof


88 
General}~\cite{Aspinall:TACAS:2000,proofgeneral}.


89 


90 
To improve readability some of the interfaces (including the shell level)


91 
offer special fonts with mathematical symbols. Therefore the usual


92 
mathematical symbols are used throughout the tutorial. Their


93 
ASCIIequivalents are shown in figure~\ref{fig:ascii} in the appendix.


94 


95 
Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,


96 
for example Proof General, require each command to be terminated by a


97 
semicolon, whereas others, for example the shell level, do not. But even at


98 
the shell level it is advisable to use semicolons to enforce that a command


99 
is executed immediately; otherwise Isabelle may wait for the next keyword


100 
before it knows that the command is complete. Note that for readibility


101 
reasons we often drop the final semicolon in the text.


102 


103 


104 
\section{Types, terms and formulae}


105 
\label{sec:TypesTermsForms}


106 
\indexbold{type}


107 


108 
Embedded in the declarations of a theory are the types, terms and formulae of


109 
HOL. HOL is a typed logic whose type system resembles that of functional


110 
programming languages like ML or Haskell. Thus there are


111 
\begin{description}


112 
\item[base types,] in particular \ttindex{bool}, the type of truth values,


113 
and \ttindex{nat}, the type of natural numbers.


114 
\item[type constructors,] in particular \texttt{list}, the type of


115 
lists, and \texttt{set}, the type of sets. Type constructors are written


116 
postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are


117 
natural numbers. Parentheses around single arguments can be dropped (as in


118 
\texttt{nat list}), multiple arguments are separated by commas (as in


119 
\texttt{(bool,nat)foo}).


120 
\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.


121 
In HOL \isasymFun\ represents {\em total} functions only. As is customary,


122 
\texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means


123 
\texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also


124 
supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}


125 
which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$


126 
\isasymFun~$\tau$}.


127 
\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in


128 
ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the


129 
type of the identity function.


130 
\end{description}


131 
\begin{warn}


132 
Types are extremely important because they prevent us from writing


133 
nonsense. Isabelle insists that all terms and formulae must be welltyped


134 
and will print an error message if a type mismatch is encountered. To


135 
reduce the amount of explicit type information that needs to be provided by


136 
the user, Isabelle infers the type of all variables automatically (this is


137 
called \bfindex{type inference}) and keeps quiet about it. Occasionally


138 
this may lead to misunderstandings between you and the system. If anything


139 
strange happens, we recommend to set the \rmindex{flag}


140 
\ttindexbold{show_types} that tells Isabelle to display type information


141 
that is usually suppressed: simply type


142 
\begin{ttbox}


143 
ML "set show_types"


144 
\end{ttbox}


145 


146 
\noindent


147 
This can be reversed by \texttt{ML "reset show_types"}. Various other flags


148 
can be set and reset in the same manner.\bfindex{flag!(re)setting}


149 
\end{warn}


150 


151 


152 
\textbf{Terms}\indexbold{term} are formed as in functional programming by


153 
applying functions to arguments. If \texttt{f} is a function of type


154 
\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type


155 
$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports


156 
infix functions like \texttt{+} and some basic constructs from functional


157 
programming:


158 
\begin{description}


159 
\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}


160 
means what you think it means and requires that


161 
$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.


162 
\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}


163 
is equivalent to $u$ where all occurrences of $x$ have been replaced by


164 
$t$. For example,


165 
\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated


166 
by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.


167 
\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ ~\dots~ $c@n$ \isasymFun~$e@n$}]


168 
\indexbold{*case}


169 
evaluates to $e@i$ if $e$ is of the form


170 
$c@i$. See~\S\ref{sec:caseexpressions} for details.


171 
\end{description}


172 


173 
Terms may also contain


174 
\isasymlambdaabstractions\indexbold{$Isalam@\isasymlambda}. For example,


175 
\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument


176 
\texttt{x} and returns \texttt{x+1}. Instead of


177 
\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write


178 
\texttt{\isasymlambda{}x~y~z.}~$t$.


179 


180 
\textbf{Formulae}\indexbold{formula}


181 
are terms of type \texttt{bool}. There are the basic


182 
constants \ttindexbold{True} and \ttindexbold{False} and the usual logical


183 
connectives (in decreasing order of priority):


184 
\indexboldpos{\isasymnot}{$HOL0not},


185 
\indexboldpos{\isasymand}{$HOL0and},


186 
\indexboldpos{\isasymor}{$HOL0or}, and


187 
\indexboldpos{\isasymimp}{$HOL0imp},


188 
all of which (except the unary \isasymnot) associate to the right. In


189 
particular \texttt{A \isasymimp~B \isasymimp~C} means


190 
\texttt{A \isasymimp~(B \isasymimp~C)} and is thus


191 
logically equivalent with \texttt{A \isasymand~B \isasymimp~C}


192 
(which is \texttt{(A \isasymand~B) \isasymimp~C}).


193 


194 
Equality is available in the form of the infix function


195 
\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a


196 
\isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$


197 
and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type


198 
\texttt{bool}, \texttt{=} acts as ifandonlyif. The formula


199 
$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for


200 
\texttt{\isasymnot($t@1$ = $t@2$)}.


201 


202 
The syntax for quantifiers is


203 
\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and


204 
\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}. There is


205 
even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqexbold}, which


206 
means that there exists exactly one \texttt{x} that satisfies $P$.


207 
Nested quantifications can be abbreviated:


208 
\texttt{\isasymforall{}x~y~z.}~$P$ means


209 
\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.


210 


211 
Despite type inference, it is sometimes necessary to attach explicit


212 
\bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as


213 
in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly


214 
and should therefore be enclosed in parentheses: \texttt{x < y::nat} is


215 
illtyped because it is interpreted as \texttt{(x < y)::nat}. The main reason


216 
for type constraints are overloaded functions like \texttt{+}, \texttt{*} and


217 
\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of


218 
overloading.)


219 


220 
\begin{warn}


221 
In general, HOL's concrete syntax tries to follow the conventions of


222 
functional programming and mathematics. Below we list the main rules that you


223 
should be familiar with to avoid certain syntactic traps. A particular


224 
problem for novices can be the priority of operators. If you are unsure, use


225 
more rather than fewer parentheses. In those cases where Isabelle echoes your


226 
input, you can see which parentheses are droppedthey were superfluous. If


227 
you are unsure how to interpret Isabelle's output because you don't know


228 
where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}


229 
\ttindexbold{show_brackets}:


230 
\begin{ttbox}


231 
ML "set show_brackets"; \(\dots\); ML "reset show_brackets";


232 
\end{ttbox}


233 
\end{warn}


234 


235 
\begin{itemize}


236 
\item


237 
Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!


238 
\item


239 
Isabelle allows infix functions like \texttt{+}. The prefix form of function


240 
application binds more strongly than anything else and hence \texttt{f~x + y}


241 
means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.


242 
\item Remember that in HOL ifandonlyif is expressed using equality. But


243 
equality has a high priority, as befitting a relation, while ifandonlyif


244 
typically has the lowest priority. Thus, \texttt{\isasymnot~\isasymnot~P =


245 
P} means \texttt{\isasymnot\isasymnot(P = P)} and not


246 
\texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean


247 
logical equivalence, enclose both operands in parentheses, as in \texttt{(A


248 
\isasymand~B) = (B \isasymand~A)}.


249 
\item


250 
Constructs with an opening but without a closing delimiter bind very weakly


251 
and should therefore be enclosed in parentheses if they appear in subterms, as


252 
in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},


253 
\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.


254 
\item


255 
Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}


256 
because \texttt{x.x} is always read as a single qualified identifier that


257 
refers to an item \texttt{x} in theory \texttt{x}. Write


258 
\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.


259 
\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.


260 
\end{itemize}


261 


262 
Remember that ASCIIequivalents of all mathematical symbols are


263 
given in figure~\ref{fig:ascii} in the appendix.


264 


265 
\section{Variables}


266 
\label{sec:variables}


267 
\indexbold{variable}


268 


269 
Isabelle distinguishes free and bound variables just as is customary. Bound


270 
variables are automatically renamed to avoid clashes with free variables. In


271 
addition, Isabelle has a third kind of variable, called a \bfindex{schematic


272 
variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts


273 
with a \texttt{?}. Logically, an unknown is a free variable. But it may be


274 
instantiated by another term during the proof process. For example, the


275 
mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},


276 
which means that Isabelle can instantiate it arbitrarily. This is in contrast


277 
to ordinary variables, which remain fixed. The programming language Prolog


278 
calls unknowns {\em logical\/} variables.


279 


280 
Most of the time you can and should ignore unknowns and work with ordinary


281 
variables. Just don't be surprised that after you have finished the proof of


282 
a theorem, Isabelle will turn your free variables into unknowns: it merely


283 
indicates that Isabelle will automatically instantiate those unknowns


284 
suitably when the theorem is used in some other proof.


285 
\begin{warn}


286 
If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential


287 
quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is


288 
interpreted as a schematic variable.


289 
\end{warn}


290 


291 
\section{Getting started}


292 


293 
Assuming you have installed Isabelle, you start it by typing \texttt{isabelle


294 
I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle I}


295 
starts the default logic, which usually is already \texttt{HOL}. This is


296 
controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle


297 
System Manual} for more details.} This presents you with Isabelle's most


298 
basic ASCII interface. In addition you need to open an editor window to


299 
create theory files. While you are developing a theory, we recommend to


300 
type each command into the file first and then enter it into Isabelle by


301 
copyandpaste, thus ensuring that you have a complete record of your theory.


302 
As mentioned earlier, Proof General offers a much superior interface.
