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