5375

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

6606

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

5375

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 
A tutorial is by definition incomplete. To fully exploit the power of the

6606

19 
system you need to consult the Isabelle Reference Manual~\cite{isabelleref}


20 
for details about Isabelle and the Isabelle/HOL manual~\cite{isabelleHOL}


21 
for details relating to HOL. Both manuals have a comprehensive index.

5375

22 


23 
\section{Theories, proofs and interaction}


24 
\label{sec:Basic:Theories}


25 


26 
Working with Isabelle means creating two different kinds of documents:


27 
theories and proof scripts. Roughly speaking, a \bfindex{theory} is a named


28 
collection of types and functions, much like a module in a programming


29 
language or a specification in a specification language. In fact, theories in


30 
HOL can be either. Theories must reside in files with the suffix


31 
\texttt{.thy}. The general format of a theory file \texttt{T.thy} is


32 
\begin{ttbox}


33 
T = B\(@1\) + \(\cdots\) + B\(@n\) +

6584

34 
\({\langle}declarations{\rangle}\)

5375

35 
end


36 
\end{ttbox}


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

6584

38 
theories that \texttt{T} is based on and ${\langle}declarations{\rangle}$ stands for the

5375

39 
newly introduced concepts (types, functions etc). The \texttt{B}$@i$ are the


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


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


42 
automatically visible. To avoid name clashes, identifiers can be qualified by


43 
theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is

6148

44 
available online at

6628

45 


46 
\begin{center}\small


47 
\begin{tabular}{l}


48 
\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\


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


50 
\end{tabular}


51 
\end{center}


52 

6148

53 
and is recommended browsing.

5375

54 
\begin{warn}


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


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


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


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


59 
\end{warn}


60 


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

6584

62 
constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template.

5375

63 
A complete grammar of the basic constructs is found in Appendix~A

6606

64 
of~\cite{isabelleref}, for reference in times of doubt.

5375

65 


66 
The tutorial is also concerned with showing you how to prove theorems about


67 
the concepts in a theory. This involves invoking predefined theorem proving


68 
commands. Because Isabelle is written in the programming language


69 
ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not


70 
confuse the two levels.} interacting with Isabelle means calling ML


71 
functions. Hence \bfindex{proof scripts} are sequences of calls to ML


72 
functions that perform specific theorem proving tasks. Nevertheless,


73 
familiarity with ML is absolutely not required. All proof scripts for theory


74 
\texttt{T} (defined in file \texttt{T.thy}) should be contained in file


75 
\texttt{T.ML}. Theory and proof scripts are loaded (and checked!) by calling


76 
the ML function \ttindexbold{use_thy}:


77 
\begin{ttbox}


78 
use_thy "T";


79 
\end{ttbox}


80 


81 
There are more advanced interfaces for Isabelle that hide the ML level from


82 
you and replace function calls by menu selection. There is even a special


83 
font with mathematical symbols. For details see the Isabelle home page. This


84 
tutorial concentrates on the bare essentials and ignores such niceties.


85 


86 
\section{Types, terms and formulae}


87 
\label{sec:TypesTermsForms}


88 


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


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


91 
programming languages like ML or Haskell. Thus there are


92 
\begin{description}


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


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


95 
\item[type constructors,] in particular \ttindex{list}, the type of


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


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


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


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


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


101 
\item[function types,] denoted by \ttindexbold{=>}. In HOL


102 
\texttt{=>} represents {\em total} functions only. As is customary,


103 
\texttt{$\tau@1$ => $\tau@2$ => $\tau@3$} means


104 
\texttt{$\tau@1$ => ($\tau@2$ => $\tau@3$)}. Isabelle also supports the


105 
notation \texttt{[$\tau@1,\dots,\tau@n$] => $\tau$} which abbreviates


106 
\texttt{$\tau@1$ => $\cdots$ => $\tau@n$ => $\tau$}.


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


108 
ML. They give rise to polymorphic types like \texttt{'a => 'a}, the type of the


109 
identity function.


110 
\end{description}


111 
\begin{warn}


112 
Types are extremely important because they prevent us from writing


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


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


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


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


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


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


119 
strange happens, we recommend to set the flag \ttindexbold{show_types} that


120 
tells Isabelle to display type information that is usually suppressed:


121 
simply type


122 
\begin{ttbox}


123 
set show_types;


124 
\end{ttbox}


125 


126 
\noindent


127 
at the MLlevel. This can be reversed by \texttt{reset show_types;}.


128 
\end{warn}


129 


130 


131 
\textbf{Terms}\indexbold{term}


132 
are formed as in functional programming by applying functions to


133 
arguments. If \texttt{f} is a function of type \texttt{$\tau@1$ => $\tau@2$}


134 
and \texttt{t} is a term of type $\tau@1$ then \texttt{f~t} is a term of type


135 
$\tau@2$. HOL also supports infix functions like \texttt{+} and some basic


136 
constructs from functional programming:


137 
\begin{description}


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


139 
means what you think it means and requires that


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


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


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


143 
$t$. For example,


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


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


146 
\item[\texttt{case $e$ of $c@1$ => $e@1$  \dots  $c@n$ => $e@n$}]


147 
\indexbold{*case}


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


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


150 
\end{description}


151 


152 
Terms may also contain $\lambda$abstractions. For example, $\lambda


153 
x. x+1$ is the function that takes an argument $x$ and returns $x+1$. In


154 
Isabelle we write \texttt{\%x.~x+1}.\index{==>@{\tt\%}bold}


155 
Instead of \texttt{\%x.~\%y.~\%z.~t} we can write \texttt{\%x~y~z.~t}.


156 


157 
\textbf{Formulae}\indexbold{formula}


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


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


160 
connectives (in decreasing order of priority):


161 
\verb$~$\index{$HOL1@{\ttnot}bold} (`not'),


162 
\texttt{\&}\index{$HOL2@{\tt\&}bold} (`and'),


163 
\texttt{}\index{$HOL2@{\ttor}bold} (`or') and


164 
\texttt{>}\index{$HOL2@{\tt>}bold} (`implies'),


165 
all of which (except the unary \verb$~$) associate to the right. In


166 
particular \texttt{A > B > C} means \texttt{A > (B > C)} and is thus


167 
logically equivalent with \texttt{A \& B > C}


168 
(which is \texttt{(A \& B) > C}).


169 


170 
Equality is available in the form of the infix function


171 
\texttt{=} of type \texttt{'a => 'a => bool}. Thus \texttt{$t@1$ = $t@2$} is


172 
a formula provided $t@1$ and $t@2$ are terms of the same type. In case $t@1$


173 
and $t@2$ are of type \texttt{bool}, \texttt{=} acts as ifandonlyif.


174 


175 
The syntax for quantifiers is


176 
\texttt{!~$x$.$\,P$}\index{$HOLQ@{\ttall}bold} (`for all $x$') and


177 
\texttt{?~$x$.$\,P$}\index{$HOLQ@{\tt?}bold} (`exists $x$').


178 
There is even \texttt{?!~$x$.$\,P$}\index{$HOLQ@{\ttuniquex}bold}, which


179 
means that there exists exactly one $x$ that satisfies $P$. Instead of


180 
\texttt{!} and \texttt{?} you may also write \texttt{ALL} and \texttt{EX}.


181 
Nested quantifications can be abbreviated:


182 
\texttt{!$x~y~z$.$\,P$} means \texttt{!$x$.~!$y$.~!$z$.$\,P$}.


183 


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


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


186 
in \texttt{x < (y::nat)}. Note that \texttt{::} binds weakly and should


187 
therefore be enclosed in parentheses: \texttt{x < y::nat} is illtyped


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


189 
constraints are overloaded functions like \texttt{+}, \texttt{*} and


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


191 
overloading.)


192 


193 
\begin{warn}


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


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


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


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


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


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


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


201 
where the (dropped) parentheses go, set (and possibly reset) the flag


202 
\ttindexbold{show_brackets}:


203 
\begin{ttbox}


204 
set show_brackets; \(\dots\); reset show_brackets;


205 
\end{ttbox}


206 
\end{warn}


207 


208 
\begin{itemize}


209 
\item


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


211 
\item


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


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


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


215 
\item


216 
Remember that in HOL ifandonlyif is expressed using equality. But equality


217 
has a high priority, as befitting a relation, while ifandonlyif typically


218 
has the lowest priority. Thus, \verb$~ ~ P = P$ means \verb$~ ~(P = P)$ and


219 
not \verb$(~ ~P) = P$. When using \texttt{=} to mean logical equivalence,


220 
enclose both operands in parentheses, as in \texttt{(A \& B) = (B \& 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


224 
in \texttt{f = (\%x.~x)}. This includes


225 
\ttindex{if}, \ttindex{let}, \ttindex{case}, \verb$%$ and quantifiers.


226 
\item


227 
Never write \texttt{\%x.x} or \texttt{!x.x=x} because \texttt{x.x} is always


228 
read as a single qualified identifier that refers to an item \texttt{x} in


229 
theory \texttt{x}. Write \texttt{\%x.~x} and \texttt{!x.~x=x} instead.


230 
\end{itemize}


231 


232 
\section{Variables}


233 
\label{sec:variables}


234 


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


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


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


238 
variable} or \bfindex{unknown}, which starts with a \texttt{?}. Logically,


239 
an unknown is a free variable. But it may be instantiated by another term


240 
during the proof process. For example, the mathematical theorem $x = x$ is


241 
represented in Isabelle as \texttt{?x = ?x}, which means that Isabelle can


242 
instantiate it arbitrarily. This is in contrast to ordinary variables, which


243 
remain fixed. The programming language Prolog calls unknowns {\em logical\/}


244 
variables.


245 


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


247 
variables. Just don't be surprised that after you have finished the

6691

248 
proof of a theorem, Isabelle (i.e.\ \ttindex{qed} at the end of a proof) will


249 
turn your free variables into unknowns: it merely indicates that Isabelle will


250 
automatically instantiate those unknowns suitably when the theorem is used in


251 
some other proof.

5375

252 
\begin{warn}


253 
The existential quantifier \texttt{?}\index{$HOLQ@{\tt?}} needs to be


254 
followed by a space. Otherwise \texttt{?x} is interpreted as a schematic


255 
variable.


256 
\end{warn}


257 


258 
\section{Getting started}


259 


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

6584

261 
HOL} in a shell window.\footnote{Simply executing \texttt{isabelle} without


262 
an argument starts the default logic, which usually is already \texttt{HOL}.


263 
This is controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The


264 
Isabelle System Manual} for more details.} This presents you with


265 
Isabelle's most basic ASCII interface. In addition you need to open an editor


266 
window to create theories (\texttt{.thy} files) and proof scripts


267 
(\texttt{.ML} files). While you are developing a proof, we recommend to type


268 
each proof command into the MLfile first and then enter it into Isabelle by


269 
copyandpaste, thus ensuring that you have a complete record of your proof.


270 
