%% $Id$

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

The Reference Manual is a comprehensive description of Isabelle, including

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

The Index provides an alphabetical listing.  Page numbers of definitions

are printed in {\bf bold}, passing references in Roman type.  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{sessions!saving|bold}\index{saving your work|bold}

Isabelle provides no means of storing theorems or proofs on files.

Theorems are simply part of the \ML{} state and are named by \ML{}

identifiers.  To save your work between sessions, you must save a copy of

the \ML{} image.  The procedure for doing so is compiler-dependent:

\begin{itemize}\index{Poly/\ML}

\item At the end of a session, Poly/\ML{} saves the state, provided you have

created a database for your own use.  You can create a database by copying

an existing one, or by calling the Poly/\ML{} function {\tt make_database};

the latter course uses much less disc space.  Note that a Poly/\ML{}

database {\bf does not} save the contents of references, such as the

current state of a backward proof.

\item With New Jersey \ML{} you must save the state explicitly before

ending the session.  While a Poly/\ML{} database can be small, a New Jersey

image occupies several megabytes.

\end{itemize}

See your \ML{} compiler's documentation for full instructions on saving the

state.

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 intelligible to others as a

formal description of your work.

Since Isabelle's user interface is the \ML{} top level, some kind of window

support is essential.  One window displays the Isabelle session, while the

other displays a file --- your proof record --- being edited.  Some people

use a screen editor such as Emacs, which supports windows and can manage

interactive sessions.  Others prefer to use a workstation running the X Window

System.

\section{Ending a session}

\index{sessions!ending|bold}

\begin{ttbox} 

quit     : unit -> unit

commit   : unit -> unit \hfill{\bf Poly/ML only}

exportML : string -> bool \hfill{\bf New Jersey ML only}

\end{ttbox}

\begin{description}

\item[\ttindexbold{quit}();]  

aborts the Isabelle session, without saving the state.

\item[\ttindexbold{commit}();]  saves the current state in your

Poly/\ML{} database without finishing the session.  Values of reference

variables are lost, so never do this during an interactive

proof!\index{Poly/\ML} 

\item[\ttindexbold{exportML} \tt"{\it file}";]  saves an

image of your session to the given {\it file}.

\end{description}

\begin{warn}

Typing control-D also finishes the session, but its effect is

compiler-dependent.  Poly/\ML{} will then save the state, if you have a

private database.  New Jersey \ML{} will discard the state!

\end{warn}

\section{Reading files of proofs and theories}

\index{files!reading|bold}

\begin{ttbox} 

cd              : string -> unit

use             : string -> unit

use_thy         : string -> unit

time_use        : string -> unit

time_use_thy    : string -> unit

update          : unit -> unit

loadpath        : string list ref

\end{ttbox}

\begin{description}

\item[\ttindexbold{cd} \tt"{\it dir}";]  changes to {\it dir\/} the default

directory for reading files.

\item[\ttindexbold{use} \tt"$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{use_thy} \tt"$tname$";] 

  reads a theory definition from file {\it tname}{\tt.thy} and also reads

  {\ML} commands from the file {\it tname}{\tt.ML}, if it exists.  If

  theory {\it tname} depends on theories that have not been read already,

  then it loads these beforehand.  See Chapter~\ref{theories} for

  details.

\item[\ttindexbold{time_use} \tt"$file$";]  

performs {\tt use~"$file$"} and prints the total execution time.

\item[\ttindexbold{time_use_thy} \tt"$tname$";]  

performs {\tt use_thy "$tname$"} and prints the total execution time.

\item[\ttindexbold{update} \tt();]  

reads all theories that have changed since the last time they have been read.

See Chapter~\ref{theories} for details.

\item[\ttindexbold{loadpath}] 

  contains a list of paths that is used by {\tt use_thy} and {\tt update}

  to find {\it tname}{\tt.ML} and {\it tname}{\tt.thy}.  See

  Chapter~\ref{theories} for details.

\end{description}

\section{Printing of terms and theorems}

\index{printing!flags|bold}

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.

\begin{description}

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

\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{description}

\subsection{Printing of meta-level hypotheses}

\index{hypotheses!meta-level!printing of|bold}

\begin{ttbox} 

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

\end{ttbox}

A theorem's hypotheses are normally displayed, since such dependence is

important.  If this information becomes too verbose, however, it can be

switched off;  each hypothesis is then displayed as a dot.

\begin{description}

\item[\ttindexbold{show_hyps} \tt:= true;]   

makes Isabelle show meta-level hypotheses when printing a theorem; setting

it to {\tt false} suppresses them.

\end{description}

\subsection{Printing of types and sorts}

\begin{ttbox} 

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

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

\end{ttbox}

These control Isabelle's display of types and sorts.  Normally terms are

printed without type and sorts because they are verbose.  Occasionally you

may require this information, say to discover why a polymorphic inference rule

fails to resolve with some goal.

\begin{description}

\item[\ttindexbold{show_types} \tt:= true;]\index{types}

makes Isabelle show types when printing a term or theorem.

\item[\ttindexbold{show_sorts} \tt:= true;]\index{sorts}

makes Isabelle show the sorts of type variables.  It has no effect unless

{\tt show_types} is~{\tt true}. 

\end{description}

\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 occasionally 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{description}

\item[\ttindexbold{eta_contract} \tt:= true;]

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{description}

\section{Displaying exceptions as error messages}

\index{printing!exceptions|bold}\index{exceptions|bold}

\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 is most

uninformative.

\begin{description}

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

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

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

\ldots{} 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}

{\tt print_exn} calls \ttindex{prin} to print terms.  This obtains pretty

printing information from the proof state last stored in the subgoal

module, and will fail if no interactive proof has begun in the current

session.

\end{description}

\section{Shell scripts}

\index{shell scripts|bold}

The following files are distributed with Isabelle, and work under

Unix$^{\rm TM}$.  They can be executed as commands to the Unix shell.  Some

of them depend upon shell environment variables.

\begin{description}

\item[\ttindexbold{make-all} $switches$] 

  compiles the Isabelle system, when executed on the source directory.

  Environment variables specify which \ML{} compiler to use.  These

  variables, and the {\it switches}, are documented on the file itself.

\item[\ttindexbold{teeinput} $program$] 

executes the {\it program}, while piping the standard input to a log file

designated by the \verb|$LISTEN| environment variable.  Normally the

program is Isabelle, and the log file receives a copy of all the Isabelle

commands.

\item[\ttindexbold{xlisten} $program$] 

  is a trivial `user interface' for the X Window System.  It creates two

  windows using {\tt xterm}.  One executes an interactive session via

  \hbox{\tt teeinput $program$}, while the other displays the log file.  To

  make a proof record, simply paste lines from the log file into an editor

  window.

\item[\ttindexbold{expandshort} $files$] 

  reads the {\it files\/} and replaces all occurrences of the shorthand

  commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the

  corresponding full commands.  Shorthand commands should appear one

  per line.  The old versions of the files

  are renamed to have the suffix~\verb'~~'.

\end{description}

\index{sessions|)}