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 \cite{Wenzel:2006:Festschrift}
55 is generic and should work reasonably well for any Isabelle
56 object-logic that conforms to the natural deduction view of the
57 Isabelle/Pure framework. Specific language elements introduced by
58 the major object-logics are described in \chref{ch:hol}
59 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf}
60 (Isabelle/ZF). The main language elements are already provided by
61 the Isabelle/Pure framework. Nevertheless, examples given in the
62 generic parts will usually refer to Isabelle/HOL as well.
64 \medskip Isar commands may be either \emph{proper} document
65 constructors, or \emph{improper commands}. Some proof methods and
66 attributes introduced later are classified as improper as well.
67 Improper Isar language elements, which are marked by ``@{text
68 "\<^sup>*"}'' in the subsequent chapters; they are often helpful
69 when developing proof documents, but their use is discouraged for
70 the final human-readable outcome. Typical examples are diagnostic
71 commands that print terms or theorems according to the current
72 context; other commands emulate old-style tactical theorem proving.
76 section {* User interfaces *}
78 subsection {* Terminal sessions *}
81 The Isabelle \texttt{tty} tool provides a very interface for running
82 the Isar interaction loop, with some support for command line
86 {\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
87 theory Foo imports Main begin;
88 definition foo :: nat where "foo == 1";
89 lemma "0 < foo" by (simp add: foo_def);
93 Any Isabelle/Isar command may be retracted by @{command "undo"}.
94 See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
95 comprehensive overview of available commands and other language
100 subsection {* Emacs Proof General *}
103 Plain TTY-based interaction as above used to be quite feasible with
104 traditional tactic based theorem proving, but developing Isar
105 documents really demands some better user-interface support. The
106 Proof~General environment by David Aspinall
107 \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
108 interface for interactive theorem provers that organizes all the
109 cut-and-paste and forward-backward walk through the text in a very
110 neat way. In Isabelle/Isar, the current position within a partial
111 proof document is equally important than the actual proof state.
112 Thus Proof~General provides the canonical working environment for
113 Isabelle/Isar, both for getting acquainted (e.g.\ by replaying
114 existing Isar documents) and for production work.
118 subsubsection{* Proof~General as default Isabelle interface *}
121 The Isabelle interface wrapper script provides an easy way to invoke
122 Proof~General (including XEmacs or GNU Emacs). The default
123 configuration of Isabelle is smart enough to detect the
124 Proof~General distribution in several canonical places (e.g.\
125 @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}). Thus the
126 capital @{verbatim Isabelle} executable would already refer to the
127 @{verbatim "ProofGeneral/isar"} interface without further ado. The
128 Isabelle interface script provides several options; pass @{verbatim
129 "-?"} to see its usage.
131 With the proper Isabelle interface setup, Isar documents may now be edited by
132 visiting appropriate theory files, e.g.\
134 Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
136 Beginners may note the tool bar for navigating forward and backward
137 through the text (this depends on the local Emacs installation).
138 Consult the Proof~General documentation \cite{proofgeneral} for
139 further basic command sequences, in particular ``@{verbatim "C-c C-return"}''
140 and ``@{verbatim "C-c u"}''.
142 \medskip Proof~General may be also configured manually by giving
143 Isabelle settings like this (see also \cite{isabelle-sys}):
146 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
147 PROOFGENERAL_OPTIONS=""
149 You may have to change @{verbatim
150 "$ISABELLE_HOME/contrib/ProofGeneral"} to the actual installation
151 directory of Proof~General.
153 \medskip Apart from the Isabelle command line, defaults for
154 interface options may be given by the @{verbatim PROOFGENERAL_OPTIONS}
155 setting. For example, the Emacs executable to be used may be
156 configured in Isabelle's settings like this:
158 PROOFGENERAL_OPTIONS="-p xemacs-mule"
161 Occasionally, a user's @{verbatim "~/.emacs"} file contains code
162 that is incompatible with the (X)Emacs version used by
163 Proof~General, causing the interface startup to fail prematurely.
164 Here the @{verbatim "-u false"} option helps to get the interface
165 process up and running. Note that additional Lisp customization
166 code may reside in @{verbatim "proofgeneral-settings.el"} of
167 @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
168 "$ISABELLE_HOME_USER/etc"}.
172 subsubsection {* The X-Symbol package *}
175 Proof~General incorporates a version of the Emacs X-Symbol package
176 \cite{x-symbol}, which handles proper mathematical symbols displayed
177 on screen. Pass option @{verbatim "-x true"} to the Isabelle
178 interface script, or check the appropriate Proof~General menu
179 setting by hand. The main challenge of getting X-Symbol to work
180 properly is the underlying (semi-automated) X11 font setup.
182 \medskip Using proper mathematical symbols in Isabelle theories can
183 be very convenient for readability of large formulas. On the other
184 hand, the plain ASCII sources easily become somewhat unintelligible.
185 For example, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according
186 the default set of Isabelle symbols. Nevertheless, the Isabelle
187 document preparation system (see \chref{ch:document-prep}) will be
188 happy to print non-ASCII symbols properly. It is even possible to
189 invent additional notation beyond the display capabilities of Emacs
194 section {* Isabelle/Isar theories *}
197 Isabelle/Isar offers the following main improvements over classic
202 \item A \emph{theory format} that integrates specifications and
203 proofs, supporting interactive development and unlimited undo
206 \item A \emph{formal proof document language} designed to support
207 intelligible semi-automated reasoning. Instead of putting together
208 unreadable tactic scripts, the author is enabled to express the
209 reasoning in way that is close to usual mathematical practice. The
210 old tactical style has been assimilated as ``improper'' language
213 \item A simple document preparation system, for typesetting formal
214 developments together with informal text. The resulting
215 hyper-linked PDF documents are equally well suited for WWW
216 presentation and as printed copies.
220 The Isar proof language is embedded into the new theory format as a
221 proper sub-language. Proof mode is entered by stating some
222 @{command "theorem"} or @{command "lemma"} at the theory level, and
223 left again with the final conclusion (e.g.\ via @{command "qed"}).
224 A few theory specification mechanisms also require some proof, such
225 as HOL's @{command "typedef"} which demands non-emptiness of the
230 section {* How to write Isar proofs anyway? \label{sec:isar-howto} *}
233 This is one of the key questions, of course. First of all, the
234 tactic script emulation of Isabelle/Isar essentially provides a
235 clarified version of the very same unstructured proof style of
236 classic Isabelle. Old-time users should quickly become acquainted
237 with that (slightly degenerative) view of Isar.
239 Writing \emph{proper} Isar proof texts targeted at human readers is
240 quite different, though. Experienced users of the unstructured
241 style may even have to unlearn some of their habits to master proof
242 composition in Isar. In contrast, new users with less experience in
243 old-style tactical proving, but a good understanding of mathematical
244 proof in general, often get started easier.
246 \medskip The present text really is only a reference manual on
247 Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to
248 give some clues of how the concepts introduced here may be put into
249 practice. Especially note that \appref{ap:refcard} provides a quick
250 reference card of the most common Isabelle/Isar language elements.
252 Further issues concerning the Isar concepts are covered in the
254 \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
255 The author's PhD thesis \cite{Wenzel-PhD} presently provides the
256 most complete exposition of Isar foundations, techniques, and
257 applications. A number of example applications are distributed with
258 Isabelle, and available via the Isabelle WWW library (e.g.\
259 \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal
260 Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of
261 examples, both in proper Isar proof style and unstructured tactic