doc-src/Ref/introduction.tex

no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.

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