doc-src/Ref/introduction.tex
author wenzelm
Wed Mar 10 16:31:33 1999 +0100 (1999-03-10)
changeset 6343 97c697a32b73
parent 6067 0f8ab32093ae
child 6568 b38bc78d9a9d
permissions -rw-r--r--
updated;
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@4317
    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
wenzelm@4317
    37
object-logic already preloaded.
wenzelm@3108
    38
wenzelm@3108
    39
Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
wenzelm@3108
    40
has been added to your shell's search path, in order to avoid typing
wenzelm@3108
    41
full path specifications of the executable files.
wenzelm@3108
    42
wenzelm@3108
    43
The object-logic image to load may be also specified explicitly as an
wenzelm@4317
    44
argument to the {\tt isabelle} command, e.g.
wenzelm@3108
    45
\begin{ttbox}
wenzelm@3108
    46
isabelle FOL
wenzelm@3108
    47
\end{ttbox}
wenzelm@3108
    48
This should put you into the world of polymorphic first-order logic
wenzelm@3108
    49
(assuming that {\FOL} has been pre-built).
paulson@2225
    50
wenzelm@3108
    51
\index{saving your work|bold} Isabelle provides no means of storing
wenzelm@4317
    52
theorems or internal proof objects on files.  Theorems are simply part
wenzelm@4317
    53
of the \ML{} state.  To save your work between sessions, you must dump
wenzelm@4317
    54
the \ML{} system state to a file.  This is done automatically when
wenzelm@4317
    55
ending the session normally (e.g.\ by typing control-D), provided that
wenzelm@4317
    56
the image has been opened \emph{writable} in the first place.  The
wenzelm@4317
    57
standard object-logic images are usually read-only, so you probably
wenzelm@4317
    58
have to create a private working copy first.  For example, the
wenzelm@4317
    59
following shell command puts you into a writable Isabelle session of
wenzelm@4317
    60
name \texttt{Foo} that initially contains just \FOL:
wenzelm@3108
    61
\begin{ttbox}
wenzelm@3108
    62
isabelle FOL Foo
wenzelm@3108
    63
\end{ttbox}
wenzelm@3108
    64
Ending the \texttt{Foo} session with control-D will cause the complete
wenzelm@3108
    65
\ML{} world to be saved somewhere in your home directory\footnote{The
wenzelm@3108
    66
  default location is in \texttt{\~\relax/isabelle/heaps}, but this
paulson@3485
    67
  depends on your local configuration.}.  Make sure there is enough
wenzelm@3108
    68
space available! Then one may later continue at exactly the same point
wenzelm@3108
    69
by running
wenzelm@3108
    70
\begin{ttbox}
wenzelm@3108
    71
isabelle Foo  
wenzelm@3108
    72
\end{ttbox}
lcp@104
    73
wenzelm@6343
    74
More details about the \texttt{isabelle} command may be found in \emph{The
wenzelm@6343
    75
  Isabelle System Manual}.
wenzelm@3108
    76
wenzelm@3108
    77
\medskip Saving the state is not enough.  Record, on a file, the
wenzelm@3108
    78
top-level commands that generate your theories and proofs.  Such a
wenzelm@3108
    79
record allows you to replay the proofs whenever required, for instance
wenzelm@3108
    80
after making minor changes to the axioms.  Ideally, your record will
wenzelm@3108
    81
be somewhat intelligible to others as a formal description of your
wenzelm@3108
    82
work.
lcp@104
    83
wenzelm@3108
    84
\medskip There are more comfortable user interfaces than the
paulson@3485
    85
bare-bones \ML{} top-level run from a text terminal.  The
wenzelm@3108
    86
\texttt{Isabelle} executable (note the capital I) runs one such
wenzelm@3108
    87
interface, depending on your local configuration.  Furthermore there
paulson@3485
    88
are a number of external utilities available.  These are started
wenzelm@4317
    89
uniformly via the \texttt{isatool} wrapper.  See the \emph{System
wenzelm@4317
    90
  Manual} for more information user interfaces and utilities.
lcp@104
    91
lcp@104
    92
lcp@104
    93
\section{Ending a session}
lcp@104
    94
\begin{ttbox} 
wenzelm@3108
    95
quit    : unit -> unit
wenzelm@3108
    96
exit    : int -> unit
wenzelm@6067
    97
commit  : unit -> bool
lcp@104
    98
\end{ttbox}
lcp@322
    99
\begin{ttdescription}
wenzelm@3108
   100
\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
wenzelm@3108
   101
  the state.
