%% $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.  All Isabelle commands are bound to

 \ML{} identifiers.

 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 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 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-logics 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 \texttt{isabelle} 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.

 Again, 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}();] same as {\tt quit}, passing a return code

   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 and for writing temporary files.

 \item[\ttindexbold{pwd}();] returns the 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

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

 (abbreviating \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 (page~\pageref{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~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{ttdescription}

 \subsection{Printing of hypotheses, brackets, types and sorts}

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

 \end{ttbox}

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

 terms and theorems.  The hypotheses are normally shown; superfluous

 parentheses are not.  Types and sorts are normally hidden.  Displaying

 types and sorts may explain why a polymorphic inference rule fails to

 resolve with some goal.

 \begin{ttdescription}

 \item[\ttindexbold{show_hyps} := false;]   

 makes Isabelle show each meta-level hypothesis as a dot.

 \item[\ttindexbold{show_brackets} := true;] 

   makes Isabelle show full bracketing.  This reveals the

   grouping of infix operators.

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

 makes Isabelle show types when printing a term or theorem.

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

 makes Isabelle show both types and the sorts of type variables.  It does not

 matter whether {\tt show_types} is also~{\tt true}. 

 \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[\ttindexbold{eta_contract} := 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{ttdescription}

 \index{printing control|)}

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

 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|)}