7 chapter {* Introduction *}
12 The \emph{Isabelle} system essentially provides a generic
13 infrastructure for building deductive systems (programmed in
14 Standard ML), with a special focus on interactive theorem proving in
15 higher-order logics. In the olden days even end-users would refer
16 to certain ML functions (goal commands, tactics, tacticals etc.) to
17 pursue their everyday theorem proving tasks
18 \cite{isabelle-intro,isabelle-ref}.
20 In contrast \emph{Isar} provides an interpreted language environment
21 of its own, which has been specifically tailored for the needs of
22 theory and proof development. Compared to raw ML, the Isabelle/Isar
23 top-level provides a more robust and comfortable development
24 platform, with proper support for theory development graphs,
25 single-step transactions with unlimited undo, etc. The
26 Isabelle/Isar version of the \emph{Proof~General} user interface
27 \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate
28 front-end for interactive theory and proof development in this
29 advanced theorem proving environment.
31 \medskip Apart from the technical advances over bare-bones ML
32 programming, the main purpose of the Isar language is to provide a
33 conceptually different view on machine-checked proofs
34 \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for
35 ``Intelligible semi-automated reasoning''. Drawing from both the
36 traditions of informal mathematical proof texts and high-level
37 programming languages, Isar offers a versatile environment for
38 structured formal proof documents. Thus properly written Isar
39 proofs become accessible to a broader audience than unstructured
40 tactic scripts (which typically only provide operational information
41 for the machine). Writing human-readable proof texts certainly
42 requires some additional efforts by the writer to achieve a good
43 presentation, both of formal and informal parts of the text. On the
44 other hand, human-readable formal texts gain some value in their own
45 right, independently of the mechanic proof-checking process.
47 Despite its grand design of structured proof texts, Isar is able to
48 assimilate the old tactical style as an ``improper'' sub-language.
49 This provides an easy upgrade path for existing tactic scripts, as
50 well as additional means for interactive experimentation and
51 debugging of structured proofs. Isabelle/Isar supports a broad
52 range of proof styles, both readable and unreadable ones.
54 \medskip The Isabelle/Isar framework is generic and should work
55 reasonably well for any Isabelle object-logic that conforms to the
56 natural deduction view of the Isabelle/Pure framework. Major
57 Isabelle logics like HOL \cite{isabelle-HOL}, HOLCF
58 \cite{MuellerNvOS99}, FOL \cite{isabelle-logics}, and ZF
59 \cite{isabelle-ZF} have already been set up for end-users.
63 section {* Quick start *}
65 subsection {* Terminal sessions *}
68 Isar is already part of Isabelle. The low-level @{verbatim
69 isabelle} binary provides option @{verbatim "-I"} to run the
70 Isabelle/Isar interaction loop at startup, rather than the raw ML
71 top-level. So the most basic way to do anything with Isabelle/Isar
73 \begin{ttbox} % FIXME update
74 isabelle -I HOL\medskip
75 \out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
76 theory Foo imports Main begin;
77 definition foo :: nat where "foo == 1";
78 lemma "0 < foo" by (simp add: foo_def);
82 Note that any Isabelle/Isar command may be retracted by @{command
83 "undo"}. See the Isabelle/Isar Quick Reference
84 (\appref{ap:refcard}) for a comprehensive overview of available
85 commands and other language elements.
89 subsection {* Proof General *}
92 Plain TTY-based interaction as above used to be quite feasible with
93 traditional tactic based theorem proving, but developing Isar
94 documents really demands some better user-interface support. The
95 Proof~General environment by David Aspinall
96 \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
97 interface for interactive theorem provers that organizes all the
98 cut-and-paste and forward-backward walk through the text in a very
99 neat way. In Isabelle/Isar, the current position within a partial
100 proof document is equally important than the actual proof state.
101 Thus Proof~General provides the canonical working environment for
102 Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
103 existing Isar documents) and for production work.
107 subsubsection{* Proof~General as default Isabelle interface *}
110 The Isabelle interface wrapper script provides an easy way to invoke
111 Proof~General (including XEmacs or GNU Emacs). The default
112 configuration of Isabelle is smart enough to detect the
113 Proof~General distribution in several canonical places (e.g.\
114 @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}). Thus the
115 capital @{verbatim Isabelle} executable would already refer to the
116 @{verbatim "ProofGeneral/isar"} interface without further ado. The
117 Isabelle interface script provides several options; pass @{verbatim
118 "-?"} to see its usage.
120 With the proper Isabelle interface setup, Isar documents may now be edited by
121 visiting appropriate theory files, e.g.\
123 Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
125 Beginners may note the tool bar for navigating forward and backward
126 through the text (this depends on the local Emacs installation).
127 Consult the Proof~General documentation \cite{proofgeneral} for
128 further basic command sequences, in particular ``@{verbatim "C-c C-return"}''
129 and ``@{verbatim "C-c u"}''.
131 \medskip Proof~General may be also configured manually by giving
132 Isabelle settings like this (see also \cite{isabelle-sys}):
135 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
136 PROOFGENERAL_OPTIONS=""
138 You may have to change @{verbatim
139 "$ISABELLE_HOME/contrib/ProofGeneral"} to the actual installation
140 directory of Proof~General.
142 \medskip Apart from the Isabelle command line, defaults for
143 interface options may be given by the @{verbatim PROOFGENERAL_OPTIONS}
144 setting. For example, the Emacs executable to be used may be
145 configured in Isabelle's settings like this:
147 PROOFGENERAL_OPTIONS="-p xemacs-mule"
150 Occasionally, a user's @{verbatim "~/.emacs"} file contains code
151 that is incompatible with the (X)Emacs version used by
152 Proof~General, causing the interface startup to fail prematurely.
153 Here the @{verbatim "-u false"} option helps to get the interface
154 process up and running. Note that additional Lisp customization
155 code may reside in @{verbatim "proofgeneral-settings.el"} of
156 @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
157 "$ISABELLE_HOME_USER/etc"}.
161 subsubsection {* The X-Symbol package *}
164 Proof~General incorporates a version of the Emacs X-Symbol package
165 \cite{x-symbol}, which handles proper mathematical symbols displayed
166 on screen. Pass option @{verbatim "-x true"} to the Isabelle
167 interface script, or check the appropriate Proof~General menu
168 setting by hand. The main challenge of getting X-Symbol to work
169 properly is the underlying (semi-automated) X11 font setup.
171 \medskip Using proper mathematical symbols in Isabelle theories can
172 be very convenient for readability of large formulas. On the other
173 hand, the plain ASCII sources easily become somewhat unintelligible.
174 For example, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
175 the default set of Isabelle symbols. Nevertheless, the Isabelle
176 document preparation system (see \secref{sec:document-prep}) will be
177 happy to print non-ASCII symbols properly. It is even possible to
178 invent additional notation beyond the display capabilities of Emacs
183 section {* Isabelle/Isar theories *}
186 Isabelle/Isar offers the following main improvements over classic
191 \item A \emph{theory format} that integrates specifications and
192 proofs, supporting interactive development and unlimited undo
195 \item A \emph{formal proof document language} designed to support
196 intelligible semi-automated reasoning. Instead of putting together
197 unreadable tactic scripts, the author is enabled to express the
198 reasoning in way that is close to usual mathematical practice. The
199 old tactical style has been assimilated as ``improper'' language
202 \item A simple document preparation system, for typesetting formal
203 developments together with informal text. The resulting
204 hyper-linked PDF documents are equally well suited for WWW
205 presentation and as printed copies.
209 The Isar proof language is embedded into the new theory format as a
210 proper sub-language. Proof mode is entered by stating some
211 @{command "theorem"} or @{command "lemma"} at the theory level, and
212 left again with the final conclusion (e.g.\ via @{command "qed"}).
213 A few theory specification mechanisms also require some proof, such
214 as HOL's @{command "typedef"} which demands non-emptiness of the
219 subsection {* Document preparation \label{sec:document-prep} *}
222 Isabelle/Isar provides a simple document preparation system based on
223 existing {PDF-\LaTeX} technology, with full support of hyper-links
224 (both local references and URLs) and bookmarks. Thus the results
225 are equally well suited for WWW browsing and as printed copies.
227 \medskip Isabelle generates {\LaTeX} output as part of the run of a
228 \emph{logic session} (see also \cite{isabelle-sys}). Getting
229 started with a working configuration for common situations is quite
230 easy by using the Isabelle @{verbatim mkdir} and @{verbatim make}
235 to initialize a separate directory for session @{verbatim Foo} ---
236 it is safe to experiment, since @{verbatim "isatool mkdir"} never
237 overwrites existing files. Ensure that @{verbatim "Foo/ROOT.ML"}
238 holds ML commands to load all theories required for this session;
239 furthermore @{verbatim "Foo/document/root.tex"} should include any
240 special {\LaTeX} macro packages required for your document (the
241 default is usually sufficient as a start).
243 The session is controlled by a separate @{verbatim IsaMakefile}
244 (with crude source dependencies by default). This file is located
245 one level up from the @{verbatim Foo} directory location. Now
250 to run the @{verbatim Foo} session, with browser information and
251 document preparation enabled. Unless any errors are reported by
252 Isabelle or {\LaTeX}, the output will appear inside the directory
253 @{verbatim ISABELLE_BROWSER_INFO}, as reported by the batch job in
256 \medskip You may also consider to tune the @{verbatim usedir}
257 options in @{verbatim IsaMakefile}, for example to change the output
258 format from @{verbatim pdf} to @{verbatim dvi}, or activate the
259 @{verbatim "-D"} option to retain a second copy of the generated
262 \medskip See \emph{The Isabelle System Manual} \cite{isabelle-sys}
263 for further details on Isabelle logic sessions and theory
264 presentation. The Isabelle/HOL tutorial \cite{isabelle-hol-book}
265 also covers theory presentation issues.
269 subsection {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
272 This is one of the key questions, of course. First of all, the
273 tactic script emulation of Isabelle/Isar essentially provides a
274 clarified version of the very same unstructured proof style of
275 classic Isabelle. Old-time users should quickly become acquainted
276 with that (slightly degenerative) view of Isar.
278 Writing \emph{proper} Isar proof texts targeted at human readers is
279 quite different, though. Experienced users of the unstructured
280 style may even have to unlearn some of their habits to master proof
281 composition in Isar. In contrast, new users with less experience in
282 old-style tactical proving, but a good understanding of mathematical
283 proof in general, often get started easier.
285 \medskip The present text really is only a reference manual on
286 Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
287 give some clues of how the concepts introduced here may be put into
288 practice. Especially note that \appref{ap:refcard} provides a quick
289 reference card of the most common Isabelle/Isar language elements.
291 Further issues concerning the Isar concepts are covered in the
293 \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
294 The author's PhD thesis \cite{Wenzel-PhD} presently provides the
295 most complete exposition of Isar foundations, techniques, and
296 applications. A number of example applications are distributed with
297 Isabelle, and available via the Isabelle WWW library (e.g.\
298 \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
299 Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
300 examples, both in proper Isar proof style and unstructured tactic