doc-src/System/basics.tex

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

% $Id$

\chapter{The Isabelle system environment}

This manual describes Isabelle together with related tools and user interfaces
as seen from an outside (system oriented) view.  See also the
\emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} and the
\emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the actual Isabelle
commands and related functions.

\medskip The Isabelle system environment emerges from a few general concepts.
\begin{itemize}
\item The \emph{Isabelle settings mechanism} provides environment variables to
  all Isabelle programs (including tools and user interfaces).
\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}) provides a generic
  startup platform for Isabelle related utilities.  Thus tools automatically
  benefit from the settings mechanism.
\item The raw \emph{Isabelle process} (\ttindex{isabelle} or
  \texttt{isabelle-process}) runs logic sessions either interactively or in
  batch mode.  In particular, this view abstracts over the invocation of the
  actual {\ML} system to be used.
\item The \emph{Isabelle interface wrapper} (\ttindex{Isabelle} or
  \texttt{isabelle-interface}) provides some abstraction over the actual user
  interface to be used.  The de-facto standard interface for Isabelle is
  Proof~General \cite{proofgeneral}.
\end{itemize}

\medskip The beginning user would probably just run the default user interface
(by invoking the capital \texttt{Isabelle}).  This assumes that the system has
already been installed, of course.  In case you have to do this yourself, see
the \ttindex{INSTALL} file in the top-level directory of the distribution of
how to proceed; binary packages for various system components are available as
well.


\section{Isabelle settings} \label{sec:settings}

The Isabelle system heavily depends on the \emph{settings
  mechanism}\indexbold{settings}.  Essentially, this is a statically scoped
collection of environment variables, such as \texttt{ISABELLE_HOME},
\texttt{ML_SYSTEM}, \texttt{ML_HOME}.  These variables are \emph{not} intended
to be set directly from the shell, though.  Isabelle employs a somewhat more
sophisticated scheme of \emph{settings files} --- one for site-wide defaults,
another for additional user-specific modifications.  With all configuration
variables in at most two places, this scheme is more maintainable and
user-friendly than global shell environment variables.

In particular, we avoid the typical situation where prospective users of a
software package are told to put several things into their shell startup
scripts, before being able to actually run the program. Isabelle requires none
such administrative chores of its end-users --- the executables can be invoked
straight away.\footnote{Occasionally, users would still want to put the
  Isabelle \texttt{bin} directory into their shell's search path, but this is
  not required.}


\subsection{Building the environment}

Whenever any of the Isabelle executables is run, their settings environment is
put together as follows.

\begin{enumerate}
\item The special variable \settdx{ISABELLE_HOME} is determined automatically
  from the location of the binary that has been run.
  
  You should not try to set \texttt{ISABELLE_HOME} manually. Also note that
  the Isabelle executables either have to be run from their original location
  in the distribution directory, or via the executable objects created by the
  \texttt{install} utility (see \S\ref{sec:tool-install}).  Just doing a plain
  copy of the \texttt{bin} files will not work!
  
\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script
  with the auto-export option for variables enabled.
  
  This file holds a rather long list of shell variable assigments, thus
  providing the site-wide default settings.  The Isabelle distribution already
  contains a global settings file with sensible defaults for most variables.
  When installing the system, only a few of these may have to be adapted
  (probably \texttt{ML_SYSTEM} etc.).
  
\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
  run in the same way as the site default settings. Note that the variable
  \texttt{ISABELLE_HOME_USER} has already been set before --- usually to
  \texttt{\~\relax/isabelle}.
  
  Thus individual users may override the site-wide defaults. See also file
  \texttt{etc/user-settings.sample} in the distribution.  Typically, a user
  settings file would contain only a few lines, just the assigments that are
  really changed.  One should definitely \emph{not} start with a full copy the
  basic \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very annoying
  maintainance problems later, when the Isabelle installation is updated or
  changed otherwise.

\end{enumerate}

Note that settings files are actually full GNU bash scripts. So one may use
complex shell commands, such as \texttt{if} or \texttt{case} statements to set
variables depending on the system architecture or other environment variables.
Such advanced features should be added only with great care, though. In
particular, external environment references should be kept at a minimum.

\medskip A few variables are somewhat special:
\begin{itemize}
\item \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to the
  absolute path names of the \texttt{isabelle-process} and \texttt{isatool}
  executables, respectively.
  
