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