8 |
8 |
9 text {* |
9 text {* |
10 The \emph{Isabelle} system essentially provides a generic |
10 The \emph{Isabelle} system essentially provides a generic |
11 infrastructure for building deductive systems (programmed in |
11 infrastructure for building deductive systems (programmed in |
12 Standard ML), with a special focus on interactive theorem proving in |
12 Standard ML), with a special focus on interactive theorem proving in |
13 higher-order logics. In the olden days even end-users would refer |
13 higher-order logics. Many years ago, even end-users would refer to |
14 to certain ML functions (goal commands, tactics, tacticals etc.) to |
14 certain ML functions (goal commands, tactics, tacticals etc.) to |
15 pursue their everyday theorem proving tasks |
15 pursue their everyday theorem proving tasks. |
16 \cite{isabelle-intro,isabelle-ref}. |
|
17 |
16 |
18 In contrast \emph{Isar} provides an interpreted language environment |
17 In contrast \emph{Isar} provides an interpreted language environment |
19 of its own, which has been specifically tailored for the needs of |
18 of its own, which has been specifically tailored for the needs of |
20 theory and proof development. Compared to raw ML, the Isabelle/Isar |
19 theory and proof development. Compared to raw ML, the Isabelle/Isar |
21 top-level provides a more robust and comfortable development |
20 top-level provides a more robust and comfortable development |
22 platform, with proper support for theory development graphs, |
21 platform, with proper support for theory development graphs, managed |
23 single-step transactions with unlimited undo, etc. The |
22 transactions with unlimited undo etc. The Isabelle/Isar version of |
24 Isabelle/Isar version of the \emph{Proof~General} user interface |
23 the \emph{Proof~General} user interface |
25 \cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate |
24 \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end |
26 front-end for interactive theory and proof development in this |
25 for interactive theory and proof development in this advanced |
27 advanced theorem proving environment. |
26 theorem proving environment, even though it is somewhat biased |
|
27 towards old-style proof scripts. |
28 |
28 |
29 \medskip Apart from the technical advances over bare-bones ML |
29 \medskip Apart from the technical advances over bare-bones ML |
30 programming, the main purpose of the Isar language is to provide a |
30 programming, the main purpose of the Isar language is to provide a |
31 conceptually different view on machine-checked proofs |
31 conceptually different view on machine-checked proofs |
32 \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. ``Isar'' stands for |
32 \cite{Wenzel:1999:TPHOL,Wenzel-PhD}. \emph{Isar} stands for |
33 ``Intelligible semi-automated reasoning''. Drawing from both the |
33 \emph{Intelligible semi-automated reasoning}. Drawing from both the |
34 traditions of informal mathematical proof texts and high-level |
34 traditions of informal mathematical proof texts and high-level |
35 programming languages, Isar offers a versatile environment for |
35 programming languages, Isar offers a versatile environment for |
36 structured formal proof documents. Thus properly written Isar |
36 structured formal proof documents. Thus properly written Isar |
37 proofs become accessible to a broader audience than unstructured |
37 proofs become accessible to a broader audience than unstructured |
38 tactic scripts (which typically only provide operational information |
38 tactic scripts (which typically only provide operational information |
43 right, independently of the mechanic proof-checking process. |
43 right, independently of the mechanic proof-checking process. |
44 |
44 |
45 Despite its grand design of structured proof texts, Isar is able to |
45 Despite its grand design of structured proof texts, Isar is able to |
46 assimilate the old tactical style as an ``improper'' sub-language. |
46 assimilate the old tactical style as an ``improper'' sub-language. |
47 This provides an easy upgrade path for existing tactic scripts, as |
47 This provides an easy upgrade path for existing tactic scripts, as |
48 well as additional means for interactive experimentation and |
48 well as some means for interactive experimentation and debugging of |
49 debugging of structured proofs. Isabelle/Isar supports a broad |
49 structured proofs. Isabelle/Isar supports a broad range of proof |
50 range of proof styles, both readable and unreadable ones. |
50 styles, both readable and unreadable ones. |
51 |
51 |
52 \medskip The generic Isabelle/Isar framework (see |
52 \medskip The generic Isabelle/Isar framework (see |
53 \chref{ch:isar-framework}) should work reasonably well for any |
53 \chref{ch:isar-framework}) works reasonably well for any Isabelle |
54 Isabelle object-logic that conforms to the natural deduction view of |
54 object-logic that conforms to the natural deduction view of the |
55 the Isabelle/Pure framework. Specific language elements introduced |
55 Isabelle/Pure framework. Specific language elements introduced by |
56 by the major object-logics are described in \chref{ch:hol} |
56 the major object-logics are described in \chref{ch:hol} |
57 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf} |
57 (Isabelle/HOL), \chref{ch:holcf} (Isabelle/HOLCF), and \chref{ch:zf} |
58 (Isabelle/ZF). The main language elements are already provided by |
58 (Isabelle/ZF). The main language elements are already provided by |
59 the Isabelle/Pure framework. Nevertheless, examples given in the |
59 the Isabelle/Pure framework. Nevertheless, examples given in the |
60 generic parts will usually refer to Isabelle/HOL as well. |
60 generic parts will usually refer to Isabelle/HOL as well. |
61 |
61 |
68 the final human-readable outcome. Typical examples are diagnostic |
68 the final human-readable outcome. Typical examples are diagnostic |
69 commands that print terms or theorems according to the current |
69 commands that print terms or theorems according to the current |
70 context; other commands emulate old-style tactical theorem proving. |
70 context; other commands emulate old-style tactical theorem proving. |
71 *} |
71 *} |
72 |
72 |
73 |
|
74 section {* User interfaces *} |
|
75 |
|
76 subsection {* Terminal sessions *} |
|
77 |
|
78 text {* |
|
79 The Isabelle \texttt{tty} tool provides a very interface for running |
|
80 the Isar interaction loop, with some support for command line |
|
81 editing. For example: |
|
82 \begin{ttbox} |
|
83 isabelle tty\medskip |
|
84 {\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip |
|
85 theory Foo imports Main begin; |
|
86 definition foo :: nat where "foo == 1"; |
|
87 lemma "0 < foo" by (simp add: foo_def); |
|
88 end; |
|
89 \end{ttbox} |
|
90 |
|
91 Any Isabelle/Isar command may be retracted by @{command undo}. |
|
92 See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a |
|
93 comprehensive overview of available commands and other language |
|
94 elements. |
|
95 *} |
|
96 |
|
97 |
|
98 subsection {* Emacs Proof General *} |
|
99 |
|
100 text {* |
|
101 Plain TTY-based interaction as above used to be quite feasible with |
|
102 traditional tactic based theorem proving, but developing Isar |
|
103 documents really demands some better user-interface support. The |
|
104 Proof~General environment by David Aspinall |
|
105 \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs |
|
106 interface for interactive theorem provers that organizes all the |
|
107 cut-and-paste and forward-backward walk through the text in a very |
|
108 neat way. In Isabelle/Isar, the current position within a partial |
|
109 proof document is equally important than the actual proof state. |
|
110 Thus Proof~General provides the canonical working environment for |
|
111 Isabelle/Isar, both for getting acquainted (e.g.\ by replaying |
|
112 existing Isar documents) and for production work. |
|
113 *} |
|
114 |
|
115 |
|
116 subsubsection{* Proof~General as default Isabelle interface *} |
|
117 |
|
118 text {* |
|
119 The Isabelle interface wrapper script provides an easy way to invoke |
|
120 Proof~General (including XEmacs or GNU Emacs). The default |
|
121 configuration of Isabelle is smart enough to detect the |
|
122 Proof~General distribution in several canonical places (e.g.\ |
|
123 @{verbatim "$ISABELLE_HOME/contrib/ProofGeneral"}). Thus the |
|
124 capital @{verbatim Isabelle} executable would already refer to the |
|
125 @{verbatim "ProofGeneral/isar"} interface without further ado. The |
|
126 Isabelle interface script provides several options; pass @{verbatim |
|
127 "-?"} to see its usage. |
|
128 |
|
129 With the proper Isabelle interface setup, Isar documents may now be edited by |
|
130 visiting appropriate theory files, e.g.\ |
|
131 \begin{ttbox} |
|
132 Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy |
|
133 \end{ttbox} |
|
134 Beginners may note the tool bar for navigating forward and backward |
|
135 through the text (this depends on the local Emacs installation). |
|
136 Consult the Proof~General documentation \cite{proofgeneral} for |
|
137 further basic command sequences, in particular ``@{verbatim "C-c C-return"}'' |
|
138 and ``@{verbatim "C-c u"}''. |
|
139 |
|
140 \medskip Proof~General may be also configured manually by giving |
|
141 Isabelle settings like this (see also \cite{isabelle-sys}): |
|
142 |
|
143 \begin{ttbox} |
|
144 ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface |
|
145 PROOFGENERAL_OPTIONS="" |
|
146 \end{ttbox} |
|
147 You may have to change @{verbatim |
|
148 "$ISABELLE_HOME/contrib/ProofGeneral"} to the actual installation |
|
149 directory of Proof~General. |
|
150 |
|
151 \medskip Apart from the Isabelle command line, defaults for |
|
152 interface options may be given by the @{verbatim PROOFGENERAL_OPTIONS} |
|
153 setting. For example, the Emacs executable to be used may be |
|
154 configured in Isabelle's settings like this: |
|
155 \begin{ttbox} |
|
156 PROOFGENERAL_OPTIONS="-p xemacs-mule" |
|
157 \end{ttbox} |
|
158 |
|
159 Occasionally, a user's @{verbatim "~/.emacs"} file contains code |
|
160 that is incompatible with the (X)Emacs version used by |
|
161 Proof~General, causing the interface startup to fail prematurely. |
|
162 Here the @{verbatim "-u false"} option helps to get the interface |
|
163 process up and running. Note that additional Lisp customization |
|
164 code may reside in @{verbatim "proofgeneral-settings.el"} of |
|
165 @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim |
|
166 "$ISABELLE_HOME_USER/etc"}. |
|
167 *} |
|
168 |
|
169 |
|
170 subsubsection {* The X-Symbol package *} |
|
171 |
|
172 text {* |
|
173 Proof~General incorporates a version of the Emacs X-Symbol package |
|
174 \cite{x-symbol}, which handles proper mathematical symbols displayed |
|
175 on screen. Pass option @{verbatim "-x true"} to the Isabelle |
|
176 interface script, or check the appropriate Proof~General menu |
|
177 setting by hand. The main challenge of getting X-Symbol to work |
|
178 properly is the underlying (semi-automated) X11 font setup. |
|
179 |
|
180 \medskip Using proper mathematical symbols in Isabelle theories can |
|
181 be very convenient for readability of large formulas. On the other |
|
182 hand, the plain ASCII sources easily become somewhat unintelligible. |
|
183 For example, @{text "\<Longrightarrow>"} would appear as @{verbatim "\<Longrightarrow>"} according |
|
184 the default set of Isabelle symbols. Nevertheless, the Isabelle |
|
185 document preparation system (see \chref{ch:document-prep}) will be |
|
186 happy to print non-ASCII symbols properly. It is even possible to |
|
187 invent additional notation beyond the display capabilities of Emacs |
|
188 and X-Symbol. |
|
189 *} |
|
190 |
|
191 |
|
192 section {* Isabelle/Isar theories *} |
|
193 |
|
194 text {* |
|
195 Isabelle/Isar offers the following main improvements over classic |
|
196 Isabelle. |
|
197 |
|
198 \begin{enumerate} |
|
199 |
|
200 \item A \emph{theory format} that integrates specifications and |
|
201 proofs, supporting interactive development and unlimited undo |
|
202 operation. |
|
203 |
|
204 \item A \emph{formal proof document language} designed to support |
|
205 intelligible semi-automated reasoning. Instead of putting together |
|
206 unreadable tactic scripts, the author is enabled to express the |
|
207 reasoning in way that is close to usual mathematical practice. The |
|
208 old tactical style has been assimilated as ``improper'' language |
|
209 elements. |
|
210 |
|
211 \item A simple document preparation system, for typesetting formal |
|
212 developments together with informal text. The resulting |
|
213 hyper-linked PDF documents are equally well suited for WWW |
|
214 presentation and as printed copies. |
|
215 |
|
216 \end{enumerate} |
|
217 |
|
218 The Isar proof language is embedded into the new theory format as a |
|
219 proper sub-language. Proof mode is entered by stating some |
|
220 @{command theorem} or @{command lemma} at the theory level, and |
|
221 left again with the final conclusion (e.g.\ via @{command qed}). |
|
222 A few theory specification mechanisms also require some proof, such |
|
223 as HOL's @{command typedef} which demands non-emptiness of the |
|
224 representing sets. |
|
225 *} |
|
226 |
|
227 |
|
228 section {* How to write Isar proofs anyway? \label{sec:isar-howto} *} |
|
229 |
|
230 text {* |
|
231 This is one of the key questions, of course. First of all, the |
|
232 tactic script emulation of Isabelle/Isar essentially provides a |
|
233 clarified version of the very same unstructured proof style of |
|
234 classic Isabelle. Old-time users should quickly become acquainted |
|
235 with that (slightly degenerative) view of Isar. |
|
236 |
|
237 Writing \emph{proper} Isar proof texts targeted at human readers is |
|
238 quite different, though. Experienced users of the unstructured |
|
239 style may even have to unlearn some of their habits to master proof |
|
240 composition in Isar. In contrast, new users with less experience in |
|
241 old-style tactical proving, but a good understanding of mathematical |
|
242 proof in general, often get started easier. |
|
243 |
|
244 \medskip The present text really is only a reference manual on |
|
245 Isabelle/Isar, not a tutorial. Nevertheless, we will attempt to |
|
246 give some clues of how the concepts introduced here may be put into |
|
247 practice. Especially note that \appref{ap:refcard} provides a quick |
|
248 reference card of the most common Isabelle/Isar language elements. |
|
249 |
|
250 Further issues concerning the Isar concepts are covered in the |
|
251 literature |
|
252 \cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}. |
|
253 The author's PhD thesis \cite{Wenzel-PhD} presently provides the |
|
254 most complete exposition of Isar foundations, techniques, and |
|
255 applications. A number of example applications are distributed with |
|
256 Isabelle, and available via the Isabelle WWW library (e.g.\ |
|
257 \url{http://isabelle.in.tum.de/library/}). The ``Archive of Formal |
|
258 Proofs'' \url{http://afp.sourceforge.net/} also provides plenty of |
|
259 examples, both in proper Isar proof style and unstructured tactic |
|
260 scripts. |
|
261 *} |
|
262 |
|
263 end |
73 end |