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
55 theory T = B\(@1\) + \(\cdots\) + B\(@n\):
56 {\rmfamily\textit{declarations, definitions, and proofs}}
59 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
60 theories that \texttt{T} is based on and \textit{declarations,
61 definitions, and proofs} represents the newly introduced concepts
62 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
63 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@.
64 Everything defined in the parent theories (and their parents, recursively) is
65 automatically visible. To avoid name clashes, identifiers can be
66 \textbf{qualified}\indexbold{identifiers!qualified}
67 by theory names as in \texttt{T.f} and~\texttt{B.f}.
68 Each theory \texttt{T} must
69 reside in a \textbf{theory file}\index{theory files} named \texttt{T.thy}.
71 This tutorial is concerned with introducing you to the different linguistic
72 constructs that can fill the \textit{declarations, definitions, and
73 proofs} above. A complete grammar of the basic
74 constructs is found in the Isabelle/Isar Reference
75 Manual~\cite{isabelle-isar-ref}.
77 HOL's theory collection is available online at
79 \url{http://isabelle.in.tum.de/library/HOL/}
81 and is recommended browsing. Note that most of the theories
82 are based on classical Isabelle without the Isar extension. This means that
83 they look slightly different than the theories in this tutorial, and that all
84 proofs are in separate ML files.
87 HOL contains a theory \thydx{Main}, the union of all the basic
88 predefined theories like arithmetic, lists, sets, etc.
89 Unless you know what you are doing, always include \isa{Main}
90 as a direct or indirect parent of all your theories.
92 There is also a growing Library~\cite{HOL-Library}\index{Library}
93 of useful theories that are not part of \isa{Main} but can be included
94 among the parents of a theory and will then be loaded automatically.%
98 \section{Types, Terms and Formulae}
99 \label{sec:TypesTermsForms}
101 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
102 logic whose type system resembles that of functional programming languages
103 like ML or Haskell. Thus there are
107 in particular \tydx{bool}, the type of truth values,
108 and \tydx{nat}, the type of natural numbers.
109 \item[type constructors,]\index{type constructors}
110 in particular \tydx{list}, the type of
111 lists, and \tydx{set}, the type of sets. Type constructors are written
112 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
113 natural numbers. Parentheses around single arguments can be dropped (as in
114 \isa{nat list}), multiple arguments are separated by commas (as in
116 \item[function types,]\index{function types}
117 denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
118 In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
119 \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
120 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
121 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
122 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
124 \item[type variables,]\index{type variables}\index{variables!type}
125 denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
126 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
130 Types are extremely important because they prevent us from writing
131 nonsense. Isabelle insists that all terms and formulae must be well-typed
132 and will print an error message if a type mismatch is encountered. To
133 reduce the amount of explicit type information that needs to be provided by
134 the user, Isabelle infers the type of all variables automatically (this is
135 called \bfindex{type inference}) and keeps quiet about it. Occasionally
136 this may lead to misunderstandings between you and the system. If anything
137 strange happens, we recommend that you set the flag\index{flags}
138 \isa{show_types}\index{*show_types (flag)}.
139 Isabelle will then display type information
140 that is usually suppressed. Simply type
146 This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
147 which we introduce as we go along, can be set and reset in the same manner.%
148 \index{flags!setting and resetting}
154 \textbf{Terms} are formed as in functional programming by
155 applying functions to arguments. If \isa{f} is a function of type
156 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
157 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
158 infix functions like \isa{+} and some basic constructs from functional
159 programming, such as conditional expressions:
161 \item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
162 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
163 \item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
164 is equivalent to $u$ where all free occurrences of $x$ have been replaced by
166 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
167 by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.
168 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
169 \index{*case expressions}
170 evaluates to $e@i$ if $e$ is of the form $c@i$.
173 Terms may also contain
174 \isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
176 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
177 returns \isa{x+1}. Instead of
178 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
179 \isa{\isasymlambda{}x~y~z.~$t$}.%
183 \textbf{Formulae} are terms of type \tydx{bool}.
184 There are the basic constants \cdx{True} and \cdx{False} and
185 the usual logical connectives (in decreasing order of priority):
186 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
187 \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
188 all of which (except the unary \isasymnot) associate to the right. In
189 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
190 \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
191 \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
193 Equality\index{equality} is available in the form of the infix function
194 \isa{=} of type \isa{'a \isasymFun~'a
195 \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
196 and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
197 \isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
199 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
200 \isa{\isasymnot($t@1$ = $t@2$)}.
202 Quantifiers\index{quantifiers} are written as
203 \isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}.
205 \isa{\isasymuniqex{}x.~$P$}, which
206 means that there exists exactly one \isa{x} that satisfies \isa{$P$}.
207 Nested quantifications can be abbreviated:
208 \isa{\isasymforall{}x~y~z.~$P$} means
209 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
212 Despite type inference, it is sometimes necessary to attach explicit
213 \bfindex{type constraints} to a term. The syntax is
214 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
215 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
216 in parentheses. For instance,
217 \isa{x < y::nat} is ill-typed because it is interpreted as
218 \isa{(x < y)::nat}. Type constraints may be needed to disambiguate
220 involving overloaded functions such as~\isa{+},
221 \isa{*} and~\isa{<}. Section~\ref{sec:overloading}
222 discusses overloading, while Table~\ref{tab:overloading} presents the most
223 important overloaded function symbols.
225 In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
226 functional programming and mathematics. Here are the main rules that you
227 should be familiar with to avoid certain syntactic traps:
230 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
232 Isabelle allows infix functions like \isa{+}. The prefix form of function
233 application binds more strongly than anything else and hence \isa{f~x + y}
234 means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
235 \item Remember that in HOL if-and-only-if is expressed using equality. But
236 equality has a high priority, as befitting a relation, while if-and-only-if
237 typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P =
238 P} means \isa{\isasymnot\isasymnot(P = P)} and not
239 \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
240 logical equivalence, enclose both operands in parentheses, as in \isa{(A
241 \isasymand~B) = (B \isasymand~A)}.
243 Constructs with an opening but without a closing delimiter bind very weakly
244 and should therefore be enclosed in parentheses if they appear in subterms, as
245 in \isa{(\isasymlambda{}x.~x) = f}. This includes
246 \isa{if},\index{*if expressions}
247 \isa{let},\index{*let expressions}
248 \isa{case},\index{*case expressions}
249 \isa{\isasymlambda}, and quantifiers.
251 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
252 because \isa{x.x} is always taken as a single qualified identifier. Write
253 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
254 \item Identifiers\indexbold{identifiers} may contain the characters \isa{_}
255 and~\isa{'}, except at the beginning.
258 For the sake of readability, we use the usual mathematical symbols throughout
259 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
264 problem for novices can be the priority of operators. If you are unsure, use
265 additional parentheses. In those cases where Isabelle echoes your
266 input, you can see which parentheses are dropped --- they were superfluous. If
267 you are unsure how to interpret Isabelle's output because you don't know
268 where the (dropped) parentheses go, set the flag\index{flags}
269 \isa{show_brackets}\index{*show_brackets (flag)}:
271 ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
277 \label{sec:variables}
280 Isabelle distinguishes free and bound variables, as is customary. Bound
281 variables are automatically renamed to avoid clashes with free variables. In
282 addition, Isabelle has a third kind of variable, called a \textbf{schematic
283 variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},
284 which must have a~\isa{?} as its first character.
285 Logically, an unknown is a free variable. But it may be
286 instantiated by another term during the proof process. For example, the
287 mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
288 which means that Isabelle can instantiate it arbitrarily. This is in contrast
289 to ordinary variables, which remain fixed. The programming language Prolog
290 calls unknowns {\em logical\/} variables.
292 Most of the time you can and should ignore unknowns and work with ordinary
293 variables. Just don't be surprised that after you have finished the proof of
294 a theorem, Isabelle will turn your free variables into unknowns. It
295 indicates that Isabelle will automatically instantiate those unknowns
296 suitably when the theorem is used in some other proof.
297 Note that for readability we often drop the \isa{?}s when displaying a theorem.
299 For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
300 of the \(\exists\) symbol. However, the \isa{?} character must then be followed
301 by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is
302 interpreted as a schematic variable. The preferred ASCII representation of
303 the \(\exists\) symbol is \isa{EX}\@.
307 \section{Interaction and Interfaces}
309 Interaction with Isabelle can either occur at the shell level or through more
310 advanced interfaces. To keep the tutorial independent of the interface, we
311 have phrased the description of the interaction in a neutral language. For
312 example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
313 shell level, which is explained the first time the phrase is used. Other
314 interfaces perform the same act by cursor movements and/or mouse clicks.
315 Although shell-based interaction is quite feasible for the kind of proof
316 scripts currently presented in this tutorial, the recommended interface for
317 Isabelle/Isar is the Emacs-based \bfindex{Proof
318 General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
320 Some interfaces (including the shell level) offer special fonts with
321 mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
322 are shown in table~\ref{tab:ascii} in the appendix.
324 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}}
325 Commands may but need not be terminated by semicolons.
326 At the shell level it is advisable to use semicolons to enforce that a command
327 is executed immediately; otherwise Isabelle may wait for the next keyword
328 before it knows that the command is complete.
331 \section{Getting Started}
333 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
334 -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
335 starts the default logic, which usually is already \texttt{HOL}. This is
336 controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
337 System Manual} for more details.} This presents you with Isabelle's most
338 basic \textsc{ascii} interface. In addition you need to open an editor window to
339 create theory files. While you are developing a theory, we recommend that you
340 type each command into the file first and then enter it into Isabelle by
341 copy-and-paste, thus ensuring that you have a complete record of your theory.
342 As mentioned above, Proof General offers a much superior interface.
343 If you have installed Proof General, you can start it by typing \texttt{Isabelle}.