doc-src/IsarRef/intro.tex

tuned;
some more stuff;

\chapter{Introduction}

\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 Isar
interaction loop at startup, rather than the plain ML top-level.  Thus the
quickest way to do anything with Isabelle/Isar is as follows:
\begin{ttbox}
isabelle -I HOL\medskip
\out{> Welcome to Isabelle/HOL (Isabelle99)}\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}; the
\texttt{help} command prints a list of available language elements.


\subsection{The Proof~General interface}

Plain TTY-based interaction as above used to be quite feasible with
traditional tactic based theorem proving, but developing Isar documents
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-based 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 real production work.

\medskip

The easiest way to use Proof~General is to make it the default Isabelle user
interface (see also \cite{isabelle-sys}).  Just put something like this into
your Isabelle settings file:
\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.  From now on, the capital
\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
interface.\footnote{There is also a \texttt{ProofGeneral/isa} interface, for
  classic Isabelle tactic scripts.}

%FIXME remove?
%Its usage is as follows:
%\begin{ttbox}
%Usage: interface [OPTIONS] [FILES ...]
%
%  Options are:
%    -l NAME      logic image name (default $ISABELLE_LOGIC=HOL)
%    -p NAME      Emacs program name (default xemacs)
%    -u BOOL      use .emacs file (default true)
%    -w BOOL      use window system (default true)
%    -x BOOL      enable x-symbol package
%  Starts Proof General for Isabelle/Isar with proof documents FILES
%  (default Scratch.thy).
%
%  PROOFGENERAL_OPTIONS=
%\end{ttbox} %$

The interface script provides several options (pass ``\texttt{-?}'' to see its
usage).  Apart from the command line, the defaults for these options may be
overridden via the \texttt{PROOFGENERAL_OPTIONS} setting as well.  For
example, plain GNU Emacs instead of XEmacs (which is the default) may be
configured in Isabelle's settings via \texttt{PROOFGENERAL_OPTIONS="-p
  emacs"}.

Occasionally, a user's \texttt{.emacs} file contains material that is
incompatible with the version of (X)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 \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.

\medskip

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,Aspinall:TACAS:2000} for further basic command sequences,
such as ``\texttt{c-c return}'' or ``\texttt{c-c u}''.

\medskip

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
already must have been properly installed.


\section{Isabelle/Isar theories}

Isabelle/Isar offers two 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.
\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 the HOL $\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 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}

Porting 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.


\section{How to write Isar proofs anyway?}

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} for further background information
on Isar.

\medskip This really is a \emph{reference manual}.  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.  There are several examples distributed with
Isabelle, and available via the Isabelle WWW library:
\begin{center}\small
  \begin{tabular}{l}
    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
    \url{http://isabelle.in.tum.de/library/} \\
    \url{http://isabelle.in.tum.de/Isar/} \\
  \end{tabular}
\end{center}

See \texttt{HOL/Isar_examples} for a collection of introductory examples, and
\texttt{HOL/HOL-Real/HahnBanach} is a big mathematics application.  Apart from
plain HTML sources, these sessions also provide actual documents (in PDF).

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