wenzelm@4317
   102
  
wenzelm@4317
   103
\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
wenzelm@4317
   104
  code \(i\) to the operating system.
lcp@104
   105
wenzelm@3108
   106
\item[\ttindexbold{commit}();] saves the current state without ending
wenzelm@6067
   107
  the session, provided that the logic image is opened read-write;
wenzelm@6067
   108
  return value {\tt false} indicates an error.
lcp@322
   109
\end{ttdescription}
lcp@104
   110
wenzelm@3108
   111
Typing control-D also finishes the session in essentially the same way
wenzelm@3108
   112
as the sequence {\tt commit(); quit();} would.
lcp@104
   113
lcp@104
   114
lcp@322
   115
\section{Reading ML files}
lcp@322
   116
\index{files!reading}
lcp@104
   117
\begin{ttbox} 
clasohm@138
   118
cd              : string -> unit
clasohm@884
   119
pwd             : unit -> string
clasohm@138
   120
use             : string -> unit
clasohm@138
   121
time_use        : string -> unit
lcp@104
   122
\end{ttbox}
lcp@322
   123
\begin{ttdescription}
wenzelm@4317
   124
\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
wenzelm@4317
   125
  {\it dir}.  This is the default directory for reading files.
wenzelm@4317
   126
  
wenzelm@4317
   127
\item[\ttindexbold{pwd}();] returns the full path of the current
wenzelm@4317
   128
  directory.
clasohm@884
   129
lcp@322
   130
\item[\ttindexbold{use} "$file$";]  
lcp@104
   131
reads the given {\it file} as input to the \ML{} session.  Reading a file
lcp@104
   132
of Isabelle commands is the usual way of replaying a proof.
lcp@104
   133
lcp@322
   134
\item[\ttindexbold{time_use} "$file$";]  
lcp@104
   135
performs {\tt use~"$file$"} and prints the total execution time.
lcp@322
   136
\end{ttdescription}
lcp@104
   137
wenzelm@6343
   138
The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
wenzelm@6343
   139
commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
wenzelm@6343
   140
expanded appropriately.  Note that \texttt{\~\relax} abbreviates
wenzelm@6343
   141
\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
wenzelm@6343
   142
\texttt{\$ISABELLE_HOME}.  Section~\ref{LoadingTheories} describes commands
wenzelm@6343
   143
for loading theory files.
wenzelm@4274
   144
lcp@104
   145
wenzelm@3108
   146
\section{Setting flags}
wenzelm@3108
   147
\begin{ttbox}
wenzelm@3108
   148
set     : bool ref -> bool
wenzelm@3108
   149
reset   : bool ref -> bool
wenzelm@3108
   150
toggle  : bool ref -> bool
wenzelm@3108
   151
\end{ttbox}\index{*set}\index{*reset}\index{*toggle}
paulson@3485
   152
These are some shorthands for manipulating boolean references.  The new
wenzelm@3108
   153
value is returned.
wenzelm@3108
   154
wenzelm@3108
   155
lcp@508
   156
\section{Printing of terms and theorems}\label{sec:printing-control}
lcp@322
   157
