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,
|
12879
|
10 |
tacticals etc.) to pursue their everyday theorem proving tasks
|
12618
|
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
|
12879
|
24 |
machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD} --- ``Isar'' stands
|
|
25 |
for ``Intelligible semi-automated reasoning''. Drawing from both the
|
12618
|
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
|
12879
|
37 |
the old tactical style as an ``improper'' sub-language. This provides an easy
|
12618
|
38 |
upgrade path for existing tactic scripts, as well as additional means for
|
12879
|
39 |
interactive experimentation and debugging of structured proofs. Isabelle/Isar
|
|
40 |
supports a broad range of proof styles, both readable and unreadable ones.
|
12618
|
41 |
|
12879
|
42 |
\medskip The Isabelle/Isar framework is generic and should work reasonably
|
|
43 |
well for any Isabelle object-logic that conforms to the natural deduction view
|
|
44 |
of the Isabelle/Pure framework. Major Isabelle logics like HOL
|
|
45 |
\cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},
|
|
46 |
and ZF \cite{isabelle-ZF} have already been set up for end-users.
|
|
47 |
Nonetheless, much of the existing body of theories still consist of old-style
|
|
48 |
theory files with accompanied ML code for proof scripts; this legacy will be
|
|
49 |
gradually converted in due time.
|
12618
|
50 |
|
|
51 |
|
7167
|
52 |
\section{Quick start}
|
|
53 |
|
8508
|
54 |
\subsection{Terminal sessions}
|
|
55 |
|
12879
|
56 |
Isar is already part of Isabelle. The low-level \texttt{isabelle} binary
|
|
57 |
provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
|
|
58 |
startup, rather than the raw ML top-level. So the most basic way to do
|
|
59 |
anything with Isabelle/Isar is as follows:
|
7175
|
60 |
\begin{ttbox}
|
|
61 |
isabelle -I HOL\medskip
|
12879
|
62 |
\out{> Welcome to Isabelle/HOL (Isabelle2002)}\medskip
|
7175
|
63 |
theory Foo = Main:
|
7297
|
64 |
constdefs foo :: nat "foo == 1";
|
|
65 |
lemma "0 < foo" by (simp add: foo_def);
|
7175
|
66 |
end
|
|
67 |
\end{ttbox}
|
9233
|
68 |
Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See
|
10160
|
69 |
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
|
10110
|
70 |
comprehensive overview of available commands and other language elements.
|
7175
|
71 |
|
8508
|
72 |
|
8843
|
73 |
\subsection{Proof~General}
|
8508
|
74 |
|
|
75 |
Plain TTY-based interaction as above used to be quite feasible with
|
8547
|
76 |
traditional tactic based theorem proving, but developing Isar documents really
|
12879
|
77 |
demands some better user-interface support. The Proof~General environment by
|
|
78 |
David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
|
|
79 |
interface for interactive theorem provers that organizes all the cut-and-paste
|
|
80 |
and forward-backward walk through the text in a very neat way. In
|
|
81 |
Isabelle/Isar, the current position within a partial proof document is equally
|
|
82 |
important than the actual proof state. Thus Proof~General provides the
|
|
83 |
canonical working environment for Isabelle/Isar, both for getting acquainted
|
|
84 |
(e.g.\ by replaying existing Isar documents) and for production work.
|
7175
|
85 |
|
8843
|
86 |
|
|
87 |
\subsubsection{Proof~General as default Isabelle interface}
|
7167
|
88 |
|
12879
|
89 |
The Isabelle interface wrapper script provides an easy way to invoke
|
|
90 |
Proof~General (and XEmacs or GNU Emacs). The default configuration of
|
|
91 |
Isabelle is smart enough to detect the Proof~General distribution in several
|
|
92 |
canonical places (e.g.\ \texttt{\$ISABELLE_HOME/contrib/ProofGeneral}). Thus
|
|
93 |
the capital \texttt{Isabelle} executable would already refer to the
|
9849
|
94 |
\texttt{ProofGeneral/isar} interface without further ado.\footnote{There is
|
|
95 |
also a \texttt{ProofGeneral/isa} interface for old tactic scripts written in
|
12879
|
96 |
ML.} The Isabelle interface script provides several options; pass \verb,-?,
|
|
97 |
to see its usage.
|
7981
|
98 |
|
7175
|
99 |
With the proper Isabelle interface setup, Isar documents may now be edited by
|
|
100 |
visiting appropriate theory files, e.g.\
|
|
101 |
\begin{ttbox}
|
12879
|
102 |
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
|
7175
|
103 |
\end{ttbox}
|
12879
|
104 |
Users may note the tool bar for navigating forward and backward through the
|
|
105 |
text (this depends on the local Emacs installation). Consult the
|
|
106 |
Proof~General documentation \cite{proofgeneral} for further basic command
|
|
107 |
sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
|
8508
|
108 |
|
9849
|
109 |
\medskip
|
|
110 |
|
|
111 |
Proof~General may be also configured manually by giving Isabelle settings like
|
|
112 |
this (see also \cite{isabelle-sys}):
|
|
113 |
\begin{ttbox}
|
|
114 |
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
|
|
115 |
PROOFGENERAL_OPTIONS=""
|
|
116 |
\end{ttbox}
|
|
117 |
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
|
|
118 |
actual installation directory of Proof~General.
|
|
119 |
|
|
120 |
\medskip
|
|
121 |
|
|
122 |
Apart from the Isabelle command line, defaults for interface options may be
|
12879
|
123 |
given by the \texttt{PROOFGENERAL_OPTIONS} setting. For example, the Emacs
|
|
124 |
executable to be used may be configured in Isabelle's settings like this:
|
9849
|
125 |
\begin{ttbox}
|
|
126 |
PROOFGENERAL_OPTIONS="-p xemacs-nomule"
|
|
127 |
\end{ttbox}
|
|
128 |
|
12879
|
129 |
Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible
|
|
130 |
with the (X)Emacs version used by Proof~General, causing the interface startup
|
|
131 |
to fail prematurely. Here the \texttt{-u false} option helps to get the
|
|
132 |
interface process up and running. Note that additional Lisp customization
|
|
133 |
code may reside in \texttt{proofgeneral-settings.el} of
|
|
134 |
\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.
|
9849
|
135 |
|
8843
|
136 |
|
|
137 |
\subsubsection{The X-Symbol package}
|
8508
|
138 |
|
12879
|
139 |
Proof~General provides native support for the Emacs X-Symbol package
|
|
140 |
\cite{x-symbol}, which handles proper mathematical symbols displayed on
|
|
141 |
screen. Pass option \texttt{-x true} to the Isabelle interface script, or
|
|
142 |
check the appropriate Proof~General menu setting by hand. In any case, the
|
|
143 |
X-Symbol package must have been properly installed already.
|
8516
|
144 |
|
8843
|
145 |
Contrary to what you may expect from the documentation of X-Symbol, the
|
9849
|
146 |
package is very easy to install and configures itself automatically. The
|
|
147 |
default configuration of Isabelle is smart enough to detect the X-Symbol
|
|
148 |
package in several canonical places (e.g.\
|
|
149 |
\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
|
8843
|
150 |
|
|
151 |
\medskip
|
|
152 |
|
|
153 |
Using proper mathematical symbols in Isabelle theories can be very convenient
|
|
154 |
for readability of large formulas. On the other hand, the plain ASCII sources
|
10160
|
155 |
easily become somewhat unintelligible. For example, $\Longrightarrow$ would
|
9849
|
156 |
appear as \verb,\<Longrightarrow>, according the default set of Isabelle
|
|
157 |
symbols. Nevertheless, the Isabelle document preparation system (see
|
|
158 |
\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
|
|
159 |
It is even possible to invent additional notation beyond the display
|
12879
|
160 |
capabilities of Emacs and X-Symbol.
|
7175
|
161 |
|
7981
|
162 |
|
|
163 |
\section{Isabelle/Isar theories}
|
|
164 |
|
8547
|
165 |
Isabelle/Isar offers the following main improvements over classic Isabelle.
|
7981
|
166 |
\begin{enumerate}
|
|
167 |
\item A new \emph{theory format}, occasionally referred to as ``new-style
|
|
168 |
theories'', supporting interactive development and unlimited undo operation.
|
|
169 |
\item A \emph{formal proof document language} designed to support intelligible
|
|
170 |
semi-automated reasoning. Instead of putting together unreadable tactic
|
|
171 |
scripts, the author is enabled to express the reasoning in way that is close
|
8508
|
172 |
to usual mathematical practice.
|
8547
|
173 |
\item A simple document preparation system, for typesetting formal
|
|
174 |
developments together with informal text. The resulting hyper-linked PDF
|
|
175 |
documents are equally well suited for WWW presentation and as printed
|
|
176 |
copies.
|
7981
|
177 |
\end{enumerate}
|
|
178 |
|
|
179 |
The Isar proof language is embedded into the new theory format as a proper
|
|
180 |
sub-language. Proof mode is entered by stating some $\THEOREMNAME$ or
|
|
181 |
$\LEMMANAME$ at the theory level, and left again with the final conclusion
|
12879
|
182 |
(e.g.\ via $\QEDNAME$). A few theory specification mechanisms also require
|
|
183 |
some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness
|
|
184 |
of the representing sets.
|
7460
|
185 |
|
7981
|
186 |
New-style theory files may still be associated with separate ML files
|
|
187 |
consisting of plain old tactic scripts. There is no longer any ML binding
|
|
188 |
generated for the theory and theorems, though. ML functions \texttt{theory},
|
|
189 |
\texttt{thm}, and \texttt{thms} retrieve this information \cite{isabelle-ref}.
|
|
190 |
Nevertheless, migration between classic Isabelle and Isabelle/Isar is
|
|
191 |
relatively easy. Thus users may start to benefit from interactive theory
|
8547
|
192 |
development and document preparation, even before they have any idea of the
|
|
193 |
Isar proof language at all.
|
7981
|
194 |
|
|
195 |
\begin{warn}
|
12879
|
196 |
Proof~General does \emph{not} support mixed interactive development of
|
|
197 |
classic Isabelle theory files or tactic scripts, together with Isar
|
|
198 |
documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
|
7981
|
199 |
Proof~General are handled as two different theorem proving systems, only one
|
|
200 |
of these may be active at the same time.
|
|
201 |
\end{warn}
|
|
202 |
|
12879
|
203 |
Manual conversion of existing tactic scripts may be done by running two
|
|
204 |
separate Proof~General sessions, one for replaying the old script and the
|
|
205 |
other for the emerging Isabelle/Isar document. Also note that Isar supports
|
|
206 |
emulation commands and methods that support traditional tactic scripts within
|
|
207 |
new-style theories, see appendix~\ref{ap:conv} for more information.
|
7981
|
208 |
|
7167
|
209 |
|
8843
|
210 |
\subsection{Document preparation}\label{sec:document-prep}
|
8684
|
211 |
|
12879
|
212 |
Isabelle/Isar provides a simple document preparation system based on existing
|
|
213 |
PDF-\LaTeX technology, with full support of hyper-links (both local references
|
|
214 |
and URLs), bookmarks, and thumbnails. Thus the results are equally well
|
|
215 |
suited for WWW browsing and as printed copies.
|
8684
|
216 |
|
|
217 |
\medskip
|
|
218 |
|
|
219 |
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
|
|
220 |
session} (see also \cite{isabelle-sys}). Getting started with a working
|
|
221 |
configuration for common situations is quite easy by using the Isabelle
|
12879
|
222 |
\texttt{mkdir} and \texttt{make} tools. First invoke
|
8684
|
223 |
\begin{ttbox}
|
12879
|
224 |
isatool mkdir Foo
|
8684
|
225 |
\end{ttbox}
|
12879
|
226 |
to initialize a separate directory for session \texttt{Foo} --- it is safe to
|
|
227 |
experiment, since \texttt{isatool mkdir} never overwrites existing files.
|
|
228 |
Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories
|
|
229 |
required for this session; furthermore \texttt{Foo/document/root.tex} should
|
|
230 |
include any special {\LaTeX} macro packages required for your document (the
|
|
231 |
default is usually sufficient as a start).
|
8684
|
232 |
|
12879
|
233 |
The session is controlled by a separate \texttt{IsaMakefile} (with crude
|
|
234 |
source dependencies by default). This file is located one level up from the
|
|
235 |
\texttt{Foo} directory location. Now invoke
|
8684
|
236 |
\begin{ttbox}
|
|
237 |
isatool make Foo
|
|
238 |
\end{ttbox}
|
|
239 |
to run the \texttt{Foo} session, with browser information and document
|
|
240 |
preparation enabled. Unless any errors are reported by Isabelle or {\LaTeX},
|
12879
|
241 |
the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as
|
|
242 |
reported by the batch job in verbose mode.
|
8684
|
243 |
|
|
244 |
\medskip
|
|
245 |
|
|
246 |
You may also consider to tune the \texttt{usedir} options in
|
|
247 |
\texttt{IsaMakefile}, for example to change the output format from
|
12879
|
248 |
\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D generated} option in
|
|
249 |
order to keep a second copy of the generated {\LaTeX} sources.
|
8684
|
250 |
|
|
251 |
\medskip
|
|
252 |
|
|
253 |
See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
|
12879
|
254 |
on Isabelle logic sessions and theory presentation. The Isabelle/HOL tutorial
|
|
255 |
\cite{isabelle-hol-book} also covers theory presentation issues.
|
8684
|
256 |
|
|
257 |
|
10160
|
258 |
\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
|
7167
|
259 |
|
12879
|
260 |
This is one of the key questions, of course. First of all, the tactic script
|
|
261 |
emulation of Isabelle/Isar essentially provides a clarified version of the
|
|
262 |
very same unstructured proof style of classic Isabelle. Old-time users should
|
|
263 |
quickly become acquainted with that (degenerative) view of Isar at the least.
|
12621
|
264 |
|
12879
|
265 |
Writing \emph{proper} Isar proof texts targeted at human readers is quite
|
|
266 |
different, though. Experienced users of the unstructured style may even have
|
|
267 |
to unlearn some of their habits to master proof composition in Isar. In
|
|
268 |
contrast, new users with less experience in old-style tactical proving, but a
|
|
269 |
good understanding of mathematical proof in general often get started easier.
|
7297
|
270 |
|
12879
|
271 |
\medskip The present text really is only a reference manual on Isabelle/Isar,
|
|
272 |
not a tutorial. Nevertheless, we will attempt to give some clues of how the
|
|
273 |
concepts introduced here may be put into practice. Appendix~\ref{ap:refcard}
|
|
274 |
provides a quick reference card of the most common Isabelle/Isar language
|
|
275 |
elements. Appendix~\ref{ap:conv} offers some practical hints on converting
|
|
276 |
existing Isabelle theories and proof scripts to the new format (without
|
|
277 |
restructuring proofs).
|
10160
|
278 |
|
12879
|
279 |
Further issues concerning the Isar concepts are covered in the literature
|
|
280 |
\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
|
|
281 |
The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete
|
|
282 |
exposition of Isar foundations, techniques, and applications. A number of
|
|
283 |
example applications are distributed with Isabelle, and available via the
|
|
284 |
Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}). As a
|
|
285 |
general rule of thumb, more recent Isabelle applications that also include a
|
|
286 |
separate ``document'' (in PDF) are more likely to consist of proper
|
|
287 |
Isabelle/Isar theories and proofs.
|
7836
|
288 |
|
12879
|
289 |
%FIXME
|
|
290 |
% The following examples may be of particular interest. Apart from the plain
|
|
291 |
% sources represented in HTML, these Isabelle sessions also provide actual
|
|
292 |
% documents (in PDF).
|
|
293 |
% \begin{itemize}
|
|
294 |
% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
|
|
295 |
% collection of introductory examples.
|
|
296 |
% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
|
|
297 |
% typical mathematics-style reasoning in ``axiomatic'' structures.
|
|
298 |
% \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
|
|
299 |
% big mathematics application on infinitary vector spaces and functional
|
|
300 |
% analysis.
|
|
301 |
% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
|
|
302 |
% properties of $\lambda$-calculus (Church-Rosser and termination).
|
10993
|
303 |
|
12879
|
304 |
% This may serve as a realistic example of porting of legacy proof scripts
|
|
305 |
% into Isar tactic emulation scripts.
|
|
306 |
% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
|
|
307 |
% model of the main aspects of the Unix file-system including its security
|
|
308 |
% model, but ignoring processes. A few odd effects caused by the general
|
|
309 |
% ``worse-is-better'' approach followed in Unix are discussed within the
|
|
310 |
% formal model.
|
10993
|
311 |
|
12879
|
312 |
% This example represents a non-trivial verification task, with all proofs
|
|
313 |
% carefully worked out using the proper part of the Isar proof language;
|
|
314 |
% unstructured scripts are only used for symbolic evaluation.
|
|
315 |
% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
|
|
316 |
% formalization of a fragment of Java, together with a corresponding virtual
|
|
317 |
% machine and a specification of its bytecode verifier and a lightweight
|
|
318 |
% bytecode verifier, including proofs of type-safety.
|
10993
|
319 |
|
12879
|
320 |
% This represents a very ``realistic'' example of large formalizations
|
|
321 |
% performed in form of tactic emulation scripts and proper Isar proof texts.
|
|
322 |
% \end{itemize}
|
8547
|
323 |
|
7167
|
324 |
|
7046
|
325 |
%%% Local Variables:
|
|
326 |
%%% mode: latex
|
|
327 |
%%% TeX-master: "isar-ref"
|
|
328 |
%%% End:
|