\chapter{Basic Use of Isabelle}\index{sessions|(}
\section{Basic interaction with Isabelle}
\index{starting up|bold}\nobreak
%
We assume that your local Isabelle administrator (this might be you!) has
already installed the Isabelle system together with appropriate object-logics.
\medskip Let $\langle isabellehome \rangle$ denote the location where
the distribution has been installed. To run Isabelle from a the shell
prompt within an ordinary text terminal session, simply type
\begin{ttbox}
\({\langle}isabellehome{\rangle}\)/bin/isabelle
\end{ttbox}
This should start an interactive \ML{} session with the default object-logic
(usually HOL) already pre-loaded.
Subsequently, we assume that the \texttt{isabelle} executable is determined
automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
\rangle\)/bin} to your search path.\footnote{Depending on your installation,
there may be stand-alone binaries located in some global directory such as
\texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle isabellehome
\rangle\)/bin/isabelle}, though! See \texttt{isabelle install} in
\emph{The Isabelle System Manual} of how to do this properly.}
\medskip
The object-logic image to load may be also specified explicitly as an argument
to the {\tt isabelle} command, e.g.
\begin{ttbox}
isabelle FOL
\end{ttbox}
This should put you into the world of polymorphic first-order logic (assuming
that an image of FOL has been pre-built).
\index{saving your session|bold} Isabelle provides no means of storing
theorems or internal proof objects on files. Theorems are simply part of the
\ML{} state. To save your work between sessions, you may dump the \ML{}
system state to a file. This is done automatically when ending the session
normally (e.g.\ by typing control-D), provided that the image has been opened
\emph{writable} in the first place. The standard object-logic images are
usually read-only, so you have to create a private working copy first. For
example, the following shell command puts you into a writable Isabelle session
of name \texttt{Foo} that initially contains just plain HOL:
\begin{ttbox}
isabelle HOL Foo
\end{ttbox}
Ending the \texttt{Foo} session with control-D will cause the complete
\ML-world to be saved somewhere in your home directory\footnote{The default
location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your
local configuration.}. Make sure there is enough space available! Then one
may later continue at exactly the same point by running
\begin{ttbox}
isabelle Foo
\end{ttbox}
\medskip Saving the {\ML} state is not enough. Record, on a file, the
top-level commands that generate your theories and proofs. Such a record
allows you to replay the proofs whenever required, for instance after making
minor changes to the axioms. Ideally, these sources will be somewhat
intelligible to others as a formal description of your work.
It is good practice to put all source files that constitute a separate
Isabelle session into an individual directory, together with an {\ML} file
called \texttt{ROOT.ML} that contains appropriate commands to load all other
files required. Running \texttt{isabelle} with option \texttt{-u}
automatically loads \texttt{ROOT.ML} on entering the session. The
\texttt{isabelle usedir} utility provides some more options to manage Isabelle
sessions, such as automatic generation of theory browsing information.
\medskip More details about the \texttt{isabelle} and \texttt{isabelle}
commands may be found in \emph{The Isabelle System Manual}.
\medskip There are more comfortable user interfaces than the bare-bones \ML{}
top-level run from a text terminal. The \texttt{Isabelle} executable (note
the capital I) runs one such interface, depending on your local configuration.
Again, see \emph{The Isabelle System Manual} for more information.
\section{Ending a session}
\begin{ttbox}
quit : unit -> unit
exit : int -> unit
commit : unit -> bool
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
the state.
\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
code \(i\) to the operating system.
\item[\ttindexbold{commit}();] saves the current state without ending
the session, provided that the logic image is opened read-write;
return value {\tt false} indicates an error.
\end{ttdescription}
Typing control-D also finishes the session in essentially the same way
as the sequence {\tt commit(); quit();} would.
\section{Reading ML files}
\index{files!reading}
\begin{ttbox}
cd : string -> unit
pwd : unit -> string
use : string -> unit
time_use : string -> unit
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
{\it dir}. This is the default directory for reading files.
\item[\ttindexbold{pwd}();] returns the full path of the current
directory.
\item[\ttindexbold{use} "$file$";]
reads the given {\it file} as input to the \ML{} session. Reading a file
of Isabelle commands is the usual way of replaying a proof.
\item[\ttindexbold{time_use} "$file$";]
performs {\tt use~"$file$"} and prints the total execution time.
\end{ttdescription}
The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
expanded appropriately. Note that \texttt{\~\relax} abbreviates
\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}. The syntax for path
specifications follows Unix conventions.
\section{Reading theories}\label{sec:intro-theories}
\index{theories!reading}
In Isabelle, any kind of declarations, definitions, etc.\ are organized around
named \emph{theory} objects. Logical reasoning always takes place within a
certain theory context, which may be switched at any time. Theory $name$ is
defined by a theory file $name$\texttt{.thy}, containing declarations of
\texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see
\S\ref{sec:ref-defining-theories} for more details on concrete syntax).
Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with
proof scripts that are to be run in the context of the theory.
\begin{ttbox}
context : theory -> unit
the_context : unit -> theory
theory : string -> theory
use_thy : string -> unit
time_use_thy : string -> unit
update_thy : string -> unit
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{context} $thy$;] switches the current theory context. Any
subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal})
will refer to $thy$ as its theory.
\item[\ttindexbold{the_context}();] obtains the current theory context, or
raises an error if absent.
\item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from
the internal data\-base of loaded theories, raising an error if absent.
\item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter
being optional). It also ensures that all parent theories are loaded as
well. In case some older versions have already been present,
\texttt{use_thy} only tries to reload $name$ itself, but is content with any
version of its ancestors.
\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
reports the time taken to process the actual theory parts and {\ML} files
separately.
\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
ensures that theory $name$ is fully up-to-date with respect to the file
system --- apart from theory $name$ itself, any of its ancestors may be
reloaded as well.
\end{ttdescription}
Note that theories of pre-built logic images (e.g.\ HOL) are marked as
\emph{finished} and cannot be updated any more. See \S\ref{sec:more-theories}
for further information on Isabelle's theory loader.
\section{Setting flags}
\begin{ttbox}
set : bool ref -> bool
reset : bool ref -> bool
toggle : bool ref -> bool
\end{ttbox}\index{*set}\index{*reset}\index{*toggle}
These are some shorthands for manipulating boolean references. The new
value is returned.
\section{Diagnostic messages}
\index{error messages}
\index{warnings}
Isabelle conceptually provides three output channels for different kinds of
messages: ordinary text, warnings, errors. Depending on the user interface
involved, these messages may appear in different text styles or colours.
The default setup of an \texttt{isabelle} terminal session is as
follows: plain output of ordinary text, warnings prefixed by
\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s. For example, a
typical warning would look like this:
\begin{ttbox}
\#\#\# Beware the Jabberwock, my son!
\#\#\# The jaws that bite, the claws that catch!
\#\#\# Beware the Jubjub Bird, and shun
\#\#\# The frumious Bandersnatch!
\end{ttbox}
\texttt{ML} programs may output diagnostic messages using the
following functions:
\begin{ttbox}
writeln : string -> unit
warning : string -> unit
error : string -> 'a
\end{ttbox}
Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
after having output the text, while \ttindex{writeln} and
\ttindex{warning} resume normal program execution.
\section{Timing}
\index{timing statistics}\index{proofs!timing}
\begin{ttbox}
timing: bool ref \hfill{\bf initially false}
\end{ttbox}
\begin{ttdescription}
\item[set \ttindexbold{timing};] enables global timing in Isabelle.
This information is compiler-dependent.
\end{ttdescription}
\index{sessions|)}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
%%% End: