doc-src/Ref/introduction.tex
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 9695 ec7d7f877712
child 12831 a2a3896f9c48
permissions -rw-r--r--
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
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
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    18
A few examples are presented.  Many example files are distributed with
286
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
%
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    25
We assume that your local Isabelle administrator (this might be you!) has
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    26
already installed the Isabelle system together with appropriate object-logics
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    27
--- otherwise see the \texttt{README} and \texttt{INSTALL} files in the
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    28
top-level directory of the distribution on how to do this.
3108
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}
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    36
This should start an interactive \ML{} session with the default object-logic
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9231
diff changeset
    37
(usually HOL) already pre-loaded.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    38
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    39
Subsequently, we assume that the \texttt{isabelle} executable is determined
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    40
automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    41
  \rangle\)/bin} to your search path.\footnote{Depending on your installation,
7990
0a604b2fc2b1 updated;
wenzelm
parents: 7592
diff changeset
    42
  there may be stand-alone binaries located in some global directory such as
0a604b2fc2b1 updated;
wenzelm
parents: 7592
diff changeset
    43
  \texttt{/usr/bin}.  Do not attempt to copy {\tt \(\langle isabellehome
0a604b2fc2b1 updated;
wenzelm
parents: 7592
diff changeset
    44
    \rangle\)/bin/isabelle}, though!  See \texttt{isatool install} in
0a604b2fc2b1 updated;
wenzelm
parents: 7592
diff changeset
    45
  \emph{The Isabelle System Manual} of how to do this properly.}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    46
6571
wenzelm
parents: 6569
diff changeset
    47
\medskip
wenzelm
parents: 6569
diff changeset
    48
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    49
The object-logic image to load may be also specified explicitly as an argument
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    50
to the {\tt isabelle} command, e.g.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    51
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    52
isabelle FOL
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    53
\end{ttbox}
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    54
This should put you into the world of polymorphic first-order logic (assuming
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9231
diff changeset
    55
that an image of FOL has been pre-built).
2225
78a8faae780f Added instructions on starting up
paulson
parents: 1372
diff changeset
    56
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    57
\index{saving your session|bold} Isabelle provides no means of storing
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    58
theorems or internal proof objects on files.  Theorems are simply part of the
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    59
\ML{} state.  To save your work between sessions, you may dump the \ML{}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    60
system state to a file.  This is done automatically when ending the session
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    61
normally (e.g.\ by typing control-D), provided that the image has been opened
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    62
\emph{writable} in the first place.  The standard object-logic images are
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    63
usually read-only, so you have to create a private working copy first.  For
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    64
example, the following shell command puts you into a writable Isabelle session
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9231
diff changeset
    65
