5 This book is a tutorial on how to use the theorem prover Isabelle/HOL as a
6 specification and verification system. Isabelle is a generic system for
7 implementing logical formalisms, and Isabelle/HOL is the specialization
8 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
9 HOL step by step following the equation
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
11 We do not assume that you are familiar with mathematical logic.
12 However, we do assume that
13 you are used to logical and set theoretic notation, as covered
14 in a good discrete mathematics course~\cite{Rosen-DMA}, and
15 that you are familiar with the basic concepts of functional
16 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
17 Although this tutorial initially concentrates on functional programming, do
18 not be misled: HOL can express most mathematical concepts, and functional
19 programming is just one particularly simple and ubiquitous instance.
21 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has
22 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
23 for us: this tutorial is based on
24 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
25 the implementation language almost completely. Thus the full name of the
26 system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
28 There are other implementations of HOL, in particular the one by Mike Gordon
30 \emph{et al.}, which is usually referred to as ``the HOL system''
31 \cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
32 its incarnation Isabelle/HOL\@.
34 A tutorial is by definition incomplete. Currently the tutorial only
35 introduces the rudiments of Isar's proof language. To fully exploit the power
36 of Isar, in particular the ability to write readable and structured proofs,
37 you need to consult the Isabelle/Isar Reference
38 Manual~\cite{isabelle-isar-ref} and Wenzel's PhD thesis~\cite{Wenzel-PhD}
39 which discusses many proof patterns. If you want to use Isabelle's ML level
40 directly (for example for writing your own proof procedures) see the Isabelle
41 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
42 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
46 \label{sec:Basic:Theories}
49 Working with Isabelle means creating theories. Roughly speaking, a
50 \textbf{theory} is a named collection of types, functions, and theorems,
51 much like a module in a programming language or a specification in a
52 specification language. In fact, theories in HOL can be either. The general
53 format of a theory \texttt{T} is
56 imports B\(@1\) \(\ldots\) B\(@n\)
58 {\rmfamily\textit{declarations, definitions, and proofs}}
61 where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing
62 theories that \texttt{T} is based on and \textit{declarations,
63 definitions, and proofs} represents the newly introduced concepts
64 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
65 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@.
66 Everything defined in the parent theories (and their parents, recursively) is
67 automatically visible. To avoid name clashes, identifiers can be
68 \textbf{qualified}\indexbold{identifiers!qualified}
69 by theory names as in \texttt{T.f} and~\texttt{B.f}.
70 Each theory \texttt{T} must
71 reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
73 This tutorial is concerned with introducing you to the different linguistic
74 constructs that can fill the \textit{declarations, definitions, and
75 proofs} above. A complete grammar of the basic
76 constructs is found in the Isabelle/Isar Reference
77 Manual~\cite{isabelle-isar-ref}.
79 HOL's theory collection is available online at
81 \url{http://isabelle.in.tum.de/library/HOL/}
83 and is recommended browsing. Note that most of the theories
84 are based on classical Isabelle without the Isar extension. This means that
85 they look slightly different than the theories in this tutorial, and that all
86 proofs are in separate ML files.
89 HOL contains a theory \thydx{Main}, the union of all the basic
90 predefined theories like arithmetic, lists, sets, etc.
91 Unless you know what you are doing, always include \isa{Main}
92 as a direct or indirect parent of all your theories.
94 There is also a growing Library~\cite{HOL-Library}\index{Library}
95 of useful theories that are not part of \isa{Main} but can be included
96 among the parents of a theory and will then be loaded automatically.%
100 \section{Types, Terms and Formulae}
101 \label{sec:TypesTermsForms}
103 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
104 logic whose type system resembles that of functional programming languages
105 like ML or Haskell. Thus there are
109 in particular \tydx{bool}, the type of truth values,
110 and \tydx{nat}, the type of natural numbers.
111 \item[type constructors,]\index{type constructors}
112 in particular \tydx{list}, the type of
113 lists, and \tydx{set}, the type of sets. Type constructors are written
114 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
115 natural numbers. Parentheses around single arguments can be dropped (as in
116 \isa{nat list}), multiple arguments are separated by commas (as in
118 \item[function types,]\index{function types}
119 denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
120 In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
121 \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
122 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
123 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
124 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
126 \item[type variables,]\index{type variables}\index{variables!type}
127 denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
128 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
132 Types are extremely important because they prevent us from writing
133 nonsense. Isabelle insists that all terms and formulae must be well-typed
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 that you set the flag\index{flags}
140 \isa{show_types}\index{*show_types (flag)}.
141 Isabelle will then display type information
142 that is usually suppressed. Simply type
148 This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
149 which we introduce as we go along, can be set and reset in the same manner.%
150 \index{flags!setting and resetting}
156 \textbf{Terms} are formed as in functional programming by
157 applying functions to arguments. If \isa{f} is a function of type
158 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
159 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
160 infix functions like \isa{+} and some basic constructs from functional
161 programming, such as conditional expressions:
163 \item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
164 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
165 \item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
166 is equivalent to $u$ where all free occurrences of $x$ have been replaced by
168 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
169 by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.
170 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
171 \index{*case expressions}
172 evaluates to $e@i$ if $e$ is of the form $c@i$.
175 Terms may also contain
176 \isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
178 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
179 returns \isa{x+1}. Instead of
180 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
181 \isa{\isasymlambda{}x~y~z.~$t$}.%
185 \textbf{Formulae} are terms of type \tydx{bool}.
186 There are the basic constants \cdx{True} and \cdx{False} and
187 the usual logical connectives (in decreasing order of priority):
188 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
189 \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
190 all of which (except the unary \isasymnot) associate to the right. In
191 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
192 \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
193 \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
195 Equality\index{equality} is available in the form of the infix function
196 \isa{=} of type \isa{'a \isasymFun~'a
197 \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
198 and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
199 \isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
201 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
202 \isa{\isasymnot($t@1$ = $t@2$)}.
204 Quantifiers\index{quantifiers} are written as
205 \isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}.
207 \isa{\isasymuniqex{}x.~$P$}, which
208 means that there exists exactly one \isa{x} that satisfies \isa{$P$}.
209 Nested quantifications can be abbreviated:
210 \isa{\isasymforall{}x~y~z.~$P$} means
211 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
214 Despite type inference, it is sometimes necessary to attach explicit
215 \bfindex{type constraints} to a term. The syntax is
216 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
217 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
218 in parentheses. For instance,
219 \isa{x < y::nat} is ill-typed because it is interpreted as
220 \isa{(x < y)::nat}. Type constraints may be needed to disambiguate
222 involving overloaded functions such as~\isa{+},
223 \isa{*} and~\isa{<}. Section~\ref{sec:overloading}
224 discusses overloading, while Table~\ref{tab:overloading} presents the most
225 important overloaded function symbols.
227 In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
228 functional programming and mathematics. Here are the main rules that you
229 should be familiar with to avoid certain syntactic traps:
232 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
234 Isabelle allows infix functions like \isa{+}. The prefix form of function
235 application binds more strongly than anything else and hence \isa{f~x + y}
236 means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
237 \item Remember that in HOL if-and-only-if is expressed using equality. But
238 equality has a high priority, as befitting a relation, while if-and-only-if
239 typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P =
240 P} means \isa{\isasymnot\isasymnot(P = P)} and not
241 \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
242 logical equivalence, enclose both operands in parentheses, as in \isa{(A
243 \isasymand~B) = (B \isasymand~A)}.
245 Constructs with an opening but without a closing delimiter bind very weakly
246 and should therefore be enclosed in parentheses if they appear in subterms, as
247 in \isa{(\isasymlambda{}x.~x) = f}. This includes
248 \isa{if},\index{*if expressions}
249 \isa{let},\index{*let expressions}
250 \isa{case},\index{*case expressions}
251 \isa{\isasymlambda}, and quantifiers.
253 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
254 because \isa{x.x} is always taken as a single qualified identifier. Write
255 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
256 \item Identifiers\indexbold{identifiers} may contain the characters \isa{_}
257 and~\isa{'}, except at the beginning.
260 For the sake of readability, we use the usual mathematical symbols throughout
261 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
266 problem for novices can be the priority of operators. If you are unsure, use
267 additional parentheses. In those cases where Isabelle echoes your
268 input, you can see which parentheses are dropped --- they were superfluous. If
269 you are unsure how to interpret Isabelle's output because you don't know
270 where the (dropped) parentheses go, set the flag\index{flags}
271 \isa{show_brackets}\index{*show_brackets (flag)}:
273 ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
279 \label{sec:variables}
282 Isabelle distinguishes free and bound variables, as is customary. Bound
283 variables are automatically renamed to avoid clashes with free variables. In
284 addition, Isabelle has a third kind of variable, called a \textbf{schematic
285 variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},
286 which must have a~\isa{?} as its first character.
287 Logically, an unknown is a free variable. But it may be
288 instantiated by another term during the proof process. For example, the
289 mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
290 which means that Isabelle can instantiate it arbitrarily. This is in contrast
291 to ordinary variables, which remain fixed. The programming language Prolog
292 calls unknowns {\em logical\/} variables.
294 Most of the time you can and should ignore unknowns and work with ordinary
295 variables. Just don't be surprised that after you have finished the proof of
296 a theorem, Isabelle will turn your free variables into unknowns. It
297 indicates that Isabelle will automatically instantiate those unknowns
298 suitably when the theorem is used in some other proof.
299 Note that for readability we often drop the \isa{?}s when displaying a theorem.
301 For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
302 of the \(\exists\) symbol. However, the \isa{?} character must then be followed
303 by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is
304 interpreted as a schematic variable. The preferred ASCII representation of
305 the \(\exists\) symbol is \isa{EX}\@.
309 \section{Interaction and Interfaces}
311 Interaction with Isabelle can either occur at the shell level or through more
312 advanced interfaces. To keep the tutorial independent of the interface, we
313 have phrased the description of the interaction in a neutral language. For
314 example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
315 shell level, which is explained the first time the phrase is used. Other
316 interfaces perform the same act by cursor movements and/or mouse clicks.
317 Although shell-based interaction is quite feasible for the kind of proof
318 scripts currently presented in this tutorial, the recommended interface for
319 Isabelle/Isar is the Emacs-based \bfindex{Proof
320 General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
322 Some interfaces (including the shell level) offer special fonts with
323 mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
324 are shown in table~\ref{tab:ascii} in the appendix.
326 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}}
327 Commands may but need not be terminated by semicolons.
328 At the shell level it is advisable to use semicolons to enforce that a command
329 is executed immediately; otherwise Isabelle may wait for the next keyword
330 before it knows that the command is complete.
333 \section{Getting Started}
335 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
336 -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
337 starts the default logic, which usually is already \texttt{HOL}. This is
338 controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
339 System Manual} for more details.} This presents you with Isabelle's most
340 basic \textsc{ascii} interface. In addition you need to open an editor window to
341 create theory files. While you are developing a theory, we recommend that you
342 type each command into the file first and then enter it into Isabelle by
343 copy-and-paste, thus ensuring that you have a complete record of your theory.
344 As mentioned above, Proof General offers a much superior interface.
345 If you have installed Proof General, you can start it by typing \texttt{Isabelle}.