doc-src/ProgProve/intro-isabelle.tex
author wenzelm
Tue, 22 May 2012 19:02:17 +0200
changeset 47885 b987aa8b9310
parent 47546 2d49b0c9d8ec
permissions -rw-r--r--
Added tag Isabelle2012 for changeset 21c42b095c84
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}. \]
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     6
We assume that the reader is familiar with the basic concepts of functional
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     7
programming and is used to logical and set theoretic notation.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     8
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     9
\autoref{sec:FP} introduces HOL as a functional programming language and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
explains how to write simple inductive proofs of mostly equational properties
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
of recursive functions.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
\sem
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
\autoref{sec:CaseStudyExp} contains a
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
little case study: arithmetic and boolean expressions, their evaluation,
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
optimization and compilation.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
\endsem
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
\autoref{ch:Logic} introduces the rest of HOL: the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
language of formulas beyond equality, automatic proof tools, single
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    19
step proofs, and inductive definitions, an essential specification construct.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
\autoref{ch:Isar} introduces Isar, Isabelle's language for writing structured
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
proofs.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
%Further material (slides, demos etc) can be found online at
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
%\url{http://www.in.tum.de/~nipkow}.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    25
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    26
% Relics:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    27
% 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
    28
% from the reader
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
% We have focussed on the core material
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
% in the intersection of computation and logic.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    31
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
This introduction to the core of Isabelle is intentionally concrete and
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
example-based: we concentrate on examples that illustrate the typical cases;
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    34
we do not explain the general case if it can be inferred from the examples.
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
For a comprehensive treatment of all things Isabelle we recommend the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    36
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    37
Isabelle distribution.
47546
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    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.
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    39
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    40
This introduction has grown out of many years of teaching Isabelle courses.
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    41
It tries to cover the essentials (from a functional programming point of
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    42
view) as quickly and compactly as possible. There is also an accompanying
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    43
set of \LaTeX-based slides available from the author on request.
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    44
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    45
\paragraph{Acknowledgements}
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    46
I wish to thank the following people for their comments on this text:
2d49b0c9d8ec tuned text, improved dependencies
nipkow
parents: 47269
diff changeset
    47
Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel.