\chapter{Introduction}

\section{Quick start}

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

Plain TTY-based interaction like this used to be quite feasible with

traditional tactic based theorem proving, but developing Isar documents

demands some better user-interface support.  \emph{Proof~General}\index{Proof

  General} of LFCS Edinburgh \cite{proofgeneral} offers a generic Emacs-based

environment for interactive theorem provers that does all the cut-and-paste

and forward-backward walk through the document in a very neat way.  Note that

in Isabelle/Isar, the current position within a partial proof document is more

informative 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 serious production work.

\medskip

The easiest way to use Proof~General is to make it the default Isabelle user

interface.  Just say something like this in your Isabelle settings file (cf.\ 

\cite{isabelle-sys}):

\begin{ttbox}

ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface

PROOFGENERAL_OPTIONS="-u false"

\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.  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)

  Starts Proof General for Isabelle/Isar with proof documents FILES

  (default Scratch.thy).

  PROOFGENERAL_OPTIONS=

\end{ttbox} %$

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 may be configured as follows:

\begin{ttbox}

PROOFGENERAL_OPTIONS="-p emacs"

\end{ttbox}

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 commands, like \texttt{c-c return} or \texttt{c-c u}.

\medskip

Occasionally, a user's \texttt{.emacs} 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.\footnote{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.}

\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 different 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.

This document really is a \emph{reference manual}.  Nevertheless, we will give

some discussions of the general principles underlying Isar in

chapter~\ref{ch:basics}, and provide some clues of how these may be put into

practice.  Some more background information on Isar is given in

\cite{Wenzel:1999:TPHOL}.  While there is no proper tutorial on Isabelle/Isar

available yet, there are several examples distributed with Isabelle.  See

\texttt{HOL/Isar_examples} and \texttt{HOL/HOL-Real/HahnBanach} in the

Isabelle 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/} \\

  \end{tabular}

\end{center}

Apart from browsable HTML sources, both example sessions also provide actual

documents.

%%% Local Variables: 

%%% mode: latex

%%% TeX-master: "isar-ref"

%%% End: