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