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