\index{printing control|(}
lcp@104
   158
Isabelle's pretty printer is controlled by a number of parameters.
lcp@104
   159
lcp@104
   160
\subsection{Printing limits}
lcp@104
   161
\begin{ttbox} 
lcp@104
   162
Pretty.setdepth  : int -> unit
lcp@104
   163
Pretty.setmargin : int -> unit
lcp@104
   164
print_depth      : int -> unit
lcp@104
   165
\end{ttbox}
wenzelm@4317
   166
These set limits for terminal output.  See also {\tt goals_limit},
wenzelm@4317
   167
which limits the number of subgoals printed
wenzelm@4317
   168
(\S\ref{sec:goals-printing}).
lcp@104
   169
lcp@322
   170
\begin{ttdescription}
lcp@322
   171
\item[\ttindexbold{Pretty.setdepth} \(d\);]  
lcp@322
   172
  tells Isabelle's pretty printer to limit the printing depth to~$d$.  This
lcp@322
   173
  affects Isabelle's display of theorems and terms.  The default value
lcp@322
   174
  is~0, which permits printing to an arbitrary depth.  Useful values for
lcp@322
   175
  $d$ are~10 and~20.
lcp@104
   176
lcp@322
   177
\item[\ttindexbold{Pretty.setmargin} \(m\);]  
lcp@322
   178
  tells Isabelle's pretty printer to assume a right margin (page width)
wenzelm@4317
   179
  of~$m$.  The initial margin is~76.
lcp@104
   180
lcp@322
   181
\item[\ttindexbold{print_depth} \(n\);]  
lcp@322
   182
  limits the printing depth of complex \ML{} values, such as theorems and
lcp@322
   183
  terms.  This command affects the \ML{} top level and its effect is
lcp@322
   184
  compiler-dependent.  Typically $n$ should be less than~10.
lcp@322
   185
\end{ttdescription}
lcp@104
   186
lcp@104
   187
wenzelm@4317
   188
\subsection{Printing of hypotheses, brackets, types etc.}
lcp@322
   189
\index{meta-assumptions!printing of}
lcp@322
   190
\index{types!printing of}\index{sorts!printing of}
lcp@104
   191
\begin{ttbox} 
lcp@508
   192
show_hyps     : bool ref \hfill{\bf initially true}
wenzelm@6343
   193
show_tags     : bool ref \hfill{\bf initially false}
lcp@508
   194
show_brackets : bool ref \hfill{\bf initially false}
lcp@508
   195
show_types    : bool ref \hfill{\bf initially false}
lcp@508
   196
show_sorts    : bool ref \hfill{\bf initially false}
wenzelm@4317
   197
show_consts   : bool ref \hfill{\bf initially false}
wenzelm@4543
   198
long_names    : bool ref \hfill{\bf initially false}
lcp@104
   199
\end{ttbox}
lcp@322
   200
These flags allow you to control how much information is displayed for
wenzelm@4317
   201
types, terms and theorems.  The hypotheses of theorems \emph{are}
wenzelm@4317
   202
normally shown.  Superfluous parentheses of types and terms are not.
wenzelm@4317
   203
Types and sorts of variables are normally hidden.
wenzelm@4317
   204
wenzelm@4317
   205
Note that displaying types and sorts may explain why a polymorphic
wenzelm@4317
   206
inference rule fails to resolve with some goal, or why a rewrite rule
wenzelm@4317
   207
does not apply as expected.
lcp@104
   208
lcp@322
   209
\begin{ttdescription}
wenzelm@4543
   210
wenzelm@4317
   211
\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
wenzelm@4317
   212
  meta-level hypothesis as a dot.
wenzelm@4317
   213
  
wenzelm@6343
   214
\item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
wenzelm@6343
   215
  (which are basically just comments that may be attached by some tools).
wenzelm@6343
   216
  
wenzelm@4317
   217
\item[set \ttindexbold{show_brackets};] makes Isabelle show full
wenzelm@4317
   218
  bracketing.  In particular, this reveals the grouping of infix
wenzelm@4317
   219
  operators.
wenzelm@4317
   220
  
wenzelm@4317
   221
\item[set \ttindexbold{show_types};] makes Isabelle show types when
wenzelm@4317
   222
  printing a term or theorem.
wenzelm@4317
   223
  
wenzelm@4317
   224
\item[set \ttindexbold{show_sorts};] makes Isabelle show both types
wenzelm@4317
   225
  and the sorts of type variables, independently of the value of
wenzelm@4317
   226
  \texttt{show_types}.
wenzelm@4543
   227
wenzelm@4317
   228
\item[set \ttindexbold{show_consts};] makes Isabelle show types of
wenzelm@4317
   229
  constants, provided that showing of types is enabled at all.  This
wenzelm@4317
   230
  is supported for printing of proof states only.  Note that the
wenzelm@4317
   231
  output can be enormous as polymorphic constants often occur at
wenzelm@4317
   232
  several different type instances.
lcp@508
   233
wenzelm@4543
   234
\item[set \ttindexbold{long_names};] forces names of all objects
wenzelm@4543
   235
  (types, constants, theorems, etc.) to be printed in their fully
wenzelm@4543
   236
  qualified internal form.
wenzelm@4543
   237
lcp@322
   238
\end{ttdescription}
lcp@104
   239
lcp@104
   240
lcp@104
   241
\subsection{$\eta$-contraction before printing}
lcp@104
   242
\begin{ttbox} 
lcp@104
   243
eta_contract: bool ref \hfill{\bf initially false}
lcp@104
   244
\end{ttbox}
lcp@104
   245
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
lcp@104
   246
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
lcp@104
   247
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
lcp@332
   248
unification frequently puts terms into a fully $\eta$-expanded form.  For
lcp@158
   249
example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
lcp@158
   250
$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
lcp@158
   251
form.
lcp@104
   252
lcp@322
   253
\begin{ttdescription}
wenzelm@4317
   254
\item[set \ttindexbold{eta_contract};]
lcp@104
   255
makes Isabelle perform $\eta$-contractions before printing, so that
lcp@104
   256
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
lcp@104
   257
distinction between a term and its $\eta$-expanded form occasionally
lcp@104
   258
matters.
lcp@322
   259
\end{ttdescription}
lcp@322
   260
\index{printing control|)}
lcp@104
   261
