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

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{ProofGeneral}\index{ProofGeneral} 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

the ProofGeneral/isar interface 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 ProofGeneral/isar 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=""

\end{ttbox}

You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the

actual installation directory of ProofGeneral.  Now the capital

\texttt{Isabelle} binary refers to the ProofGeneral/isar interface.  It's

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 false)

  -w BOOL      use window system (default true)

Starts ProofGeneral for Isabelle/Isar with proof documents FILES

(default Scratch.thy).

\end{ttbox}

The defaults for these options may be changed via the

\texttt{PROOFGENERAL_OPTIONS} setting.  For example, GNU Emacs with loading of

the startup file enabled may be configured as follows:\footnote{The interface

  disables \texttt{.emacs} by default to ensure successful startup despite any

  strange commands that tend to occur there.}

\begin{ttbox}

PROOFGENERAL_OPTIONS="-p emacs -u true"

\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 toolbar for navigating forward and backward

through the text.  Consult the ProofGeneral documentation for further basic

commands, such as \texttt{c-c return} or \texttt{c-c u}.

\section{How to write Isar proofs anyway?}

FIXME

%%% Local Variables: 

%%% mode: latex

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

%%% End: