doc-src/IsarRef/intro.tex

first stage of major update;

\chapter{Introduction}

\section{Overview}

The \emph{Isabelle} system essentially provides a generic infrastructure for
building deductive systems (programmed in Standard ML), with a special focus
on interactive theorem proving in higher-order logics.  In the olden days even
end-users would refer to certain ML functions (goal commands, tactics,
tacticals etc.) to pursue their everyday theorem proving needs
\cite{isabelle-intro,isabelle-ref}.
  
In contrast \emph{Isar} provides an interpreted language environment of its
own, which has been specifically tailored for the needs of theory and proof
development.  Compared to raw ML, the Isabelle/Isar top-level provides a more
robust and comfortable development platform, with proper support for theory
development graphs, single-step evaluation with unlimited undo, etc.  The
Isabelle/Isar version of the \emph{Proof~General} user interface
\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
interactive theory and proof development.

\medskip Apart from these technical advances over bare-bones ML programming,
the main intention of Isar is to provide a conceptually different view on
machine-checked proofs \cite{Wenzel:1999:TPHOL, Wenzel-PhD} --- ``Isar''
stands for ``Intelligible semi-automated reasoning''.  Drawing from both the
traditions of informal mathematical proof texts and high-level programming
languages, Isar provides a versatile environment for structured formal proof
documents.  Thus properly written Isar proof texts become accessible to a
broader audience than unstructured tactic scripts (which typically only
provide operational information for the machine).  Writing human-readable
proof texts certainly requires some additional efforts by the writer in order
to achieve a good presentation --- both of formal and informal parts of the
text.  On the other hand, human-readable formal texts gain some value in their
own right, independently of the mechanic proof-checking process.

Despite its grand design of structured proof texts, Isar is able to assimilate
the old-style tactical as an ``improper'' sub-language.  This provides an easy
upgrade path for existing tactic scripts, as well as additional means for
experimentation and debugging of interactive proofs.  Isabelle/Isar freely
supports a broad range of proof styles, including unreadable ones.

\medskip The Isabelle/Isar framework generic and should work for reasonably
well for any object-logic that directly conforms to the view of natural
deduction according to the Isabelle/Pure framework.  Major Isabelle logics
(HOL \cite{isabelle-HOL}, HOLCF, FOL \cite{isabelle-logics}, ZF
\cite{isabelle-ZF}) have already been setup for immediate use by end-users.

Note that much of the existing body of theories still consist of old-style
theory files with accompanied ML code for proof scripts.  This legacy will be
converted as time goes by.


\section{Quick start}

\subsection{Terminal sessions}

Isar is already part of Isabelle (as of version Isabelle99, or later).  The
\texttt{isabelle} binary provides option \texttt{-I} to run the Isabelle/Isar
interaction loop at startup, rather than the raw ML top-level.  So the
quickest way to do anything with Isabelle/Isar is as follows:
\begin{ttbox}
isabelle -I HOL\medskip
\out{> Welcome to Isabelle/HOL (Isabelle99-1)}\medskip
theory Foo = Main:
constdefs foo :: nat  "foo == 1";
lemma "0 < foo" by (simp add: foo_def);
end
\end{ttbox}
Note that any Isabelle/Isar command may be retracted by \texttt{undo}.  See
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
comprehensive overview of available commands and other language elements.


\subsection{Proof~General}

Plain TTY-based interaction as above used to be quite feasible with
traditional tactic based theorem proving, but developing Isar documents really
demands some better user-interface support.  David Aspinall's
\emph{Proof~General}\index{Proof General} environment
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for
interactive theorem provers that does all the cut-and-paste and
forward-backward walk through the text in a very neat way.  In Isabelle/Isar,
the current position within a partial proof document is equally important than
the actual proof state.  Thus Proof~General provides the canonical working
environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
existing Isar documents) and for production work.


\subsubsection{Proof~General as default Isabelle interface}

The easiest way to invoke Proof~General is via the Isabelle interface wrapper
script.  The default configuration of Isabelle is smart enough to detect the
Proof~General distribution in several canonical places (e.g.\ 
\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}).  Thus the capital
\texttt{Isabelle} executable would already refer to the
\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
  also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
  ML.} The Isabelle interface script provides several options, just pass
