1 \chapter{Basic Concepts}
5 This is a tutorial on how to use Isabelle/HOL as a specification and
6 verification system. Isabelle is a generic system for implementing logical
7 formalisms, and Isabelle/HOL is the specialization of Isabelle for
8 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
11 We assume that the reader is familiar with the basic concepts of both fields.
12 For excellent introductions to functional programming consult the textbooks
13 by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{Paulson-ML}. Although
14 this tutorial initially concentrates on functional programming, do not be
15 misled: HOL can express most mathematical concepts, and functional
16 programming is just one particularly simple and ubiquitous instance.
18 A tutorial is by definition incomplete. To fully exploit the power of the
19 system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man}
20 for details about Isabelle and the HOL chapter of the Logics
21 manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a
24 \section{Theories, proofs and interaction}
25 \label{sec:Basic:Theories}
27 Working with Isabelle means creating two different kinds of documents:
28 theories and proof scripts. Roughly speaking, a \bfindex{theory} is a named
29 collection of types and functions, much like a module in a programming
30 language or a specification in a specification language. In fact, theories in
31 HOL can be either. Theories must reside in files with the suffix
32 \texttt{.thy}. The general format of a theory file \texttt{T.thy} is
34 T = B\(@1\) + \(\cdots\) + B\(@n\) +
35 \({<}declarations{>}\)
38 where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
39 theories that \texttt{T} is based on and ${<}declarations{>}$ stands for the
40 newly introduced concepts (types, functions etc). The \texttt{B}$@i$ are the
41 direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
42 Everything defined in the parent theories (and their parents \dots) is
43 automatically visible. To avoid name clashes, identifiers can be qualified by
44 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is
45 available online at \verb$http://www.in.tum.de/~isabelle/library/HOL/$ and is
48 HOL contains a theory \ttindexbold{Main}, the union of all the basic
49 predefined theories like arithmetic, lists, sets, etc.\ (see the online
50 library). Unless you know what you are doing, always include \texttt{Main}
51 as a direct or indirect parent theory of all your theories.
54 This tutorial is concerned with introducing you to the different linguistic
55 constructs that can fill ${<}declarations{>}$ in the above theory template.
56 A complete grammar of the basic constructs is found in Appendix~A
57 of~\cite{Isa-Ref-Man}, for reference in times of doubt.
59 The tutorial is also concerned with showing you how to prove theorems about
60 the concepts in a theory. This involves invoking predefined theorem proving
61 commands. Because Isabelle is written in the programming language
62 ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not
63 confuse the two levels.} interacting with Isabelle means calling ML
64 functions. Hence \bfindex{proof scripts} are sequences of calls to ML
65 functions that perform specific theorem proving tasks. Nevertheless,
66 familiarity with ML is absolutely not required. All proof scripts for theory
67 \texttt{T} (defined in file \texttt{T.thy}) should be contained in file
68 \texttt{T.ML}. Theory and proof scripts are loaded (and checked!) by calling
69 the ML function \ttindexbold{use_thy}:
74 There are more advanced interfaces for Isabelle that hide the ML level from
75 you and replace function calls by menu selection. There is even a special
76 font with mathematical symbols. For details see the Isabelle home page. This
77 tutorial concentrates on the bare essentials and ignores such niceties.
79 \section{Types, terms and formulae}
80 \label{sec:TypesTermsForms}
82 Embedded in the declarations of a theory are the types, terms and formulae of
83 HOL. HOL is a typed logic whose type system resembles that of functional
84 programming languages like ML or Haskell. Thus there are
86 \item[base types,] in particular \ttindex{bool}, the type of truth values,
87 and \ttindex{nat}, the type of natural numbers.
88 \item[type constructors,] in particular \ttindex{list}, the type of
89 lists, and \ttindex{set}, the type of sets. Type constructors are written
90 postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
91 natural numbers. Parentheses around single arguments can be dropped (as in
92 \texttt{nat list}), multiple arguments are separated by commas (as in
93 \texttt{(bool,nat)foo}).
94 \item[function types,] denoted by \ttindexbold{=>}. In HOL
95 \texttt{=>} represents {\em total} functions only. As is customary,
96 \texttt{$\tau@1$ => $\tau@2$ => $\tau@3$} means
97 \texttt{$\tau@1$ => ($\tau@2$ => $\tau@3$)}. Isabelle also supports the
98 notation \texttt{[$\tau@1,\dots,\tau@n$] => $\tau$} which abbreviates
99 \texttt{$\tau@1$ => $\cdots$ => $\tau@n$ => $\tau$}.
100 \item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
101 ML. They give rise to polymorphic types like \texttt{'a => 'a}, the type of the
105 Types are extremely important because they prevent us from writing
106 nonsense. Isabelle insists that all terms and formulae must be well-typed
107 and will print an error message if a type mismatch is encountered. To
108 reduce the amount of explicit type information that needs to be provided by
109 the user, Isabelle infers the type of all variables automatically (this is
110 called \bfindex{type inference}) and keeps quiet about it. Occasionally
111 this may lead to misunderstandings between you and the system. If anything
112 strange happens, we recommend to set the flag \ttindexbold{show_types} that
113 tells Isabelle to display type information that is usually suppressed:
120 at the ML-level. This can be reversed by \texttt{reset show_types;}.
124 \textbf{Terms}\indexbold{term}
125 are formed as in functional programming by applying functions to
126 arguments. If \texttt{f} is a function of type \texttt{$\tau@1$ => $\tau@2$}
127 and \texttt{t} is a term of type $\tau@1$ then \texttt{f~t} is a term of type
128 $\tau@2$. HOL also supports infix functions like \texttt{+} and some basic
129 constructs from functional programming:
131 \item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
132 means what you think it means and requires that
133 $b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
134 \item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
135 is equivalent to $u$ where all occurrences of $x$ have been replaced by
137 \texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
138 by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
139 \item[\texttt{case $e$ of $c@1$ => $e@1$ | \dots | $c@n$ => $e@n$}]
141 evaluates to $e@i$ if $e$ is of the form
142 $c@i$. See~\S\ref{sec:case-expressions} for details.
145 Terms may also contain $\lambda$-abstractions. For example, $\lambda
146 x. x+1$ is the function that takes an argument $x$ and returns $x+1$. In
147 Isabelle we write \texttt{\%x.~x+1}.\index{==>@{\tt\%}|bold}
148 Instead of \texttt{\%x.~\%y.~\%z.~t} we can write \texttt{\%x~y~z.~t}.
150 \textbf{Formulae}\indexbold{formula}
151 are terms of type \texttt{bool}. There are the basic
152 constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
153 connectives (in decreasing order of priority):
154 \verb$~$\index{$HOL1@{\ttnot}|bold} (`not'),
155 \texttt{\&}\index{$HOL2@{\tt\&}|bold} (`and'),
156 \texttt{|}\index{$HOL2@{\ttor}|bold} (`or') and
157 \texttt{-->}\index{$HOL2@{\tt-->}|bold} (`implies'),
158 all of which (except the unary \verb$~$) associate to the right. In
159 particular \texttt{A --> B --> C} means \texttt{A --> (B --> C)} and is thus
160 logically equivalent with \texttt{A \& B --> C}
161 (which is \texttt{(A \& B) --> C}).
163 Equality is available in the form of the infix function
164 \texttt{=} of type \texttt{'a => 'a => bool}. Thus \texttt{$t@1$ = $t@2$} is
165 a formula provided $t@1$ and $t@2$ are terms of the same type. In case $t@1$
166 and $t@2$ are of type \texttt{bool}, \texttt{=} acts as if-and-only-if.
168 The syntax for quantifiers is
169 \texttt{!~$x$.$\,P$}\index{$HOLQ@{\ttall}|bold} (`for all $x$') and
170 \texttt{?~$x$.$\,P$}\index{$HOLQ@{\tt?}|bold} (`exists $x$').
171 There is even \texttt{?!~$x$.$\,P$}\index{$HOLQ@{\ttuniquex}|bold}, which
172 means that there exists exactly one $x$ that satisfies $P$. Instead of
173 \texttt{!} and \texttt{?} you may also write \texttt{ALL} and \texttt{EX}.
174 Nested quantifications can be abbreviated:
175 \texttt{!$x~y~z$.$\,P$} means \texttt{!$x$.~!$y$.~!$z$.$\,P$}.
177 Despite type inference, it is sometimes necessary to attach explicit
178 \bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as
179 in \texttt{x < (y::nat)}. Note that \texttt{::} binds weakly and should
180 therefore be enclosed in parentheses: \texttt{x < y::nat} is ill-typed
181 because it is interpreted as \texttt{(x < y)::nat}. The main reason for type
182 constraints are overloaded functions like \texttt{+}, \texttt{*} and
183 \texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
187 In general, HOL's concrete syntax tries to follow the conventions of
188 functional programming and mathematics. Below we list the main rules that you
189 should be familiar with to avoid certain syntactic traps. A particular
190 problem for novices can be the priority of operators. If you are unsure, use
191 more rather than fewer parentheses. In those cases where Isabelle echoes your
192 input, you can see which parentheses are dropped---they were superfluous. If
193 you are unsure how to interpret Isabelle's output because you don't know
194 where the (dropped) parentheses go, set (and possibly reset) the flag
195 \ttindexbold{show_brackets}:
197 set show_brackets; \(\dots\); reset show_brackets;
203 Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
205 Isabelle allows infix functions like \texttt{+}. The prefix form of function
206 application binds more strongly than anything else and hence \texttt{f~x + y}
207 means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
209 Remember that in HOL if-and-only-if is expressed using equality. But equality
210 has a high priority, as befitting a relation, while if-and-only-if typically
211 has the lowest priority. Thus, \verb$~ ~ P = P$ means \verb$~ ~(P = P)$ and
212 not \verb$(~ ~P) = P$. When using \texttt{=} to mean logical equivalence,
213 enclose both operands in parentheses, as in \texttt{(A \& B) = (B \& A)}.
215 Constructs with an opening but without a closing delimiter bind very weakly
216 and should therefore be enclosed in parentheses if they appear in subterms, as
217 in \texttt{f = (\%x.~x)}. This includes
218 \ttindex{if}, \ttindex{let}, \ttindex{case}, \verb$%$ and quantifiers.
220 Never write \texttt{\%x.x} or \texttt{!x.x=x} because \texttt{x.x} is always
221 read as a single qualified identifier that refers to an item \texttt{x} in
222 theory \texttt{x}. Write \texttt{\%x.~x} and \texttt{!x.~x=x} instead.
226 \label{sec:variables}
228 Isabelle distinguishes free and bound variables just as is customary. Bound
229 variables are automatically renamed to avoid clashes with free variables. In
230 addition, Isabelle has a third kind of variable, called a \bfindex{schematic
231 variable} or \bfindex{unknown}, which starts with a \texttt{?}. Logically,
232 an unknown is a free variable. But it may be instantiated by another term
233 during the proof process. For example, the mathematical theorem $x = x$ is
234 represented in Isabelle as \texttt{?x = ?x}, which means that Isabelle can
235 instantiate it arbitrarily. This is in contrast to ordinary variables, which
236 remain fixed. The programming language Prolog calls unknowns {\em logical\/}
239 Most of the time you can and should ignore unknowns and work with ordinary
240 variables. Just don't be surprised that after you have finished the
241 proof of a theorem, Isabelle will turn your free variables into unknowns: it
242 merely indicates that Isabelle will automatically instantiate those unknowns
243 suitably when the theorem is used in some other proof.
245 The existential quantifier \texttt{?}\index{$HOLQ@{\tt?}} needs to be
246 followed by a space. Otherwise \texttt{?x} is interpreted as a schematic
250 \section{Getting started}
252 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
253 HOL} in a shell window.\footnote{Since you will always want to use HOL when
254 studying this tutorial, you can set the shell variable
255 \texttt{ISABELLE_LOGIC} to \texttt{HOL} once and for all and simply execute
256 \texttt{isabelle}.} This presents you with Isabelle's most basic ASCII
257 interface. In addition you need to open an editor window to create theories
258 (\texttt{.thy} files) and proof scripts (\texttt{.ML} files). While you are
259 developing a proof, we recommend to type each proof command into the ML-file
260 first and then enter it into Isabelle by copy-and-paste, thus ensuring that
261 you have a complete record of your proof.