\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 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~{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$ will

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}

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.

\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?}

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.

%FIXME cite [HahnBanach-in-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 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}

See \texttt{HOL/Isar_examples} for a collection of introductory examples, and

\texttt{HOL/HOL-Real/HahnBanach} for 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: