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

8771

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

8743

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

8771

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

8743

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}

9541

68 
and is recommended browsing. Note that most of the theories in the library


69 
are based on classical Isabelle without the Isar extension. This means that


70 
they look slightly different than the theories in this tutorial, and that all


71 
proofs are in separate ML files.


72 

8743

73 
\begin{warn}

9792

74 
HOL contains a theory \isaindexbold{Main}, the union of all the basic

8743

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

9933

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

8743

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


78 
\end{warn}


79 


80 


81 
\section{Types, terms and formulae}


82 
\label{sec:TypesTermsForms}


83 
\indexbold{type}


84 

8771

85 
Embedded in a theory are the types, terms and formulae of HOL. HOL is a typed


86 
logic whose type system resembles that of functional programming languages


87 
like ML or Haskell. Thus there are

8743

88 
\begin{description}

8771

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


90 
and \isaindex{nat}, the type of natural numbers.


91 
\item[type constructors,] in particular \isaindex{list}, the type of


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


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

8743

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

8771

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


96 
\isa{(bool,nat)ty}).

8743

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

8771

98 
In HOL \isasymFun\ represents \emph{total} functions only. As is customary,


99 
\isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means


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


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


102 
which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$

8743

103 
\isasymFun~$\tau$}.

8771

104 
\item[type variables,]\indexbold{type variable}\indexbold{variable!type}


105 
denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise


106 
to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity


107 
function.

8743

108 
\end{description}


109 
\begin{warn}


110 
Types are extremely important because they prevent us from writing


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


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


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


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


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


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


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

9792

118 
\isaindexbold{show_types} that tells Isabelle to display type information

8743

119 
that is usually suppressed: simply type


120 
\begin{ttbox}


121 
ML "set show_types"


122 
\end{ttbox}


123 


124 
\noindent


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

8771

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

8743

127 
\end{warn}


128 


129 


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

8771

131 
applying functions to arguments. If \isa{f} is a function of type


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


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


134 
infix functions like \isa{+} and some basic constructs from functional

8743

135 
programming:


136 
\begin{description}

8771

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

8743

138 
means what you think it means and requires that

8771

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


140 
\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}

8743

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


142 
$t$. For example,

8771

143 
\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated


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


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

8743

146 
\indexbold{*case}

8771

147 
evaluates to $e@i$ if $e$ is of the form $c@i$.

8743

148 
\end{description}


149 


150 
Terms may also contain


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

8771

152 
\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and


153 
returns \isa{x+1}. Instead of


154 
\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write


155 
\isa{\isasymlambda{}x~y~z.~$t$}.

8743

156 

8771

157 
\textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.


158 
There are the basic constants \isaindexbold{True} and \isaindexbold{False} and


159 
the usual logical connectives (in decreasing order of priority):


160 
\indexboldpos{\isasymnot}{$HOL0not}, \indexboldpos{\isasymand}{$HOL0and},


161 
\indexboldpos{\isasymor}{$HOL0or}, and \indexboldpos{\isasymimp}{$HOL0imp},

8743

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

8771

163 
particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B


164 
\isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B


165 
\isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).

8743

166 


167 
Equality is available in the form of the infix function

8771

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


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

8743

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

8771

171 
\isa{bool}, \isa{=} acts as ifandonlyif. The formula


172 
\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for


173 
\isa{\isasymnot($t@1$ = $t@2$)}.

8743

174 


175 
The syntax for quantifiers is

8771

176 
\isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and


177 
\isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}. There is


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


179 
means that there exists exactly one \isa{x} that satisfies \isa{$P$}. Nested


180 
quantifications can be abbreviated: \isa{\isasymforall{}x~y~z.~$P$} means


181 
\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.

8743

182 


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

8771

184 
\textbf{type constraints}\indexbold{type constraint} to a term. The syntax is


185 
\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that


186 
\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed


187 
in parentheses: \isa{x < y::nat} is illtyped because it is interpreted as


188 
\isa{(x < y)::nat}. The main reason for type constraints are overloaded


189 
functions like \isa{+}, \isa{*} and \isa{<}. (See \S\ref{sec:TypeClasses} for


190 
a full discussion of overloading.)

8743

191 


192 
\begin{warn}


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


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


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


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


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


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


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


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

9792

201 
\isaindexbold{show_brackets}:

8743

202 
\begin{ttbox}


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


204 
\end{ttbox}


205 
\end{warn}


206 


207 
\begin{itemize}


208 
\item

8771

209 
Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!

8743

210 
\item

8771

211 
Isabelle allows infix functions like \isa{+}. The prefix form of function


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


213 
means \isa{(f~x)~+~y} and not \isa{f(x+y)}.

8743

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


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

8771

216 
typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P =


217 
P} means \isa{\isasymnot\isasymnot(P = P)} and not


218 
\isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean


219 
logical equivalence, enclose both operands in parentheses, as in \isa{(A

8743

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


221 
\item


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


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

8771

224 
in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},


225 
\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.

8743

226 
\item

8771

227 
Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}


228 
because \isa{x.x} is always read as a single qualified identifier that


229 
refers to an item \isa{x} in theory \isa{x}. Write


230 
\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.


231 
\item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.

8743

232 
\end{itemize}


233 

8771

234 
For the sake of readability the usual mathematical symbols are used throughout


235 
the tutorial. Their ASCIIequivalents are shown in figure~\ref{fig:ascii} in


236 
the appendix.


237 

8743

238 


239 
\section{Variables}


240 
\label{sec:variables}


241 
\indexbold{variable}


242 


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


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


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


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

8771

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

8743

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

8771

249 
mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},

8743

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


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


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


253 


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


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


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


257 
indicates that Isabelle will automatically instantiate those unknowns


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

9689

259 
Note that for readability we often drop the \isa{?}s when displaying a theorem.

8743

260 
\begin{warn}

8771

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


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

8743

263 
interpreted as a schematic variable.


264 
\end{warn}


265 

8771

266 
\section{Interaction and interfaces}


267 


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


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


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


271 
example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the


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


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


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


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


276 
Isabelle/Isar is the Emacsbased \bfindex{Proof


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


278 


279 
Some interfaces (including the shell level) offer special fonts with


280 
mathematical symbols. For those that do not, remember that ASCIIequivalents


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


282 

9541

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


284 
Commands may but need not be terminated by semicolons.


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

8771

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

9541

287 
before it knows that the command is complete.

8771

288 


289 

8743

290 
\section{Getting started}


291 


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


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


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


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


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


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


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


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


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

8771

301 
As mentioned above, Proof General offers a much superior interface.

9541

302 
If you have installed Proof General, you can start it with \texttt{Isabelle}.