\item \settdx{ISABELLE_OUTPUT} will have the {\ML} system identifier
  (according to \texttt{ML_IDENTIFIER}) automatically appended to its value.
\end{itemize}

\medskip The Isabelle settings scheme is conceptually simple, but not
completely trivial.  For debugging purposes, the resulting environment may be
inspected with the \texttt{getenv} utility, see \S\ref{sec:tool-getenv}.


\subsection{Common variables}

This is a reference of common Isabelle settings variables. Note that the list
is somewhat open-ended. Third-party utilities or interfaces may add their own
selection. Variables that are special in some sense are marked with *.

\begin{description}
\item[\settdx{ISABELLE_HOME}*] is the location of the top-level Isabelle
  distribution directory. This is automatically determined from the Isabelle
  executable that has been invoked.  Do not attempt to set
  \texttt{ISABELLE_HOME} yourself from the shell.
  
\item[\settdx{ISABELLE_HOME_USER}] is the user-specific counterpart of
  \texttt{ISABELLE_HOME}. The default value is \texttt{\~\relax/isabelle},
  under rare circumstances this may be changed in the global setting file.
  Typically, the \texttt{ISABELLE_HOME_USER} directory mimics
  \texttt{ISABELLE_HOME} to some extend. In particular, site-wide defaults may
  be overridden by a private \texttt{etc/settings}.
  
\item[\settdx{ISABELLE}*, \settdx{ISATOOL}*] are automatically set to the full
  path names of the \texttt{isabelle-process} and \texttt{isatool}
  executables, respectively.  Thus other tools and scripts need not assume
  that the Isabelle \texttt{bin} directory is on the current search path of
  the shell.
  
\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS},
  \settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML}
  system to be used for Isabelle.  There is only a fixed set of admissable
  \texttt{ML_SYSTEM} names (see the \texttt{etc/settings} file of the
  distribution).
  
  The actual compiler binary will be run from the directory \texttt{ML_HOME},
  with \texttt{ML_OPTIONS} as first arguments on the command line.  The
  optional \texttt{ML_PLATFORM} may specify the binary format of ML heap
  images, which is useful for cross-platform installations.  The value of
  \texttt{ML_IDENTIFIER} is automatically obtained by composing the
  \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM} values.
  
\item[\settdx{ISABELLE_PATH}] is a list of directories (separated by colons)
  where Isabelle logic images may reside.  When looking up heaps files, the
  value of \texttt{ML_IDENTIFIER} is appended to each component internally.
  
\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap files should
  be stored by default. The \texttt{ML_SYSTEM} identifier is appended here,
  too.
  
\item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory browser
  information (HTML text, graph data, and printable documents) is stored (see
  also \S\ref{sec:info}).  The default value is
  \texttt{\$ISABELLE_HOME_USER/browser_info}.
  
\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is
  given explicitely by the user.  The default value is \texttt{HOL}.
  
\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the command
  line of any \texttt{isatool usedir} invocation (see also
  \S\ref{sec:tool-usedir}). This typically contains compilation options for
  object-logics --- \texttt{usedir} is the basic utility for managing logic
  sessions (cf.\ the \texttt{IsaMakefile}s in the distribution).
  
\item[\settdx{ISABELLE_LATEX}, \settdx{ISABELLE_PDFLATEX},
  \settdx{ISABELLE_BIBTEX}, \settdx{ISABELLE_DVIPS}] refer to {\LaTeX} related
  tools for Isabelle document preparation (see also \S\ref{sec:tool-latex}).
  
\item[\settdx{ISABELLE_TOOLS}] is a colon separated list of directories that
  are scanned by \texttt{isatool} for external utility programs (see also
  \S\ref{sec:isatool}).
  
\item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories with
  documentation files.
  
\item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying
  \texttt{dvi} files.
  
\item[\settdx{ISABELLE_TMP_PREFIX}*] is the prefix from which any running
  \texttt{isabelle} process derives an individual directory for temporary
  files.  The default is somewhere in \texttt{/tmp}.
  
\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the actual
  user interface that the capital \texttt{Isabelle} or
  \texttt{isabelle-interface} should invoke.  See \S\ref{sec:interface} for
  more details.

