doc-src/Ref/introduction.tex
author lcp
Mon Mar 21 11:02:57 1994 +0100 (1994-03-21)
changeset 286 e7efbf03562b
parent 159 3d0324f9417b
child 322 bacfaeeea007
permissions -rw-r--r--
first draft of Springer book
lcp@104
     1
%% $Id$
lcp@286
     2
\chapter{Basic Use of Isabelle}\index{sessions|(} 
lcp@286
     3
The Reference Manual is a comprehensive description of Isabelle, including
lcp@286
     4
all commands, functions and packages.  It really is intended for reference,
lcp@286
     5
perhaps for browsing, but not for reading through.  It is not a tutorial,
lcp@286
     6
but assumes familiarity with the basic concepts of Isabelle.
lcp@104
     7
lcp@286
     8
When you are looking for a way of performing some task, scan the Table of
lcp@286
     9
Contents for a relevant heading.  Functions are organized by their purpose,
lcp@286
    10
by their operands (subgoals, tactics, theorems), and by their usefulness.
lcp@286
    11
In each section, basic functions appear first, then advanced functions, and
lcp@286
    12
finally esoteric functions.
lcp@104
    13
lcp@104
    14
The Index provides an alphabetical listing.  Page numbers of definitions
lcp@104
    15
are printed in {\bf bold}, passing references in Roman type.  Use the Index
lcp@104
    16
when you are looking for the 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}
lcp@104
    23
\index{sessions!saving|bold}\index{saving your work|bold}
lcp@104
    24
Isabelle provides no means of storing theorems or proofs on files.
lcp@104
    25
Theorems are simply part of the \ML{} state and are named by \ML{}
lcp@104
    26
identifiers.  To save your work between sessions, you must save a copy of
lcp@104
    27
the \ML{} image.  The procedure for doing so is compiler-dependent:
lcp@286
    28
\begin{itemize}\index{Poly/\ML}
lcp@104
    29
\item At the end of a session, Poly/\ML{} saves the state, provided you have
lcp@104
    30
created a database for your own use.  You can create a database by copying
lcp@104
    31
an existing one, or by calling the Poly/\ML{} function {\tt make_database};
lcp@104
    32
the latter course uses much less disc space.  Note that a Poly/\ML{}
lcp@104
    33
database {\bf does not} save the contents of references, such as the
lcp@104
    34
current state of a backward proof.
lcp@104
    35
lcp@104
    36
\item With New Jersey \ML{} you must save the state explicitly before
wenzelm@149
    37
ending the session.  While a Poly/\ML{} database can be small, a New Jersey
lcp@104
    38
image occupies several megabytes.
lcp@104
    39
\end{itemize}
lcp@104
    40
See your \ML{} compiler's documentation for full instructions on saving the
lcp@104
    41
state.
lcp@104
    42
lcp@104
    43
Saving the state is not enough.  Record, on a file, the top-level commands
lcp@104
    44
that generate your theories and proofs.  Such a record allows you to replay
lcp@104
    45
the proofs whenever required, for instance after making minor changes to
lcp@104
    46
the axioms.  Ideally, your record will be intelligible to others as a
lcp@104
    47
formal description of your work.
lcp@104
    48
lcp@104
    49
Since Isabelle's user interface is the \ML{} top level, some kind of window
lcp@104
    50
support is essential.  One window displays the Isabelle session, while the
lcp@104
    51
other displays a file --- your proof record --- being edited.  Some people
lcp@104
    52
use a screen editor such as Emacs, which supports windows and can manage
lcp@104
    53
interactive sessions.  Others prefer to use a workstation running the X Window
lcp@104
    54
System.
lcp@104
    55
lcp@104
    56
lcp@104
    57
\section{Ending a session}
lcp@104
    58
\index{sessions!ending|bold}
lcp@104
    59
\begin{ttbox} 
lcp@104
    60
quit     : unit -> unit
lcp@104
    61
commit   : unit -> unit \hfill{\bf Poly/ML only}
lcp@104
    62
exportML : string -> bool \hfill{\bf New Jersey ML only}
lcp@104
    63
\end{ttbox}
lcp@104
    64
\begin{description}
lcp@104
    65
