author | wenzelm |
Thu, 13 Nov 2008 21:59:02 +0100 | |
changeset 28774 | 0e25ef17b06b |
parent 28504 | 7ad7d7d6df47 |
child 29716 | b6266c4c68fe |
child 30240 | 5b25fee0362c |
permissions | -rw-r--r-- |
27035 | 1 |
(* $Id$ *) |
2 |
||
3 |
theory Introduction |
|
27050 | 4 |
imports Main |
27035 | 5 |
begin |
6 |
||
7 |
chapter {* Introduction *} |
|
8 |
||
9 |
section {* Overview *} |
|
10 |
||
11 |
text {* |
|
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}. |
|
19 |
||
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. |
|
30 |
||
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. |
|
46 |
||
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. |
|
53 |
||
27058 | 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. |
|
27040 | 63 |
|
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. |
|
27035 | 73 |
*} |
74 |
||
75 |
||
27050 | 76 |
section {* User interfaces *} |
27035 | 77 |
|
78 |
subsection {* Terminal sessions *} |
|
79 |
||
80 |
text {* |
|
27036 | 81 |
The Isabelle \texttt{tty} tool provides a very interface for running |
82 |
the Isar interaction loop, with some support for command line |
|
83 |
editing. For example: |
|
27035 | 84 |
\begin{ttbox} |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
27354
diff
changeset
|
85 |
isabelle tty\medskip |
27036 | 86 |
{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip |
27035 | 87 |
theory Foo imports Main begin; |
88 |
definition foo :: nat where "foo == 1"; |
|
89 |
lemma "0 < foo" by (simp add: foo_def); |
|
90 |
end; |
|
91 |
\end{ttbox} |
|
92 |
||
27354 | 93 |
Any Isabelle/Isar command may be retracted by @{command undo}. |
27036 | 94 |
See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a |
95 |
comprehensive overview of available commands and other language |
|
96 |
elements. |
|
27035 | 97 |
*} |
98 |
||
99 |
||
27040 | 100 |
subsection {* Emacs Proof General *} |
27035 | 101 |
|
102 |
text {* |
|
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. |
|
115 |
*} |
|
116 |
||
117 |
||
118 |
subsubsection{* Proof~General as default Isabelle interface *} |
|
119 |
||
120 |
text {* |
|
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. |
|
130 |
||
131 |
With the proper Isabelle interface setup, Isar documents may now be edited by |
|
132 |
visiting appropriate theory files, e.g.\ |
|
133 |
\begin{ttbox} |
|
134 |
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy |
|
135 |
\end{ttbox} |
|
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"}''. |
|
141 |
||
142 |
\medskip Proof~General may be also configured manually by giving |
|
143 |
Isabelle settings like this (see also \cite{isabelle-sys}): |
|
144 |
||
145 |
\begin{ttbox} |
|
146 |
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface |
|
147 |
PROOFGENERAL_OPTIONS="" |
|
148 |
\end{ttbox} |
|
149 |
You may have to change @{verbatim |
|
150 |
"$ISABELLE_HOME/contrib/ProofGeneral"} to the actual installation |
|
151 |
directory of Proof~General. |
|
152 |
||
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: |
|
157 |
\begin{ttbox} |
|
158 |
PROOFGENERAL_OPTIONS="-p xemacs-mule" |
|
159 |
\end{ttbox} |
|
160 |
||
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"}. |
|
169 |
*} |
|
170 |
||
171 |
||
172 |
subsubsection {* The X-Symbol package *} |
|
173 |
||
174 |
text {* |
|
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. |
|
181 |
||
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 |
|
27040 | 187 |
document preparation system (see \chref{ch:document-prep}) will be |
27035 | 188 |
happy to print non-ASCII symbols properly. It is even possible to |
189 |
invent additional notation beyond the display capabilities of Emacs |
|
190 |
and X-Symbol. |
|
191 |
*} |
|
192 |
||
193 |
||
194 |
section {* Isabelle/Isar theories *} |
|
195 |
||
196 |
text {* |
|
197 |
Isabelle/Isar offers the following main improvements over classic |
|
198 |
Isabelle. |
|
199 |
||
200 |
\begin{enumerate} |
|
201 |
||
202 |
\item A \emph{theory format} that integrates specifications and |
|
203 |
proofs, supporting interactive development and unlimited undo |
|
204 |
operation. |
|
205 |
||
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 |
|
211 |
elements. |
|
212 |
||
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. |
|
217 |
||
218 |
\end{enumerate} |
|
219 |
||
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 |
|
27354 | 222 |
@{command theorem} or @{command lemma} at the theory level, and |
223 |
left again with the final conclusion (e.g.\ via @{command qed}). |
|
27035 | 224 |
A few theory specification mechanisms also require some proof, such |
27354 | 225 |
as HOL's @{command typedef} which demands non-emptiness of the |
27035 | 226 |
representing sets. |
227 |
*} |
|
228 |
||
229 |
||
27050 | 230 |
section {* How to write Isar proofs anyway? \label{sec:isar-howto} *} |
27035 | 231 |
|
232 |
text {* |
|
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. |
|
238 |
||
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. |
|
245 |
||
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. |
|
251 |
||
252 |
Further issues concerning the Isar concepts are covered in the |
|
253 |
literature |
|
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 |
|
262 |
scripts. |
|
263 |
*} |
|
264 |
||
265 |
end |