doc-src/Ref/introduction.tex
author clasohm
Fri Jan 27 12:42:03 1995 +0100 (1995-01-27)
changeset 884 35c836adf48f
parent 508 d8b6999ca364
child 1102 a203181678d3
permissions -rw-r--r--
added documentation of pwd
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@884
    82
pwd             : unit -> string
clasohm@138
    83
use             : string -> unit
clasohm@138
    84
time_use        : string -> unit
lcp@104
    85
\end{ttbox}
lcp@322
    86
Section~\ref{LoadingTheories} describes commands for loading theory files.
lcp@322
    87
\begin{ttdescription}
lcp@322
    88
\item[\ttindexbold{cd} "{\it dir}";]
lcp@322
    89
  changes the current directory to {\it dir}.  This is the default directory
lcp@322
    90
  for reading files and for writing temporary files.
lcp@104
    91
clasohm@884
    92
\item[\ttindexbold{pwd} ();] returns the path of the current directory.
clasohm@884
    93
lcp@322
    94
\item[\ttindexbold{use} "$file$";]  
lcp@104
    95
reads the given {\it file} as input to the \ML{} session.  Reading a file
lcp@104
    96
of Isabelle commands is the usual way of replaying a proof.
lcp@104
    97
lcp@322
    98
\item[\ttindexbold{time_use} "$file$";]  
lcp@104
    99
performs {\tt use~"$file$"} and prints the total execution time.
lcp@322
   100
\end{ttdescription}
lcp@104
   101
lcp@104
   102
lcp@508
   103
\section{Printing of terms and theorems}\label{sec:printing-control}
lcp@322
   104
\index{printing control|(}
lcp@104
   105
Isabelle's pretty printer is controlled by a number of parameters.
lcp@104
   106
lcp@104
   107
\subsection{Printing limits}
lcp@104
   108
\begin{ttbox} 
lcp@104
   109
Pretty.setdepth  : int -> unit
lcp@104
   110
Pretty.setmargin : int -> unit
lcp@104
   111
print_depth      : int -> unit
lcp@104
   112
\end{ttbox}
lcp@508
   113
These set limits for terminal output.  See also {\tt goals_limit}, which
lcp@508
   114
limits the number of subgoals printed (page~\pageref{sec:goals-printing}).
lcp@104
   115
lcp@322
   116
\begin{ttdescription}
lcp@322
   117
\item[\ttindexbold{Pretty.setdepth} \(d\);]  
lcp@322
   118
  tells Isabelle's pretty printer to limit the printing depth to~$d$.  This
lcp@322
   119
  affects Isabelle's display of theorems and terms.  The default value
lcp@322
   120
  is~0, which permits printing to an arbitrary depth.  Useful values for
lcp@322
   121
  $d$ are~10 and~20.
lcp@104
   122
lcp@322
   123
\item[\ttindexbold{Pretty.setmargin} \(m\);]  
lcp@322
   124
  tells Isabelle's pretty printer to assume a right margin (page width)
lcp@322
   125
  of~$m$.  The initial margin is~80.
lcp@104
   126
lcp@322
   127
\item[\ttindexbold{print_depth} \(n\);]  
lcp@322
   128
  limits the printing depth of complex \ML{} values, such as theorems and
lcp@322
   129
  terms.  This command affects the \ML{} top level and its effect is
lcp@322
   130
  compiler-dependent.  Typically $n$ should be less than~10.
lcp@322
   131
\end{ttdescription}
lcp@104
   132
lcp@104
   133
lcp@508
   134
\subsection{Printing of hypotheses, brackets, types and sorts}
lcp@322
   135
\index{meta-assumptions!printing of}
lcp@322
   136
\index{types!printing of}\index{sorts!printing of}
lcp@104
   137
\begin{ttbox} 
lcp@508
   138
show_hyps     : bool ref \hfill{\bf initially true}
lcp@508
   139
show_brackets : bool ref \hfill{\bf initially false}
lcp@508
   140
show_types    : bool ref \hfill{\bf initially false}
lcp@508
   141
show_sorts    : bool ref \hfill{\bf initially false}
lcp@104
   142
\end{ttbox}
lcp@322
   143
These flags allow you to control how much information is displayed for
lcp@508
   144
terms and theorems.  The hypotheses are normally shown; superfluous
lcp@508
   145
parentheses are not.  Types and sorts are normally hidden.  Displaying
lcp@508
   146
types and sorts may explain why a polymorphic inference rule fails to
lcp@508
   147
resolve with some goal.
lcp@104
   148
lcp@322
   149
\begin{ttdescription}
lcp@322
   150
\item[\ttindexbold{show_hyps} := false;]   
lcp@332
   151
makes Isabelle show each meta-level hypothesis as a dot.
lcp@104
   152
lcp@508
   153
\item[\ttindexbold{show_brackets} := true;] 
lcp@508
   154
  makes Isabelle show full bracketing.  This reveals the
lcp@508
   155
  grouping of infix operators.
lcp@508
   156
lcp@322
   157
\item[\ttindexbold{show_types} := true;]
lcp@104
   158
makes Isabelle show types when printing a term or theorem.
lcp@104
   159
lcp@322
   160
\item[\ttindexbold{show_sorts} := true;]
lcp@104
   161
makes Isabelle show the sorts of type variables.  It has no effect unless
lcp@104
   162
{\tt show_types} is~{\tt true}. 
lcp@322
   163
\end{ttdescription}
lcp@104
   164
lcp@104
   165
lcp@104
   166
\subsection{$\eta$-contraction before printing}
lcp@104
   167
\begin{ttbox} 
lcp@104
   168
eta_contract: bool ref \hfill{\bf initially false}
lcp@104
   169
\end{ttbox}
lcp@104
   170
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
lcp@104
   171
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
lcp@104
   172
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
lcp@332
   173
unification frequently puts terms into a fully $\eta$-expanded form.  For
lcp@158
   174
example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
lcp@158
   175
$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
lcp@158
   176
form.
lcp@104
   177
lcp@322
   178
\begin{ttdescription}
lcp@322
   179
\item[\ttindexbold{eta_contract} := true;]
lcp@104
   180
makes Isabelle perform $\eta$-contractions before printing, so that
lcp@104
   181
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
lcp@104
   182
distinction between a term and its $\eta$-expanded form occasionally
lcp@104
   183
matters.
lcp@322
   184
\end{ttdescription}
lcp@322
   185
\index{printing control|)}
lcp@104
   186
