src/Doc/Prog_Prove/document/intro-isabelle.tex
author wenzelm
Sun Aug 10 14:34:43 2014 +0200 (2014-08-10)
changeset 57882 38bf4de248a6
parent 57881 37920df63ab9
parent 57847 85b8cc142384
child 58483 d5f24630c104
permissions -rw-r--r--
merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
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 Higher-Order 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 set-theoretic notation
nipkow@52782
     7
and is familiar with the basic concepts of functional programming.
nipkow@52782
     8
\ifsem
nipkow@52782
     9
Open-minded 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, single-step
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
example-based: 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.concrete-semantics.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.concrete-semantics.org}{Concrete Semantics}.  The web
wenzelm@57847
    84
pages for \href{http://www.concrete-semantics.org}{Concrete Semantics}
nipkow@57819
    85
also provide a set of \LaTeX-based 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