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