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