nipkow@47269

1 
Isabelle is a generic system for

nipkow@47269

2 
implementing logical formalisms, and Isabelle/HOL is the specialization

nipkow@47269

3 
of Isabelle for HOL, which abbreviates HigherOrder Logic. We introduce

nipkow@47269

4 
HOL step by step following the equation

nipkow@47269

5 
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]

nipkow@56989

6 
We assume that the reader is used to logical and settheoretic notation

nipkow@52782

7 
and is familiar with the basic concepts of functional programming.

nipkow@52782

8 
\ifsem

nipkow@52782

9 
Openminded readers have been known to pick up functional

nipkow@52782

10 
programming through the wealth of examples in \autoref{sec:FP}

nipkow@52782

11 
and \autoref{sec:CaseStudyExp}.

nipkow@52782

12 
\fi

nipkow@47269

13 

nipkow@47269

14 
\autoref{sec:FP} introduces HOL as a functional programming language and

nipkow@47269

15 
explains how to write simple inductive proofs of mostly equational properties

nipkow@47269

16 
of recursive functions.

nipkow@52782

17 
\ifsem

nipkow@47269

18 
\autoref{sec:CaseStudyExp} contains a

nipkow@54508

19 
small case study: arithmetic and boolean expressions, their evaluation,

nipkow@47269

20 
optimization and compilation.

nipkow@52782

21 
\fi

nipkow@47269

22 
\autoref{ch:Logic} introduces the rest of HOL: the

nipkow@56989

23 
language of formulas beyond equality, automatic proof tools, singlestep

nipkow@56989

24 
proofs, and inductive definitions, an essential specification construct.

nipkow@47269

25 
\autoref{ch:Isar} introduces Isar, Isabelle's language for writing structured

nipkow@47269

26 
proofs.

nipkow@47269

27 

nipkow@47269

28 
%Further material (slides, demos etc) can be found online at

nipkow@47269

29 
%\url{http://www.in.tum.de/~nipkow}.

nipkow@47269

30 

nipkow@47269

31 
% Relics:

nipkow@47269

32 
% We aim to minimise the amount of background knowledge of logic we expect

nipkow@47269

33 
% from the reader

nipkow@47269

34 
% We have focussed on the core material

nipkow@47269

35 
% in the intersection of computation and logic.

nipkow@47269

36 

nipkow@47269

37 
This introduction to the core of Isabelle is intentionally concrete and

nipkow@54508

38 
examplebased: we concentrate on examples that illustrate the typical cases

nipkow@54508

39 
without explaining the general case if it can be inferred from the examples.

nipkow@52782

40 
We cover the essentials (from a functional programming point of view) as

nipkow@52782

41 
quickly and compactly as possible.

nipkow@52782

42 
\ifsem

nipkow@52782

43 
After all, this book is primarily about semantics.

nipkow@52782

44 
\fi

nipkow@52782

45 

nipkow@47269

46 
For a comprehensive treatment of all things Isabelle we recommend the

nipkow@47269

47 
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the

nipkow@47269

48 
Isabelle distribution.

nipkow@54508

49 
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 does not cover the structured proof language Isar.

nipkow@47546

50 

nipkow@52782

51 
%This introduction to Isabelle has grown out of many years of teaching

nipkow@52782

52 
%Isabelle courses.

nipkow@52782

53 

nipkow@52814

54 
\ifsem

nipkow@52814

55 
\subsection*{Getting Started with Isabelle}

nipkow@52814

56 

nipkow@52814

57 
If you have not done so already, download and install Isabelle

nipkow@52814

58 
from \url{http://isabelle.in.tum.de}. You can start it by clicking

nipkow@52814

59 
on the application icon. This will launch Isabelle's

nipkow@52814

60 
user interface based on the text editor \concept{jedit}. Below you see

nipkow@52814

61 
a typical example snapshot of a jedit session. At this point we merely explain

nipkow@52814

62 
the layout of the window, not its contents.

nipkow@52814

63 

nipkow@52814

64 
\begin{center}

nipkow@52814

65 
\includegraphics[width=\textwidth]{jedit.png}

nipkow@52814

66 
\end{center}

nipkow@52814

67 
The upper part of the window shows the input typed by the user, i.e.\ the

nipkow@52814

68 
gradually growing Isabelle text of definitions, theorems, proofs, etc. The

nipkow@52814

69 
interface processes the user input automatically while it is typed, just like

nipkow@52814

70 
modern Java IDEs. Isabelle's response to the user input is shown in the

nipkow@52814

71 
lower part of the window. You can examine the response to any input phrase

nipkow@52814

72 
by clicking on that phrase or by hovering over underlined text.

nipkow@52814

73 

nipkow@52814

74 
This should suffice to get started with the jedit interface.

nipkow@52814

75 
Now you need to learn what to type into it.

nipkow@52814

76 
\else

nipkow@52782

77 
If you want to apply what you have learned about Isabelle we recommend you

nipkow@52782

78 
donwload and read the book

wenzelm@57847

79 
\href{http://www.concretesemantics.org}{Concrete

nipkow@52782

80 
Semantics}~\cite{ConcreteSemantics}, a guided tour of the wonderful world of

nipkow@52782

81 
programming langage semantics formalised in Isabelle. In fact,

nipkow@52782

82 
\emph{Programming and Proving in Isabelle/HOL} constitutes part~I of

wenzelm@57847

83 
\href{http://www.concretesemantics.org}{Concrete Semantics}. The web

wenzelm@57847

84 
pages for \href{http://www.concretesemantics.org}{Concrete Semantics}

nipkow@57819

85 
also provide a set of \LaTeXbased slides and Isabelle demo files

nipkow@57819

86 
for teaching \emph{Programming and Proving in Isabelle/HOL}.

nipkow@52782

87 
\fi

nipkow@47546

88 

nipkow@52814

89 
\ifsem\else

nipkow@47546

90 
\paragraph{Acknowledgements}

nipkow@54467

91 
I wish to thank the following people for their comments on this document:

nipkow@57819

92 
Florian Haftmann, Peter Johnson, Ren\'{e} Thiemann, Sean Seefried,

nipkow@57819

93 
Christian Sternagel and Carl Witty.

nipkow@52814

94 
\fi 