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 example 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!) has
26 already installed the Isabelle system together with appropriate object-logics
27 --- otherwise see the \texttt{README} and \texttt{INSTALL} files in the
28 top-level directory of the distribution on how to do this.
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 object-logic
37 (usually {\HOL}) already pre-loaded.
39 Subsequently, we assume that the \texttt{isabelle} executable is determined
40 automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
41 \rangle\)/bin} to your search path.\footnote{Depending on your installation,
42 there might be also stand-alone binaries located in some global directory
43 such as \texttt{/usr/bin}. Do not attempt to copy {\tt \(\langle
44 isabellehome \rangle\)/bin/isabelle}, though! See \texttt{isatool
45 install} in \emph{The Isabelle System Manual} of how to do this properly.}
47 The object-logic image to load may be also specified explicitly as an argument
48 to the {\tt isabelle} command, e.g.
52 This should put you into the world of polymorphic first-order logic (assuming
53 that an image of {\FOL} has been pre-built).
55 \index{saving your session|bold} Isabelle provides no means of storing
56 theorems or internal proof objects on files. Theorems are simply part of the
57 \ML{} state. To save your work between sessions, you may dump the \ML{}
58 system state to a file. This is done automatically when ending the session
59 normally (e.g.\ by typing control-D), provided that the image has been opened
60 \emph{writable} in the first place. The standard object-logic images are
61 usually read-only, so you have to create a private working copy first. For
62 example, the following shell command puts you into a writable Isabelle session
63 of name \texttt{Foo} that initially contains just plain \HOL:
67 Ending the \texttt{Foo} session with control-D will cause the complete
68 \ML-world to be saved somewhere in your home directory\footnote{The default
69 location is in \texttt{\~\relax/isabelle/heaps}, but this depends on your
70 local configuration.}. Make sure there is enough space available! Then one
71 may later continue at exactly the same point by running
76 \medskip Saving the {\ML} state is not enough. Record, on a file, the
77 top-level commands that generate your theories and proofs. Such a record
78 allows you to replay the proofs whenever required, for instance after making
79 minor changes to the axioms. Ideally, your these sources will be somewhat
80 intelligible to others as a formal description of your work.
82 It is good practice to put all source files that constitute a separate
83 Isabelle session into an individual directory, together with an {\ML} file
84 called \texttt{ROOT.ML} that contains appropriate commands to load all other
85 files required. Running \texttt{isabelle} with option \texttt{-u}
86 automatically loads \texttt{ROOT.ML} on entering the session. The
87 \texttt{isatool usedir} utility provides some more options to manage your
88 sessions, such as automatic generation of theory browsing information.
90 \medskip More details about the \texttt{isabelle} and \texttt{isatool}
91 commands may be found in \emph{The Isabelle System Manual}.
93 \medskip There are more comfortable user interfaces than the bare-bones \ML{}
94 top-level run from a text terminal. The \texttt{Isabelle} executable (note
95 the capital I) runs one such interface, depending on your local configuration.
96 Again, see \emph{The Isabelle System Manual} for more information.
99 \section{Ending a session}
103 commit : unit -> bool
105 \begin{ttdescription}
106 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
109 \item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
110 code \(i\) to the operating system.
112 \item[\ttindexbold{commit}();] saves the current state without ending
113 the session, provided that the logic image is opened read-write;
114 return value {\tt false} indicates an error.
117 Typing control-D also finishes the session in essentially the same way
118 as the sequence {\tt commit(); quit();} would.
121 \section{Reading ML files}
122 \index{files!reading}
127 time_use : string -> unit
129 \begin{ttdescription}
130 \item[\ttindexbold{cd} "{\it dir}";] changes the current directory to
131 {\it dir}. This is the default directory for reading files.
133 \item[\ttindexbold{pwd}();] returns the full path of the current
136 \item[\ttindexbold{use} "$file$";]
137 reads the given {\it file} as input to the \ML{} session. Reading a file
138 of Isabelle commands is the usual way of replaying a proof.
140 \item[\ttindexbold{time_use} "$file$";]
141 performs {\tt use~"$file$"} and prints the total execution time.
144 The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
145 commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
146 expanded appropriately. Note that \texttt{\~\relax} abbreviates
147 \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
148 \texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}.
151 \section{Reading theories}\label{sec:intro-theories}
152 \index{theories!reading}
154 In Isabelle, any kind of declarations, definitions, etc.\ are organized around
155 named \emph{theory} objects. Logical reasoning always takes place within a
156 certain theory context, which may be switched at any time. Theory $name$ is
157 defined by a theory file $name$\texttt{.thy}, containing declarations of
158 \texttt{consts}, \texttt{types}, \texttt{defs}, etc.\ (see
159 \S\ref{sec:ref-defining-theories} for more details on concrete syntax).
160 Furthermore, there may be an associated {\ML} file $name$\texttt{.ML} with
161 proof scripts that are to be run in the context of the theory.
164 context : theory -> unit
165 the_context : unit -> theory
166 theory : string -> theory
167 use_thy : string -> unit
168 time_use_thy : string -> unit
171 \begin{ttdescription}
173 \item[\ttindexbold{context} $thy$;] switches the current theory context. Any
174 subsequent command with ``implicit theory argument'' (e.g.\ \texttt{Goal})
175 will refer to $thy$ as its theory.
177 \item[\ttindexbold{the_context}();] obtains the current theory context, or
178 raises an error if absent.
180 \item[\ttindexbold{theory} "$name$";] retrieves the theory called $name$ from
181 the internal database of loaded theories, raising an error if absent.
183 \item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file
184 system, looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML};
185 also makes sure that all parent theories are loaded as well. In case some
186 older versions have already been present, \texttt{use_thy} only tries to
187 reload $name$ itself, but is content with any version of its parents.
189 \item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but
190 reports the time taken to process the actual theory parts and {\ML} files
195 See \S\ref{sec:more-theories} for further information on Isabelle's theory
199 \section{Setting flags}
201 set : bool ref -> bool
202 reset : bool ref -> bool
203 toggle : bool ref -> bool
204 \end{ttbox}\index{*set}\index{*reset}\index{*toggle}
205 These are some shorthands for manipulating boolean references. The new
209 \section{Printing of terms and theorems}\label{sec:printing-control}
210 \index{printing control|(}
211 Isabelle's pretty printer is controlled by a number of parameters.
213 \subsection{Printing limits}
215 Pretty.setdepth : int -> unit
216 Pretty.setmargin : int -> unit
217 print_depth : int -> unit
219 These set limits for terminal output. See also {\tt goals_limit},
220 which limits the number of subgoals printed
221 (\S\ref{sec:goals-printing}).
223 \begin{ttdescription}
224 \item[\ttindexbold{Pretty.setdepth} \(d\);]
225 tells Isabelle's pretty printer to limit the printing depth to~$d$. This
226 affects Isabelle's display of theorems and terms. The default value
227 is~0, which permits printing to an arbitrary depth. Useful values for
230 \item[\ttindexbold{Pretty.setmargin} \(m\);]
231 tells Isabelle's pretty printer to assume a right margin (page width)
232 of~$m$. The initial margin is~76.
234 \item[\ttindexbold{print_depth} \(n\);]
235 limits the printing depth of complex \ML{} values, such as theorems and
236 terms. This command affects the \ML{} top level and its effect is
237 compiler-dependent. Typically $n$ should be less than~10.
241 \subsection{Printing of hypotheses, brackets, types etc.}
242 \index{meta-assumptions!printing of}
243 \index{types!printing of}\index{sorts!printing of}
245 show_hyps : bool ref \hfill{\bf initially true}
246 show_tags : bool ref \hfill{\bf initially false}
247 show_brackets : bool ref \hfill{\bf initially false}
248 show_types : bool ref \hfill{\bf initially false}
249 show_sorts : bool ref \hfill{\bf initially false}
250 show_consts : bool ref \hfill{\bf initially false}
251 long_names : bool ref \hfill{\bf initially false}
253 These flags allow you to control how much information is displayed for
254 types, terms and theorems. The hypotheses of theorems \emph{are}
255 normally shown. Superfluous parentheses of types and terms are not.
256 Types and sorts of variables are normally hidden.
258 Note that displaying types and sorts may explain why a polymorphic
259 inference rule fails to resolve with some goal, or why a rewrite rule
260 does not apply as expected.
262 \begin{ttdescription}
264 \item[reset \ttindexbold{show_hyps};] makes Isabelle show each
265 meta-level hypothesis as a dot.
267 \item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
268 (which are basically just comments that may be attached by some tools).
270 \item[set \ttindexbold{show_brackets};] makes Isabelle show full
271 bracketing. In particular, this reveals the grouping of infix
274 \item[set \ttindexbold{show_types};] makes Isabelle show types when
275 printing a term or theorem.
277 \item[set \ttindexbold{show_sorts};] makes Isabelle show both types
278 and the sorts of type variables, independently of the value of
281 \item[set \ttindexbold{show_consts};] makes Isabelle show types of
282 constants, provided that showing of types is enabled at all. This
283 is supported for printing of proof states only. Note that the
284 output can be enormous as polymorphic constants often occur at
285 several different type instances.
287 \item[set \ttindexbold{long_names};] forces names of all objects
288 (types, constants, theorems, etc.) to be printed in their fully
289 qualified internal form.
294 \subsection{$\eta$-contraction before printing}
296 eta_contract: bool ref \hfill{\bf initially false}
298 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
299 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of
300 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order
301 unification frequently puts terms into a fully $\eta$-expanded form. For
302 example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
303 $\lambda h.F(\lambda x.h(x))$. By default, the user sees this expanded
306 \begin{ttdescription}
307 \item[set \ttindexbold{eta_contract};]
308 makes Isabelle perform $\eta$-contractions before printing, so that
309 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$. The
310 distinction between a term and its $\eta$-expanded form occasionally
313 \index{printing control|)}
315 \section{Diagnostic messages}
316 \index{error messages}
319 Isabelle conceptually provides three output channels for different kinds of
320 messages: ordinary text, warnings, errors. Depending on the user interface
321 involved, these messages may appear in different text styles or colours.
323 The default setup of an \texttt{isabelle} terminal session is as
324 follows: plain output of ordinary text, warnings prefixed by
325 \texttt{\#\#\#}'s, errors prefixed by \texttt{***}'s. For example, a
326 typical warning would look like this:
328 \#\#\# Beware the Jabberwock, my son!
329 \#\#\# The jaws that bite, the claws that catch!
330 \#\#\# Beware the Jubjub Bird, and shun
331 \#\#\# The frumious Bandersnatch!
334 \texttt{ML} programs may output diagnostic messages using the
337 writeln : string -> unit
338 warning : string -> unit
341 Note that \ttindex{error} fails by raising exception \ttindex{ERROR}
342 after having output the text, while \ttindex{writeln} and
343 \ttindex{warning} resume normal program execution.
346 \section{Displaying exceptions as error messages}
347 \index{exceptions!printing of}
351 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
352 and {\tt RSN}, are called both interactively and from programs. They
353 indicate errors not by printing messages, but by raising exceptions. For
354 interactive use, \ML's reporting of an uncaught exception may be
355 uninformative. The Poly/ML function {\tt exception_trace} can generate a
356 backtrace.\index{Poly/{\ML} compiler}
358 \begin{ttdescription}
359 \item[\ttindexbold{print_exn} $e$]
360 displays the exception~$e$ in a readable manner, and then re-raises~$e$.
361 Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
362 $EXP$ is an expression that may raise an exception.
364 {\tt print_exn} can display the following common exceptions, which concern
365 types, terms, theorems and theories, respectively. Each carries a message
366 and related information.
368 exception TYPE of string * typ list * term list
369 exception TERM of string * term list
370 exception THM of string * int * thm list
371 exception THEORY of string * theory list
375 {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
376 pretty printing information from the proof state last stored in the
377 subgoal module. The appearance of the output thus depends upon the
378 theory used in the last interactive proof.
386 %%% TeX-master: "ref"