author | oheimb |
Fri, 20 Dec 1996 10:33:54 +0100 | |
changeset 2458 | 566a0fc5a3e0 |
parent 2225 | 78a8faae780f |
child 3108 | 335efc3f5632 |
permissions | -rw-r--r-- |
104 | 1 |
%% $Id$ |
286 | 2 |
\chapter{Basic Use of Isabelle}\index{sessions|(} |
3 |
The Reference Manual is a comprehensive description of Isabelle, including |
|
4 |
all commands, functions and packages. It really is intended for reference, |
|
5 |
perhaps for browsing, but not for reading through. It is not a tutorial, |
|
6 |
but assumes familiarity with the basic concepts of Isabelle. |
|
104 | 7 |
|
286 | 8 |
When you are looking for a way of performing some task, scan the Table of |
9 |
Contents for a relevant heading. Functions are organized by their purpose, |
|
10 |
by their operands (subgoals, tactics, theorems), and by their usefulness. |
|
11 |
In each section, basic functions appear first, then advanced functions, and |
|
322 | 12 |
finally esoteric functions. Use the Index when you are looking for the |
13 |
definition of a particular Isabelle function. |
|
104 | 14 |
|
286 | 15 |
A few examples are presented. Many examples files are distributed with |
16 |
Isabelle, however; please experiment interactively. |
|
104 | 17 |
|
18 |
||
19 |
\section{Basic interaction with Isabelle} |
|
2225 | 20 |
\index{starting up|bold}\nobreak |
21 |
% |
|
22 |
First, read the instructions on file {\tt README} in the top-level |
|
23 |
distribution directory. Follow them to create the object-logics you need |
|
24 |
on a directory you have created to hold binary images. Suppose the |
|
25 |
environment variable {\tt ISABELLEBIN} refers to this directory. The |
|
26 |
instructions for starting up a logic (say {\tt HOL}) depend upon which |
|
27 |
Standard ML compiler you are using. |
|
28 |
\begin{itemize} |
|
29 |
\item With Standard ML of New Jersey, type \verb|$ISABELLEBIN/HOL|. |
|
30 |
\item With Poly/ML, type \verb|poly $ISABELLEBIN/HOL|, possibly prefixing the |
|
31 |
command with the directory where {\tt poly} is kept. |
|
32 |
\end{itemize} |
|
33 |
Either way, you will find yourself at the \ML{} top level. All Isabelle |
|
34 |
commands are bound to \ML{} identifiers. |
|
35 |
||
322 | 36 |
\index{saving your work|bold} |
104 | 37 |
Isabelle provides no means of storing theorems or proofs on files. |
38 |
Theorems are simply part of the \ML{} state and are named by \ML{} |
|
39 |
identifiers. To save your work between sessions, you must save a copy of |
|
40 |
the \ML{} image. The procedure for doing so is compiler-dependent: |
|
322 | 41 |
\begin{itemize}\index{Poly/{\ML} compiler} |
42 |
\item At the end of a session, Poly/\ML{} saves the state, provided you |
|
43 |
have created a database for your own use. You can create a database by |
|
44 |
copying an existing one, or by calling the Poly/\ML{} function {\tt |
|
45 |
make_database}; the latter course uses much less disc space. A |
|
46 |
Poly/\ML{} database {\em does not\/} save the contents of references, |
|
47 |
such as the current state of a backward proof. |
|
104 | 48 |
|
49 |
\item With New Jersey \ML{} you must save the state explicitly before |
|
149 | 50 |
ending the session. While a Poly/\ML{} database can be small, a New Jersey |
104 | 51 |
image occupies several megabytes. |
52 |
\end{itemize} |
|
53 |
See your \ML{} compiler's documentation for full instructions on saving the |
|
54 |
state. |
|
55 |
||
56 |
Saving the state is not enough. Record, on a file, the top-level commands |
|
57 |
that generate your theories and proofs. Such a record allows you to replay |
|
58 |
the proofs whenever required, for instance after making minor changes to |
|
59 |
the axioms. Ideally, your record will be intelligible to others as a |
|
60 |
formal description of your work. |
|
61 |
||
62 |
Since Isabelle's user interface is the \ML{} top level, some kind of window |
|
63 |
support is essential. One window displays the Isabelle session, while the |
|
322 | 64 |
other displays a file --- your proof record --- being edited. The Emacs |
65 |
editor supports windows and can manage interactive sessions. |
|
104 | 66 |
|
67 |
||
68 |
\section{Ending a session} |
|
69 |
\begin{ttbox} |
|
70 |
quit : unit -> unit |
|
71 |
commit : unit -> unit \hfill{\bf Poly/ML only} |
|
72 |
exportML : string -> bool \hfill{\bf New Jersey ML only} |
|
73 |
\end{ttbox} |
|
322 | 74 |
\begin{ttdescription} |
104 | 75 |
\item[\ttindexbold{quit}();] |
76 |
aborts the Isabelle session, without saving the state. |
|
77 |
||
322 | 78 |
\item[\ttindexbold{commit}();] |
79 |
saves the current state in your Poly/\ML{} database without ending the |
|
80 |
session. The contents of references are lost, so never do this during an |
|
81 |
interactive proof!\index{Poly/{\ML} compiler} |
|
104 | 82 |
|
322 | 83 |
\item[\ttindexbold{exportML} "{\it file}";] saves an |
104 | 84 |
image of your session to the given {\it file}. |
322 | 85 |
\end{ttdescription} |
104 | 86 |
|
87 |
\begin{warn} |
|
88 |
Typing control-D also finishes the session, but its effect is |
|
89 |
compiler-dependent. Poly/\ML{} will then save the state, if you have a |
|
90 |
private database. New Jersey \ML{} will discard the state! |
|
91 |
\end{warn} |
|
92 |
||
93 |
||
322 | 94 |
\section{Reading ML files} |
95 |
\index{files!reading} |
|
104 | 96 |
\begin{ttbox} |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
97 |
cd : string -> unit |
884 | 98 |
pwd : unit -> string |
138
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
99 |
use : string -> unit |
9ba8bff1addc
added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents:
104
diff
changeset
|
100 |
time_use : string -> unit |
104 | 101 |
\end{ttbox} |
322 | 102 |
Section~\ref{LoadingTheories} describes commands for loading theory files. |
103 |
\begin{ttdescription} |
|
104 |
\item[\ttindexbold{cd} "{\it dir}";] |
|
105 |
changes the current directory to {\it dir}. This is the default directory |
|
106 |
for reading files and for writing temporary files. |
|
104 | 107 |
|
884 | 108 |
\item[\ttindexbold{pwd} ();] returns the path of the current directory. |
109 |
||
322 | 110 |
\item[\ttindexbold{use} "$file$";] |
104 | 111 |
reads the given {\it file} as input to the \ML{} session. Reading a file |
112 |
of Isabelle commands is the usual way of replaying a proof. |
|
113 |
||
322 | 114 |
\item[\ttindexbold{time_use} "$file$";] |
104 | 115 |
performs {\tt use~"$file$"} and prints the total execution time. |
322 | 116 |
\end{ttdescription} |
104 | 117 |
|
118 |
||
508 | 119 |
\section{Printing of terms and theorems}\label{sec:printing-control} |
322 | 120 |
\index{printing control|(} |
104 | 121 |
Isabelle's pretty printer is controlled by a number of parameters. |
122 |
||
123 |
\subsection{Printing limits} |
|
124 |
\begin{ttbox} |
|
125 |
Pretty.setdepth : int -> unit |
|
126 |
Pretty.setmargin : int -> unit |
|
127 |
print_depth : int -> unit |
|
128 |
\end{ttbox} |
|
508 | 129 |
These set limits for terminal output. See also {\tt goals_limit}, which |
130 |
limits the number of subgoals printed (page~\pageref{sec:goals-printing}). |
|
104 | 131 |
|
322 | 132 |
\begin{ttdescription} |
133 |
\item[\ttindexbold{Pretty.setdepth} \(d\);] |
|
134 |
tells Isabelle's pretty printer to limit the printing depth to~$d$. This |
|
135 |
affects Isabelle's display of theorems and terms. The default value |
|
136 |
is~0, which permits printing to an arbitrary depth. Useful values for |
|
137 |
$d$ are~10 and~20. |
|
104 | 138 |
|
322 | 139 |
\item[\ttindexbold{Pretty.setmargin} \(m\);] |
140 |
tells Isabelle's pretty printer to assume a right margin (page width) |
|
141 |
of~$m$. The initial margin is~80. |
|
104 | 142 |
|
322 | 143 |
\item[\ttindexbold{print_depth} \(n\);] |
144 |
limits the printing depth of complex \ML{} values, such as theorems and |
|
145 |
terms. This command affects the \ML{} top level and its effect is |
|
146 |
compiler-dependent. Typically $n$ should be less than~10. |
|
147 |
\end{ttdescription} |
|
104 | 148 |
|
149 |
||
508 | 150 |
\subsection{Printing of hypotheses, brackets, types and sorts} |
322 | 151 |
\index{meta-assumptions!printing of} |
152 |
\index{types!printing of}\index{sorts!printing of} |
|
104 | 153 |
\begin{ttbox} |
508 | 154 |
show_hyps : bool ref \hfill{\bf initially true} |
155 |
show_brackets : bool ref \hfill{\bf initially false} |
|
156 |
show_types : bool ref \hfill{\bf initially false} |
|
157 |
show_sorts : bool ref \hfill{\bf initially false} |
|
104 | 158 |
\end{ttbox} |
322 | 159 |
These flags allow you to control how much information is displayed for |
508 | 160 |
terms and theorems. The hypotheses are normally shown; superfluous |
161 |
parentheses are not. Types and sorts are normally hidden. Displaying |
|
162 |
types and sorts may explain why a polymorphic inference rule fails to |
|
163 |
resolve with some goal. |
|
104 | 164 |
|
322 | 165 |
\begin{ttdescription} |
166 |
\item[\ttindexbold{show_hyps} := false;] |
|
332 | 167 |
makes Isabelle show each meta-level hypothesis as a dot. |
104 | 168 |
|
508 | 169 |
\item[\ttindexbold{show_brackets} := true;] |
170 |
makes Isabelle show full bracketing. This reveals the |
|
171 |
grouping of infix operators. |
|
172 |
||
322 | 173 |
\item[\ttindexbold{show_types} := true;] |
104 | 174 |
makes Isabelle show types when printing a term or theorem. |
175 |
||
322 | 176 |
\item[\ttindexbold{show_sorts} := true;] |
1102 | 177 |
makes Isabelle show both types and the sorts of type variables. It does not |
178 |
matter whether {\tt show_types} is also~{\tt true}. |
|
322 | 179 |
\end{ttdescription} |
104 | 180 |
|
181 |
||
182 |
\subsection{$\eta$-contraction before printing} |
|
183 |
\begin{ttbox} |
|
184 |
eta_contract: bool ref \hfill{\bf initially false} |
|
185 |
\end{ttbox} |
|
186 |
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, |
|
187 |
provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of |
|
188 |
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order |
|
332 | 189 |
unification frequently puts terms into a fully $\eta$-expanded form. For |
158 | 190 |
example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is |
191 |
$\lambda h.F(\lambda x.h(x))$. By default, the user sees this expanded |
|
192 |
form. |
|
104 | 193 |
|
322 | 194 |
\begin{ttdescription} |
195 |
\item[\ttindexbold{eta_contract} := true;] |
|
104 | 196 |
makes Isabelle perform $\eta$-contractions before printing, so that |
197 |
$\lambda h.F(\lambda x.h(x))$ appears simply as~$F$. The |
|
198 |
distinction between a term and its $\eta$-expanded form occasionally |
|
199 |
matters. |
|
322 | 200 |
\end{ttdescription} |
201 |
\index{printing control|)} |
|
104 | 202 |
|
203 |
||
204 |
\section{Displaying exceptions as error messages} |
|
322 | 205 |
\index{exceptions!printing of} |
104 | 206 |
\begin{ttbox} |
207 |
print_exn: exn -> 'a |
|
208 |
\end{ttbox} |
|
209 |
Certain Isabelle primitives, such as the forward proof functions {\tt RS} |
|
210 |
and {\tt RSN}, are called both interactively and from programs. They |
|
211 |
indicate errors not by printing messages, but by raising exceptions. For |
|
322 | 212 |
interactive use, \ML's reporting of an uncaught exception is |
213 |
uninformative. The Poly/ML function {\tt exception_trace} can generate a |
|
214 |
backtrace.\index{Poly/{\ML} compiler} |
|
104 | 215 |
|
322 | 216 |
\begin{ttdescription} |
104 | 217 |
\item[\ttindexbold{print_exn} $e$] |
218 |
displays the exception~$e$ in a readable manner, and then re-raises~$e$. |
|
322 | 219 |
Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where |
220 |
$EXP$ is an expression that may raise an exception. |
|
104 | 221 |
|
222 |
{\tt print_exn} can display the following common exceptions, which concern |
|
223 |
types, terms, theorems and theories, respectively. Each carries a message |
|
224 |
and related information. |
|
225 |
\begin{ttbox} |
|
226 |
exception TYPE of string * typ list * term list |
|
227 |
exception TERM of string * term list |
|
228 |
exception THM of string * int * thm list |
|
229 |
exception THEORY of string * theory list |
|
230 |
\end{ttbox} |
|
322 | 231 |
\end{ttdescription} |
232 |
\begin{warn} |
|
233 |
{\tt print_exn} prints terms by calling \ttindex{prin}, which obtains |
|
234 |
pretty printing information from the proof state last stored in the |
|
235 |
subgoal module. The appearance of the output thus depends upon the |
|
236 |
theory used in the last interactive proof. |
|
237 |
\end{warn} |
|
104 | 238 |
|
1372 | 239 |
\section{Shell scripts}\label{sec:shell-scripts} |
322 | 240 |
\index{shell scripts|bold} The following files are distributed with |
241 |
Isabelle, and work under Unix$^{\rm TM}$. They can be executed as commands |
|
242 |
to the Unix shell. Some of them depend upon shell environment variables. |
|
243 |
\begin{ttdescription} |
|
244 |
\item[make-all $switches$] \index{*make-all shell script} |
|
286 | 245 |
compiles the Isabelle system, when executed on the source directory. |
246 |
Environment variables specify which \ML{} compiler to use. These |
|
247 |
variables, and the {\it switches}, are documented on the file itself. |
|
104 | 248 |
|
322 | 249 |
\item[teeinput $program$] \index{*teeinput shell script} |
250 |
executes the {\it program}, while piping the standard input to a log file |
|
251 |
designated by the \verb|$LISTEN| environment variable. Normally the |
|
252 |
program is Isabelle, and the log file receives a copy of all the Isabelle |
|
253 |
commands. |
|
104 | 254 |
|
322 | 255 |
\item[xlisten $program$] \index{*xlisten shell script} |
104 | 256 |
is a trivial `user interface' for the X Window System. It creates two |
257 |
windows using {\tt xterm}. One executes an interactive session via |
|
258 |
\hbox{\tt teeinput $program$}, while the other displays the log file. To |
|
259 |
make a proof record, simply paste lines from the log file into an editor |
|
260 |
window. |
|
261 |
||
322 | 262 |
\item[expandshort $files$] \index{*expandshort shell script} |
104 | 263 |
reads the {\it files\/} and replaces all occurrences of the shorthand |
286 | 264 |
commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the |
265 |
corresponding full commands. Shorthand commands should appear one |
|
104 | 266 |
per line. The old versions of the files |
267 |
are renamed to have the suffix~\verb'~~'. |
|
322 | 268 |
\end{ttdescription} |
104 | 269 |
|
270 |
\index{sessions|)} |