doc-src/Ref/introduction.tex
author paulson
Fri, 27 Nov 1998 13:13:22 +0100
changeset 5980 2e9314c07146
parent 5371 e27558a68b8d
child 6067 0f8ab32093ae
permissions -rw-r--r--
added Real/Hyperreal
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3200
ea2310ba01da sysman refs;
wenzelm
parents: 3108
diff changeset
     1
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
%% $Id$
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     3
286
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
     4
\chapter{Basic Use of Isabelle}\index{sessions|(} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     5
The Reference Manual is a comprehensive description of Isabelle
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     6
proper, including all \ML{} commands, functions and packages.  It
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     7
really is intended for reference, perhaps for browsing, but not for
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     8
reading through.  It is not a tutorial, but assumes familiarity with
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
     9
the basic logical concepts of Isabelle.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
286
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
    11
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
    12
Contents for a relevant heading.  Functions are organized by their purpose,
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
    13
by their operands (subgoals, tactics, theorems), and by their usefulness.
e7efbf03562b first draft of Springer book
lcp
parents: 159
diff changeset
    14
In each section, basic functions appear first, then advanced functions, and
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
    15
finally esoteric functions.  Use the Index when you are looking for the
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
    16
definition of a particular Isabelle function.
104
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}
2225
78a8faae780f Added instructions on starting up
paulson
parents: 1372
diff changeset
    23
\index{starting up|bold}\nobreak
78a8faae780f Added instructions on starting up
paulson
parents: 1372
diff changeset
    24
%
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    25
We assume that your local Isabelle administrator (this might be you!)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    26
has already installed the \Pure\ system and several object-logics
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    27
properly --- otherwise see the {\tt INSTALL} file in the top-level
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    28
directory of the distribution on how to build it.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    29
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    30
\medskip Let $\langle isabellehome \rangle$ denote the location where
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3200
diff changeset
    31
the distribution has been installed.  To run Isabelle from a the shell
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    32
prompt within an ordinary text terminal session, simply type
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    33
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    34
\({\langle}isabellehome{\rangle}\)/bin/isabelle
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    35
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    36
This should start an interactive \ML{} session with the default
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    37
object-logic already preloaded.
3108
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
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    44
argument to the {\tt isabelle} command, e.g.
3108
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
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    52
theorems or internal proof objects on files.  Theorems are simply part
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    53
of the \ML{} state.  To save your work between sessions, you must dump
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    54
the \ML{} system state to a file.  This is done automatically when
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    55
ending the session normally (e.g.\ by typing control-D), provided that
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    56
the image has been opened \emph{writable} in the first place.  The
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    57
standard object-logic images are usually read-only, so you probably
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    58
have to create a private working copy first.  For example, the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    59
following shell command puts you into a writable Isabelle session of
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    60
name \texttt{Foo} that initially contains just \FOL:
3108
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
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3200
diff changeset
    67
  depends on your local configuration.}.  Make sure there is enough
3108
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
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    74
More details about the \texttt{isabelle} command may be found in the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    75
\emph{System Manual}.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    76
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    77
\medskip Saving the state is not enough.  Record, on a file, the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    78
top-level commands that generate your theories and proofs.  Such a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    79
record allows you to replay the proofs whenever required, for instance
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    80
after making minor changes to the axioms.  Ideally, your record will
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    81
be somewhat intelligible to others as a formal description of your
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    82
work.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    84
\medskip There are more comfortable user interfaces than the
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3200
diff changeset
    85
bare-bones \ML{} top-level run from a text terminal.  The
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    86
\texttt{Isabelle} executable (note the capital I) runs one such
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    87
interface, depending on your local configuration.  Furthermore there
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3200
diff changeset
    88
are a number of external utilities available.  These are started
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    89
uniformly via the \texttt{isatool} wrapper.  See the \emph{System
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
    90
  Manual} for more information user interfaces and utilities.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\section{Ending a session}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    95
quit    : unit -> unit
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    96
exit    : int -> unit
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    97
commit  : unit -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
    99
\begin{ttdescription}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   100
\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   101
  the state.
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   102
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   103
\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   104
  code \(i\) to the operating system.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   106
