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