doc-src/Ref/introduction.tex
author lcp
Fri Apr 22 18:18:37 1994 +0200 (1994-04-22)
changeset 332 01b87a921967
parent 322 bacfaeeea007
child 508 d8b6999ca364
permissions -rw-r--r--
final Springer copy
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@322
    12
finally esoteric functions.  Use the Index when you are looking for the
lcp@322
    13
definition of a particular Isabelle function.
lcp@104
    14
lcp@286
    15
A few examples are presented.  Many examples files are distributed with
lcp@286
    16
Isabelle, however; please experiment interactively.
lcp@104
    17
lcp@104
    18
lcp@104
    19
\section{Basic interaction with Isabelle}
lcp@322
    20
\index{saving your work|bold}
lcp@104
    21
Isabelle provides no means of storing theorems or proofs on files.
lcp@104
    22
Theorems are simply part of the \ML{} state and are named by \ML{}
lcp@104
    23
identifiers.  To save your work between sessions, you must save a copy of
lcp@104
    24
the \ML{} image.  The procedure for doing so is compiler-dependent:
lcp@322
    25
\begin{itemize}\index{Poly/{\ML} compiler}
lcp@322
    26
\item At the end of a session, Poly/\ML{} saves the state, provided you
lcp@322
    27
  have created a database for your own use.  You can create a database by
lcp@322
    28
  copying an existing one, or by calling the Poly/\ML{} function {\tt
lcp@322
    29
    make_database}; the latter course uses much less disc space.  A
lcp@322
    30
  Poly/\ML{} database {\em does not\/} save the contents of references,
lcp@322
    31
  such as the current state of a backward proof.
lcp@104
    32
lcp@104
    33
\item With New Jersey \ML{} you must save the state explicitly before
wenzelm@149
    34
ending the session.  While a Poly/\ML{} database can be small, a New Jersey
lcp@104
    35
image occupies several megabytes.
lcp@104
    36
\end{itemize}
lcp@104
    37
See your \ML{} compiler's documentation for full instructions on saving the
lcp@104
    38
state.
lcp@104
    39
lcp@104
    40
Saving the state is not enough.  Record, on a file, the top-level commands
lcp@104
    41
that generate your theories and proofs.  Such a record allows you to replay
lcp@104
    42
the proofs whenever required, for instance after making minor changes to
lcp@104
    43
the axioms.  Ideally, your record will be intelligible to others as a
lcp@104
    44
formal description of your work.
lcp@104
    45
lcp@104
    46
Since Isabelle's user interface is the \ML{} top level, some kind of window
lcp@104
    47
support is essential.  One window displays the Isabelle session, while the
lcp@322
    48
other displays a file --- your proof record --- being edited.  The Emacs
lcp@322
    49
editor supports windows and can manage interactive sessions.
lcp@104
    50
lcp@104
    51
lcp@104
    52
\section{Ending a session}
lcp@104
    53
\begin{ttbox} 
lcp@104
    54
quit     : unit -> unit
lcp@104
    55
commit   : unit -> unit \hfill{\bf Poly/ML only}
lcp@104
    56
exportML : string -> bool \hfill{\bf New Jersey ML only}
lcp@104
    57
\end{ttbox}
lcp@322
    58
\begin{ttdescription}
lcp@104
    59
\item[\ttindexbold{quit}();]  
lcp@104
    60
aborts the Isabelle session, without saving the state.
lcp@104
    61
lcp@322
    62
\item[\ttindexbold{commit}();] 
lcp@322
    63
  saves the current state in your Poly/\ML{} database without ending the
lcp@322
    64
  session.  The contents of references are lost, so never do this during an
lcp@322
    65
  interactive proof!\index{Poly/{\ML} compiler}
lcp@104
    66
lcp@322
    67
\item[\ttindexbold{exportML} "{\it file}";]  saves an
lcp@104
    68
image of your session to the given {\it file}.
lcp@322
    69
\end{ttdescription}
lcp@104
    70
lcp@104
    71
\begin{warn}
lcp@104
    72
Typing control-D also finishes the session, but its effect is
lcp@104
    73
compiler-dependent.  Poly/\ML{} will then save the state, if you have a
lcp@104
    74
private database.  New Jersey \ML{} will discard the state!
lcp@104
    75
\end{warn}
lcp@104
    76
lcp@104
    77
lcp@322
    78
\section{Reading ML files}
lcp@322
    79
\index{files!reading}
lcp@104
    80
\begin{ttbox} 
clasohm@138
    81
cd              : string -> unit
clasohm@138
    82
use             : string -> unit
clasohm@138
    83
time_use        : string -> unit
lcp@104
    84
\end{ttbox}
lcp@322
    85