\verb,-?, to see its usage.

With the proper Isabelle interface setup, Isar documents may now be edited by
visiting appropriate theory files, e.g.\ 
\begin{ttbox}
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
\end{ttbox}
Users of XEmacs may note the tool bar for navigating forward and backward
through the text.  Consult the Proof~General documentation \cite{proofgeneral}
for further basic command sequences, such as ``\texttt{C-c C-return}'' or
``\texttt{C-c u}''.

\medskip

Proof~General may be also configured manually by giving Isabelle settings like
this (see also \cite{isabelle-sys}):
\begin{ttbox}
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
PROOFGENERAL_OPTIONS=""
\end{ttbox}
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
actual installation directory of Proof~General.

\medskip

Apart from the Isabelle command line, defaults for interface options may be
given by the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For example, the
Emacs executable to be used may be configured in Isabelle's settings like this:
\begin{ttbox}
PROOFGENERAL_OPTIONS="-p xemacs-nomule"  
\end{ttbox}

Occasionally, the user's \verb,~/.emacs, file contains material that is
incompatible with the version of Emacs that Proof~General prefers.  Then
proper startup may be still achieved by using the \texttt{-u false} option.
Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
is automatically loaded by the Proof~General interface script as well.


\subsubsection{The X-Symbol package}

Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
provides a nice way to get proper mathematical symbols displayed on screen.
Just pass option \texttt{-x true} to the Isabelle interface script, or check
the appropriate menu setting by hand.  In any case, the X-Symbol package must
have been properly installed already.

Contrary to what you may expect from the documentation of X-Symbol, the
package is very easy to install and configures itself automatically.  The
default configuration of Isabelle is smart enough to detect the X-Symbol
package in several canonical places (e.g.\ 
\texttt{\$ISABELLE_HOME/contrib/x-symbol}).

\medskip

Using proper mathematical symbols in Isabelle theories can be very convenient
for readability of large formulas.  On the other hand, the plain ASCII sources
easily become somewhat unintelligible.  For example, $\Longrightarrow$ would
appear as \verb,\<Longrightarrow>, according the default set of Isabelle
symbols.  Nevertheless, the Isabelle document preparation system (see
\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
It is even possible to invent additional notation beyond the display
capabilities of XEmacs and X-Symbol.


\section{Isabelle/Isar theories}

Isabelle/Isar offers the following main improvements over classic Isabelle.
\begin{enumerate}
\item A new \emph{theory format}, occasionally referred to as ``new-style
  theories'', supporting interactive development and unlimited undo operation.
\item A \emph{formal proof document language} designed to support intelligible
  semi-automated reasoning.  Instead of putting together unreadable tactic
  scripts, the author is enabled to express the reasoning in way that is close
  to usual mathematical practice.
\item A simple document preparation system, for typesetting formal
  developments together with informal text.  The resulting hyper-linked PDF
  documents are equally well suited for WWW presentation and as printed
  copies.
\end{enumerate}

The Isar proof language is embedded into the new theory format as a proper
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
$\LEMMANAME$ at the theory level, and left again with the final conclusion
(e.g.\ via $\QEDNAME$).  A few theory extension mechanisms require proof as
well, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness of the
representing sets.

New-style theory files may still be associated with separate ML files
consisting of plain old tactic scripts.  There is no longer any ML binding
generated for the theory and theorems, though.  ML functions \texttt{theory},
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
relatively easy.  Thus users may start to benefit from interactive theory
development and document preparation, even before they have any idea of the
Isar proof language at all.

\begin{warn}
  Currently, Proof~General does \emph{not} support mixed interactive
  development of classic Isabelle theory files or tactic scripts, together
  with Isar documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
  Proof~General are handled as two different theorem proving systems, only one
  of these may be active at the same time.
\end{warn}

Conversion of existing tactic scripts is best done by running two separate
Proof~General sessions, one for replaying the old script and the other for the
emerging Isabelle/Isar document.  Also note that Isar supports emulation
commands and methods that support traditional tactic scripts within new-style
theories, see appendix~\ref{ap:conv} for more information.


\subsection{Document preparation}\label{sec:document-prep}

Isabelle/Isar provides a simple document preparation system based on current
(PDF) {\LaTeX} technology, with full support of hyper-links (both local
references and URLs), bookmarks, thumbnails etc.  Thus the results are equally
well suited for WWW browsing and as printed copies.

\medskip

Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
  session} (see also \cite{isabelle-sys}).  Getting started with a working
