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