Section~\ref{LoadingTheories} describes commands for loading theory files.
lcp@322
    86
\begin{ttdescription}
lcp@322
    87
\item[\ttindexbold{cd} "{\it dir}";]
lcp@322
    88
  changes the current directory to {\it dir}.  This is the default directory
lcp@322
    89
  for reading files and for writing temporary files.
lcp@104
    90
lcp@322
    91
\item[\ttindexbold{use} "$file$";]  
lcp@104
    92
reads the given {\it file} as input to the \ML{} session.  Reading a file
lcp@104
    93
of Isabelle commands is the usual way of replaying a proof.
lcp@104
    94
lcp@322
    95
\item[\ttindexbold{time_use} "$file$";]  
lcp@104
    96
performs {\tt use~"$file$"} and prints the total execution time.
lcp@322
    97
\end{ttdescription}
lcp@104
    98
lcp@104
    99
lcp@104
   100
\section{Printing of terms and theorems}
lcp@322
   101
\index{printing control|(}
lcp@104
   102
Isabelle's pretty printer is controlled by a number of parameters.
lcp@104
   103
lcp@104
   104
\subsection{Printing limits}
lcp@104
   105
\begin{ttbox} 
lcp@104
   106
Pretty.setdepth  : int -> unit
lcp@104
   107
Pretty.setmargin : int -> unit
lcp@104
   108
print_depth      : int -> unit
lcp@104
   109
\end{ttbox}
lcp@104
   110
These set limits for terminal output.
lcp@104
   111
lcp@322
   112
\begin{ttdescription}
lcp@322
   113
\item[\ttindexbold{Pretty.setdepth} \(d\);]  
lcp@322
   114
  tells Isabelle's pretty printer to limit the printing depth to~$d$.  This
lcp@322
   115
  affects Isabelle's display of theorems and terms.  The default value
lcp@322
   116
  is~0, which permits printing to an arbitrary depth.  Useful values for
lcp@322
   117
  $d$ are~10 and~20.
lcp@104
   118
lcp@322
   119
\item[\ttindexbold{Pretty.setmargin} \(m\);]  
lcp@322
   120
  tells Isabelle's pretty printer to assume a right margin (page width)
lcp@322
   121
  of~$m$.  The initial margin is~80.
lcp@104
   122
lcp@322
   123
\item[\ttindexbold{print_depth} \(n\);]  
lcp@322
   124
  limits the printing depth of complex \ML{} values, such as theorems and
lcp@322
   125
  terms.  This command affects the \ML{} top level and its effect is
lcp@322
   126
  compiler-dependent.  Typically $n$ should be less than~10.
lcp@322
   127
\end{ttdescription}
lcp@104
   128
lcp@104
   129
lcp@322
   130
\subsection{Printing of hypotheses, types and sorts}
lcp@322
   131
\index{meta-assumptions!printing of}
lcp@322
   132
\index{types!printing of}\index{sorts!printing of}
lcp@104
   133
\begin{ttbox} 
lcp@322
   134
show_hyps  : bool ref \hfill{\bf initially true}
lcp@322
   135
show_types : bool ref \hfill{\bf initially false}
lcp@322
   136
show_sorts : bool ref \hfill{\bf initially false}
lcp@104
   137
\end{ttbox}
lcp@322
   138
These flags allow you to control how much information is displayed for
lcp@322
   139
terms and theorems.  The hypotheses are normally shown; types and sorts are
lcp@322
   140
not.  Displaying types and sorts may explain why a polymorphic inference
lcp@322
   141
rule fails to resolve with some goal.
lcp@104
   142
lcp@322
   143
\begin{ttdescription}
lcp@322
   144
\item[\ttindexbold{show_hyps} := false;]   
lcp@332
   145
makes Isabelle show each meta-level hypothesis as a dot.
lcp@104
   146
lcp@322
   147
\item[\ttindexbold{show_types} := true;]
lcp@104
   148
makes Isabelle show types when printing a term or theorem.
lcp@104
   149
lcp@322
   150
\item[\ttindexbold{show_sorts} := true;]
lcp@104
   151
makes Isabelle show the sorts of type variables.  It has no effect unless
lcp@104
   152
{\tt show_types} is~{\tt true}. 
lcp@322
   153
\end{ttdescription}
lcp@104
   154
lcp@104
   155
lcp@104
   156
\subsection{$\eta$-contraction before printing}
lcp@104
   157
\begin{ttbox} 
lcp@104
   158
eta_contract: bool ref \hfill{\bf initially false}
lcp@104
   159
\end{ttbox}
lcp@104
   160
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
lcp@104
   161
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
lcp@104
   162
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
lcp@332
   163
unification frequently puts terms into a fully $\eta$-expanded form.  For
lcp@158
   164
example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
lcp@158
   165
$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
lcp@158
   166
form.
lcp@104
   167
lcp@322
   168
\begin{ttdescription}
lcp@322
   169
\item[\ttindexbold{eta_contract} := true;]
lcp@104
   170
makes Isabelle perform $\eta$-contractions before printing, so that
lcp@104
   171
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
lcp@104
   172
distinction between a term and its $\eta$-expanded form occasionally
lcp@104
   173
matters.
lcp@322
   174
\end{ttdescription}
lcp@322
   175
\index{printing control|)}
lcp@104
   176