of name \texttt{Foo} that initially contains just plain HOL:
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    66
\begin{ttbox}
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    67
isabelle HOL Foo
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    68
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    69
Ending the \texttt{Foo} session with control-D will cause the complete
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    70
\ML-world to be saved somewhere in your home directory\footnote{The default
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    71
  location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    72
  local configuration.}.  Make sure there is enough space available! Then one
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    73
may later continue at exactly the same point by running
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    74
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    75
isabelle Foo  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    76
\end{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    78
\medskip Saving the {\ML} state is not enough.  Record, on a file, the
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    79
top-level commands that generate your theories and proofs.  Such a record
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    80
allows you to replay the proofs whenever required, for instance after making
6571
wenzelm
parents: 6569
diff changeset
    81
minor changes to the axioms.  Ideally, these sources will be somewhat
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    82
intelligible to others as a formal description of your work.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
    83
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    84
It is good practice to put all source files that constitute a separate
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    85
Isabelle session into an individual directory, together with an {\ML} file
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    86
called \texttt{ROOT.ML} that contains appropriate commands to load all other
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    87
files required.  Running \texttt{isabelle} with option \texttt{-u}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    88
automatically loads \texttt{ROOT.ML} on entering the session.  The
6571
wenzelm
parents: 6569
diff changeset
    89
\texttt{isatool usedir} utility provides some more options to manage Isabelle
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    90
sessions, such as automatic generation of theory browsing information.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    92
\medskip More details about the \texttt{isabelle} and \texttt{isatool}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    93
commands may be found in \emph{The Isabelle System Manual}.
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    94
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    95
\medskip There are more comfortable user interfaces than the bare-bones \ML{}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    96
top-level run from a text terminal.  The \texttt{Isabelle} executable (note
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    97
the capital I) runs one such interface, depending on your local configuration.
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
    98
Again, see \emph{The Isabelle System Manual} for more information.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
\section{Ending a session}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
\begin{ttbox} 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   103
quit    : unit -> unit
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   104
exit    : int -> unit
6067
0f8ab32093ae fixed commit spec;
wenzelm
parents: 5371
diff changeset
   105
commit  : unit -> bool
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   107
\begin{ttdescription}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   108
\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   109
  the state.
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   110
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   111
\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   112
  code \(i\) to the operating system.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   114
\item[\ttindexbold{commit}();] saves the current state without ending
6067
0f8ab32093ae fixed commit spec;
wenzelm
parents: 5371
diff changeset
   115
  the session, provided that the logic image is opened read-write;
0f8ab32093ae fixed commit spec;
wenzelm
parents: 5371
diff changeset
   116
  return value {\tt false} indicates an error.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   117
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   119
Typing control-D also finishes the session in essentially the same way
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   120
as the sequence {\tt commit(); quit();} would.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   123
\section{Reading ML files}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   124
\index{files!reading}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
\begin{ttbox} 
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   126
cd              : string -> unit
884
35c836adf48f added documentation of pwd
clasohm
parents: 508
diff changeset
   127
pwd             : unit -> string
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   128
use             : string -> unit
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   129
time_use        : string -> unit
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   131
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   132
\item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   133
  {\it dir}.  This is the default directory for reading files.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   134
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   135
\item[\ttindexbold{pwd}();] returns the full path of the current
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   136
  directory.
884
35c836adf48f added documentation of pwd
clasohm
parents: 508
diff changeset
   137
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   138
\item[\ttindexbold{use} "$file$";]  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
reads the given {\it file} as input to the \ML{} session.  Reading a file
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
of Isabelle commands is the usual way of replaying a proof.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   142
\item[\ttindexbold{time_use} "$file$";]  
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
performs {\tt use~"$file$"} and prints the total execution time.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   144
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
6343
97c697a32b73 updated;
wenzelm
parents: 6067
diff changeset
   146
The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
97c697a32b73 updated;
wenzelm
parents: 6067
diff changeset
   147
commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
97c697a32b73 updated;
wenzelm
parents: 6067
diff changeset
   148
expanded appropriately.  Note that \texttt{\~\relax} abbreviates
97c697a32b73 updated;
wenzelm
parents: 6067
diff changeset
   149
\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
6571
wenzelm
parents: 6569
diff changeset
   150
\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}.  The syntax for path
wenzelm
parents: 6569
diff changeset
   151
specifications follows Unix conventions.
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   152
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   153
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   154
\section{Reading theories}\label{sec:intro-theories}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   155
\index{theories!reading}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   156
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   157
In Isabelle, any kind of declarations, definitions, etc.\ are organized around
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   158
named \emph{theory} objects.  Logical reasoning always takes place within a
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   159
certain theory context, which may be switched at any time.  Theory $name$ is
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   160
defined by a theory file $name$\texttt{.thy}, containing declarations of
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   161
\texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   162
\S\ref{sec:ref-defining-theories} for more details on concrete syntax).
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   163
Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   164
proof scripts that are to be run in the context of the theory.
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   165
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   166
\begin{ttbox}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   167
context      : theory -> unit
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   168
the_context  : unit -> theory
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   169
theory       : string -> theory
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   170
use_thy      : string -> unit
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   171
time_use_thy : string -> unit
7136
71f6eef45713 added update_thy_only;
wenzelm
parents: 6618
diff changeset
   172
update_thy   : string -> unit
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   173
\end{ttbox}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   174
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   175
\begin{ttdescription}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   176
  
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   177
\item[\ttindexbold{context} $thy$;] switches the current theory context.  Any
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   178
  subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal})
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   179
  will refer to $thy$ as its theory.
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   180
  
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   181
\item[\ttindexbold{the_context}();] obtains the current theory context, or
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   182
  raises an error if absent.
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   183
  
6569
wenzelm
parents: 6568
diff changeset
   184
\item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 7990
diff changeset
   185
  the internal data\-base of loaded theories, raising an error if absent.
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   186
  
6569
wenzelm
parents: 6568
diff changeset
   187
\item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
6571
wenzelm
parents: 6569
diff changeset
   188
  system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter
wenzelm
parents: 6569
diff changeset
   189
  being optional).  It also ensures that all parent theories are loaded as
wenzelm
parents: 6569
diff changeset
   190
  well.  In case some older versions have already been present,
wenzelm
parents: 6569
diff changeset
   191
  \texttt{use_thy} only tries to reload $name$ itself, but is content with any
wenzelm
parents: 6569
diff changeset
   192
  version of its ancestors.
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   193
  
6569
wenzelm
parents: 6568
diff changeset
   194
\item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   195
  reports the time taken to process the actual theory parts and {\ML} files
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   196
  separately.
7592
wenzelm
parents: 7282
diff changeset
   197
  
7136
71f6eef45713 added update_thy_only;
wenzelm
parents: 6618
diff changeset
   198
