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 the reader is familiar with mathematical logic but that
12 (s)he is used to logical and set theoretic notation, such as covered
13 in a good discrete math course~\cite{Rosen-DMA}. In contrast, we do assume
14 that the reader is familiar with the basic concepts of functional
15 programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
16 Although this tutorial initially concentrates on functional programming, do
17 not be misled: HOL can express most mathematical concepts, and functional
18 programming is just one particularly simple and ubiquitous instance.
20 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has
21 influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
22 for us because this tutorial is based on
23 Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
24 the implementation language almost completely. Thus the full name of the
25 system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
27 There are other implementations of HOL, in particular the one by Mike Gordon
28 \emph{et al.}, which is usually referred to as ``the HOL system''
29 \cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
30 its incarnation Isabelle/HOL.
32 A tutorial is by definition incomplete. Currently the tutorial only
33 introduces the rudiments of Isar's proof language. To fully exploit the power
34 of Isar, in particular the ability to write readable and structured proofs,
35 you need to consult the Isabelle/Isar Reference
36 Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
37 directly (for example for writing your own proof procedures) see the Isabelle
38 Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
39 Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
43 \label{sec:Basic:Theories}
45 Working with Isabelle means creating theories. Roughly speaking, a
46 \bfindex{theory} is a named collection of types, functions, and theorems,
47 much like a module in a programming language or a specification in a
48 specification language. In fact, theories in HOL can be either. The general
49 format of a theory \texttt{T} is
51 theory T = B\(@1\) + \(\cdots\) + B\(@n\):
52 \(\textit{declarations, definitions, and proofs}\)
55 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
56 theories that \texttt{T} is based on and \texttt{\textit{declarations,
57 definitions, and proofs}} represents the newly introduced concepts
58 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
59 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
60 Everything defined in the parent theories (and their parents \dots) is
61 automatically visible. To avoid name clashes, identifiers can be
62 \textbf{qualified} by theory names as in \texttt{T.f} and
63 \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
64 reside in a \bfindex{theory file} named \texttt{T.thy}.
66 This tutorial is concerned with introducing you to the different linguistic
67 constructs that can fill \textit{\texttt{declarations, definitions, and
68 proofs}} in the above theory template. A complete grammar of the basic
69 constructs is found in the Isabelle/Isar Reference Manual.
71 HOL's theory collection is available online at
73 \url{http://isabelle.in.tum.de/library/HOL/}
75 and is recommended browsing. Note that most of the theories
76 are based on classical Isabelle without the Isar extension. This means that
77 they look slightly different than the theories in this tutorial, and that all
78 proofs are in separate ML files.
81 HOL contains a theory \isaindexbold{Main}, the union of all the basic
82 predefined theories like arithmetic, lists, sets, etc.
83 Unless you know what you are doing, always include \isa{Main}
84 as a direct or indirect parent of all your theories.
88 \section{Types, Terms and Formulae}
89 \label{sec:TypesTermsForms}
92 Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
93 logic whose type system resembles that of functional programming languages
94 like ML or Haskell. Thus there are
96 \item[base types,] in particular \isaindex{bool}, the type of truth values,
97 and \isaindex{nat}, the type of natural numbers.
98 \item[type constructors,] in particular \isaindex{list}, the type of
99 lists, and \isaindex{set}, the type of sets. Type constructors are written
100 postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
101 natural numbers. Parentheses around single arguments can be dropped (as in
102 \isa{nat list}), multiple arguments are separated by commas (as in
104 \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
105 In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
106 \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
107 \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
108 supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
109 which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
111 \item[type variables,]\indexbold{type variable}\indexbold{variable!type}
112 denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
113 to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
117 Types are extremely important because they prevent us from writing
118 nonsense. Isabelle insists that all terms and formulae must be well-typed
119 and will print an error message if a type mismatch is encountered. To
120 reduce the amount of explicit type information that needs to be provided by
121 the user, Isabelle infers the type of all variables automatically (this is
122 called \bfindex{type inference}) and keeps quiet about it. Occasionally
123 this may lead to misunderstandings between you and the system. If anything
124 strange happens, we recommend to set the \rmindex{flag}
125 \isaindexbold{show_types} that tells Isabelle to display type information
126 that is usually suppressed: simply type
132 This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
133 which we introduce as we go along,
134 can be set and reset in the same manner.\indexbold{flag!(re)setting}
138 \textbf{Terms}\indexbold{term} are formed as in functional programming by
139 applying functions to arguments. If \isa{f} is a function of type
140 \isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
141 $\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
142 infix functions like \isa{+} and some basic constructs from functional
145 \item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
146 means what you think it means and requires that
147 $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
148 \item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}
149 is equivalent to $u$ where all occurrences of $x$ have been replaced by
151 \isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
152 by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
153 \item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
155 evaluates to $e@i$ if $e$ is of the form $c@i$.
158 Terms may also contain
159 \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
160 \isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
161 returns \isa{x+1}. Instead of
162 \isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
163 \isa{\isasymlambda{}x~y~z.~$t$}.
165 \textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
166 There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
167 the usual logical connectives (in decreasing order of priority):
168 \indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
169 \indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
170 all of which (except the unary \isasymnot) associate to the right. In
171 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
172 \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
173 \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
175 Equality is available in the form of the infix function
176 \isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a
177 \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
178 and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
179 \isa{bool}, \isa{=} acts as if-and-only-if. The formula
180 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
181 \isa{\isasymnot($t@1$ = $t@2$)}.
183 Quantifiers are written as
184 \isa{\isasymforall{}x.~$P$}\index{$HOL0All@\isasymforall|bold} and
185 \isa{\isasymexists{}x.~$P$}\index{$HOL0Ex@\isasymexists|bold}.
187 \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
188 means that there exists exactly one \isa{x} that satisfies \isa{$P$}.
189 Nested quantifications can be abbreviated:
190 \isa{\isasymforall{}x~y~z.~$P$} means
191 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
193 Despite type inference, it is sometimes necessary to attach explicit
194 \textbf{type constraints}\indexbold{type constraint} to a term. The syntax is
195 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
196 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
197 in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
198 \isa{(x < y)::nat}. The main reason for type constraints is overloading of
199 functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for
200 a full discussion of overloading and Table~\ref{tab:overloading} for the most
201 important overloaded function symbols.
204 In general, HOL's concrete syntax tries to follow the conventions of
205 functional programming and mathematics. Below we list the main rules that you
206 should be familiar with to avoid certain syntactic traps. A particular
207 problem for novices can be the priority of operators. If you are unsure, use
208 additional parentheses. In those cases where Isabelle echoes your
209 input, you can see which parentheses are dropped --- they were superfluous. If
210 you are unsure how to interpret Isabelle's output because you don't know
211 where the (dropped) parentheses go, set the \rmindex{flag}
212 \isaindexbold{show_brackets}:
214 ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
220 Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
222 Isabelle allows infix functions like \isa{+}. The prefix form of function
223 application binds more strongly than anything else and hence \isa{f~x + y}
224 means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
225 \item Remember that in HOL if-and-only-if is expressed using equality. But
226 equality has a high priority, as befitting a relation, while if-and-only-if
227 typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P =
228 P} means \isa{\isasymnot\isasymnot(P = P)} and not
229 \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
230 logical equivalence, enclose both operands in parentheses, as in \isa{(A
231 \isasymand~B) = (B \isasymand~A)}.
233 Constructs with an opening but without a closing delimiter bind very weakly
234 and should therefore be enclosed in parentheses if they appear in subterms, as
235 in \isa{(\isasymlambda{}x.~x) = f}. This includes \isaindex{if},
236 \isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
238 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
239 because \isa{x.x} is always read as a single qualified identifier that
240 refers to an item \isa{x} in theory \isa{x}. Write
241 \isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
242 \item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.
245 For the sake of readability the usual mathematical symbols are used throughout
246 the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
251 \label{sec:variables}
254 Isabelle distinguishes free and bound variables just as is customary. Bound
255 variables are automatically renamed to avoid clashes with free variables. In
256 addition, Isabelle has a third kind of variable, called a \bfindex{schematic
257 variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
258 with a \isa{?}. Logically, an unknown is a free variable. But it may be
259 instantiated by another term during the proof process. For example, the
260 mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
261 which means that Isabelle can instantiate it arbitrarily. This is in contrast
262 to ordinary variables, which remain fixed. The programming language Prolog
263 calls unknowns {\em logical\/} variables.
265 Most of the time you can and should ignore unknowns and work with ordinary
266 variables. Just don't be surprised that after you have finished the proof of
267 a theorem, Isabelle will turn your free variables into unknowns: it merely
268 indicates that Isabelle will automatically instantiate those unknowns
269 suitably when the theorem is used in some other proof.
270 Note that for readability we often drop the \isa{?}s when displaying a theorem.
272 If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential
273 quantifier, it needs to be followed by a space. Otherwise \isa{?x} is
274 interpreted as a schematic variable.
277 \section{Interaction and Interfaces}
279 Interaction with Isabelle can either occur at the shell level or through more
280 advanced interfaces. To keep the tutorial independent of the interface, we
281 have phrased the description of the interaction in a neutral language. For
282 example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
283 shell level, which is explained the first time the phrase is used. Other
284 interfaces perform the same act by cursor movements and/or mouse clicks.
285 Although shell-based interaction is quite feasible for the kind of proof
286 scripts currently presented in this tutorial, the recommended interface for
287 Isabelle/Isar is the Emacs-based \bfindex{Proof
288 General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
290 Some interfaces (including the shell level) offer special fonts with
291 mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
292 are shown in table~\ref{tab:ascii} in the appendix.
294 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}}
295 Commands may but need not be terminated by semicolons.
296 At the shell level it is advisable to use semicolons to enforce that a command
297 is executed immediately; otherwise Isabelle may wait for the next keyword
298 before it knows that the command is complete.
301 \section{Getting Started}
303 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
304 -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
305 starts the default logic, which usually is already \texttt{HOL}. This is
306 controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
307 System Manual} for more details.} This presents you with Isabelle's most
308 basic \textsc{ascii} interface. In addition you need to open an editor window to
309 create theory files. While you are developing a theory, we recommend to
310 type each command into the file first and then enter it into Isabelle by
311 copy-and-paste, thus ensuring that you have a complete record of your theory.
312 As mentioned above, Proof General offers a much superior interface.
313 If you have installed Proof General, you can start it by typing \texttt{Isabelle}.