\item[\ttindexbold{commit}();] saves the current state without ending
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   107
  the session, provided that the logic image is opened read-write.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   108
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   110
Typing control-D also finishes the session in essentially the same way
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   111
as the sequence {\tt commit(); quit();} would.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   114
\section{Reading ML files}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   115
\index{files!reading}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
\begin{ttbox} 
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   117
cd              : string -> unit
884
35c836adf48f added documentation of pwd
clasohm
parents: 508
diff changeset
   118
pwd             : unit -> string
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   119
use             : string -> unit
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   120
time_use        : string -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   122
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   123
\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   124
  {\it dir}.  This is the default directory for reading files.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   125
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   126
\item[\ttindexbold{pwd}();] returns the full path of the current
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   127
  directory.
884
35c836adf48f added documentation of pwd
clasohm
parents: 508
diff changeset
   128
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   129
\item[\ttindexbold{use} "$file$";]  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
reads the given {\it file} as input to the \ML{} session.  Reading a file
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
of Isabelle commands is the usual way of replaying a proof.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   133
\item[\ttindexbold{time_use} "$file$";]  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
performs {\tt use~"$file$"} and prints the total execution time.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   135
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
4274
2048e7a79d09 cd, use: path variables;
wenzelm
parents: 3485
diff changeset
   137
The $dir$ and $file$ specifications of the \texttt{cd} and
2048e7a79d09 cd, use: path variables;
wenzelm
parents: 3485
diff changeset
   138
\texttt{use} commands may contain path variables that are expanded
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   139
appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   140
(which abbreviates \texttt{\$HOME}).  Section~\ref{LoadingTheories}
4274
2048e7a79d09 cd, use: path variables;
wenzelm
parents: 3485
diff changeset
   141
describes commands for loading theory files.
2048e7a79d09 cd, use: path variables;
wenzelm
parents: 3485
diff changeset
   142
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   144
\section{Setting flags}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   145
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   146
set     : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   147
reset   : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   148
toggle  : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   149
\end{ttbox}\index{*set}\index{*reset}\index{*toggle}
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3200
diff changeset
   150