\item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but
71f6eef45713 added update_thy_only;
wenzelm
parents: 6618
diff changeset
   199
  ensures that theory $name$ is fully up-to-date with respect to the file
7592
wenzelm
parents: 7282
diff changeset
   200
  system --- apart from theory $name$ itself, any of its ancestors may be
wenzelm
parents: 7282
diff changeset
   201
  reloaded as well.
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   202
  
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   203
\end{ttdescription}
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   204
9695
ec7d7f877712 proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm
parents: 9231
diff changeset
   205
Note that theories of pre-built logic images (e.g.\ HOL) are marked as
7282
69d601df351c finished theories;
wenzelm
parents: 7136
diff changeset
   206
\emph{finished} and cannot be updated any more.  See \S\ref{sec:more-theories}
69d601df351c finished theories;
wenzelm
parents: 7136
diff changeset
   207
for further information on Isabelle's theory loader.
4274
2048e7a79d09 cd, use: path variables;
wenzelm
parents: 3485
diff changeset
   208
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   210
\section{Setting flags}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   211
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   212
set     : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   213
reset   : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   214
toggle  : bool ref -> bool
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   215
\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
   216
These are some shorthands for manipulating boolean references.  The new
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   217
value is returned.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   218
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 2225
diff changeset
   219
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   220
\section{Printing of terms and theorems}\label{sec:printing-control}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   221
\index{printing control|(}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
Isabelle's pretty printer is controlled by a number of parameters.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
\subsection{Printing limits}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
Pretty.setdepth  : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
Pretty.setmargin : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
print_depth      : int -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
\end{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   230
These set limits for terminal output.  See also {\tt goals_limit},
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   231
which limits the number of subgoals printed
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   232
(\S\ref{sec:goals-printing}).
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   234
\begin{ttdescription}
6571
wenzelm
parents: 6569
diff changeset
   235
\item[\ttindexbold{Pretty.setdepth} \(d\);] tells Isabelle's pretty printer to
wenzelm
parents: 6569
diff changeset
   236
  limit the printing depth to~$d$.  This affects the display of theorems and
wenzelm
parents: 6569
diff changeset
   237
  terms.  The default value is~0, which permits printing to an arbitrary
wenzelm
parents: 6569
diff changeset
   238
  depth.  Useful values for $d$ are~10 and~20.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   240
\item[\ttindexbold{Pretty.setmargin} \(m\);]  
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   241
  tells Isabelle's pretty printer to assume a right margin (page width)
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   242
  of~$m$.  The initial margin is~76.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   244
\item[\ttindexbold{print_depth} \(n\);]  
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   245
  limits the printing depth of complex \ML{} values, such as theorems and
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   246
  terms.  This command affects the \ML{} top level and its effect is
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   247
  compiler-dependent.  Typically $n$ should be less than~10.
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   248
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   251
\subsection{Printing of hypotheses, brackets, types etc.}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   252
\index{meta-assumptions!printing of}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   253
\index{types!printing of}\index{sorts!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
\begin{ttbox} 
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   255
show_hyps     : bool ref \hfill{\bf initially true}
6343
97c697a32b73 updated;
wenzelm
parents: 6067
diff changeset
   256
show_tags     : bool ref \hfill{\bf initially false}
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   257
show_brackets : bool ref \hfill{\bf initially false}
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   258
show_types    : bool ref \hfill{\bf initially false}
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   259
show_sorts    : bool ref \hfill{\bf initially false}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   260
show_consts   : bool ref \hfill{\bf initially false}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   261
long_names    : bool ref \hfill{\bf initially false}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   263
These flags allow you to control how much information is displayed for
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   264
types, terms and theorems.  The hypotheses of theorems \emph{are}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   265
normally shown.  Superfluous parentheses of types and terms are not.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   266
Types and sorts of variables are normally hidden.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   267
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   268
Note that displaying types and sorts may explain why a polymorphic
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   269
inference rule fails to resolve with some goal, or why a rewrite rule
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   270
does not apply as expected.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   272
\begin{ttdescription}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   273
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   274
\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   275
  meta-level hypothesis as a dot.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   276
  
6343
97c697a32b73 updated;
wenzelm
parents: 6067
diff changeset
   277
\item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
97c697a32b73 updated;
wenzelm
parents: 6067
diff changeset
   278
  (which are basically just comments that may be attached by some tools).
97c697a32b73 updated;
wenzelm
parents: 6067
diff changeset
   279
  
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   280
\item[set \ttindexbold{show_brackets};] makes Isabelle show full
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   281
  bracketing.  In particular, this reveals the grouping of infix
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   282
  operators.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   283
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   284
\item[set \ttindexbold{show_types};] makes Isabelle show types when
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   285
  printing a term or theorem.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   286
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   287
\item[set \ttindexbold{show_sorts};] makes Isabelle show both types
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   288
  and the sorts of type variables, independently of the value of
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   289
  \texttt{show_types}.
8908
25f2bdc02123 show_consts no longer requires show_types;
wenzelm
parents: 8136
diff changeset
   290
  
25f2bdc02123 show_consts no longer requires show_types;
wenzelm
parents: 8136
diff changeset
   291
\item[set \ttindexbold{show_consts};] makes Isabelle show types of constants
25f2bdc02123 show_consts no longer requires show_types;
wenzelm
parents: 8136
diff changeset
   292
  when printing proof states.  Note that the output can be enormous as
25f2bdc02123 show_consts no longer requires show_types;
wenzelm
parents: 8136
diff changeset
   293
  polymorphic constants often occur at several different type instances.
508
d8b6999ca364 addition of show_brackets
lcp
parents: 332
diff changeset
   294
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   295
\item[set \ttindexbold{long_names};] forces names of all objects
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   296
  (types, constants, theorems, etc.) to be printed in their fully
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   297
  qualified internal form.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4317
diff changeset
   298
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   299
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
6618
13293a7d4a57 pdf setup;
wenzelm
parents: 6571
diff changeset
   302
\subsection{Eta-contraction before printing}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
\begin{ttbox} 
9231
8812a07d52ee eta_contract: no default;
wenzelm
parents: 8908
diff changeset
   304
eta_contract: bool ref
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
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
   309
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
   310
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
   311
$\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
   312
form.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   314
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   315
\item[set \ttindexbold{eta_contract};]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
makes Isabelle perform $\eta$-contractions before printing, so that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
distinction between a term and its $\eta$-expanded form occasionally
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
matters.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   320
\end{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   321
\index{printing control|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   323
\section{Diagnostic messages}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   324
\index{error messages}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   325
\index{warnings}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   326
6568
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   327
Isabelle conceptually provides three output channels for different kinds of
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   328
messages: ordinary text, warnings, errors.  Depending on the user interface
b38bc78d9a9d theory loader stuff updated and improved;
wenzelm
parents: 6343
diff changeset
   329
involved, these messages may appear in different text styles or colours.
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   330
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   331
The default setup of an \texttt{isabelle} terminal session is as
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   332
follows: plain output of ordinary text, warnings prefixed by
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   333
\texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s.  For example, a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   334
typical warning would look like this:
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   335
\begin{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   336
\#\#\# Beware the Jabberwock, my son!
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   337
\#\#\# The jaws that bite, the claws that catch!
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   338
\#\#\# Beware the Jubjub Bird, and shun
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   339
\#\#\# The frumious Bandersnatch!
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   340
\end{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   341
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   342
\texttt{ML} programs may output diagnostic messages using the
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   343
following functions:
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   344
\begin{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   345
writeln : string -> unit
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   346
warning : string -> unit
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   347
error   : string -> 'a
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   348
\end{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   349
Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   350
after having output the text, while \ttindex{writeln} and
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   351
\ttindex{warning} resume normal program execution.
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   352
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
\section{Displaying exceptions as error messages}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   355
\index{exceptions!printing of}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
print_exn: exn -> 'a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
Certain Isabelle primitives, such as the forward proof functions {\tt RS}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
and {\tt RSN}, are called both interactively and from programs.  They
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
indicate errors not by printing messages, but by raising exceptions.  For
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 4274
diff changeset
   362
interactive use, \ML's reporting of an uncaught exception may be
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   363
uninformative.  The Poly/ML function {\tt exception_trace} can generate a
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   364
backtrace.\index{Poly/{\ML} compiler}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   366
\begin{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
\item[\ttindexbold{print_exn} $e$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
displays the exception~$e$ in a readable manner, and then re-raises~$e$.
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   369
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   370
$EXP$ is an expression that may raise an exception.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
{\tt print_exn} can display the following common exceptions, which concern
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
types, terms, theorems and theories, respectively.  Each carries a message
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
and related information.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
exception TYPE   of string * typ list * term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
exception TERM   of string * term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
exception THM    of string * int * thm list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
exception THEORY of string * theory list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
\end{ttbox}
322
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   381
\end{ttdescription}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   382
\begin{warn}
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   383
  {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   384
  pretty printing information from the proof state last stored in the
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   385
  subgoal module.  The appearance of the output thus depends upon the
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   386
  theory used in the last interactive proof.
bacfaeeea007 penultimate Springer draft
lcp
parents: 286
diff changeset
   387
\end{warn}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
\index{sessions|)}
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   390
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   391
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   392
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   393
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   394
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 4543
diff changeset
   395
%%% End: