doc-src/Ref/introduction.tex
author paulson
Wed Jul 02 16:46:36 1997 +0200 (1997-07-02)
changeset 3485 f27a30a18a17
parent 3200 ea2310ba01da
child 4274 2048e7a79d09
permissions -rw-r--r--
Now there are TWO spaces after each full stop, so that the Emacs sentence
primitives work
wenzelm@3200
     1
lcp@104
     2
%% $Id$
wenzelm@3108
     3
lcp@286
     4
\chapter{Basic Use of Isabelle}\index{sessions|(} 
wenzelm@3108
     5
The Reference Manual is a comprehensive description of Isabelle
wenzelm@3108
     6
proper, including all \ML{} commands, functions and packages.  It
wenzelm@3108
     7
really is intended for reference, perhaps for browsing, but not for
wenzelm@3108
     8
reading through.  It is not a tutorial, but assumes familiarity with
wenzelm@3108
     9
the basic logical concepts of Isabelle.
lcp@104
    10
lcp@286
    11
When you are looking for a way of performing some task, scan the Table of
lcp@286
    12
Contents for a relevant heading.  Functions are organized by their purpose,
lcp@286
    13
by their operands (subgoals, tactics, theorems), and by their usefulness.
lcp@286
    14
In each section, basic functions appear first, then advanced functions, and
lcp@322
    15
finally esoteric functions.  Use the Index when you are looking for the
lcp@322
    16
definition of a particular Isabelle function.
lcp@104
    17
lcp@286
    18
A few examples are presented.  Many examples files are distributed with
lcp@286
    19
Isabelle, however; please experiment interactively.
lcp@104
    20
lcp@104
    21
lcp@104
    22
\section{Basic interaction with Isabelle}
paulson@2225
    23
\index{starting up|bold}\nobreak
paulson@2225
    24
%
wenzelm@3108
    25
We assume that your local Isabelle administrator (this might be you!)
wenzelm@3108
    26
has already installed the \Pure\ system and several object-logics
wenzelm@3108
    27
properly --- otherwise see the {\tt INSTALL} file in the top-level
wenzelm@3108
    28
directory of the distribution on how to build it.
wenzelm@3108
    29
wenzelm@3108
    30
\medskip Let $\langle isabellehome \rangle$ denote the location where
paulson@3485
    31
the distribution has been installed.  To run Isabelle from a the shell
wenzelm@3108
    32
prompt within an ordinary text terminal session, simply type:
wenzelm@3108
    33
\begin{ttbox}
wenzelm@3108
    34
\({\langle}isabellehome{\rangle}\)/bin/isabelle
wenzelm@3108
    35
\end{ttbox}
wenzelm@3108
    36
This should start an interactive \ML{} session with the default
paulson@3485
    37
object-logic already preloaded.  All Isabelle commands are bound to
wenzelm@3108
    38
\ML{} identifiers.
wenzelm@3108
    39
wenzelm@3108
    40
Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
wenzelm@3108
    41
has been added to your shell's search path, in order to avoid typing
wenzelm@3108
    42
full path specifications of the executable files.
wenzelm@3108
    43
wenzelm@3108
    44
The object-logic image to load may be also specified explicitly as an
wenzelm@3108
    45
argument to the {\tt isabelle} command, e.g.:
wenzelm@3108
    46
\begin{ttbox}
wenzelm@3108
    47
isabelle FOL
wenzelm@3108
    48
\end{ttbox}
wenzelm@3108
    49
This should put you into the world of polymorphic first-order logic
wenzelm@3108
    50
(assuming that {\FOL} has been pre-built).
paulson@2225
    51
wenzelm@3108
    52
\index{saving your work|bold} Isabelle provides no means of storing
wenzelm@3108
    53
theorems or proofs on files.  Theorems are simply part of the \ML{}
wenzelm@3108
    54
state and are named by \ML{} identifiers.  To save your work between
paulson@3485
    55
sessions, you must dump the \ML{} system state to a file.  This is done
wenzelm@3108
    56
automatically when ending the session normally (e.g.\ by typing
wenzelm@3108
    57
control-D), provided that the image has been opened \emph{writable} in
paulson@3485
    58
the first place.  The standard object-logics are usually read-only, so
paulson@3485
    59
you probably have to create a private working copy first.  For example,
wenzelm@3108
    60
the following shell command puts you into a writable Isabelle session
wenzelm@3108
    61
of name \texttt{Foo} that initially contains just \FOL:
wenzelm@3108
    62
\begin{ttbox}
wenzelm@3108
    63
isabelle FOL Foo
wenzelm@3108
    64
\end{ttbox}
wenzelm@3108
    65
Ending the \texttt{Foo} session with control-D will cause the complete
wenzelm@3108
    66
\ML{} world to be saved somewhere in your home directory\footnote{The
wenzelm@3108
    67
  default location is in \texttt{\~\relax/isabelle/heaps}, but this
paulson@3485
    68
  depends on your local configuration.}.  Make sure there is enough
wenzelm@3108
    69
space available! Then one may later continue at exactly the same point
wenzelm@3108
    70
by running
wenzelm@3108
    71
\begin{ttbox}
wenzelm@3108
    72
isabelle Foo  
wenzelm@3108
    73
\end{ttbox}
lcp@104
    74
wenzelm@3200
    75
More details about \texttt{isabelle} may be found in the \emph{System
wenzelm@3200
    76
  Manual}.
wenzelm@3108
    77
wenzelm@3108
    78
\medskip Saving the state is not enough.  Record, on a file, the
wenzelm@3108
    79
top-level commands that generate your theories and proofs.  Such a
wenzelm@3108
    80
record allows you to replay the proofs whenever required, for instance
wenzelm@3108
    81
after making minor changes to the axioms.  Ideally, your record will
wenzelm@3108
    82
be somewhat intelligible to others as a formal description of your
wenzelm@3108
    83
work.
lcp@104
    84
wenzelm@3108
    85
\medskip There are more comfortable user interfaces than the
paulson@3485
    86
bare-bones \ML{} top-level run from a text terminal.  The
wenzelm@3108
    87
\texttt{Isabelle} executable (note the capital I) runs one such
wenzelm@3108
    88
interface, depending on your local configuration.  Furthermore there
paulson@3485
    89
are a number of external utilities available.  These are started
wenzelm@3108
    90
uniformly via the \texttt{isatool} wrapper.
lcp@104
    91
wenzelm@3200
    92
Again, see the \emph{System Manual} for more information user
wenzelm@3200
    93
interfaces and utilities.
lcp@104
    94
lcp@104
    95
lcp@104
    96
\section{Ending a session}
lcp@104
    97
\begin{ttbox} 
wenzelm@3108
    98
quit    : unit -> unit
wenzelm@3108
    99
exit    : int -> unit
wenzelm@3108
   100
commit  : unit -> unit
lcp@104
   101
\end{ttbox}
lcp@322
   102
\begin{ttdescription}
wenzelm@3108
   103
\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
wenzelm@3108
   104
  the state.
lcp@104
   105
wenzelm@3108
   106
\item[\ttindexbold{exit}();] same as {\tt quit}, passing a return code
wenzelm@3108
   107
  to the operating system.
lcp@104
   108
wenzelm@3108
   109
\item[\ttindexbold{commit}();] saves the current state without ending
wenzelm@3108
   110
  the session, provided that the logic image is opened read-write.
lcp@322
   111
\end{ttdescription}
lcp@104
   112
wenzelm@3108
   113
Typing control-D also finishes the session in essentially the same way
wenzelm@3108
   114
as the sequence {\tt commit(); quit();} would.
lcp@104
   115
lcp@104
   116
lcp@322
   117
\section{Reading ML files}
lcp@322
   118
\index{files!reading}
lcp@104
   119
\begin{ttbox} 
clasohm@138
   120
cd              : string -> unit
clasohm@884
   121
pwd             : unit -> string
clasohm@138
   122
use             : string -> unit
clasohm@138
   123
time_use        : string -> unit
lcp@104
   124
\end{ttbox}
lcp@322
   125
Section~\ref{LoadingTheories} describes commands for loading theory files.
lcp@322
   126
\begin{ttdescription}
lcp@322
   127
\item[\ttindexbold{cd} "{\it dir}";]
lcp@322
   128
  changes the current directory to {\it dir}.  This is the default directory
lcp@322
   129
  for reading files and for writing temporary files.
lcp@104
   130
wenzelm@3108
   131
\item[\ttindexbold{pwd}();] returns the path of the current directory.
clasohm@884
   132
lcp@322
   133
\item[\ttindexbold{use} "$file$";]  
lcp@104
   134
reads the given {\it file} as input to the \ML{} session.  Reading a file
lcp@104
   135
of Isabelle commands is the usual way of replaying a proof.
lcp@104
   136
lcp@322
   137
\item[\ttindexbold{time_use} "$file$";]  
lcp@104
   138
performs {\tt use~"$file$"} and prints the total execution time.
lcp@322
   139
\end{ttdescription}
lcp@104
   140
lcp@104
   141
wenzelm@3108
   142
\section{Setting flags}
wenzelm@3108
   143
\begin{ttbox}
wenzelm@3108
   144
set     : bool ref -> bool
wenzelm@3108
   145
reset   : bool ref -> bool
wenzelm@3108
   146
toggle  : bool ref -> bool
wenzelm@3108
   147
\end{ttbox}\index{*set}\index{*reset}\index{*toggle}
paulson@3485
   148
These are some shorthands for manipulating boolean references.  The new
wenzelm@3108
   149
value is returned.
wenzelm@3108
   150
wenzelm@3108
   151
lcp@508
   152
\section{Printing of terms and theorems}\label{sec:printing-control}
lcp@322
   153
\index{printing control|(}
lcp@104
   154
Isabelle's pretty printer is controlled by a number of parameters.
lcp@104
   155
lcp@104
   156
\subsection{Printing limits}
lcp@104
   157
\begin{ttbox} 
lcp@104
   158
Pretty.setdepth  : int -> unit
lcp@104
   159
Pretty.setmargin : int -> unit
lcp@104
   160
print_depth      : int -> unit
lcp@104
   161
\end{ttbox}
lcp@508
   162
These set limits for terminal output.  See also {\tt goals_limit}, which
lcp@508
   163
limits the number of subgoals printed (page~\pageref{sec:goals-printing}).
lcp@104
   164
lcp@322
   165
\begin{ttdescription}
lcp@322
   166
\item[\ttindexbold{Pretty.setdepth} \(d\);]  
lcp@322
   167
  tells Isabelle's pretty printer to limit the printing depth to~$d$.  This
lcp@322
   168
  affects Isabelle's display of theorems and terms.  The default value
lcp@322
   169
  is~0, which permits printing to an arbitrary depth.  Useful values for
lcp@322
   170
  $d$ are~10 and~20.
lcp@104
   171
lcp@322
   172
\item[\ttindexbold{Pretty.setmargin} \(m\);]  
lcp@322
   173
  tells Isabelle's pretty printer to assume a right margin (page width)
lcp@322
   174
  of~$m$.  The initial margin is~80.
lcp@104
   175
lcp@322
   176
\item[\ttindexbold{print_depth} \(n\);]  
lcp@322
   177
  limits the printing depth of complex \ML{} values, such as theorems and
lcp@322
   178
  terms.  This command affects the \ML{} top level and its effect is
lcp@322
   179
  compiler-dependent.  Typically $n$ should be less than~10.
lcp@322
   180
\end{ttdescription}
lcp@104
   181
lcp@104
   182
lcp@508
   183
\subsection{Printing of hypotheses, brackets, types and sorts}
lcp@322
   184
\index{meta-assumptions!printing of}
lcp@322
   185
\index{types!printing of}\index{sorts!printing of}
lcp@104
   186
\begin{ttbox} 
lcp@508
   187
show_hyps     : bool ref \hfill{\bf initially true}
lcp@508
   188
show_brackets : bool ref \hfill{\bf initially false}
lcp@508
   189
show_types    : bool ref \hfill{\bf initially false}
lcp@508
   190
show_sorts    : bool ref \hfill{\bf initially false}
lcp@104
   191
\end{ttbox}
lcp@322
   192
These flags allow you to control how much information is displayed for
lcp@508
   193
terms and theorems.  The hypotheses are normally shown; superfluous
lcp@508
   194
parentheses are not.  Types and sorts are normally hidden.  Displaying
lcp@508
   195
types and sorts may explain why a polymorphic inference rule fails to
lcp@508
   196
resolve with some goal.
lcp@104
   197
lcp@322
   198
\begin{ttdescription}
lcp@322
   199
\item[\ttindexbold{show_hyps} := false;]   
lcp@332
   200
makes Isabelle show each meta-level hypothesis as a dot.
lcp@104
   201
lcp@508
   202
\item[\ttindexbold{show_brackets} := true;] 
lcp@508
   203
  makes Isabelle show full bracketing.  This reveals the
lcp@508
   204
  grouping of infix operators.
lcp@508
   205
lcp@322
   206
\item[\ttindexbold{show_types} := true;]
lcp@104
   207
makes Isabelle show types when printing a term or theorem.
lcp@104
   208
lcp@322
   209
\item[\ttindexbold{show_sorts} := true;]
lcp@1102
   210
makes Isabelle show both types and the sorts of type variables.  It does not
lcp@1102
   211
matter whether {\tt show_types} is also~{\tt true}. 
lcp@322
   212
\end{ttdescription}
lcp@104
   213
lcp@104
   214
lcp@104
   215
\subsection{$\eta$-contraction before printing}
lcp@104
   216
\begin{ttbox} 
lcp@104
   217
eta_contract: bool ref \hfill{\bf initially false}
lcp@104
   218
\end{ttbox}
lcp@104
   219
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
lcp@104
   220
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
lcp@104
   221
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
lcp@332
   222
unification frequently puts terms into a fully $\eta$-expanded form.  For
lcp@158
   223
example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
lcp@158
   224
$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
lcp@158
   225
form.
lcp@104
   226
lcp@322
   227
\begin{ttdescription}
lcp@322
   228
\item[\ttindexbold{eta_contract} := true;]
lcp@104
   229
makes Isabelle perform $\eta$-contractions before printing, so that
lcp@104
   230
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
lcp@104
   231
distinction between a term and its $\eta$-expanded form occasionally
lcp@104
   232
matters.
lcp@322
   233
\end{ttdescription}
lcp@322
   234
\index{printing control|)}
lcp@104
   235
lcp@104
   236
lcp@104
   237
\section{Displaying exceptions as error messages}
lcp@322
   238
\index{exceptions!printing of}
lcp@104
   239
\begin{ttbox} 
lcp@104
   240
print_exn: exn -> 'a
lcp@104
   241
\end{ttbox}
lcp@104
   242
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
lcp@104
   243
and {\tt RSN}, are called both interactively and from programs.  They
lcp@104
   244
indicate errors not by printing messages, but by raising exceptions.  For
lcp@322
   245
interactive use, \ML's reporting of an uncaught exception is 
lcp@322
   246
uninformative.  The Poly/ML function {\tt exception_trace} can generate a
lcp@322
   247
backtrace.\index{Poly/{\ML} compiler}
lcp@104
   248
lcp@322
   249
\begin{ttdescription}
lcp@104
   250
\item[\ttindexbold{print_exn} $e$] 
lcp@104
   251
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
lcp@322
   252
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
lcp@322
   253
$EXP$ is an expression that may raise an exception.
lcp@104
   254
lcp@104
   255
{\tt print_exn} can display the following common exceptions, which concern
lcp@104
   256
types, terms, theorems and theories, respectively.  Each carries a message
lcp@104
   257
and related information.
lcp@104
   258
\begin{ttbox} 
lcp@104
   259
exception TYPE   of string * typ list * term list
lcp@104
   260
exception TERM   of string * term list
lcp@104
   261
exception THM    of string * int * thm list
lcp@104
   262
exception THEORY of string * theory list
lcp@104
   263
\end{ttbox}
lcp@322
   264
\end{ttdescription}
lcp@322
   265
\begin{warn}
lcp@322
   266
  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
lcp@322
   267
  pretty printing information from the proof state last stored in the
lcp@322
   268
  subgoal module.  The appearance of the output thus depends upon the
lcp@322
   269
  theory used in the last interactive proof.
lcp@322
   270
\end{warn}
lcp@104
   271
lcp@104
   272
\index{sessions|)}