\item[\ttindexbold{quit}();]  
lcp@104
    66
aborts the Isabelle session, without saving the state.
lcp@104
    67
lcp@104
    68
\item[\ttindexbold{commit}();]  saves the current state in your
lcp@104
    69
Poly/\ML{} database without finishing the session.  Values of reference
lcp@286
    70
variables are lost, so never do this during an interactive
lcp@286
    71
proof!\index{Poly/\ML} 
lcp@104
    72
lcp@104
    73
\item[\ttindexbold{exportML} \tt"{\it file}";]  saves an
lcp@104
    74
image of your session to the given {\it file}.
lcp@104
    75
\end{description}
lcp@104
    76
lcp@104
    77
\begin{warn}
lcp@104
    78
Typing control-D also finishes the session, but its effect is
lcp@104
    79
compiler-dependent.  Poly/\ML{} will then save the state, if you have a
lcp@104
    80
private database.  New Jersey \ML{} will discard the state!
lcp@104
    81
\end{warn}
lcp@104
    82
lcp@104
    83
lcp@104
    84
\section{Reading files of proofs and theories}
lcp@286
    85
\index{files!reading|bold}
lcp@104
    86
\begin{ttbox} 
clasohm@138
    87
cd              : string -> unit
clasohm@138
    88
use             : string -> unit
clasohm@138
    89
use_thy         : string -> unit
clasohm@138
    90
time_use        : string -> unit
clasohm@138
    91
time_use_thy    : string -> unit
clasohm@138
    92
update          : unit -> unit
clasohm@138
    93
loadpath        : string list ref
lcp@104
    94
\end{ttbox}
lcp@104
    95
\begin{description}
lcp@104
    96
\item[\ttindexbold{cd} \tt"{\it dir}";]  changes to {\it dir\/} the default
lcp@104
    97
directory for reading files.
lcp@104
    98
lcp@104
    99
\item[\ttindexbold{use} \tt"$file$";]  
lcp@104
   100
reads the given {\it file} as input to the \ML{} session.  Reading a file
lcp@104
   101
of Isabelle commands is the usual way of replaying a proof.
lcp@104
   102
lcp@159
   103
\item[\ttindexbold{use_thy} \tt"$tname$";] 
lcp@159
   104
  reads a theory definition from file {\it tname}{\tt.thy} and also reads
lcp@159
   105
  {\ML} commands from the file {\it tname}{\tt.ML}, if it exists.  If
lcp@159
   106
  theory {\it tname} depends on theories that have not been read already,
lcp@159
   107
  then it loads these beforehand.  See Chapter~\ref{theories} for
lcp@159
   108
  details.
lcp@104
   109
lcp@104
   110
\item[\ttindexbold{time_use} \tt"$file$";]  
lcp@104
   111
performs {\tt use~"$file$"} and prints the total execution time.
lcp@104
   112
lcp@104
   113
\item[\ttindexbold{time_use_thy} \tt"$tname$";]  
lcp@104
   114
performs {\tt use_thy "$tname$"} and prints the total execution time.
clasohm@138
   115
clasohm@138
   116
\item[\ttindexbold{update} \tt();]  
clasohm@138
   117
reads all theories that have changed since the last time they have been read.
clasohm@138
   118
See Chapter~\ref{theories} for details.
clasohm@138
   119
lcp@286
   120
\item[\ttindexbold{loadpath}] 
lcp@286
   121
  contains a list of paths that is used by {\tt use_thy} and {\tt update}
lcp@286
   122
  to find {\it tname}{\tt.ML} and {\it tname}{\tt.thy}.  See
lcp@286
   123
  Chapter~\ref{theories} for details.
lcp@104
   124
\end{description}
lcp@104
   125
lcp@104
   126
lcp@104
   127
\section{Printing of terms and theorems}
lcp@104
   128
\index{printing!flags|bold}
lcp@104
   129
Isabelle's pretty printer is controlled by a number of parameters.
lcp@104
   130
lcp@104
   131
\subsection{Printing limits}
lcp@104
   132
\begin{ttbox} 
lcp@104
   133
Pretty.setdepth  : int -> unit
lcp@104
   134
Pretty.setmargin : int -> unit
lcp@104
   135