lcp@104
   187
lcp@104
   188
\section{Displaying exceptions as error messages}
lcp@322
   189
\index{exceptions!printing of}
lcp@104
   190
\begin{ttbox} 
lcp@104
   191
print_exn: exn -> 'a
lcp@104
   192
\end{ttbox}
lcp@104
   193
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
lcp@104
   194
and {\tt RSN}, are called both interactively and from programs.  They
lcp@104
   195
indicate errors not by printing messages, but by raising exceptions.  For
lcp@322
   196
interactive use, \ML's reporting of an uncaught exception is 
lcp@322
   197
uninformative.  The Poly/ML function {\tt exception_trace} can generate a
lcp@322
   198
backtrace.\index{Poly/{\ML} compiler}
lcp@104
   199
lcp@322
   200
\begin{ttdescription}
lcp@104
   201
\item[\ttindexbold{print_exn} $e$] 
lcp@104
   202
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
lcp@322
   203
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
lcp@322
   204
$EXP$ is an expression that may raise an exception.
lcp@104
   205
lcp@104
   206
{\tt print_exn} can display the following common exceptions, which concern
lcp@104
   207
types, terms, theorems and theories, respectively.  Each carries a message
lcp@104
   208
and related information.
lcp@104
   209
\begin{ttbox} 
lcp@104
   210
exception TYPE   of string * typ list * term list
lcp@104
   211
exception TERM   of string * term list
lcp@104
   212
exception THM    of string * int * thm list
lcp@104
   213
exception THEORY of string * theory list
lcp@104
   214
\end{ttbox}
lcp@322
   215
\end{ttdescription}
lcp@322
   216
\begin{warn}
lcp@322
   217
  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
lcp@322
   218
  pretty printing information from the proof state last stored in the
lcp@322
   219
  subgoal module.  The appearance of the output thus depends upon the
lcp@322
   220
  theory used in the last interactive proof.
lcp@322
   221
\end{warn}
lcp@104
   222
lcp@104
   223
\section{Shell scripts}
lcp@322
   224
\index{shell scripts|bold} The following files are distributed with
lcp@322
   225
Isabelle, and work under Unix$^{\rm TM}$.  They can be executed as commands
lcp@322
   226
to the Unix shell.  Some of them depend upon shell environment variables.
lcp@322
   227
\begin{ttdescription}
lcp@322
   228
\item[make-all $switches$] \index{*make-all shell script}
lcp@286
   229
  compiles the Isabelle system, when executed on the source directory.
lcp@286
   230
  Environment variables specify which \ML{} compiler to use.  These
lcp@286
   231
  variables, and the {\it switches}, are documented on the file itself.
lcp@104
   232
lcp@322
   233
\item[teeinput $program$] \index{*teeinput shell script}
lcp@322
   234
  executes the {\it program}, while piping the standard input to a log file
lcp@322
   235
  designated by the \verb|$LISTEN| environment variable.  Normally the
lcp@322
   236
  program is Isabelle, and the log file receives a copy of all the Isabelle
lcp@322
   237
  commands.
lcp@104
   238
lcp@322
   239
\item[xlisten $program$] \index{*xlisten shell script}
lcp@104
   240
  is a trivial `user interface' for the X Window System.  It creates two
lcp@104
   241
  windows using {\tt xterm}.  One executes an interactive session via
lcp@104
   242
  \hbox{\tt teeinput $program$}, while the other displays the log file.  To
lcp@104
   243
  make a proof record, simply paste lines from the log file into an editor
lcp@104
   244
  window.
lcp@104
   245
lcp@322
   246
\item[expandshort $files$]  \index{*expandshort shell script}
lcp@104
   247
  reads the {\it files\/} and replaces all occurrences of the shorthand
lcp@286
   248
  commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the
lcp@286
   249
  corresponding full commands.  Shorthand commands should appear one
lcp@104
   250
  per line.  The old versions of the files
lcp@104
   251
  are renamed to have the suffix~\verb'~~'.
lcp@322
   252
\end{ttdescription}
lcp@104
   253
lcp@104
   254
\index{sessions|)}