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