doc-src/Ref/introduction.tex
author wenzelm
Tue, 06 May 1997 12:50:16 +0200
changeset 3108 335efc3f5632
parent 2225 78a8faae780f
child 3200 ea2310ba01da
permissions -rw-r--r--
misc updates, tuning, cleanup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     2
286
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
     3
\chapter{Basic Use of Isabelle}\index{sessions|(} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     4
The Reference Manual is a comprehensive description of Isabelle
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     5
proper, including all \ML{} commands, functions and packages.  It
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     6
really is intended for reference, perhaps for browsing, but not for
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     7
reading through.  It is not a tutorial, but assumes familiarity with
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     8
the basic logical concepts of Isabelle.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
286
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
    10
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
    11
Contents for a relevant heading.  Functions are organized by their purpose,
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
    12
by their operands (subgoals, tactics, theorems), and by their usefulness.
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
    13
In each section, basic functions appear first, then advanced functions, and
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
    14
finally esoteric functions.  Use the Index when you are looking for the
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
    15
definition of a particular Isabelle function.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
286
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
    17
A few examples are presented.  Many examples files are distributed with
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
    18
Isabelle, however; please experiment interactively.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
\section{Basic interaction with Isabelle}
2225
78a8faae780f Added instructions on starting up
paulson
parents: 1372
diff changeset
    22
\index{starting up|bold}\nobreak
78a8faae780f Added instructions on starting up
paulson
parents: 1372
diff changeset
    23
%
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    24
We assume that your local Isabelle administrator (this might be you!)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    25
has already installed the \Pure\ system and several object-logics
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    26
properly --- otherwise see the {\tt INSTALL} file in the top-level
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    27
directory of the distribution on how to build it.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    28
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    29
\medskip Let $\langle isabellehome \rangle$ denote the location where
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    30
the distribution has been installed. To run Isabelle from a the shell
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    31
prompt within an ordinary text terminal session, simply type:
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    32
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    33
\({\langle}isabellehome{\rangle}\)/bin/isabelle
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    34
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    35
This should start an interactive \ML{} session with the default
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    36
object-logic already preloaded. All Isabelle commands are bound to
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    37
\ML{} identifiers.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    38
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    39
Subsequently we assume that {\tt \(\langle isabellehome \rangle\)/bin}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    40
has been added to your shell's search path, in order to avoid typing
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    41
full path specifications of the executable files.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    42
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    43
The object-logic image to load may be also specified explicitly as an
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    44
argument to the {\tt isabelle} command, e.g.:
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    45
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    46
isabelle FOL
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    47
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    48
This should put you into the world of polymorphic first-order logic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    49
(assuming that {\FOL} has been pre-built).
2225
78a8faae780f Added instructions on starting up
paulson
parents: 1372
diff changeset
    50
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    51
\index{saving your work|bold} Isabelle provides no means of storing
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    52
theorems or proofs on files.  Theorems are simply part of the \ML{}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    53
state and are named by \ML{} identifiers.  To save your work between
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    54
sessions, you must dump the \ML{} system state to a file. This is done
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    55
automatically when ending the session normally (e.g.\ by typing
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    56
control-D), provided that the image has been opened \emph{writable} in
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    57
the first place. The standard object-logics are usually read-only, so
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    58
you probably have to create a private working copy first. For example,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    59
the following shell command puts you into a writable Isabelle session
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    60
of name \texttt{Foo} that initially contains just \FOL:
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    61
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    62
isabelle FOL Foo
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    63
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    64
Ending the \texttt{Foo} session with control-D will cause the complete
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    65
\ML{} world to be saved somewhere in your home directory\footnote{The
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    66
  default location is in \texttt{\~\relax/isabelle/heaps}, but this
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    67
  depends on your local configuration.}. Make sure there is enough
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    68
space available! Then one may later continue at exactly the same point
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    69
by running
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    70
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    71
isabelle Foo  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    72
\end{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    74
%FIXME not yet
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    75
%More details about \texttt{isabelle} may be found in the \emph{System
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    76
%  Manual}.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    77
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    78
\medskip Saving the state is not enough.  Record, on a file, the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    79
top-level commands that generate your theories and proofs.  Such a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    80
record allows you to replay the proofs whenever required, for instance
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    81
after making minor changes to the axioms.  Ideally, your record will
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    82
be somewhat intelligible to others as a formal description of your
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    83
work.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    85
\medskip There are more comfortable user interfaces than the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    86
bare-bones \ML{} top-level run from a text terminal. The
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    87
\texttt{Isabelle} executable (note the capital I) runs one such
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    88
interface, depending on your local configuration.  Furthermore there
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    89
are a number of external utilities available. These are started
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    90
uniformly via the \texttt{isatool} wrapper.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    92
%FIXME not yet
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    93
%Again, see the \emph{System Manual} for more information user
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    94
%interfaces and utilities.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
\section{Ending a session}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    99
quit    : unit -> unit
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   100
exit    : int -> unit
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   101
commit  : unit -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   103
\begin{ttdescription}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   104
\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   105
  the state.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   107
\item[\ttindexbold{exit}();] same as {\tt quit}, passing a return code
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   108
  to the operating system.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   110
\item[\ttindexbold{commit}();] saves the current state without ending
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   111
  the session, provided that the logic image is opened read-write.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   112
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   114
Typing control-D also finishes the session in essentially the same way
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   115
as the sequence {\tt commit(); quit();} would.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   118
\section{Reading ML files}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   119
\index{files!reading}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
\begin{ttbox} 
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   121
cd              : string -> unit
884
35c836adf48f added documentation of pwd
clasohm
parents: 508
diff changeset
   122
pwd             : unit -> string
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   123
use             : string -> unit
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   124
time_use        : string -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   126
Section~\ref{LoadingTheories} describes commands for loading theory files.
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   127
\begin{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   128
\item[\ttindexbold{cd} "{\it dir}";]
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   129
  changes the current directory to {\it dir}.  This is the default directory
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   130
  for reading files and for writing temporary files.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   132
\item[\ttindexbold{pwd}();] returns the path of the current directory.
884
35c836adf48f added documentation of pwd
clasohm
parents: 508
diff changeset
   133
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   134
\item[\ttindexbold{use} "$file$";]  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
reads the given {\it file} as input to the \ML{} session.  Reading a file
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
of Isabelle commands is the usual way of replaying a proof.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   138
\item[\ttindexbold{time_use} "$file$";]  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
performs {\tt use~"$file$"} and prints the total execution time.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   140
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   143
\section{Setting flags}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   144
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   145
set     : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   146
reset   : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   147
toggle  : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   148
\end{ttbox}\index{*set}\index{*reset}\index{*toggle}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   149
These are some shorthands for manipulating boolean references. The new
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   150
value is returned.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   151
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   152
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   153
\section{Printing of terms and theorems}\label{sec:printing-control}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   154
\index{printing control|(}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
Isabelle's pretty printer is controlled by a number of parameters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\subsection{Printing limits}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
Pretty.setdepth  : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
Pretty.setmargin : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
print_depth      : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
\end{ttbox}
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   163
These set limits for terminal output.  See also {\tt goals_limit}, which
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   164
limits the number of subgoals printed (page~\pageref{sec:goals-printing}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   166
\begin{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   167
\item[\ttindexbold{Pretty.setdepth} \(d\);]  
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   168
  tells Isabelle's pretty printer to limit the printing depth to~$d$.  This
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   169
  affects Isabelle's display of theorems and terms.  The default value
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   170
  is~0, which permits printing to an arbitrary depth.  Useful values for
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   171
  $d$ are~10 and~20.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   173
\item[\ttindexbold{Pretty.setmargin} \(m\);]  
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   174
  tells Isabelle's pretty printer to assume a right margin (page width)
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   175
  of~$m$.  The initial margin is~80.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   177
\item[\ttindexbold{print_depth} \(n\);]  
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   178
  limits the printing depth of complex \ML{} values, such as theorems and
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   179
  terms.  This command affects the \ML{} top level and its effect is
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   180
  compiler-dependent.  Typically $n$ should be less than~10.
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   181
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   184
\subsection{Printing of hypotheses, brackets, types and sorts}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   185
\index{meta-assumptions!printing of}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   186
\index{types!printing of}\index{sorts!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\begin{ttbox} 
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   188
show_hyps     : bool ref \hfill{\bf initially true}
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   189
show_brackets : bool ref \hfill{\bf initially false}
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   190
show_types    : bool ref \hfill{\bf initially false}
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   191
show_sorts    : bool ref \hfill{\bf initially false}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   193
These flags allow you to control how much information is displayed for
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   194
terms and theorems.  The hypotheses are normally shown; superfluous
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   195
parentheses are not.  Types and sorts are normally hidden.  Displaying
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   196
types and sorts may explain why a polymorphic inference rule fails to
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   197
resolve with some goal.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   199
\begin{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   200
\item[\ttindexbold{show_hyps} := false;]   
332
01b87a921967 final Springer copy
lcp
parents: 322
diff changeset
   201
makes Isabelle show each meta-level hypothesis as a dot.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   203
\item[\ttindexbold{show_brackets} := true;] 
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   204
  makes Isabelle show full bracketing.  This reveals the
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   205
  grouping of infix operators.
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   206
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   207
\item[\ttindexbold{show_types} := true;]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
makes Isabelle show types when printing a term or theorem.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   210
\item[\ttindexbold{show_sorts} := true;]
1102
a203181678d3 show_sorts:=true forces display of types
lcp
parents: 884
diff changeset
   211
makes Isabelle show both types and the sorts of type variables.  It does not
a203181678d3 show_sorts:=true forces display of types
lcp
parents: 884
diff changeset
   212
matter whether {\tt show_types} is also~{\tt true}. 
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   213
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
\subsection{$\eta$-contraction before printing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
eta_contract: bool ref \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
332
01b87a921967 final Springer copy
lcp
parents: 322
diff changeset
   223
unification frequently puts terms into a fully $\eta$-expanded form.  For
158
c2fcb6c07689 Correction to eta-contraction; thanks to Markus W.
lcp
parents: 149
diff changeset
   224
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
   225
$\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
   226
form.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   228
\begin{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   229
\item[\ttindexbold{eta_contract} := true;]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
makes Isabelle perform $\eta$-contractions before printing, so that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
distinction between a term and its $\eta$-expanded form occasionally
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
matters.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   234
\end{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   235
\index{printing control|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
\section{Displaying exceptions as error messages}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   239
\index{exceptions!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
print_exn: exn -> 'a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
and {\tt RSN}, are called both interactively and from programs.  They
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
indicate errors not by printing messages, but by raising exceptions.  For
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   246
interactive use, \ML's reporting of an uncaught exception is 
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   247
uninformative.  The Poly/ML function {\tt exception_trace} can generate a
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   248
backtrace.\index{Poly/{\ML} compiler}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   250
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
\item[\ttindexbold{print_exn} $e$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   253
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   254
$EXP$ is an expression that may raise an exception.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
{\tt print_exn} can display the following common exceptions, which concern
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
types, terms, theorems and theories, respectively.  Each carries a message
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
and related information.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
exception TYPE   of string * typ list * term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
exception TERM   of string * term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
exception THM    of string * int * thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
exception THEORY of string * theory list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   265
\end{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   266
\begin{warn}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   267
  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   268
  pretty printing information from the proof state last stored in the
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   269
  subgoal module.  The appearance of the output thus depends upon the
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   270
  theory used in the last interactive proof.
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   271
\end{warn}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   273
%FIXME remove
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   274
%\section{Shell scripts}\label{sec:shell-scripts}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   275
%\index{shell scripts|bold} The following files are distributed with
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   276
%Isabelle, and work under Unix$^{\rm TM}$.  They can be executed as commands
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   277
%to the Unix shell.  Some of them depend upon shell environment variables.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   278
%\begin{ttdescription}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   279
%\item[make-all $switches$] \index{*make-all shell script}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   280
%  compiles the Isabelle system, when executed on the source directory.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   281
%  Environment variables specify which \ML{} compiler to use.  These
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   282
%  variables, and the {\it switches}, are documented on the file itself.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   283
%
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   284
%\item[teeinput $program$] \index{*teeinput shell script}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   285
%  executes the {\it program}, while piping the standard input to a log file
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   286
%  designated by the \verb|$LISTEN| environment variable.  Normally the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   287
%  program is Isabelle, and the log file receives a copy of all the Isabelle
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   288
%  commands.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   289
%
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   290
%\item[xlisten $program$] \index{*xlisten shell script}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   291
%  is a trivial `user interface' for the X Window System.  It creates two
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   292
%  windows using {\tt xterm}.  One executes an interactive session via
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   293
%  \hbox{\tt teeinput $program$}, while the other displays the log file.  To
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   294
%  make a proof record, simply paste lines from the log file into an editor
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   295
%  window.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   296
%
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   297
%\item[expandshort $files$]  \index{*expandshort shell script}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   298
%  reads the {\it files\/} and replaces all occurrences of the shorthand
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   299
%  commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   300
%  corresponding full commands.  Shorthand commands should appear one
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   301
%  per line.  The old versions of the files
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   302
%  are renamed to have the suffix~\verb'~~'.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   303
%\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
\index{sessions|)}