These are some shorthands for manipulating boolean references.  The new
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   151
value is returned.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   152
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   153
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   154
\section{Printing of terms and theorems}\label{sec:printing-control}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   155
\index{printing control|(}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
Isabelle's pretty printer is controlled by a number of parameters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
\subsection{Printing limits}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
Pretty.setdepth  : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
Pretty.setmargin : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
print_depth      : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
\end{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   164
These set limits for terminal output.  See also {\tt goals_limit},
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   165
which limits the number of subgoals printed
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   166
(\S\ref{sec:goals-printing}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   168
\begin{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   169
\item[\ttindexbold{Pretty.setdepth} \(d\);]  
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   170
  tells Isabelle's pretty printer to limit the printing depth to~$d$.  This
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   171
  affects Isabelle's display of theorems and terms.  The default value
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   172
  is~0, which permits printing to an arbitrary depth.  Useful values for
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   173
  $d$ are~10 and~20.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   175
\item[\ttindexbold{Pretty.setmargin} \(m\);]  
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   176
  tells Isabelle's pretty printer to assume a right margin (page width)
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   177
  of~$m$.  The initial margin is~76.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   179
\item[\ttindexbold{print_depth} \(n\);]  
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   180
  limits the printing depth of complex \ML{} values, such as theorems and
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   181
  terms.  This command affects the \ML{} top level and its effect is
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   182
  compiler-dependent.  Typically $n$ should be less than~10.
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   183
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   186
\subsection{Printing of hypotheses, brackets, types etc.}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   187
\index{meta-assumptions!printing of}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   188
\index{types!printing of}\index{sorts!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
\begin{ttbox} 
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   190
show_hyps     : bool ref \hfill{\bf initially true}
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   191
show_brackets : bool ref \hfill{\bf initially false}
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   192
show_types    : bool ref \hfill{\bf initially false}
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   193
show_sorts    : bool ref \hfill{\bf initially false}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   194
show_consts   : bool ref \hfill{\bf initially false}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   195
long_names    : bool ref \hfill{\bf initially false}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   197
These flags allow you to control how much information is displayed for
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   198
types, terms and theorems.  The hypotheses of theorems \emph{are}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   199
normally shown.  Superfluous parentheses of types and terms are not.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   200
Types and sorts of variables are normally hidden.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   201
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   202
Note that displaying types and sorts may explain why a polymorphic
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   203
inference rule fails to resolve with some goal, or why a rewrite rule
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   204
does not apply as expected.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   206
\begin{ttdescription}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   207
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   208
\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   209
  meta-level hypothesis as a dot.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   210
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   211
\item[set \ttindexbold{show_brackets};] makes Isabelle show full
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   212
  bracketing.  In particular, this reveals the grouping of infix
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   213
  operators.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   214
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   215
\item[set \ttindexbold{show_types};] makes Isabelle show types when
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   216
  printing a term or theorem.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   217
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   218
\item[set \ttindexbold{show_sorts};] makes Isabelle show both types
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   219
  and the sorts of type variables, independently of the value of
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   220
  \texttt{show_types}.
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   221
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   222
\item[set \ttindexbold{show_consts};] makes Isabelle show types of
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   223
  constants, provided that showing of types is enabled at all.  This
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   224
  is supported for printing of proof states only.  Note that the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   225
  output can be enormous as polymorphic constants often occur at
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   226
  several different type instances.
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   227
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   228
\item[set \ttindexbold{long_names};] forces names of all objects
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   229
  (types, constants, theorems, etc.) to be printed in their fully
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   230
  qualified internal form.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   231
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   232
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
\subsection{$\eta$-contraction before printing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
eta_contract: bool ref \hfill{\bf initially false}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
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
   242
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
   243
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
   244
$\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
   245
form.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   247
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   248
\item[set \ttindexbold{eta_contract};]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
makes Isabelle perform $\eta$-contractions before printing, so that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
distinction between a term and its $\eta$-expanded form occasionally
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
matters.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   253
\end{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   254
\index{printing control|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   256
\section{Diagnostic messages}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   257
\index{error messages}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   258
\index{warnings}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   259
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   260
Isabelle conceptually provides three output channels for different
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   261
kinds of messages: ordinary text, warnings, errors.  Depending on the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   262
user interface involved, these messages may appear in different text
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   263
styles or colours, even within separate windows.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   264
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   265
The default setup of an \texttt{isabelle} terminal session is as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   266
follows: plain output of ordinary text, warnings prefixed by
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   267
\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   268
typical warning would look like this:
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   269
\begin{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   270
\#\#\# Beware the Jabberwock, my son!
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   271
\#\#\# The jaws that bite, the claws that catch!
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   272
\#\#\# Beware the Jubjub Bird, and shun
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   273
\#\#\# The frumious Bandersnatch!
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   274
\end{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   275
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   276
\texttt{ML} programs may output diagnostic messages using the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   277
following functions:
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   278
\begin{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   279
writeln : string -> unit
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   280
warning : string -> unit
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   281
error   : string -> 'a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   282
\end{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   283
Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   284
after having output the text, while \ttindex{writeln} and
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   285
\ttindex{warning} resume normal program execution.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   286
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
\section{Displaying exceptions as error messages}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   289
\index{exceptions!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
print_exn: exn -> 'a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
and {\tt RSN}, are called both interactively and from programs.  They
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
indicate errors not by printing messages, but by raising exceptions.  For
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   296
interactive use, \ML's reporting of an uncaught exception may be
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   297
uninformative.  The Poly/ML function {\tt exception_trace} can generate a
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   298
backtrace.\index{Poly/{\ML} compiler}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   300
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
\item[\ttindexbold{print_exn} $e$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   303
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   304
$EXP$ is an expression that may raise an exception.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
{\tt print_exn} can display the following common exceptions, which concern
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
types, terms, theorems and theories, respectively.  Each carries a message
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
and related information.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
exception TYPE   of string * typ list * term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
exception TERM   of string * term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
exception THM    of string * int * thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
exception THEORY of string * theory list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   315
\end{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   316
\begin{warn}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   317
  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   318
  pretty printing information from the proof state last stored in the
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   319
  subgoal module.  The appearance of the output thus depends upon the
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   320
  theory used in the last interactive proof.
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   321
\end{warn}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
\index{sessions|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   324
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   325
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   326
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   327
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   328
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   329
%%% End: