src/Doc/Prog_Prove/document/intro-isabelle.tex

tuned

Isabelle is a generic system for
implementing logical formalisms, and Isabelle/HOL is the specialization
of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
HOL step by step following the equation
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
We assume that the reader is used to logical and set-theoretic notation
and is familiar with the basic concepts of functional programming.
\ifsem
Open-minded readers have been known to pick up functional
programming through the wealth of examples in \autoref{sec:FP}
and \autoref{sec:CaseStudyExp}.
\fi

\autoref{sec:FP} introduces HOL as a functional programming language and
explains how to write simple inductive proofs of mostly equational properties
of recursive functions.
\ifsem
\autoref{sec:CaseStudyExp} contains a
small case study: arithmetic and boolean expressions, their evaluation,
optimization and compilation.
\fi
\autoref{ch:Logic} introduces the rest of HOL: the
language of formulas beyond equality, automatic proof tools, single-step
proofs, and inductive definitions, an essential specification construct.
\autoref{ch:Isar} introduces Isar, Isabelle's language for writing structured
proofs.

%Further material (slides, demos etc) can be found online at
%\url{http://www.in.tum.de/~nipkow}.

% Relics:
% We aim to minimise the amount of background knowledge of logic we expect
% from the reader
% We have focussed on the core material
% in the intersection of computation and logic.

This introduction to the core of Isabelle is intentionally concrete and
example-based: we concentrate on examples that illustrate the typical cases
without explaining the general case if it can be inferred from the examples.
We cover the essentials (from a functional programming point of view) as
quickly and compactly as possible.
\ifsem
After all, this book is primarily about semantics.
\fi

For a comprehensive treatment of all things Isabelle we recommend the
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
Isabelle distribution.
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.

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

\ifsem
\subsection*{Getting Started with Isabelle}

If you have not done so already, download and install Isabelle
(this book is compatible with Isabelle2018)
from \url{https://isabelle.in.tum.de}. You can start it by clicking
on the application icon. This will launch Isabelle's
user interface based on the text editor \concept{jEdit}. Below you see
a typical example snapshot of a session. At this point we merely explain
the layout of the window, not its contents.

\begin{center}
\includegraphics[width=\textwidth]{jedit.png}
\end{center}
The upper part of the window shows the input typed by the user, i.e., the
gradually growing Isabelle text of definitions, theorems, proofs, etc.  The
interface processes the user input automatically while it is typed, just like
modern Java IDEs.  Isabelle's response to the user input is shown in the
lower part of the window. You can examine the response to any input phrase
by clicking on that phrase or by hovering over underlined text.

\begin{warn}\label{proof-state}
Part I frequently refers to the proof state.
You can see the proof state if you press the ``State'' button.
If you want to see the proof state combined with other system output, press ``Output'' and tick the ``Proof state'' box.
\end{warn}

This should suffice to get started with the jEdit interface.
Now you need to learn what to type into it.
\else
If you want to apply what you have learned about Isabelle we recommend you
download and read the book
\href{http://www.concrete-semantics.org}{Concrete
Semantics}~\cite{ConcreteSemantics}, a guided tour of the wonderful world of
programming langage semantics formalised in Isabelle.  In fact,
\emph{Programming and Proving in Isabelle/HOL} constitutes part~I of
\href{http://www.concrete-semantics.org}{Concrete Semantics}.  The web
pages for \href{http://www.concrete-semantics.org}{Concrete Semantics}
also provide a set of \LaTeX-based slides and Isabelle demo files
for teaching \emph{Programming and Proving in Isabelle/HOL}.
\fi

\ifsem\else
\paragraph{Acknowledgements}
I wish to thank the following people for their comments on this document:
Florian Haftmann, Peter Johnson, Ren\'{e} Thiemann, Sean Seefried,
Christian Sternagel and Carl Witty.
\fi