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;
     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 used to logical and set-theoretic notation

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

     8 \ifsem

     9 Open-minded readers have been known to pick up functional

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

    11 and \autoref{sec:CaseStudyExp}.

    12 \fi

    13

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

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

    16 of recursive functions.

    17 \ifsem

    18 \autoref{sec:CaseStudyExp} contains a

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

    20 optimization and compilation.

    21 \fi

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

    23 language of formulas beyond equality, automatic proof tools, single-step

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

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

    26 proofs.

    27

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

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

    30

    31 % Relics:

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

    33 % from the reader

    34 % We have focussed on the core material

    35 % in the intersection of computation and logic.

    36

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

    38 example-based: we concentrate on examples that illustrate the typical cases

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

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

    41 quickly and compactly as possible.

    42 \ifsem

    43 After all, this book is primarily about semantics.

    44 \fi

    45

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

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

    48 Isabelle distribution.

    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.

    50

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

    52 %Isabelle courses.

    53

    54 \ifsem

    55 \subsection*{Getting Started with Isabelle}

    56

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

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

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

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

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

    62 the layout of the window, not its contents.

    63

    64 \begin{center}

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

    66 \end{center}

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

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

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

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

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

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

    73

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

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

    76 \else

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

    78 donwload and read the book

    79 \href{http://www.concrete-semantics.org}{Concrete

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

    81 programming langage semantics formalised in Isabelle.  In fact,

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

    83 \href{http://www.concrete-semantics.org}{Concrete Semantics}.  The web

    84 pages for \href{http://www.concrete-semantics.org}{Concrete Semantics}

    85 also provide a set of \LaTeX-based slides and Isabelle demo files

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

    87 \fi

    88

    89 \ifsem\else

    90 \paragraph{Acknowledgements}

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

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

    93 Christian Sternagel and Carl Witty.

    94 \fi