%% $Id$

\chapter{Basic Use of Isabelle}\index{sessions|(} 

The Reference Manual is a comprehensive description of Isabelle

proper, including all \ML{} commands, functions and packages.  It

really is intended for reference, perhaps for browsing, but not for

reading through.  It is not a tutorial, but assumes familiarity with

the basic logical concepts of Isabelle.

When you are looking for a way of performing some task, scan the Table of

Contents for a relevant heading.  Functions are organized by their purpose,

by their operands (subgoals, tactics, theorems), and by their usefulness.

In each section, basic functions appear first, then advanced functions, and

finally esoteric functions.  Use the Index when you are looking for the

definition of a particular Isabelle function.

A few examples are presented.  Many examples files are distributed with

Isabelle, however; please experiment interactively.

\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 \Pure\ system and several object-logics

properly --- otherwise see the {\tt INSTALL} file in the top-level

directory of the distribution on how to build it.

\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 already preloaded.

Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}

has been added to your shell's search path, in order to avoid typing

full path specifications of the executable files.

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 {\FOL} has been pre-built).

\index{saving your work|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 must 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 probably

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

\begin{ttbox}

isabelle FOL 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}

More details about the \texttt{isabelle} command may be found in the

\emph{System Manual}.

\medskip Saving the 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, your record will

be somewhat intelligible to others as a formal description of your

work.

\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.  Furthermore there

are a number of external utilities available.  These are started

uniformly via the \texttt{isatool} wrapper.  See the \emph{System

  Manual} for more information user interfaces and utilities.

\section{Ending a session}

\begin{ttbox} 

quit    : unit -> unit

exit    : int -> unit

commit  : unit -> unit

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

\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 that are expanded

appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}

(which abbreviates \texttt{\$HOME}).  Section~\ref{LoadingTheories}

describes commands for loading theory files.

\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{Printing of terms and theorems}\label{sec:printing-control}

\index{printing control|(}

Isabelle's pretty printer is controlled by a number of parameters.

\subsection{Printing limits}

\begin{ttbox} 

Pretty.setdepth  : int -> unit

Pretty.setmargin : int -> unit

print_depth      : int -> unit

\end{ttbox}

These set limits for terminal output.  See also {\tt goals_limit},

which limits the number of subgoals printed

(\S\ref{sec:goals-printing}).

\begin{ttdescription}

\item[\ttindexbold{Pretty.setdepth} \(d\);]  

  tells Isabelle's pretty printer to limit the printing depth to~$d$.  This

  affects Isabelle's display of theorems and terms.  The default value

  is~0, which permits printing to an arbitrary depth.  Useful values for

  $d$ are~10 and~20.

\item[\ttindexbold{Pretty.setmargin} \(m\);]  

  tells Isabelle's pretty printer to assume a right margin (page width)

  of~$m$.  The initial margin is~76.

\item[\ttindexbold{print_depth} \(n\);]  

  limits the printing depth of complex \ML{} values, such as theorems and

  terms.  This command affects the \ML{} top level and its effect is

  compiler-dependent.  Typically $n$ should be less than~10.

\end{ttdescription}

\subsection{Printing of hypotheses, brackets, types etc.}

\index{meta-assumptions!printing of}

\index{types!printing of}\index{sorts!printing of}

\begin{ttbox} 

show_hyps     : bool ref \hfill{\bf initially true}

show_brackets : bool ref \hfill{\bf initially false}

show_types    : bool ref \hfill{\bf initially false}

show_sorts    : bool ref \hfill{\bf initially false}

show_consts   : bool ref \hfill{\bf initially false}

\end{ttbox}

These flags allow you to control how much information is displayed for

types, terms and theorems.  The hypotheses of theorems \emph{are}

normally shown.  Superfluous parentheses of types and terms are not.

Types and sorts of variables are normally hidden.

Note that displaying types and sorts may explain why a polymorphic

inference rule fails to resolve with some goal, or why a rewrite rule

does not apply as expected.

\begin{ttdescription}

\item[reset \ttindexbold{show_hyps};] makes Isabelle show each

  meta-level hypothesis as a dot.

\item[set \ttindexbold{show_brackets};] makes Isabelle show full

  bracketing.  In particular, this reveals the grouping of infix

  operators.

\item[set \ttindexbold{show_types};] makes Isabelle show types when

  printing a term or theorem.

\item[set \ttindexbold{show_sorts};] makes Isabelle show both types

  and the sorts of type variables, independently of the value of

  \texttt{show_types}.

\item[set \ttindexbold{show_consts};] makes Isabelle show types of

  constants, provided that showing of types is enabled at all.  This

  is supported for printing of proof states only.  Note that the

  output can be enormous as polymorphic constants often occur at

  several different type instances.

\end{ttdescription}

\subsection{$\eta$-contraction before printing}

\begin{ttbox} 

eta_contract: bool ref \hfill{\bf initially false}

\end{ttbox}

The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,

provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of

functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order

unification frequently puts terms into a fully $\eta$-expanded form.  For

example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is

$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded

form.

\begin{ttdescription}

\item[set \ttindexbold{eta_contract};]

makes Isabelle perform $\eta$-contractions before printing, so that

$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The

distinction between a term and its $\eta$-expanded form occasionally

matters.

\end{ttdescription}

\index{printing control|)}

\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, even within separate windows.

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{Displaying exceptions as error messages}

\index{exceptions!printing of}

\begin{ttbox} 

print_exn: exn -> 'a

\end{ttbox}

Certain Isabelle primitives, such as the forward proof functions {\tt RS}

and {\tt RSN}, are called both interactively and from programs.  They

indicate errors not by printing messages, but by raising exceptions.  For

interactive use, \ML's reporting of an uncaught exception may be

uninformative.  The Poly/ML function {\tt exception_trace} can generate a

backtrace.\index{Poly/{\ML} compiler}

\begin{ttdescription}

\item[\ttindexbold{print_exn} $e$] 

displays the exception~$e$ in a readable manner, and then re-raises~$e$.

Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where

$EXP$ is an expression that may raise an exception.

{\tt print_exn} can display the following common exceptions, which concern

types, terms, theorems and theories, respectively.  Each carries a message

and related information.

\begin{ttbox} 

exception TYPE   of string * typ list * term list

exception TERM   of string * term list

exception THM    of string * int * thm list

exception THEORY of string * theory list

\end{ttbox}

\end{ttdescription}

\begin{warn}

  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains

  pretty printing information from the proof state last stored in the

  subgoal module.  The appearance of the output thus depends upon the

  theory used in the last interactive proof.

\end{warn}

\index{sessions|)}