\end{description}


\section{The Isabelle tools wrapper} \label{sec:isatool}

All Isabelle related utilities are called via a common wrapper ---
\ttindex{isatool}:
\begin{ttbox}
Usage: isatool TOOL [ARGS ...]

  Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
  for more specific help.

  Available tools are:

    browser - Isabelle graph browser
    \dots
\end{ttbox}
In principle, Isabelle tools are ordinary executable scripts that are run
within the Isabelle settings environment, see \S\ref{sec:settings}.  The set
of available tools is collected by \texttt{isatool} from the directories
listed in the \texttt{ISABELLE_TOOLS} setting.  Do not try to call the scripts
directly from the shell.  Neither should you add the tool directories to your
shell's search path!


\subsubsection*{Examples}

Show the list of available documentation of the current Isabelle installation
like this:
\begin{ttbox}
  isatool doc
\end{ttbox}

View a certain document as follows:
\begin{ttbox}
  isatool doc isar-ref
\end{ttbox}

Create an Isabelle session derived from HOL (see also \S\ref{sec:tool-mkdir}
and \S\ref{sec:tool-make}):
\begin{ttbox}
  isatool mkdir HOL Test && isatool make
\end{ttbox}
Note that \texttt{isatool mkdir} is usually only invoked once; existing
sessions (including document output etc.) are then updated by \texttt{isatool
  make} alone.


\section{The raw Isabelle process}

The \ttindex{isabelle} (or \ttindex{isabelle-process}) executable runs
bare-bones Isabelle logic sessions --- either interactively or in batch mode.
It provides an abstraction over the underlying {\ML} system, and over the
actual heap file locations.  Its usage is:
\begin{ttbox}
Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]

  Options are:
    -C           tell ML system to copy output image
    -I           startup Isar interaction mode
    -P           startup Proof General interaction mode
    -c           tell ML system to compress output image
    -e MLTEXT    pass MLTEXT to the ML session
    -f           pass 'Session.finish();' to the ML session
    -m MODE      add print mode for output
    -q           non-interactive session
    -r           open heap file read-only
    -u           pass 'use"ROOT.ML";' to the ML session
    -w           reset write permissions on OUTPUT

  INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
  These are either names to be searched in the Isabelle path, or
  actual file names (containing at least one /).
  If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
\end{ttbox}
Input files without path specifications are looked up in the
\texttt{ISABELLE_PATH} setting, which may consist of multiple components
separated by colons --- these are tried in the given order with the value of
\texttt{ML_IDENTIFIER} appended internally.  In a similar way, base names are
relative to the directory specified by \texttt{ISABELLE_OUTPUT}.  In any case,
actual file locations may also be given by including at least one slash
(\texttt{/}) in the name (hint: use \texttt{./} to refer to the current
directory).


\subsection*{Options}

If the input heap file does not have write permission bits set, or the
\texttt{-r} option is given explicitely, then the session started will be
read-only.  That is, the {\ML} world cannot be committed back into the image
file.  Otherwise, a writable session enables commits into either the input
file, or into another output heap file (if that is given as the second
argument on the command line).

The read-write state of sessions is determined at startup only, it cannot be
changed intermediately. Also note that heap images may require considerable
amounts of disk space (approximately 20--40~MB). Users are responsible for
themselves to dispose their heap files when they are no longer needed.

\medskip The \texttt{-w} option makes the output heap file read-only after
terminating.  Thus subsequent invocations cause the logic image to be
read-only automatically.

\medskip The \texttt{-c} option tells the underlying ML system to compress the
output heap (fully transparently).  On Poly/ML for example, the image is
garbage collected and all stored values are maximally shared, resulting in up
to 50\% less disk space consumption.

\medskip The \texttt{-C} option tells the ML system to produce a completely
self-contained output image, probably including a copy of the ML runtime
system itself.

\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to
the Isabelle session from the command line. Multiple \texttt{-e}'s are
evaluated in the given order. Strange things may happen when errorneous {\ML}
code is provided. Also make sure that the {\ML} commands are terminated
properly by semicolon.

\medskip The \texttt{-u} option is a shortcut for \texttt{-e} passing
``\texttt{use"ROOT.ML";}'' to the {\ML} session.  The \texttt{-f} option
passes ``\texttt{Session.finish();}'', which is intended mainly for
administrative purposes.

