7046
|
1 |
|
|
2 |
\chapter{Introduction}
|
|
3 |
|
12618
|
4 |
\section{Overview}
|
|
5 |
|
|
6 |
The \emph{Isabelle} system essentially provides a generic infrastructure for
|
|
7 |
building deductive systems (programmed in Standard ML), with a special focus
|
|
8 |
on interactive theorem proving in higher-order logics. In the olden days even
|
|
9 |
end-users would refer to certain ML functions (goal commands, tactics,
|
|
10 |
tacticals etc.) to pursue their everyday theorem proving needs
|
|
11 |
\cite{isabelle-intro,isabelle-ref}.
|
|
12 |
|
|
13 |
In contrast \emph{Isar} provides an interpreted language environment of its
|
|
14 |
own, which has been specifically tailored for the needs of theory and proof
|
|
15 |
development. Compared to raw ML, the Isabelle/Isar top-level provides a more
|
|
16 |
robust and comfortable development platform, with proper support for theory
|
|
17 |
development graphs, single-step evaluation with unlimited undo, etc. The
|
|
18 |
Isabelle/Isar version of the \emph{Proof~General} user interface
|
|
19 |
\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
|
|
20 |
interactive theory and proof development.
|
|
21 |
|
|
22 |
\medskip Apart from these technical advances over bare-bones ML programming,
|
|
23 |
the main intention of Isar is to provide a conceptually different view on
|
|
24 |
machine-checked proofs \cite{Wenzel:1999:TPHOL, Wenzel-PhD} --- ``Isar''
|
|
25 |
stands for ``Intelligible semi-automated reasoning''. Drawing from both the
|
|
26 |
traditions of informal mathematical proof texts and high-level programming
|
|
27 |
languages, Isar provides a versatile environment for structured formal proof
|
|
28 |
documents. Thus properly written Isar proof texts become accessible to a
|
|
29 |
broader audience than unstructured tactic scripts (which typically only
|
|
30 |
provide operational information for the machine). Writing human-readable
|
|
31 |
proof texts certainly requires some additional efforts by the writer in order
|
|
32 |
to achieve a good presentation --- both of formal and informal parts of the
|
|
33 |
text. On the other hand, human-readable formal texts gain some value in their
|
|
34 |
own right, independently of the mechanic proof-checking process.
|
|
35 |
|
|
36 |
Despite its grand design of structured proof texts, Isar is able to assimilate
|
|
37 |
the old-style tactical as an ``improper'' sub-language. This provides an easy
|
|
38 |
upgrade path for existing tactic scripts, as well as additional means for
|
|
39 |
experimentation and debugging of interactive proofs. Isabelle/Isar freely
|
|
40 |
supports a broad range of proof styles, including unreadable ones.
|
|
41 |
|
|
42 |
\medskip The Isabelle/Isar framework generic and should work for reasonably
|
|
43 |
well for any object-logic that directly conforms to the view of natural
|
|
44 |
deduction according to the Isabelle/Pure framework. Major Isabelle logics
|
|
45 |
(HOL \cite{isabelle-HOL}, HOLCF, FOL \cite{isabelle-logics}, ZF
|
|
46 |
\cite{isabelle-ZF}) have already been setup for immediate use by end-users.
|
|
47 |
|
|
48 |
Note that much of the existing body of theories still consist of old-style
|
|
49 |
theory files with accompanied ML code for proof scripts. This legacy will be
|
|
50 |
converted as time goes by.
|
|
51 |
|
|
52 |
|
7167
|
53 |
\section{Quick start}
|
|
54 |
|
8508
|
55 |
\subsection{Terminal sessions}
|
|
56 |
|
7175
|
57 |
Isar is already part of Isabelle (as of version Isabelle99, or later). The
|
9604
|
58 |
\texttt{isabelle} binary provides option \texttt{-I} to run the Isabelle/Isar
|
|
59 |
interaction loop at startup, rather than the raw ML top-level. So the
|
|
60 |
quickest way to do anything with Isabelle/Isar is as follows:
|
7175
|
61 |
\begin{ttbox}
|
|
62 |
isabelle -I HOL\medskip
|
9272
|
63 |
\out{> Welcome to Isabelle/HOL (Isabelle99-1)}\medskip
|
7175
|
64 |
theory Foo = Main:
|
7297
|
65 |
constdefs foo :: nat "foo == 1";
|
|
66 |
lemma "0 < foo" by (simp add: foo_def);
|
7175
|
67 |
end
|
|
68 |
\end{ttbox}
|
9233
|
69 |
Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See
|
10160
|
70 |
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
|
10110
|
71 |
comprehensive overview of available commands and other language elements.
|
7175
|
72 |
|
8508
|
73 |
|
8843
|
74 |
\subsection{Proof~General}
|
8508
|
75 |
|
|
76 |
Plain TTY-based interaction as above used to be quite feasible with
|
8547
|
77 |
traditional tactic based theorem proving, but developing Isar documents really
|
8508
|
78 |
demands some better user-interface support. David Aspinall's
|
|
79 |
\emph{Proof~General}\index{Proof General} environment
|
8547
|
80 |
\cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs interface for
|
|
81 |
interactive theorem provers that does all the cut-and-paste and
|
8508
|
82 |
forward-backward walk through the text in a very neat way. In Isabelle/Isar,
|
|
83 |
the current position within a partial proof document is equally important than
|
|
84 |
the actual proof state. Thus Proof~General provides the canonical working
|
|
85 |
environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
|
8547
|
86 |
existing Isar documents) and for production work.
|
7175
|
87 |
|
8843
|
88 |
|
|
89 |
\subsubsection{Proof~General as default Isabelle interface}
|
7167
|
90 |
|
9849
|
91 |
The easiest way to invoke Proof~General is via the Isabelle interface wrapper
|
|
92 |
script. The default configuration of Isabelle is smart enough to detect the
|
|
93 |
Proof~General distribution in several canonical places (e.g.\
|
|
94 |
\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus the capital
|
|
95 |
\texttt{Isabelle} executable would already refer to the
|
|
96 |
\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
|
|
97 |
also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
|
|
98 |
ML.} The Isabelle interface script provides several options, just pass
|
|
99 |
\verb,-?, to see its usage.
|
7981
|
100 |
|
7175
|
101 |
With the proper Isabelle interface setup, Isar documents may now be edited by
|
|
102 |
visiting appropriate theory files, e.g.\
|
|
103 |
\begin{ttbox}
|
|
104 |
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
|
|
105 |
\end{ttbox}
|
7315
|
106 |
Users of XEmacs may note the tool bar for navigating forward and backward
|
8516
|
107 |
through the text. Consult the Proof~General documentation \cite{proofgeneral}
|
8547
|
108 |
for further basic command sequences, such as ``\texttt{C-c C-return}'' or
|
|
109 |
``\texttt{C-c u}''.
|
8508
|
110 |
|
9849
|
111 |
\medskip
|
|
112 |
|
|
113 |
Proof~General may be also configured manually by giving Isabelle settings like
|
|
114 |
this (see also \cite{isabelle-sys}):
|
|
115 |
\begin{ttbox}
|
|
116 |
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
|
|
117 |
PROOFGENERAL_OPTIONS=""
|
|
118 |
\end{ttbox}
|
|
119 |
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
|
|
120 |
actual installation directory of Proof~General.
|
|
121 |
|
|
122 |
\medskip
|
|
123 |
|
|
124 |
Apart from the Isabelle command line, defaults for interface options may be
|
|
125 |
given by the \texttt{PROOFGENERAL_OPTIONS} setting as well. For example, the
|
|
126 |
Emacs executable to be used may be configured in Isabelle's settings like this:
|
|
127 |
\begin{ttbox}
|
|
128 |
PROOFGENERAL_OPTIONS="-p xemacs-nomule"
|
|
129 |
\end{ttbox}
|
|
130 |
|
|
131 |
Occasionally, the user's \verb,~/.emacs, file contains material that is
|
|
132 |
incompatible with the version of Emacs that Proof~General prefers. Then
|
|
133 |
proper startup may be still achieved by using the \texttt{-u false} option.
|
|
134 |
Also note that any Emacs lisp file called \texttt{proofgeneral-settings.el}
|
|
135 |
occurring in \texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}
|
|
136 |
is automatically loaded by the Proof~General interface script as well.
|
|
137 |
|
8843
|
138 |
|
|
139 |
\subsubsection{The X-Symbol package}
|
8508
|
140 |
|
|
141 |
Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which
|
|
142 |
provides a nice way to get proper mathematical symbols displayed on screen.
|
|
143 |
Just pass option \texttt{-x true} to the Isabelle interface script, or check
|
8516
|
144 |
the appropriate menu setting by hand. In any case, the X-Symbol package must
|
|
145 |
have been properly installed already.
|
|
146 |
|
8843
|
147 |
Contrary to what you may expect from the documentation of X-Symbol, the
|
9849
|
148 |
package is very easy to install and configures itself automatically. The
|
|
149 |
default configuration of Isabelle is smart enough to detect the X-Symbol
|
|
150 |
package in several canonical places (e.g.\
|
|
151 |
\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
|
8843
|
152 |
|
|
153 |
\medskip
|
|
154 |
|
|
155 |
Using proper mathematical symbols in Isabelle theories can be very convenient
|
|
156 |
for readability of large formulas. On the other hand, the plain ASCII sources
|
10160
|
157 |
easily become somewhat unintelligible. For example, $\Longrightarrow$ would
|
9849
|
158 |
appear as \verb,\<Longrightarrow>, according the default set of Isabelle
|
|
159 |
symbols. Nevertheless, the Isabelle document preparation system (see
|
|
160 |
\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
|
|
161 |
It is even possible to invent additional notation beyond the display
|
|
162 |
capabilities of XEmacs and X-Symbol.
|
7175
|
163 |
|
7981
|
164 |
|
|
165 |
\section{Isabelle/Isar theories}
|
|
166 |
|
8547
|
167 |
Isabelle/Isar offers the following main improvements over classic Isabelle.
|
7981
|
168 |
\begin{enumerate}
|
|
169 |
\item A new \emph{theory format}, occasionally referred to as ``new-style
|
|
170 |
theories'', supporting interactive development and unlimited undo operation.
|
|
171 |
\item A \emph{formal proof document language} designed to support intelligible
|
|
172 |
semi-automated reasoning. Instead of putting together unreadable tactic
|
|
173 |
scripts, the author is enabled to express the reasoning in way that is close
|
8508
|
174 |
to usual mathematical practice.
|
8547
|
175 |
\item A simple document preparation system, for typesetting formal
|
|
176 |
developments together with informal text. The resulting hyper-linked PDF
|
|
177 |
documents are equally well suited for WWW presentation and as printed
|
|
178 |
copies.
|
7981
|
179 |
\end{enumerate}
|
|
180 |
|
|
181 |
The Isar proof language is embedded into the new theory format as a proper
|
|
182 |
sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
|
|
183 |
$\LEMMANAME$ at the theory level, and left again with the final conclusion
|
|
184 |
(e.g.\ via $\QEDNAME$). A few theory extension mechanisms require proof as
|
8547
|
185 |
well, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness of the
|
|
186 |
representing sets.
|
7460
|
187 |
|
7981
|
188 |
New-style theory files may still be associated with separate ML files
|
|
189 |
consisting of plain old tactic scripts. There is no longer any ML binding
|
|
190 |
generated for the theory and theorems, though. ML functions \texttt{theory},
|
|
191 |
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
|
|
192 |
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
|
|
193 |
relatively easy. Thus users may start to benefit from interactive theory
|
8547
|
194 |
development and document preparation, even before they have any idea of the
|
|
195 |
Isar proof language at all.
|
7981
|
196 |
|
|
197 |
\begin{warn}
|
8547
|
198 |
Currently, Proof~General does \emph{not} support mixed interactive
|
7981
|
199 |
development of classic Isabelle theory files or tactic scripts, together
|
|
200 |
with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
|
|
201 |
Proof~General are handled as two different theorem proving systems, only one
|
|
202 |
of these may be active at the same time.
|
|
203 |
\end{warn}
|
|
204 |
|
10160
|
205 |
Conversion of existing tactic scripts is best done by running two separate
|
7981
|
206 |
Proof~General sessions, one for replaying the old script and the other for the
|
10160
|
207 |
emerging Isabelle/Isar document. Also note that Isar supports emulation
|
|
208 |
commands and methods that support traditional tactic scripts within new-style
|
|
209 |
theories, see appendix~\ref{ap:conv} for more information.
|
7981
|
210 |
|
7167
|
211 |
|
8843
|
212 |
\subsection{Document preparation}\label{sec:document-prep}
|
8684
|
213 |
|
|
214 |
Isabelle/Isar provides a simple document preparation system based on current
|
|
215 |
(PDF) {\LaTeX} technology, with full support of hyper-links (both local
|
|
216 |
references and URLs), bookmarks, thumbnails etc. Thus the results are equally
|
|
217 |
well suited for WWW browsing and as printed copies.
|
|
218 |
|
|
219 |
\medskip
|
|
220 |
|
|
221 |
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
|
|
222 |
session} (see also \cite{isabelle-sys}). Getting started with a working
|
|
223 |
configuration for common situations is quite easy by using the Isabelle
|
|
224 |
\texttt{mkdir} and \texttt{make} tools. Just invoke
|
|
225 |
\begin{ttbox}
|
|
226 |
isatool mkdir -d Foo
|
|
227 |
\end{ttbox}
|
|
228 |
to setup a separate directory for session \texttt{Foo}.\footnote{It is safe to
|
|
229 |
experiment, since \texttt{isatool mkdir} never overwrites existing files.}
|
|
230 |
Ensure that \texttt{Foo/ROOT.ML} loads all theories required for this session.
|
|
231 |
Furthermore \texttt{Foo/document/root.tex} should include any special {\LaTeX}
|
|
232 |
macro packages required for your document (the default is usually sufficient
|
|
233 |
as a start).
|
|
234 |
|
|
235 |
The session is controlled by a separate \texttt{IsaMakefile} (with very crude
|
|
236 |
source dependencies only by default). This file is located one level up from
|
|
237 |
the \texttt{Foo} directory location. At that point just invoke
|
|
238 |
\begin{ttbox}
|
|
239 |
isatool make Foo
|
|
240 |
\end{ttbox}
|
|
241 |
to run the \texttt{Foo} session, with browser information and document
|
|
242 |
preparation enabled. Unless any errors are reported by Isabelle or {\LaTeX},
|
|
243 |
the output will appear inside the directory indicated by \texttt{isatool
|
|
244 |
getenv ISABELLE_BROWSER_INFO}, with the logical session prefix added (e.g.\
|
|
245 |
\texttt{HOL/Foo}). Note that the \texttt{index.html} located there provides a
|
|
246 |
link to the finished {\LaTeX} document, too.
|
|
247 |
|
|
248 |
Note that this really is batch processing --- better let Isabelle check your
|
|
249 |
theory and proof developments beforehand in interactive mode.
|
|
250 |
|
|
251 |
\medskip
|
|
252 |
|
|
253 |
You may also consider to tune the \texttt{usedir} options in
|
|
254 |
\texttt{IsaMakefile}, for example to change the output format from
|
|
255 |
\texttt{dvi} to \texttt{pdf}, or activate the \texttt{-D document} option in
|
|
256 |
order to preserve a copy of the generated {\LaTeX} sources. The latter
|
|
257 |
feature is very useful for debugging {\LaTeX} errors, while avoiding repeated
|
|
258 |
runs of Isabelle.
|
|
259 |
|
|
260 |
\medskip
|
|
261 |
|
|
262 |
See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
|
|
263 |
on Isabelle logic sessions and theory presentation.
|
|
264 |
|
|
265 |
|
10160
|
266 |
\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
|
7167
|
267 |
|
7297
|
268 |
This is one of the key questions, of course. Isar offers a rather different
|
|
269 |
approach to formal proof documents than plain old tactic scripts. Experienced
|
|
270 |
users of existing interactive theorem proving systems may have to learn
|
7895
|
271 |
thinking differently in order to make effective use of Isabelle/Isar. On the
|
7297
|
272 |
other hand, Isabelle/Isar comes much closer to existing mathematical practice
|
|
273 |
of formal proof, so users with less experience in old-style tactical proving,
|
7895
|
274 |
but a good understanding of mathematical proof, might cope with Isar even
|
10160
|
275 |
better. See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further
|
|
276 |
background information on Isar.
|
7297
|
277 |
|
10160
|
278 |
\medskip This really is a reference manual on Isabelle/Isar, not a tutorial.
|
|
279 |
Nevertheless, we will also give some clues of how the concepts introduced here
|
|
280 |
may be put into practice. Appendix~\ref{ap:refcard} provides a quick
|
|
281 |
reference card of the most common Isabelle/Isar language elements.
|
|
282 |
Appendix~\ref{ap:conv} offers some practical hints on converting existing
|
|
283 |
Isabelle theories and proof scripts to the new format.
|
|
284 |
|
|
285 |
Several example applications are distributed with Isabelle, and available via
|
|
286 |
the Isabelle WWW library as well as the Isabelle/Isar page:
|
7836
|
287 |
\begin{center}\small
|
|
288 |
\begin{tabular}{l}
|
|
289 |
\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
|
8516
|
290 |
\url{http://isabelle.in.tum.de/library/} \\[1ex]
|
8508
|
291 |
\url{http://isabelle.in.tum.de/Isar/} \\
|
7836
|
292 |
\end{tabular}
|
|
293 |
\end{center}
|
|
294 |
|
10160
|
295 |
The following examples may be of particular interest. Apart from the plain
|
|
296 |
sources represented in HTML, these Isabelle sessions also provide actual
|
|
297 |
documents (in PDF).
|
|
298 |
\begin{itemize}
|
|
299 |
\item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
|
|
300 |
collection of introductory examples.
|
|
301 |
\item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
|
|
302 |
typical mathematics-style reasoning in ``axiomatic'' structures.
|
|
303 |
\item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
|
|
304 |
big mathematics application on infinitary vector spaces and functional
|
|
305 |
analysis.
|
|
306 |
\item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
|
10993
|
307 |
properties of $\lambda$-calculus (Church-Rosser and termination).
|
|
308 |
|
|
309 |
This may serve as a realistic example of porting of legacy proof scripts
|
|
310 |
into Isar tactic emulation scripts.
|
|
311 |
\item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
|
|
312 |
model of the main aspects of the Unix file-system including its security
|
|
313 |
model, but ignoring processes. A few odd effects caused by the general
|
|
314 |
``worse-is-better'' approach followed in Unix are discussed within the
|
|
315 |
formal model.
|
|
316 |
|
|
317 |
This example represents a non-trivial verification task, with all proofs
|
|
318 |
carefully worked out using the proper part of the Isar proof language;
|
|
319 |
unstructured scripts are only used for symbolic evaluation.
|
10160
|
320 |
\item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
|
|
321 |
formalization of a fragment of Java, together with a corresponding virtual
|
|
322 |
machine and a specification of its bytecode verifier and a lightweight
|
10993
|
323 |
bytecode verifier, including proofs of type-safety.
|
|
324 |
|
|
325 |
This represents a very ``realistic'' example of large formalizations
|
11041
|
326 |
performed in form of tactic emulation scripts and proper Isar proof texts.
|
10160
|
327 |
\end{itemize}
|
8547
|
328 |
|
7167
|
329 |
|
7046
|
330 |
%%% Local Variables:
|
|
331 |
%%% mode: latex
|
|
332 |
%%% TeX-master: "isar-ref"
|
|
333 |
%%% End:
|