\end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsection{User interfaces%

 }

 \isamarkuptrue%

 %

 \isamarkupsubsection{Terminal sessions%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 The Isabelle \texttt{tty} tool provides a very interface for running

   the Isar interaction loop, with some support for command line

   editing.  For example:

 \begin{ttbox}

 isabelle tty\medskip

 {\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip

 theory Foo imports Main begin;

 definition foo :: nat where "foo == 1";

 lemma "0 < foo" by (simp add: foo_def);

 end;

 \end{ttbox}

   Any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.

   See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a

   comprehensive overview of available commands and other language

   elements.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsection{Emacs Proof General%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

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

   Proof~General environment by David Aspinall

   \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs

   interface for interactive theorem provers that organizes 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.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{Proof~General as default Isabelle interface%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 The Isabelle interface wrapper script provides an easy way to invoke

   Proof~General (including XEmacs or GNU Emacs).  The default

   configuration of Isabelle is smart enough to detect the

   Proof~General distribution in several canonical places (e.g.\

   \verb|$ISABELLE_HOME/contrib/ProofGeneral|).  Thus the

   capital \verb|Isabelle| executable would already refer to the

   \verb|ProofGeneral/isar| interface without further ado.  The

   Isabelle interface script provides several options; 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/Summation.thy

 \end{ttbox}

   Beginners may note the tool bar for navigating forward and backward

   through the text (this depends on the local Emacs installation).

   Consult the Proof~General documentation \cite{proofgeneral} for

   further basic command sequences, in particular ``\verb|C-c C-return|''

   and ``\verb|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 \verb|$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 \verb|PROOFGENERAL_OPTIONS|

   setting.  For example, the Emacs executable to be used may be

   configured in Isabelle's settings like this:

 \begin{ttbox}

 PROOFGENERAL_OPTIONS="-p xemacs-mule"  

 \end{ttbox}

   Occasionally, a user's \verb|~/.emacs| file contains code

   that is incompatible with the (X)Emacs version used by

   Proof~General, causing the interface startup to fail prematurely.

   Here the \verb|-u false| option helps to get the interface

   process up and running.  Note that additional Lisp customization

   code may reside in \verb|proofgeneral-settings.el| of

   \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsubsubsection{The X-Symbol package%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 Proof~General incorporates a version of the Emacs X-Symbol package

   \cite{x-symbol}, which handles proper mathematical symbols displayed

   on screen.  Pass option \verb|-x true| to the Isabelle

   interface script, or check the appropriate Proof~General menu

   setting by hand.  The main challenge of getting X-Symbol to work

   properly is the underlying (semi-automated) X11 font setup.

   \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, \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} would appear as \verb|\<Longrightarrow>| according

   the default set of Isabelle symbols.  Nevertheless, the Isabelle

   document preparation system (see \chref{ch:document-prep}) will be

   happy to print non-ASCII symbols properly.  It is even possible to

   invent additional notation beyond the display capabilities of Emacs

   and X-Symbol.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

 \isamarkupsection{Isabelle/Isar theories%

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 Isabelle/Isar offers the following main improvements over classic

   Isabelle.

   \begin{enumerate}

   \item A \emph{theory format} that integrates specifications and

   proofs, 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.  The

   old tactical style has been assimilated as ``improper'' language

   elements.

   \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

   \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and

   left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).

   A few theory specification mechanisms also require some proof, such

   as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the

   representing sets.%

 \end{isamarkuptext}%

 \isamarkuptrue%

 %

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

 }

 \isamarkuptrue%

 %

 \begin{isamarkuptext}%

 This is one of the key questions, of course.  First of all, the

   tactic script emulation of Isabelle/Isar essentially provides a

   clarified version of the very same unstructured proof style of

   classic Isabelle.  Old-time users should quickly become acquainted

   with that (slightly degenerative) view of Isar.

   Writing \emph{proper} Isar proof texts targeted at human readers is

   quite different, though.  Experienced users of the unstructured

   style may even have to unlearn some of their habits to master proof

   composition in Isar.  In contrast, new users with less experience in

   old-style tactical proving, but a good understanding of mathematical

   proof in general, often get started easier.

   \medskip The present text really is only a reference manual on

   Isabelle/Isar, not a tutorial.  Nevertheless, we will attempt to

   give some clues of how the concepts introduced here may be put into

   practice.  Especially note that \appref{ap:refcard} provides a quick

   reference card of the most common Isabelle/Isar language elements.

   Further issues concerning the Isar concepts are covered in the

   literature

   \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.

   The author's PhD thesis \cite{Wenzel-PhD} presently provides the

   most complete exposition of Isar foundations, techniques, and

   applications.  A number of example applications are distributed with

   Isabelle, and available via the Isabelle WWW library (e.g.\

   \url{http://isabelle.in.tum.de/library/}).  The ``Archive of Formal

   Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of

   examples, both in proper Isar proof style and unstructured tactic

   scripts.%