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