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