configuration for common situations is quite easy by using the Isabelle
\texttt{mkdir} and \texttt{make} tools.  Just invoke
\begin{ttbox}
  isatool mkdir -d Foo
\end{ttbox}
to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
  experiment, since \texttt{isatool mkdir} never overwrites existing files.}
Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
macro packages required for your document (the default is usually sufficient
as a start).

The session is controlled by a separate \texttt{IsaMakefile} (with very crude
source dependencies only by default).  This file is located one level up from
the \texttt{Foo} directory location.  At that point just invoke
\begin{ttbox}
  isatool make Foo
\end{ttbox}
to run the \texttt{Foo} session, with browser information and document
preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},
the output will appear inside the directory indicated by \texttt{isatool
  getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\ 
\texttt{HOL/Foo}).  Note that the \texttt{index.html} located there provides a
link to the finished {\LaTeX} document, too.

Note that this really is batch processing --- better let Isabelle check your
theory and proof developments beforehand in interactive mode.

\medskip

You may also consider to tune the \texttt{usedir} options in
\texttt{IsaMakefile}, for example to change the output format from
\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
order to preserve a copy of the generated {\LaTeX} sources.  The latter
feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
runs of Isabelle.

\medskip

See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
on Isabelle logic sessions and theory presentation.


\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}

This is one of the key questions, of course.  Isar offers a rather different
approach to formal proof documents than plain old tactic scripts.  Experienced
users of existing interactive theorem proving systems may have to learn
thinking differently in order to make effective use of Isabelle/Isar.  On the
other hand, Isabelle/Isar comes much closer to existing mathematical practice
of formal proof, so users with less experience in old-style tactical proving,
but a good understanding of mathematical proof, might cope with Isar even
better.  See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further
background information on Isar.

\medskip This really is a reference manual on Isabelle/Isar, not a tutorial.
Nevertheless, we will also give some clues of how the concepts introduced here
may be put into practice.  Appendix~\ref{ap:refcard} provides a quick
reference card of the most common Isabelle/Isar language elements.
Appendix~\ref{ap:conv} offers some practical hints on converting existing
Isabelle theories and proof scripts to the new format.

Several example applications are distributed with Isabelle, and available via
the Isabelle WWW library as well as the Isabelle/Isar page:
\begin{center}\small
  \begin{tabular}{l}
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
    \url{http://isabelle.in.tum.de/library/} \\[1ex]
    \url{http://isabelle.in.tum.de/Isar/} \\
  \end{tabular}
\end{center}

The following examples may be of particular interest.  Apart from the plain
sources represented in HTML, these Isabelle sessions also provide actual
documents (in PDF).
\begin{itemize}
\item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
  collection of introductory examples.
\item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
  typical mathematics-style reasoning in ``axiomatic'' structures.
\item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
  big mathematics application on infinitary vector spaces and functional
  analysis.
\item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
  properties of $\lambda$-calculus (Church-Rosser and termination).
  
  This may serve as a realistic example of porting of legacy proof scripts
  into Isar tactic emulation scripts.
\item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
  model of the main aspects of the Unix file-system including its security
  model, but ignoring processes.  A few odd effects caused by the general
  ``worse-is-better'' approach followed in Unix are discussed within the
  formal model.
  
  This example represents a non-trivial verification task, with all proofs
  carefully worked out using the proper part of the Isar proof language;
  unstructured scripts are only used for symbolic evaluation.
\item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
  formalization of a fragment of Java, together with a corresponding virtual
  machine and a specification of its bytecode verifier and a lightweight
  bytecode verifier, including proofs of type-safety.
  
  This represents a very ``realistic'' example of large formalizations
  performed in form of tactic emulation scripts and proper Isar proof texts.
\end{itemize}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "isar-ref"
%%% End: