doc-src/Ref/introduction.tex

repaired critical proofs depending on the order inside non-confluent SimpSets,
(temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"

%% $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.  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{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} compiler}
\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.  A
  Poly/\ML{} database {\em 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.  The Emacs
editor supports windows and can manage interactive sessions.


\section{Ending a session}
\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{ttdescription}
\item[\ttindexbold{quit}();]  
aborts the Isabelle session, without saving the state.

\item[\ttindexbold{commit}();] 
  saves the current state in your Poly/\ML{} database without ending the
  session.  The contents of references are lost, so never do this during an
  interactive proof!\index{Poly/{\ML} compiler}

\item[\ttindexbold{exportML} "{\it file}";]  saves an
image of your session to the given {\it file}.
\end{ttdescription}

\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 ML files}
\index{files!reading}
\begin{ttbox} 
cd              : string -> unit
pwd             : unit -> string
use             : string -> unit
time_use        : string -> unit
\end{ttbox}
Section~\ref{LoadingTheories} describes commands for loading theory files.
\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}


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

\section{Shell scripts}\label{sec: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{ttdescription}
\item[make-all $switches$] \index{*make-all shell script}
  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[teeinput $program$] \index{*teeinput shell script}
  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[xlisten $program$] \index{*xlisten shell script}
  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[expandshort $files$]  \index{*expandshort shell script}
  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{ttdescription}

\index{sessions|)}