print_depth      : int -> unit
lcp@104
   136
\end{ttbox}
lcp@104
   137
These set limits for terminal output.
lcp@104
   138
lcp@104
   139
\begin{description}
lcp@104
   140
\item[\ttindexbold{Pretty.setdepth} \(d\);]  tells
lcp@104
   141
Isabelle's pretty printer to limit the printing depth to~$d$.  This affects
lcp@104
   142
Isabelle's display of theorems and terms.  The default value is~0, which
lcp@104
   143
permits printing to an arbitrary depth.  Useful values for $d$ are~10 and~20.
lcp@104
   144
lcp@104
   145
\item[\ttindexbold{Pretty.setmargin} \(m\);]  tells
lcp@104
   146
Isabelle's pretty printer to assume a right margin (page width) of~$m$.
lcp@104
   147
The initial margin is~80.
lcp@104
   148
lcp@104
   149
\item[\ttindexbold{print_depth} \(n\);]  limits
lcp@104
   150
the printing depth of complex \ML{} values, such as theorems and terms.
lcp@104
   151
This command affects the \ML{} top level and its effect is
lcp@104
   152
compiler-dependent.  Typically $n$ should be less than~10.
lcp@104
   153
\end{description}
lcp@104
   154
lcp@104
   155
lcp@104
   156
\subsection{Printing of meta-level hypotheses}
lcp@104
   157
\index{hypotheses!meta-level!printing of|bold}
lcp@104
   158
\begin{ttbox} 
lcp@104
   159
show_hyps: bool ref \hfill{\bf initially true}
lcp@104
   160
\end{ttbox}
lcp@104
   161
A theorem's hypotheses are normally displayed, since such dependence is
lcp@104
   162
important.  If this information becomes too verbose, however, it can be
lcp@104
   163
switched off;  each hypothesis is then displayed as a dot.
lcp@104
   164
\begin{description}
lcp@104
   165
\item[\ttindexbold{show_hyps} \tt:= true;]   
lcp@104
   166
makes Isabelle show meta-level hypotheses when printing a theorem; setting
lcp@104
   167
it to {\tt false} suppresses them.
lcp@104
   168
\end{description}
lcp@104
   169
lcp@104
   170
lcp@104
   171
\subsection{Printing of types and sorts}
lcp@104
   172
\begin{ttbox} 
lcp@104
   173
show_types: bool ref \hfill{\bf initially false}
lcp@104
   174
show_sorts: bool ref \hfill{\bf initially false}
lcp@104
   175
\end{ttbox}
lcp@104
   176
These control Isabelle's display of types and sorts.  Normally terms are
lcp@104
   177
printed without type and sorts because they are verbose.  Occasionally you
lcp@104
   178
may require this information, say to discover why a polymorphic inference rule
lcp@104
   179
fails to resolve with some goal.
lcp@104
   180
lcp@104
   181
\begin{description}
lcp@104
   182
\item[\ttindexbold{show_types} \tt:= true;]\index{types}
lcp@104
   183
makes Isabelle show types when printing a term or theorem.
lcp@104
   184
lcp@104
   185
\item[\ttindexbold{show_sorts} \tt:= true;]\index{sorts}
lcp@104
   186
makes Isabelle show the sorts of type variables.  It has no effect unless
lcp@104
   187
{\tt show_types} is~{\tt true}. 
lcp@104
   188
\end{description}
lcp@104
   189
lcp@104
   190
lcp@104
   191
\subsection{$\eta$-contraction before printing}
lcp@104
   192
\begin{ttbox} 
lcp@104
   193
eta_contract: bool ref \hfill{\bf initially false}
lcp@104
   194
\end{ttbox}
lcp@104
   195
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
lcp@104
   196
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
lcp@104
   197
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
lcp@158
   198
unification occasionally puts terms into a fully $\eta$-expanded form.  For
lcp@158
   199
example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
lcp@158
   200
$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
lcp@158
   201
form.
lcp@104
   202
lcp@104
   203
\begin{description}
lcp@104
   204
\item[\ttindexbold{eta_contract} \tt:= true;]
lcp@104
   205
makes Isabelle perform $\eta$-contractions before printing, so that
lcp@104
   206
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
lcp@104
   207
