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 HigherOrder 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{BirdWadler} or Paulson~\cite{paulsonml2}. 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{isabelleisarref},

nipkow@8743

19 
which is an extension of Isabelle~\cite{paulsonisabook} 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{isabelleisarref}. 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{isabelleref}; for details relating to HOL see the

nipkow@8743

32 
Isabelle/HOL manual~\cite{isabelleHOL}. 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@8771

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@8771

57 
reside in a \bfindex{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 

paulson@10885

64 
HOL's theory collection 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}

paulson@10885

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

nipkow@9541

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

nipkow@9541

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

nipkow@9541

71 
proofs are in separate ML files.

nipkow@9541

72 

nipkow@8743

73 
\begin{warn}

nipkow@9792

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

paulson@10885

75 
predefined theories like arithmetic, lists, sets, etc.

paulson@10885

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

nipkow@8743

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

nipkow@8743

78 
\end{warn}

nipkow@8743

79 

nipkow@8743

80 

paulson@10885

81 
\section{Types, Terms and Formulae}

nipkow@8743

82 
\label{sec:TypesTermsForms}

nipkow@8743

83 
\indexbold{type}

nipkow@8743

84 

paulson@10795

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

nipkow@8771

86 
logic whose type system resembles that of functional programming languages

nipkow@8771

87 
like ML or Haskell. Thus there are

nipkow@8743

88 
\begin{description}

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

103 
\isasymFun~$\tau$}.

nipkow@8771

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

paulson@10795

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

nipkow@8771

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

nipkow@8771

107 
function.

nipkow@8743

108 
\end{description}

nipkow@8743

109 
\begin{warn}

nipkow@8743

110 
Types are extremely important because they prevent us from writing

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@9792

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

nipkow@8743

119 
that is usually suppressed: simply type

nipkow@8743

120 
\begin{ttbox}

nipkow@8743

121 
ML "set show_types"

nipkow@8743

122 
\end{ttbox}

nipkow@8743

123 

nipkow@8743

124 
\noindent

nipkow@8743

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

nipkow@8771

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

nipkow@8743

127 
\end{warn}

nipkow@8743

128 

nipkow@8743

129 

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

135 
programming:

nipkow@8743

136 
\begin{description}

nipkow@8771

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

nipkow@8743

138 
means what you think it means and requires that

nipkow@8771

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

nipkow@8771

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

nipkow@8743

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

nipkow@8743

142 
$t$. For example,

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

146 
\indexbold{*case}

nipkow@8771

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

nipkow@8743

148 
\end{description}

nipkow@8743

149 

nipkow@8743

150 
Terms may also contain

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

156 

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

166 

nipkow@8743

167 
Equality is available in the form of the infix function

nipkow@8771

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

nipkow@8771

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

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

174 

paulson@10795

175 
Quantifiers are written as

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

182 

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@10538

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

nipkow@8771

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

paulson@10795

188 
\isa{(x < y)::nat}. The main reason for type constraints is overloading of

nipkow@10538

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

nipkow@10695

190 
a full discussion of overloading and Table~\ref{tab:overloading} for the most

nipkow@10695

191 
important overloaded function symbols.

nipkow@8743

192 

nipkow@8743

193 
\begin{warn}

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

paulson@10795

198 
additional parentheses. In those cases where Isabelle echoes your

nipkow@8743

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

nipkow@8743

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

paulson@10795

201 
where the (dropped) parentheses go, set the \rmindex{flag}

nipkow@9792

202 
\isaindexbold{show_brackets}:

nipkow@8743

203 
\begin{ttbox}

nipkow@8743

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

nipkow@8743

205 
\end{ttbox}

nipkow@8743

206 
\end{warn}

nipkow@8743

207 

nipkow@8743

208 
\begin{itemize}

nipkow@8743

209 
\item

nipkow@8771

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

nipkow@8743

211 
\item

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

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

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

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

nipkow@8743

222 
\item

nipkow@8743

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

nipkow@8743

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

227 
\item

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8743

233 
\end{itemize}

nipkow@8743

234 

nipkow@8771

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

nipkow@8771

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

nipkow@8771

237 
the appendix.

nipkow@8771

238 

nipkow@8743

239 

nipkow@8743

240 
\section{Variables}

nipkow@8743

241 
\label{sec:variables}

nipkow@8743

242 
\indexbold{variable}

nipkow@8743

243 

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8771

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

nipkow@8743

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

nipkow@8771

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

254 

nipkow@8743

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

nipkow@8743

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

nipkow@8743

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

nipkow@8743

258 
indicates that Isabelle will automatically instantiate those unknowns

nipkow@8743

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

nipkow@9689

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

nipkow@8743

261 
\begin{warn}

nipkow@8771

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

nipkow@8771

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

nipkow@8743

264 
interpreted as a schematic variable.

nipkow@8743

265 
\end{warn}

nipkow@8743

266 

paulson@10885

267 
\section{Interaction and Interfaces}

nipkow@8771

268 

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

277 
Isabelle/Isar is the Emacsbased \bfindex{Proof

nipkow@8771

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

nipkow@8771

279 

nipkow@8771

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

nipkow@8771

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

nipkow@8771

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

nipkow@8771

283 

nipkow@9541

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

nipkow@9541

285 
Commands may but need not be terminated by semicolons.

nipkow@9541

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

nipkow@8771

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

nipkow@9541

288 
before it knows that the command is complete.

nipkow@8771

289 

nipkow@8771

290 

paulson@10885

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 
copyandpaste, thus ensuring that you have a complete record of your theory.

nipkow@8771

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

paulson@10795

303 
If you have installed Proof General, you can start it by typing \texttt{Isabelle}.
