1 \chapter{Basic Concepts}
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.
95 \section{Types, Terms and Formulae}
96 \label{sec:TypesTermsForms}
98 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
99 logic whose type system resembles that of functional programming languages
100 like ML or Haskell. Thus there are
104 in particular \tydx{bool}, the type of truth values,
105 and \tydx{nat}, the type of natural numbers.
106 \item[type constructors,]\index{type constructors}
107 in particular \tydx{list}, the type of
108 lists, and \tydx{set}, the type of sets. Type constructors are written
109 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
110 natural numbers. Parentheses around single arguments can be dropped (as in
111 \isa{nat list}), multiple arguments are separated by commas (as in
113 \item[function types,]\index{function types}
114 denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
115 In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
116 \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
117 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
118 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
119 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
121 \item[type variables,]\index{type variables}\index{variables!type}
122 denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
123 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
127 Types are extremely important because they prevent us from writing
128 nonsense. Isabelle insists that all terms and formulae must be well-typed
129 and will print an error message if a type mismatch is encountered. To
130 reduce the amount of explicit type information that needs to be provided by
131 the user, Isabelle infers the type of all variables automatically (this is
132 called \bfindex{type inference}) and keeps quiet about it. Occasionally
133 this may lead to misunderstandings between you and the system. If anything
134 strange happens, we recommend that you set the flag\index{flags}
135 \isa{show_types}\index{*show_types (flag)}.
136 Isabelle will then display type information
137 that is usually suppressed. Simply type
143 This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
144 which we introduce as we go along, can be set and reset in the same manner.%
145 \index{flags!setting and resetting}
151 \textbf{Terms} are formed as in functional programming by
152 applying functions to arguments. If \isa{f} is a function of type
153 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
154 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
155 infix functions like \isa{+} and some basic constructs from functional
156 programming, such as conditional expressions:
158 \item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
159 Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
160 \item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
161 is equivalent to $u$ where all occurrences of $x$ have been replaced by
163 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
164 by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
165 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
166 \index{*case expressions}
167 evaluates to $e@i$ if $e$ is of the form $c@i$.
170 Terms may also contain
171 \isasymlambda-abstractions.\index{lambda@$\lambda$ expressions}
173 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
174 returns \isa{x+1}. Instead of
175 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
176 \isa{\isasymlambda{}x~y~z.~$t$}.%
180 \textbf{Formulae} are terms of type \tydx{bool}.
181 There are the basic constants \cdx{True} and \cdx{False} and
182 the usual logical connectives (in decreasing order of priority):
183 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
184 \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
185 all of which (except the unary \isasymnot) associate to the right. In
186 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
187 \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
188 \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
190 Equality\index{equality} is available in the form of the infix function
191 \isa{=} of type \isa{'a \isasymFun~'a
192 \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
193 and $t@2$ are terms of the same type. If $t@1$ and $t@2$ are of type
194 \isa{bool} then \isa{=} acts as \rmindex{if-and-only-if}.
196 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
197 \isa{\isasymnot($t@1$ = $t@2$)}.
199 Quantifiers\index{quantifiers} are written as
200 \isa{\isasymforall{}x.~$P$} and \isa{\isasymexists{}x.~$P$}.
202 \isa{\isasymuniqex{}x.~$P$}, which
203 means that there exists exactly one \isa{x} that satisfies \isa{$P$}.
204 Nested quantifications can be abbreviated:
205 \isa{\isasymforall{}x~y~z.~$P$} means
206 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.%
209 Despite type inference, it is sometimes necessary to attach explicit
210 \bfindex{type constraints} to a term. The syntax is
211 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
212 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
213 in parentheses. For instance,
214 \isa{x < y::nat} is ill-typed because it is interpreted as
215 \isa{(x < y)::nat}. Type constraints may be needed to disambiguate
217 involving overloaded functions such as~\isa{+},
218 \isa{*} and~\isa{<}. Section~\ref{sec:overloading}
219 discusses overloading, while Table~\ref{tab:overloading} presents the most
220 important overloaded function symbols.
222 In general, HOL's concrete \rmindex{syntax} tries to follow the conventions of
223 functional programming and mathematics. Here are the main rules that you
224 should be familiar with to avoid certain syntactic traps:
227 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
229 Isabelle allows infix functions like \isa{+}. The prefix form of function
230 application binds more strongly than anything else and hence \isa{f~x + y}
231 means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
232 \item Remember that in HOL if-and-only-if is expressed using equality. But
233 equality has a high priority, as befitting a relation, while if-and-only-if
234 typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P =
235 P} means \isa{\isasymnot\isasymnot(P = P)} and not
236 \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
237 logical equivalence, enclose both operands in parentheses, as in \isa{(A
238 \isasymand~B) = (B \isasymand~A)}.
240 Constructs with an opening but without a closing delimiter bind very weakly
241 and should therefore be enclosed in parentheses if they appear in subterms, as
242 in \isa{(\isasymlambda{}x.~x) = f}. This includes
243 \isa{if},\index{*if expressions}
244 \isa{let},\index{*let expressions}
245 \isa{case},\index{*case expressions}
246 \isa{\isasymlambda}, and quantifiers.
248 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
249 because \isa{x.x} is always taken as a single qualified identifier. Write
250 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
251 \item Identifiers\indexbold{identifiers} may contain the characters \isa{_}
252 and~\isa{'}, except at the beginning.
255 For the sake of readability, we use the usual mathematical symbols throughout
256 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
261 problem for novices can be the priority of operators. If you are unsure, use
262 additional parentheses. In those cases where Isabelle echoes your
263 input, you can see which parentheses are dropped --- they were superfluous. If
264 you are unsure how to interpret Isabelle's output because you don't know
265 where the (dropped) parentheses go, set the flag\index{flags}
266 \isa{show_brackets}\index{*show_brackets (flag)}:
268 ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
274 \label{sec:variables}
277 Isabelle distinguishes free and bound variables, as is customary. Bound
278 variables are automatically renamed to avoid clashes with free variables. In
279 addition, Isabelle has a third kind of variable, called a \textbf{schematic
280 variable}\index{variables!schematic} or \textbf{unknown}\index{unknowns},
281 which must a~\isa{?} as its first character.
282 Logically, an unknown is a free variable. But it may be
283 instantiated by another term during the proof process. For example, the
284 mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
285 which means that Isabelle can instantiate it arbitrarily. This is in contrast
286 to ordinary variables, which remain fixed. The programming language Prolog
287 calls unknowns {\em logical\/} variables.
289 Most of the time you can and should ignore unknowns and work with ordinary
290 variables. Just don't be surprised that after you have finished the proof of
291 a theorem, Isabelle will turn your free variables into unknowns. It
292 indicates that Isabelle will automatically instantiate those unknowns
293 suitably when the theorem is used in some other proof.
294 Note that for readability we often drop the \isa{?}s when displaying a theorem.
296 For historical reasons, Isabelle accepts \isa{?} as an ASCII representation
297 of the \(\exists\) symbol. However, the \isa{?} character must then be followed
298 by a space, as in \isa{?~x. f(x) = 0}. Otherwise, \isa{?x} is
299 interpreted as a schematic variable. The preferred ASCII representation of
300 the \(\exists\) symbol is \isa{EX}\@.
304 \section{Interaction and Interfaces}
306 Interaction with Isabelle can either occur at the shell level or through more
307 advanced interfaces. To keep the tutorial independent of the interface, we
308 have phrased the description of the interaction in a neutral language. For
309 example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
310 shell level, which is explained the first time the phrase is used. Other
311 interfaces perform the same act by cursor movements and/or mouse clicks.
312 Although shell-based interaction is quite feasible for the kind of proof
313 scripts currently presented in this tutorial, the recommended interface for
314 Isabelle/Isar is the Emacs-based \bfindex{Proof
315 General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
317 Some interfaces (including the shell level) offer special fonts with
318 mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
319 are shown in table~\ref{tab:ascii} in the appendix.
321 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}}
322 Commands may but need not be terminated by semicolons.
323 At the shell level it is advisable to use semicolons to enforce that a command
324 is executed immediately; otherwise Isabelle may wait for the next keyword
325 before it knows that the command is complete.
328 \section{Getting Started}
330 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
331 -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
332 starts the default logic, which usually is already \texttt{HOL}. This is
333 controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
334 System Manual} for more details.} This presents you with Isabelle's most
335 basic \textsc{ascii} interface. In addition you need to open an editor window to
336 create theory files. While you are developing a theory, we recommend that you
337 type each command into the file first and then enter it into Isabelle by
338 copy-and-paste, thus ensuring that you have a complete record of your theory.
339 As mentioned above, Proof General offers a much superior interface.
340 If you have installed Proof General, you can start it by typing \texttt{Isabelle}.