103 |
103 |
104 \medskip |
104 \medskip |
105 |
105 |
106 Using proper mathematical symbols in Isabelle theories can be very convenient |
106 Using proper mathematical symbols in Isabelle theories can be very convenient |
107 for readability of large formulas. On the other hand, the plain ASCII sources |
107 for readability of large formulas. On the other hand, the plain ASCII sources |
108 easily become somewhat unintelligible. For example, $\Longrightarrow$ will |
108 easily become somewhat unintelligible. For example, $\Longrightarrow$ would |
109 appear as \verb,\<Longrightarrow>, according the default set of Isabelle |
109 appear as \verb,\<Longrightarrow>, according the default set of Isabelle |
110 symbols. Nevertheless, the Isabelle document preparation system (see |
110 symbols. Nevertheless, the Isabelle document preparation system (see |
111 \S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly. |
111 \S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly. |
112 It is even possible to invent additional notation beyond the display |
112 It is even possible to invent additional notation beyond the display |
113 capabilities of XEmacs and X-Symbol. |
113 capabilities of XEmacs and X-Symbol. |
151 with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of |
151 with Isar documents. The ``\texttt{isa}'' and ``\texttt{isar}'' versions of |
152 Proof~General are handled as two different theorem proving systems, only one |
152 Proof~General are handled as two different theorem proving systems, only one |
153 of these may be active at the same time. |
153 of these may be active at the same time. |
154 \end{warn} |
154 \end{warn} |
155 |
155 |
156 Porting of existing tactic scripts is best done by running two separate |
156 Conversion of existing tactic scripts is best done by running two separate |
157 Proof~General sessions, one for replaying the old script and the other for the |
157 Proof~General sessions, one for replaying the old script and the other for the |
158 emerging Isabelle/Isar document. |
158 emerging Isabelle/Isar document. Also note that Isar supports emulation |
|
159 commands and methods that support traditional tactic scripts within new-style |
|
160 theories, see appendix~\ref{ap:conv} for more information. |
159 |
161 |
160 |
162 |
161 \subsection{Document preparation}\label{sec:document-prep} |
163 \subsection{Document preparation}\label{sec:document-prep} |
162 |
164 |
163 Isabelle/Isar provides a simple document preparation system based on current |
165 Isabelle/Isar provides a simple document preparation system based on current |
210 |
212 |
211 See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details |
213 See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details |
212 on Isabelle logic sessions and theory presentation. |
214 on Isabelle logic sessions and theory presentation. |
213 |
215 |
214 |
216 |
215 \subsection{How to write Isar proofs anyway?} |
217 \subsection{How to write Isar proofs anyway?}\label{sec:isar-howto} |
216 |
218 |
217 This is one of the key questions, of course. Isar offers a rather different |
219 This is one of the key questions, of course. Isar offers a rather different |
218 approach to formal proof documents than plain old tactic scripts. Experienced |
220 approach to formal proof documents than plain old tactic scripts. Experienced |
219 users of existing interactive theorem proving systems may have to learn |
221 users of existing interactive theorem proving systems may have to learn |
220 thinking differently in order to make effective use of Isabelle/Isar. On the |
222 thinking differently in order to make effective use of Isabelle/Isar. On the |
221 other hand, Isabelle/Isar comes much closer to existing mathematical practice |
223 other hand, Isabelle/Isar comes much closer to existing mathematical practice |
222 of formal proof, so users with less experience in old-style tactical proving, |
224 of formal proof, so users with less experience in old-style tactical proving, |
223 but a good understanding of mathematical proof, might cope with Isar even |
225 but a good understanding of mathematical proof, might cope with Isar even |
224 better. See also \cite{Wenzel:1999:TPHOL} for further background information |
226 better. See also \cite{Wenzel:1999:TPHOL,Bauer-Wenzel:2000:HB} for further |
225 on Isar. |
227 background information on Isar. |
226 %FIXME cite [HahnBanach-in-Isar] |
228 |
227 |
229 \medskip This really is a reference manual on Isabelle/Isar, not a tutorial. |
228 \medskip This really is a \emph{reference manual}. Nevertheless, we will also |
230 Nevertheless, we will also give some clues of how the concepts introduced here |
229 give some clues of how the concepts introduced here may be put into practice. |
231 may be put into practice. Appendix~\ref{ap:refcard} provides a quick |
230 Appendix~\ref{ap:refcard} provides a quick reference card of the most common |
232 reference card of the most common Isabelle/Isar language elements. |
231 Isabelle/Isar language elements. There are several examples distributed with |
233 Appendix~\ref{ap:conv} offers some practical hints on converting existing |
232 Isabelle, and available via the Isabelle WWW library as well as the |
234 Isabelle theories and proof scripts to the new format. |
233 Isabelle/Isar page: |
235 |
|
236 Several example applications are distributed with Isabelle, and available via |
|
237 the Isabelle WWW library as well as the Isabelle/Isar page: |
234 \begin{center}\small |
238 \begin{center}\small |
235 \begin{tabular}{l} |
239 \begin{tabular}{l} |
236 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ |
240 \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ |
237 \url{http://isabelle.in.tum.de/library/} \\[1ex] |
241 \url{http://isabelle.in.tum.de/library/} \\[1ex] |
238 \url{http://isabelle.in.tum.de/Isar/} \\ |
242 \url{http://isabelle.in.tum.de/Isar/} \\ |
239 \end{tabular} |
243 \end{tabular} |
240 \end{center} |
244 \end{center} |
241 |
245 |
242 See \texttt{HOL/Isar_examples} for a collection of introductory examples, and |
246 The following examples may be of particular interest. Apart from the plain |
243 \texttt{HOL/HOL-Real/HahnBanach} for a big mathematics application. Apart |
247 sources represented in HTML, these Isabelle sessions also provide actual |
244 from plain HTML sources, these sessions also provide actual documents (in |
248 documents (in PDF). |
245 PDF). |
249 \begin{itemize} |
|
250 \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a |
|
251 collection of introductory examples. |
|
252 \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of |
|
253 typical mathematics-style reasoning in ``axiomatic'' structures. |
|
254 \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a |
|
255 big mathematics application on infinitary vector spaces and functional |
|
256 analysis. |
|
257 \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental |
|
258 properties of $\lambda$-calculus (Church-Rosser and termination). This may |
|
259 serve as a realistic example of porting of legacy proof scripts into Isar |
|
260 tactic emulation scripts. |
|
261 \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a |
|
262 formalization of a fragment of Java, together with a corresponding virtual |
|
263 machine and a specification of its bytecode verifier and a lightweight |
|
264 bytecode verifier, including proofs of type-safety. This represents a very |
|
265 ``realistic'' example of large formalizations performed in either form of |
|
266 legacy scripts, tactic emulation scripts, and proper Isar proof texts. |
|
267 \end{itemize} |
246 |
268 |
247 |
269 |
248 %%% Local Variables: |
270 %%% Local Variables: |
249 %%% mode: latex |
271 %%% mode: latex |
250 %%% TeX-master: "isar-ref" |
272 %%% TeX-master: "isar-ref" |