|
47269
|
1 |
Isabelle is a generic system for
|
|
|
2 |
implementing logical formalisms, and Isabelle/HOL is the specialization
|
|
|
3 |
of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
|
|
|
4 |
HOL step by step following the equation
|
|
|
5 |
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
|
|
|
6 |
We assume that the reader is familiar with the basic concepts of functional
|
|
|
7 |
programming and is used to logical and set theoretic notation.
|
|
|
8 |
|
|
|
9 |
\autoref{sec:FP} introduces HOL as a functional programming language and
|
|
|
10 |
explains how to write simple inductive proofs of mostly equational properties
|
|
|
11 |
of recursive functions.
|
|
|
12 |
\sem
|
|
|
13 |
\autoref{sec:CaseStudyExp} contains a
|
|
|
14 |
little case study: arithmetic and boolean expressions, their evaluation,
|
|
|
15 |
optimization and compilation.
|
|
|
16 |
\endsem
|
|
|
17 |
\autoref{ch:Logic} introduces the rest of HOL: the
|
|
|
18 |
language of formulas beyond equality, automatic proof tools, single
|
|
|
19 |
step proofs, and inductive definitions, an essential specification construct.
|
|
|
20 |
\autoref{ch:Isar} introduces Isar, Isabelle's language for writing structured
|
|
|
21 |
proofs.
|
|
|
22 |
|
|
|
23 |
%Further material (slides, demos etc) can be found online at
|
|
|
24 |
%\url{http://www.in.tum.de/~nipkow}.
|
|
|
25 |
|
|
|
26 |
% Relics:
|
|
|
27 |
% We aim to minimise the amount of background knowledge of logic we expect
|
|
|
28 |
% from the reader
|
|
|
29 |
% We have focussed on the core material
|
|
|
30 |
% in the intersection of computation and logic.
|
|
|
31 |
|
|
|
32 |
This introduction to the core of Isabelle is intentionally concrete and
|
|
|
33 |
example-based: we concentrate on examples that illustrate the typical cases;
|
|
|
34 |
we do not explain the general case if it can be inferred from the examples.
|
|
|
35 |
For a comprehensive treatment of all things Isabelle we recommend the
|
|
|
36 |
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
|
|
|
37 |
Isabelle distribution.
|
|
47546
|
38 |
The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.
|
|
|
39 |
|
|
|
40 |
This introduction has grown out of many years of teaching Isabelle courses.
|
|
|
41 |
It tries to cover the essentials (from a functional programming point of
|
|
|
42 |
view) as quickly and compactly as possible. There is also an accompanying
|
|
|
43 |
set of \LaTeX-based slides available from the author on request.
|
|
|
44 |
|
|
|
45 |
\paragraph{Acknowledgements}
|
|
|
46 |
I wish to thank the following people for their comments on this text:
|
|
|
47 |
Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel. |