src/Doc/ProgProve/document/intro-isabelle.tex
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 54572 95a33ff3984b
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     1
Isabelle is a generic system for
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     2
implementing logical formalisms, and Isabelle/HOL is the specialization
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     3
of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     4
HOL step by step following the equation
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     5
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
52782
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
     6
We assume that the reader is used to logical and set theoretic notation
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
     7
and is familiar with the basic concepts of functional programming.
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
     8
\ifsem
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
     9
Open-minded readers have been known to pick up functional
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    10
programming through the wealth of examples in \autoref{sec:FP}
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    11
and \autoref{sec:CaseStudyExp}.
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    12
\fi
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
\autoref{sec:FP} introduces HOL as a functional programming language and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
explains how to write simple inductive proofs of mostly equational properties
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
of recursive functions.
52782
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    17
\ifsem
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
\autoref{sec:CaseStudyExp} contains a
54508
nipkow
parents: 54467
diff changeset
    19
small case study: arithmetic and boolean expressions, their evaluation,
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
optimization and compilation.
52782
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    21
\fi
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
\autoref{ch:Logic} introduces the rest of HOL: the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
language of formulas beyond equality, automatic proof tools, single
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
step proofs, and inductive definitions, an essential specification construct.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    25
\autoref{ch:Isar} introduces Isar, Isabelle's language for writing structured
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    26
proofs.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    27
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    28
%Further material (slides, demos etc) can be found online at
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
%\url{http://www.in.tum.de/~nipkow}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    31
% Relics:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
% We aim to minimise the amount of background knowledge of logic we expect
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
% from the reader
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    34
% We have focussed on the core material
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
% in the intersection of computation and logic.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    36
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    37
This introduction to the core of Isabelle is intentionally concrete and
54508
nipkow
parents: 54467
diff changeset
    38
example-based: we concentrate on examples that illustrate the typical cases
nipkow
parents: 54467
diff changeset
    39
without explaining the general case if it can be inferred from the examples.
52782
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    40
We cover the essentials (from a functional programming point of view) as
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    41
quickly and compactly as possible.
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    42
\ifsem
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    43
After all, this book is primarily about semantics.
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    44
\fi
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    45
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    46
For a comprehensive treatment of all things Isabelle we recommend the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    47
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    48
Isabelle distribution.
54508
nipkow
parents: 54467
diff changeset
    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.
47546
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    50
52782
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    51
%This introduction to Isabelle has grown out of many years of teaching
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    52
%Isabelle courses. 
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    53
52814
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    54
\ifsem
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    55
\subsection*{Getting Started with Isabelle}
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    56
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    57
If you have not done so already, download and install Isabelle
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    58
from \url{http://isabelle.in.tum.de}. You can start it by clicking
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    59
on the application icon. This will launch Isabelle's
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    60
user interface based on the text editor \concept{jedit}. Below you see
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    61
a typical example snapshot of a jedit session. At this point we merely explain
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    62
the layout of the window, not its contents.
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    63
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    64
\begin{center}
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    65
\includegraphics[width=\textwidth]{jedit.png}
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    66
\end{center}
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    67
The upper part of the window shows the input typed by the user, i.e.\ the
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    68
gradually growing Isabelle text of definitions, theorems, proofs, etc.  The
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    69
interface processes the user input automatically while it is typed, just like
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    70
modern Java IDEs.  Isabelle's response to the user input is shown in the
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    71
lower part of the window. You can examine the response to any input phrase
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    72
by clicking on that phrase or by hovering over underlined text.
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    73
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    74
This should suffice to get started with the jedit interface.
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    75
Now you need to learn what to type into it.
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    76
\else
52782
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    77
If you want to apply what you have learned about Isabelle we recommend you
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    78
donwload and read the book
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    79
\href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    80
Semantics}~\cite{ConcreteSemantics}, a guided tour of the wonderful world of
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    81
programming langage semantics formalised in Isabelle.  In fact,
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    82
\emph{Programming and Proving in Isabelle/HOL} constitutes part~I of
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    83
\href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete Semantics}.  The web
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    84
pages for \href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete Semantics}
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    85
also provide a set of \LaTeX-based slides for teaching \emph{Programming and
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    86
Proving in Isabelle/HOL}.
b11d73dbfb76 tuned intro
nipkow
parents: 48985
diff changeset
    87
\fi
47546
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    88
52814
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    89
\ifsem\else
47546
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    90
\paragraph{Acknowledgements}
54467
663a927fdc88 comments by Sean Seefried
nipkow
parents: 52814
diff changeset
    91
I wish to thank the following people for their comments on this document:
54572
nipkow
parents: 54508
diff changeset
    92
Florian Haftmann, Ren\'{e} Thiemann, Sean Seefried, Christian Sternagel
nipkow
parents: 54508
diff changeset
    93
and Carl Witty.
52814
ba5135f45f75 added Getting Started text
nipkow
parents: 52782
diff changeset
    94
\fi