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.
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
12 finally esoteric functions. Use the Index when you are looking for the
13 definition of a particular Isabelle function.
15 A few examples are presented. Many examples files are distributed with
16 Isabelle, however; please experiment interactively.
19 \section{Basic interaction with Isabelle}
20 \index{saving your work|bold}
21 Isabelle provides no means of storing theorems or proofs on files.
22 Theorems are simply part of the \ML{} state and are named by \ML{}
23 identifiers. To save your work between sessions, you must save a copy of
24 the \ML{} image. The procedure for doing so is compiler-dependent:
25 \begin{itemize}\index{Poly/{\ML} compiler}
26 \item At the end of a session, Poly/\ML{} saves the state, provided you
27 have created a database for your own use. You can create a database by
28 copying an existing one, or by calling the Poly/\ML{} function {\tt
29 make_database}; the latter course uses much less disc space. A
30 Poly/\ML{} database {\em does not\/} save the contents of references,
31 such as the current state of a backward proof.
33 \item With New Jersey \ML{} you must save the state explicitly before
34 ending the session. While a Poly/\ML{} database can be small, a New Jersey
35 image occupies several megabytes.
37 See your \ML{} compiler's documentation for full instructions on saving the
40 Saving the state is not enough. Record, on a file, the top-level commands
41 that generate your theories and proofs. Such a record allows you to replay
42 the proofs whenever required, for instance after making minor changes to
43 the axioms. Ideally, your record will be intelligible to others as a
44 formal description of your work.
46 Since Isabelle's user interface is the \ML{} top level, some kind of window
47 support is essential. One window displays the Isabelle session, while the
48 other displays a file --- your proof record --- being edited. The Emacs
49 editor supports windows and can manage interactive sessions.
52 \section{Ending a session}
55 commit : unit -> unit \hfill{\bf Poly/ML only}
56 exportML : string -> bool \hfill{\bf New Jersey ML only}
59 \item[\ttindexbold{quit}();]
60 aborts the Isabelle session, without saving the state.
62 \item[\ttindexbold{commit}();]
63 saves the current state in your Poly/\ML{} database without ending the
64 session. The contents of references are lost, so never do this during an
65 interactive proof!\index{Poly/{\ML} compiler}
67 \item[\ttindexbold{exportML} "{\it file}";] saves an
68 image of your session to the given {\it file}.
72 Typing control-D also finishes the session, but its effect is
73 compiler-dependent. Poly/\ML{} will then save the state, if you have a
74 private database. New Jersey \ML{} will discard the state!
78 \section{Reading ML files}
83 time_use : string -> unit
85 Section~\ref{LoadingTheories} describes commands for loading theory files.
87 \item[\ttindexbold{cd} "{\it dir}";]
88 changes the current directory to {\it dir}. This is the default directory
89 for reading files and for writing temporary files.
91 \item[\ttindexbold{use} "$file$";]
92 reads the given {\it file} as input to the \ML{} session. Reading a file
93 of Isabelle commands is the usual way of replaying a proof.
95 \item[\ttindexbold{time_use} "$file$";]
96 performs {\tt use~"$file$"} and prints the total execution time.
100 \section{Printing of terms and theorems}
101 \index{printing control|(}
102 Isabelle's pretty printer is controlled by a number of parameters.
104 \subsection{Printing limits}
106 Pretty.setdepth : int -> unit
107 Pretty.setmargin : int -> unit
108 print_depth : int -> unit
110 These set limits for terminal output.
112 \begin{ttdescription}
113 \item[\ttindexbold{Pretty.setdepth} \(d\);]
114 tells Isabelle's pretty printer to limit the printing depth to~$d$. This
115 affects Isabelle's display of theorems and terms. The default value
116 is~0, which permits printing to an arbitrary depth. Useful values for
119 \item[\ttindexbold{Pretty.setmargin} \(m\);]
120 tells Isabelle's pretty printer to assume a right margin (page width)
121 of~$m$. The initial margin is~80.
123 \item[\ttindexbold{print_depth} \(n\);]
124 limits the printing depth of complex \ML{} values, such as theorems and
125 terms. This command affects the \ML{} top level and its effect is
126 compiler-dependent. Typically $n$ should be less than~10.
130 \subsection{Printing of hypotheses, types and sorts}
131 \index{meta-assumptions!printing of}
132 \index{types!printing of}\index{sorts!printing of}
134 show_hyps : bool ref \hfill{\bf initially true}
135 show_types : bool ref \hfill{\bf initially false}
136 show_sorts : bool ref \hfill{\bf initially false}
138 These flags allow you to control how much information is displayed for
139 terms and theorems. The hypotheses are normally shown; types and sorts are
140 not. Displaying types and sorts may explain why a polymorphic inference
141 rule fails to resolve with some goal.
143 \begin{ttdescription}
144 \item[\ttindexbold{show_hyps} := false;]
145 makes Isabelle show each meta-level hypothesis as a dot.
147 \item[\ttindexbold{show_types} := true;]
148 makes Isabelle show types when printing a term or theorem.
150 \item[\ttindexbold{show_sorts} := true;]
151 makes Isabelle show the sorts of type variables. It has no effect unless
152 {\tt show_types} is~{\tt true}.
156 \subsection{$\eta$-contraction before printing}
158 eta_contract: bool ref \hfill{\bf initially false}
160 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
161 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of
162 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order
163 unification frequently puts terms into a fully $\eta$-expanded form. For
164 example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
165 $\lambda h.F(\lambda x.h(x))$. By default, the user sees this expanded
168 \begin{ttdescription}
169 \item[\ttindexbold{eta_contract} := true;]
170 makes Isabelle perform $\eta$-contractions before printing, so that
171 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$. The
172 distinction between a term and its $\eta$-expanded form occasionally
175 \index{printing control|)}
178 \section{Displaying exceptions as error messages}
179 \index{exceptions!printing of}
183 Certain Isabelle primitives, such as the forward proof functions {\tt RS}
184 and {\tt RSN}, are called both interactively and from programs. They
185 indicate errors not by printing messages, but by raising exceptions. For
186 interactive use, \ML's reporting of an uncaught exception is
187 uninformative. The Poly/ML function {\tt exception_trace} can generate a
188 backtrace.\index{Poly/{\ML} compiler}
190 \begin{ttdescription}
191 \item[\ttindexbold{print_exn} $e$]
192 displays the exception~$e$ in a readable manner, and then re-raises~$e$.
193 Typical usage is~\hbox{\tt $EXP$ handle e => print_exn e;}, where
194 $EXP$ is an expression that may raise an exception.
196 {\tt print_exn} can display the following common exceptions, which concern
197 types, terms, theorems and theories, respectively. Each carries a message
198 and related information.
200 exception TYPE of string * typ list * term list
201 exception TERM of string * term list
202 exception THM of string * int * thm list
203 exception THEORY of string * theory list
207 {\tt print_exn} prints terms by calling \ttindex{prin}, which obtains
208 pretty printing information from the proof state last stored in the
209 subgoal module. The appearance of the output thus depends upon the
210 theory used in the last interactive proof.
213 \section{Shell scripts}
214 \index{shell scripts|bold} The following files are distributed with
215 Isabelle, and work under Unix$^{\rm TM}$. They can be executed as commands
216 to the Unix shell. Some of them depend upon shell environment variables.
217 \begin{ttdescription}
218 \item[make-all $switches$] \index{*make-all shell script}
219 compiles the Isabelle system, when executed on the source directory.
220 Environment variables specify which \ML{} compiler to use. These
221 variables, and the {\it switches}, are documented on the file itself.
223 \item[teeinput $program$] \index{*teeinput shell script}
224 executes the {\it program}, while piping the standard input to a log file
225 designated by the \verb|$LISTEN| environment variable. Normally the
226 program is Isabelle, and the log file receives a copy of all the Isabelle
229 \item[xlisten $program$] \index{*xlisten shell script}
230 is a trivial `user interface' for the X Window System. It creates two
231 windows using {\tt xterm}. One executes an interactive session via
232 \hbox{\tt teeinput $program$}, while the other displays the log file. To
233 make a proof record, simply paste lines from the log file into an editor
236 \item[expandshort $files$] \index{*expandshort shell script}
237 reads the {\it files\/} and replaces all occurrences of the shorthand
238 commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the
239 corresponding full commands. Shorthand commands should appear one
240 per line. The old versions of the files
241 are renamed to have the suffix~\verb'~~'.