lcp@104
   177
lcp@104
   178
\section{Displaying exceptions as error messages}
lcp@322
   179
\index{exceptions!printing of}
lcp@104
   180
\begin{ttbox} 
lcp@104
   181
print_exn: exn -> 'a
lcp@104
   182
\end{ttbox}
lcp@104
   183
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
lcp@104
   184
and {\tt RSN}, are called both interactively and from programs.  They
lcp@104
   185
indicate errors not by printing messages, but by raising exceptions.  For
lcp@322
   186
interactive use, \ML's reporting of an uncaught exception is 
lcp@322
   187
uninformative.  The Poly/ML function {\tt exception_trace} can generate a
lcp@322
   188
backtrace.\index{Poly/{\ML} compiler}
lcp@104
   189
lcp@322
   190
\begin{ttdescription}
lcp@104
   191
\item[\ttindexbold{print_exn} $e$] 
lcp@104
   192
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
lcp@322
   193
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
lcp@322
   194
$EXP$ is an expression that may raise an exception.
lcp@104
   195
lcp@104
   196
{\tt print_exn} can display the following common exceptions, which concern
lcp@104
   197
types, terms, theorems and theories, respectively.  Each carries a message
lcp@104
   198
and related information.
lcp@104
   199
\begin{ttbox} 
lcp@104
   200
exception TYPE   of string * typ list * term list
lcp@104
   201
exception TERM   of string * term list
lcp@104
   202
exception THM    of string * int * thm list
lcp@104
   203
exception THEORY of string * theory list
lcp@104
   204
\end{ttbox}
lcp@322
   205
\end{ttdescription}
lcp@322
   206
\begin{warn}
lcp@322
   207
  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
lcp@322
   208
  pretty printing information from the proof state last stored in the
lcp@322
   209
  subgoal module.  The appearance of the output thus depends upon the
lcp@322
   210
  theory used in the last interactive proof.
lcp@322
   211
\end{warn}
lcp@104
   212
lcp@104
   213
\section{Shell scripts}
lcp@322
   214
\index{shell scripts|bold} The following files are distributed with
lcp@322
   215
Isabelle, and work under Unix$^{\rm TM}$.  They can be executed as commands
lcp@322
   216
to the Unix shell.  Some of them depend upon shell environment variables.
lcp@322
   217
\begin{ttdescription}
lcp@322
   218
\item[make-all $switches$] \index{*make-all shell script}
lcp@286
   219
  compiles the Isabelle system, when executed on the source directory.
lcp@286
   220
  Environment variables specify which \ML{} compiler to use.  These
lcp@286
   221
  variables, and the {\it switches}, are documented on the file itself.
lcp@104
   222
lcp@322
   223
\item[teeinput $program$] \index{*teeinput shell script}
lcp@322
   224
  executes the {\it program}, while piping the standard input to a log file
lcp@322
   225
  designated by the \verb|$LISTEN| environment variable.  Normally the
lcp@322
   226
  program is Isabelle, and the log file receives a copy of all the Isabelle
lcp@322
   227
  commands.
lcp@104
   228
lcp@322
   229
\item[xlisten $program$] \index{*xlisten shell script}
lcp@104
   230
  is a trivial `user interface' for the X Window System.  It creates two
lcp@104
   231
  windows using {\tt xterm}.  One executes an interactive session via
lcp@104
   232
  \hbox{\tt teeinput $program$}, while the other displays the log file.  To
lcp@104
   233
  make a proof record, simply paste lines from the log file into an editor
lcp@104
   234
  window.
lcp@104
   235
lcp@322
   236
\item[expandshort $files$]  \index{*expandshort shell script}
lcp@104
   237
  reads the {\it files\/} and replaces all occurrences of the shorthand
lcp@286
   238
  commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the
lcp@286
   239
  corresponding full commands.  Shorthand commands should appear one
lcp@104
   240
  per line.  The old versions of the files
lcp@104
   241
  are renamed to have the suffix~\verb'~~'.
lcp@322
   242
\end{ttdescription}
lcp@104
   243
lcp@104
   244
\index{sessions|)}