4 \chapter{Basic Use of Isabelle}\index{sessions|(}
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.
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
15 finally esoteric functions. Use the Index when you are looking for the
16 definition of a particular Isabelle function.
18 A few examples are presented. Many examples files are distributed with
19 Isabelle, however; please experiment interactively.
22 \section{Basic interaction with Isabelle}
23 \index{starting up|bold}\nobreak
25 We assume that your local Isabelle administrator (this might be you!)
26 has already installed the \Pure\ system and several object-logics
27 properly --- otherwise see the {\tt INSTALL} file in the top-level
28 directory of the distribution on how to build it.
30 \medskip Let $\langle isabellehome \rangle$ denote the location where
31 the distribution has been installed. To run Isabelle from a the shell
32 prompt within an ordinary text terminal session, simply type
34 \({\langle}isabellehome{\rangle}\)/bin/isabelle
36 This should start an interactive \ML{} session with the default
37 object-logic already preloaded.
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.
43 The object-logic image to load may be also specified explicitly as an
44 argument to the {\tt isabelle} command, e.g.
48 This should put you into the world of polymorphic first-order logic
49 (assuming that {\FOL} has been pre-built).
51 \index{saving your work|bold} Isabelle provides no means of storing
52 theorems or internal proof objects on files. Theorems are simply part
53 of the \ML{} state. To save your work between sessions, you must dump
54 the \ML{} system state to a file. This is done automatically when
55 ending the session normally (e.g.\ by typing control-D), provided that
56 the image has been opened \emph{writable} in the first place. The
57 standard object-logic images are usually read-only, so you probably
58 have to create a private working copy first. For example, the
59 following shell command puts you into a writable Isabelle session of
60 name \texttt{Foo} that initially contains just \FOL:
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
74 More details about the \texttt{isabelle} command may be found in the
77 \medskip Saving the state is not enough. Record, on a file, the
78 top-level commands that generate your theories and proofs. Such a
79 record allows you to replay the proofs whenever required, for instance
80 after making minor changes to the axioms. Ideally, your record will
81 be somewhat intelligible to others as a formal description of your
84 \medskip There are more comfortable user interfaces than the
85 bare-bones \ML{} top-level run from a text terminal. The
86 \texttt{Isabelle} executable (note the capital I) runs one such
87 interface, depending on your local configuration. Furthermore there
88 are a number of external utilities available. These are started
89 uniformly via the \texttt{isatool} wrapper. See the \emph{System
90 Manual} for more information user interfaces and utilities.
93 \section{Ending a session}
100 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
103 \item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
104 code \(i\) to the operating system.
106 \item[\ttindexbold{commit}();] saves the current state without ending
107 the session, provided that the logic image is opened read-write.
110 Typing control-D also finishes the session in essentially the same way
111 as the sequence {\tt commit(); quit();} would.
114 \section{Reading ML files}
115 \index{files!reading}
120 time_use : string -> unit
122 \begin{ttdescription}
123 \item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
124 {\it dir}. This is the default directory for reading files.
126 \item[\ttindexbold{pwd}();] returns the full path of the current
129 \item[\ttindexbold{use} "$file$";]
130 reads the given {\it file} as input to the \ML{} session. Reading a file
131 of Isabelle commands is the usual way of replaying a proof.
133 \item[\ttindexbold{time_use} "$file$";]
134 performs {\tt use~"$file$"} and prints the total execution time.
137 The $dir$ and $file$ specifications of the \texttt{cd} and
138 \texttt{use} commands may contain path variables that are expanded
139 appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}
140 (which abbreviates \texttt{\$HOME}). Section~\ref{LoadingTheories}
141 describes commands for loading theory files.
144 \section{Setting flags}
146 set : bool ref -> bool
147 reset : bool ref -> bool
148 toggle : bool ref -> bool
149 \end{ttbox}\index{*set}\index{*reset}\index{*toggle}
150 These are some shorthands for manipulating boolean references. The new
154 \section{Printing of terms and theorems}\label{sec:printing-control}
155 \index{printing control|(}
156 Isabelle's pretty printer is controlled by a number of parameters.
158 \subsection{Printing limits}
160 Pretty.setdepth : int -> unit
161 Pretty.setmargin : int -> unit
162 print_depth : int -> unit
164 These set limits for terminal output. See also {\tt goals_limit},
165 which limits the number of subgoals printed
166 (\S\ref{sec:goals-printing}).
168 \begin{ttdescription}
169 \item[\ttindexbold{Pretty.setdepth} \(d\);]
170 tells Isabelle's pretty printer to limit the printing depth to~$d$. This
171 affects Isabelle's display of theorems and terms. The default value
172 is~0, which permits printing to an arbitrary depth. Useful values for
175 \item[\ttindexbold{Pretty.setmargin} \(m\);]
176 tells Isabelle's pretty printer to assume a right margin (page width)
177 of~$m$. The initial margin is~76.
179 \item[\ttindexbold{print_depth} \(n\);]
180 limits the printing depth of complex \ML{} values, such as theorems and
181 terms. This command affects the \ML{} top level and its effect is
182 compiler-dependent. Typically $n$ should be less than~10.
186 \subsection{Printing of hypotheses, brackets, types etc.}
187 \index{meta-assumptions!printing of}
188 \index{types!printing of}\index{sorts!printing of}
190 show_hyps : bool ref \hfill{\bf initially true}
191 show_brackets : bool ref \hfill{\bf initially false}
192 show_types : bool ref \hfill{\bf initially false}
193 show_sorts : bool ref \hfill{\bf initially false}
194 show_consts : bool ref \hfill{\bf initially false}
195 long_names : bool ref \hfill{\bf initially false}
197 These flags allow you to control how much information is displayed for
198 types, terms and theorems. The hypotheses of theorems \emph{are}
199 normally shown. Superfluous parentheses of types and terms are not.
200 Types and sorts of variables are normally hidden.
202 Note that displaying types and sorts may explain why a polymorphic
203 inference rule fails to resolve with some goal, or why a rewrite rule
204 does not apply as expected.
206 \begin{ttdescription}
208 \item[reset \ttindexbold{show_hyps};] makes Isabelle show each
209 meta-level hypothesis as a dot.
211 \item[set \ttindexbold{show_brackets};] makes Isabelle show full
212 bracketing. In particular, this reveals the grouping of infix
215 \item[set \ttindexbold{show_types};] makes Isabelle show types when
216 printing a term or theorem.
218 \item[set \ttindexbold{show_sorts};] makes Isabelle show both types
219 and the sorts of type variables, independently of the value of
222 \item[set \ttindexbold{show_consts};] makes Isabelle show types of
223 constants, provided that showing of types is enabled at all. This
224 is supported for printing of proof states only. Note that the
225 output can be enormous as polymorphic constants often occur at
226 several different type instances.
228 \item[set \ttindexbold{long_names};] forces names of all objects
229 (types, constants, theorems, etc.) to be printed in their fully
230 qualified internal form.
235 \subsection{$\eta$-contraction before printing}
237 eta_contract: bool ref \hfill{\bf initially false}
239 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
240 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of
241 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order
242 unification frequently puts terms into a fully $\eta$-expanded form. For
243 example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
244 $\lambda h.F(\lambda x.h(x))$. By default, the user sees this expanded
247 \begin{ttdescription}
248 \item[set \ttindexbold{eta_contract};]
249 makes Isabelle perform $\eta$-contractions before printing, so that
250 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$. The
251 distinction between a term and its $\eta$-expanded form occasionally
254 \index{printing control|)}
256 \section{Diagnostic messages}
257 \index{error messages}
260 Isabelle conceptually provides three output channels for different
261 kinds of messages: ordinary text, warnings, errors. Depending on the
262 user interface involved, these messages may appear in different text
263 styles or colours, even within separate windows.
265 The default setup of an \texttt{isabelle} terminal session is as
266 follows: plain output of ordinary text, warnings prefixed by
267 \texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s. For example, a
268 typical warning would look like this:
270 \#\#\# Beware the Jabberwock, my son!
271 \#\#\# The jaws that bite, the claws that catch!
272 \#\#\# Beware the Jubjub Bird, and shun
273 \#\#\# The frumious Bandersnatch!
276 \texttt{ML} programs may output diagnostic messages using the
279 writeln : string -> unit
280 warning : string -> unit
283 Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
284 after having output the text, while \ttindex{writeln} and
285 \ttindex{warning} resume normal program execution.
288 \section{Displaying exceptions as error messages}
289 \index{exceptions!printing of}
293 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
294 and {\tt RSN}, are called both interactively and from programs. They
295 indicate errors not by printing messages, but by raising exceptions. For
296 interactive use, \ML's reporting of an uncaught exception may be
297 uninformative. The Poly/ML function {\tt exception_trace} can generate a
298 backtrace.\index{Poly/{\ML} compiler}
300 \begin{ttdescription}
301 \item[\ttindexbold{print_exn} $e$]
302 displays the exception~$e$ in a readable manner, and then re-raises~$e$.
303 Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
304 $EXP$ is an expression that may raise an exception.
306 {\tt print_exn} can display the following common exceptions, which concern
307 types, terms, theorems and theories, respectively. Each carries a message
308 and related information.
310 exception TYPE of string * typ list * term list
311 exception TERM of string * term list
312 exception THM of string * int * thm list
313 exception THEORY of string * theory list
317 {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
318 pretty printing information from the proof state last stored in the
319 subgoal module. The appearance of the output thus depends upon the
320 theory used in the last interactive proof.
328 %%% TeX-master: "ref"