distinction between a term and its $\eta$-expanded form occasionally
lcp@104
   208
matters.
lcp@104
   209
\end{description}
lcp@104
   210
lcp@104
   211
lcp@104
   212
\section{Displaying exceptions as error messages}
lcp@104
   213
\index{printing!exceptions|bold}\index{exceptions|bold}
lcp@104
   214
\begin{ttbox} 
lcp@104
   215
print_exn: exn -> 'a
lcp@104
   216
\end{ttbox}
lcp@104
   217
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
lcp@104
   218
and {\tt RSN}, are called both interactively and from programs.  They
lcp@104
   219
indicate errors not by printing messages, but by raising exceptions.  For
lcp@104
   220
interactive use, \ML's reporting of an uncaught exception is most
lcp@104
   221
uninformative.
lcp@104
   222
lcp@104
   223
\begin{description}
lcp@104
   224
\item[\ttindexbold{print_exn} $e$] 
lcp@104
   225
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
lcp@104
   226
Typical usage is~\hbox{\tt \ldots{} handle e => print_exn e;}, where
lcp@104
   227
\ldots{} is an expression that may raise an exception.
lcp@104
   228
lcp@104
   229
{\tt print_exn} can display the following common exceptions, which concern
lcp@104
   230
types, terms, theorems and theories, respectively.  Each carries a message
lcp@104
   231
and related information.
lcp@104
   232
\begin{ttbox} 
lcp@104
   233
exception TYPE   of string * typ list * term list
lcp@104
   234
exception TERM   of string * term list
lcp@104
   235
exception THM    of string * int * thm list
lcp@104
   236
exception THEORY of string * theory list
lcp@104
   237
\end{ttbox}
lcp@104
   238
{\tt print_exn} calls \ttindex{prin} to print terms.  This obtains pretty
lcp@104
   239
printing information from the proof state last stored in the subgoal
lcp@104
   240
module, and will fail if no interactive proof has begun in the current
lcp@104
   241
session.
lcp@104
   242
\end{description}
lcp@104
   243
lcp@104
   244
lcp@104
   245
\section{Shell scripts}
lcp@104
   246
\index{shell scripts|bold}
lcp@104
   247
The following files are distributed with Isabelle, and work under
lcp@104
   248
Unix$^{\rm TM}$.  They can be executed as commands to the Unix shell.  Some
lcp@104
   249
of them depend upon shell environment variables.
lcp@104
   250
\begin{description}
lcp@104
   251
\item[\ttindexbold{make-all} $switches$] 
lcp@286
   252
  compiles the Isabelle system, when executed on the source directory.
lcp@286
   253
  Environment variables specify which \ML{} compiler to use.  These
lcp@286
   254
  variables, and the {\it switches}, are documented on the file itself.
lcp@104
   255
lcp@104
   256
\item[\ttindexbold{teeinput} $program$] 
lcp@104
   257
executes the {\it program}, while piping the standard input to a log file
lcp@104
   258
designated by the \verb|$LISTEN| environment variable.  Normally the
lcp@104
   259
program is Isabelle, and the log file receives a copy of all the Isabelle
lcp@104
   260
commands.
lcp@104
   261
lcp@104
   262
\item[\ttindexbold{xlisten} $program$] 
lcp@104
   263
  is a trivial `user interface' for the X Window System.  It creates two
lcp@104
   264
  windows using {\tt xterm}.  One executes an interactive session via
lcp@104
   265
  \hbox{\tt teeinput $program$}, while the other displays the log file.  To
lcp@104
   266
  make a proof record, simply paste lines from the log file into an editor
lcp@104
   267
  window.
lcp@104
   268
lcp@104
   269
\item[\ttindexbold{expandshort} $files$] 
lcp@104
   270
  reads the {\it files\/} and replaces all occurrences of the shorthand
lcp@286
   271
  commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the
lcp@286
   272
  corresponding full commands.  Shorthand commands should appear one
lcp@104
   273
  per line.  The old versions of the files
lcp@104
   274
  are renamed to have the suffix~\verb'~~'.
lcp@104
   275
\end{description}
lcp@104
   276
lcp@104
   277
\index{sessions|)}