wenzelm@4317
   262
\section{Diagnostic messages}
wenzelm@4317
   263
\index{error messages}
wenzelm@4317
   264
\index{warnings}
wenzelm@4317
   265
wenzelm@4317
   266
Isabelle conceptually provides three output channels for different
wenzelm@4317
   267
kinds of messages: ordinary text, warnings, errors.  Depending on the
wenzelm@4317
   268
user interface involved, these messages may appear in different text
wenzelm@4317
   269
styles or colours, even within separate windows.
wenzelm@4317
   270
wenzelm@4317
   271
The default setup of an \texttt{isabelle} terminal session is as
wenzelm@4317
   272
follows: plain output of ordinary text, warnings prefixed by
wenzelm@4317
   273
\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
wenzelm@4317
   274
typical warning would look like this:
wenzelm@4317
   275
\begin{ttbox}
wenzelm@4317
   276
\#\#\# Beware the Jabberwock, my son!
wenzelm@4317
   277
\#\#\# The jaws that bite, the claws that catch!
wenzelm@4317
   278
\#\#\# Beware the Jubjub Bird, and shun
wenzelm@4317
   279
\#\#\# The frumious Bandersnatch!
wenzelm@4317
   280
\end{ttbox}
wenzelm@4317
   281
wenzelm@4317
   282
\texttt{ML} programs may output diagnostic messages using the
wenzelm@4317
   283
following functions:
wenzelm@4317
   284
\begin{ttbox}
wenzelm@4317
   285
writeln : string -> unit
wenzelm@4317
   286
warning : string -> unit
wenzelm@4317
   287
error   : string -> 'a
wenzelm@4317
   288
\end{ttbox}
wenzelm@4317
   289
Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
wenzelm@4317
   290
after having output the text, while \ttindex{writeln} and
wenzelm@4317
   291
\ttindex{warning} resume normal program execution.
wenzelm@4317
   292
lcp@104
   293
lcp@104
   294
\section{Displaying exceptions as error messages}
lcp@322
   295
\index{exceptions!printing of}
lcp@104
   296
\begin{ttbox} 
lcp@104
   297
print_exn: exn -> 'a
lcp@104
   298
\end{ttbox}
lcp@104
   299
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
lcp@104
   300
and {\tt RSN}, are called both interactively and from programs.  They
lcp@104
   301
indicate errors not by printing messages, but by raising exceptions.  For
wenzelm@4317
   302
interactive use, \ML's reporting of an uncaught exception may be
lcp@322
   303
uninformative.  The Poly/ML function {\tt exception_trace} can generate a
lcp@322
   304
backtrace.\index{Poly/{\ML} compiler}
lcp@104
   305
lcp@322
   306
\begin{ttdescription}
lcp@104
   307
\item[\ttindexbold{print_exn} $e$] 
lcp@104
   308
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
lcp@322
   309
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
lcp@322
   310
$EXP$ is an expression that may raise an exception.
lcp@104
   311
lcp@104
   312
{\tt print_exn} can display the following common exceptions, which concern
lcp@104
   313
types, terms, theorems and theories, respectively.  Each carries a message
lcp@104
   314
and related information.
lcp@104
   315
\begin{ttbox} 
lcp@104
   316
exception TYPE   of string * typ list * term list
lcp@104
   317
exception TERM   of string * term list
lcp@104
   318
exception THM    of string * int * thm list
lcp@104
   319
exception THEORY of string * theory list
lcp@104
   320
\end{ttbox}
lcp@322
   321
\end{ttdescription}
lcp@322
   322
\begin{warn}
lcp@322
   323
  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
lcp@322
   324
  pretty printing information from the proof state last stored in the
lcp@322
   325
  subgoal module.  The appearance of the output thus depends upon the
lcp@322
   326
  theory used in the last interactive proof.
lcp@322
   327
\end{warn}
lcp@104
   328
lcp@104
   329
\index{sessions|)}
wenzelm@5371
   330
wenzelm@5371
   331
wenzelm@5371
   332
%%% Local Variables: 
wenzelm@5371
   333
%%% mode: latex
wenzelm@5371
   334
%%% TeX-master: "ref"
wenzelm@5371
   335
%%% End: