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