\medskip The \texttt{-m} option adds identifiers of print modes to be made
active for this session. Typically, this is used by some user interface, e.g.\ 
to enable output of proper mathematical symbols.

\medskip Isabelle normally enters an interactive top-level loop (after
processing the \texttt{-e} texts). The \texttt{-q} option inhibits
interaction, thus providing a pure batch mode facility.

\medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
startup, instead of the primitive {\ML} top-level.  The \texttt{-P} option
configures the top-level loop for interaction with the Proof~General user
interface; do not enable this in plain TTY sessions.


\subsection*{Examples}

Run an interactive session of the default object-logic (as specified
by the \texttt{ISABELLE_LOGIC} setting) like this:
\begin{ttbox}
isabelle
\end{ttbox}
Usually \texttt{ISABELLE_LOGIC} refers to one of the standard logic
images, which are read-only by default.  A writable session --- based
on \texttt{FOL}, but output to \texttt{Foo} (in the directory
specified by the \texttt{ISABELLE_OUTPUT} setting) --- may be invoked
as follows:
\begin{ttbox}
isabelle FOL Foo
\end{ttbox}
Ending this session normally (e.g.\ by typing control-D) dumps the whole {\ML}
system state into \texttt{Foo}. Be prepared for several tens of megabytes.

The \texttt{Foo} session may be continued later (still in writable
state) by:
\begin{ttbox}
isabelle Foo
\end{ttbox}
A read-only \texttt{Foo} session may be started by:
\begin{ttbox}
isabelle -r Foo
\end{ttbox}

\medskip Note that manual session management like this does \emph{not} provide
proper setup for theory presentation.  This would require the \texttt{usedir}
utility, see \S\ref{sec:tool-usedir}.

\bigskip The next example demonstrates batch execution of Isabelle. We print a
certain theorem of \texttt{FOL}:
\begin{ttbox}
isabelle -e "prth allE;" -q -r FOL
\end{ttbox}
Note that the output text will be interspersed with additional junk messages
by the {\ML} runtime environment.


\section{The Isabelle interface wrapper}\label{sec:interface}

Isabelle is a generic theorem prover, even w.r.t.\ its user interface.  The
\ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
uniform way for end-users to invoke a certain interface; which one to start is
determined by the \settdx{ISABELLE_INTERFACE} setting variable.  Also note
that the \texttt{install} utility provides some options to install desktop
environment icons as well (see \S\ref{sec:tool-install}).

An interface may be specified either by giving an identifier that the Isabelle
distribution knows about, or by specifying an actual path name (containing a
slash ``\texttt{/}'') of some executable.  Currently, the following interfaces
are available:

\begin{itemize}
\item \texttt{none} is just a pass-through to raw \texttt{isabelle}. Thus
  \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.  This is
  the factory default.

\item \texttt{emacs} refers to David Aspinall's \emph{Isamode}\index{user
    interface!Isamode} for emacs.  Isabelle just provides a wrapper for this,
  the actual Isamode distribution is available elsewhere \cite{isamode}.
  
\item Proof~General~\cite{proofgeneral}\index{user interface!Proof General} is
  an advanced interface for common theorem proving environments.  It has
  become the de-facto standard for Isabelle recently, supporting both the old
  ML top-level of classic Isabelle and the more convenient Isabelle/Isar
  interpreter loop.  The Proof~General distributions includes separate
  interface wrapper scripts (in \texttt{ProofGeneral/isa} and
  \texttt{ProofGeneral/isar}).  The canonical settings for Isabelle/Isar are
  as follows:
  \begin{ttbox}
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
PROOFGENERAL_OPTIONS=""
  \end{ttbox}
  Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
  the Proof~General Lisp packages.  There are some options available, such as
  \texttt{-l} for passing the logic image to be used by default, or
  \texttt{-m} to tune the standard print mode.  The \texttt{-I} option allows
  to switch between the Isar and ML view, independently of the interface
  script being used.
  
  \medskip Note that the world may be also seen the other way round: Emacs may
  be started first (with proper setup of Proof~General mode), and
  \texttt{isabelle} run from within.  This requires further Emacs Lisp
  configuration, see the Proof~General documentation \cite{proofgeneral} for
  more information.

\end{itemize}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"
%%% End: