1826
|
1 |
\documentclass[]{article}
|
|
2 |
\usepackage{latexsym,amssymb,isa2latex}
|
|
3 |
|
|
4 |
\newcommand{\bt}[1]{{\tt #1}}
|
|
5 |
|
|
6 |
\title{The Isabelle 8bit Package}
|
|
7 |
\author{
|
|
8 |
David von Oheimb and Franz Regensburger\\
|
|
9 |
Technical University of Munich, Germany\\
|
|
10 |
E-mail: \bt{\{oheimb|regensbu\}@informatik.tu-muenchen.de}
|
|
11 |
}
|
|
12 |
\date{\today}
|
|
13 |
|
|
14 |
\begin{document}
|
|
15 |
\maketitle
|
|
16 |
|
|
17 |
|
|
18 |
|
|
19 |
|
|
20 |
\section{Introduction}
|
|
21 |
|
|
22 |
The 8bit package enables you to view, edit and print Isabelle files and perform
|
|
23 |
proofs in a quite pleasant form.
|
|
24 |
|
|
25 |
Instead of representing logical operators with ASCII character sequences,
|
|
26 |
a special graphical character font, resp. a \LaTeX{}
|
|
27 |
command format, is provided. There are editors and a terminal
|
|
28 |
capable of inputting and displaying the graphical characters, and converters
|
|
29 |
between the different representations. The graphical font extends the normal
|
|
30 |
ASCII 7bit character coding with (non-standard) character codes having the
|
|
31 |
8th bit set. All this is described in section \ref{graph} of this manual.
|
|
32 |
|
|
33 |
Even without employing the 8bit font, the \LaTeX{} output for
|
|
34 |
Isabelle files can be used for manuals, papers etc. This is the focus of
|
|
35 |
section \ref{latex}.
|
|
36 |
|
|
37 |
|
|
38 |
|
|
39 |
|
|
40 |
\section{Graphical Isabelle}
|
|
41 |
\label{graph}
|
|
42 |
|
|
43 |
This section describes the main purpose of the 8bit package, which is to provide
|
|
44 |
an extension to the ASCII character set that allows to formulate and display
|
|
45 |
many logical operators as graphical symbols.
|
|
46 |
|
|
47 |
\subsection{Usage}
|
|
48 |
|
|
49 |
To employ the graphical font within Isabelle, just (re-)formulate the
|
|
50 |
logical operators of your Isabelle theory (and proof) files using this font.
|
|
51 |
A graphical terminal and suitable editors are described in subsection
|
|
52 |
\ref{commands}.
|
|
53 |
|
|
54 |
As a typical example, consider the following fragment of an Isabelle theory,
|
|
55 |
an alternative formulation of the bounded universal quantifier within the
|
|
56 |
set theory of \bt{HOL}.
|
|
57 |
|
|
58 |
\label{ex}
|
|
59 |
Without graphical characters, the operator is defined as follows.
|
|
60 |
\I@isa
|
|
61 |
consts
|
|
62 |
Ball :: "'a set => ('a => bool) => bool"
|
|
63 |
syntax
|
|
64 |
"@Ball" :: "pttrn => 'a set => bool => bool" ("(3!_:_./ _)" 10)
|
|
65 |
translations
|
|
66 |
"!x:A. P" == "Ball A (%x. P)"
|
|
67 |
defs
|
|
68 |
Ball_def "Ball A P == ! x. x:A --> P x"
|
|
69 |
\I@isa
|
|
70 |
|
|
71 |
Using the graphical font (and assuming a corresponding re-formulation of
|
|
72 |
\bt{HOL} operators), the definition of the operator can be improved to the following.
|
|
73 |
|
|
74 |
\I@isa
|
|
75 |
consts
|
|
76 |
Ball :: "'a set ë ('a ë bool) ë bool"
|
|
77 |
syntax
|
|
78 |
"GBall" :: "pttrn ë 'a set ë bool ë bool" ("(3Â_Î_./ _)" 10)
|
|
79 |
translations
|
|
80 |
"ÂxÎA. P" == "Ball A (³x. P)"
|
|
81 |
defs
|
|
82 |
Ball_def "Ball A P Ú Âx. xÎA çè P x"
|
|
83 |
\I@isa
|
|
84 |
|
|
85 |
Note the appearance of the graphical characters, which makes the code much more
|
|
86 |
legible.
|
|
87 |
|
|
88 |
\label{compat}
|
|
89 |
It is also possible to retain pure ASCII versions of the logical operators while
|
|
90 |
offering the possibility of graphical input and output.
|
|
91 |
This may be necessary for compatibility reasons or for providing
|
|
92 |
graphical versions of the meta logic \I@Pure\I@ or object logics already
|
|
93 |
defined. In these cases, the graphical syntax can be supplied additionally with
|
|
94 |
appropriate \I@types\I@, \I@syntax\I@, and \I@translations\I@ sections, as done
|
|
95 |
for example in the Isabelle distribution of \bt{HOL}.
|
|
96 |
|
|
97 |
In the example given above, the ASCII formulation of the quantifier can be
|
|
98 |
augmented with a graphical version by the following definition.
|
|
99 |
|
|
100 |
\I@isa
|
|
101 |
syntax
|
|
102 |
"GBall" :: "pttrn => 'a set => bool => bool" ("(3Â_Î_./ _)" 10)
|
|
103 |
translations
|
|
104 |
"ÂxÎA. P" == "!x:A. P"
|
|
105 |
\I@isa
|
|
106 |
|
|
107 |
With this approach, the operators can still be entered in ASCII form, which is
|
|
108 |
important for the usability of old (pure ASCII) Isabelle files, while they are
|
|
109 |
displayed in the new graphical form. The additional level of syntax
|
|
110 |
translations introduced in this way may interfere with other translation rules
|
|
111 |
and should therefore be designed carefully.
|
|
112 |
|
|
113 |
|
|
114 |
\subsection{User commands}
|
|
115 |
\label{commands}
|
|
116 |
|
|
117 |
|
|
118 |
A number of commands for manipulating files with graphical characters are
|
|
119 |
available, as described in this subsection.
|
|
120 |
|
|
121 |
\subsubsection{Editors}
|
|
122 |
|
|
123 |
The first group of commands includes versions of the most common editors that
|
|
124 |
can handle the graphical font for both keyboard input and display input.
|
|
125 |
See the files \bt{doc/\{fontindex|keyindex|fkmatrix\}.dvi} for the keystrokes
|
|
126 |
defined for inputting the special characters. The editors are
|
|
127 |
|
|
128 |
\begin{itemize}
|
|
129 |
\item \bt{isa\_xemacs} replaces \bt{xemacs}. You may provide a
|
|
130 |
specific init file called
|
|
131 |
\bt{.emacs\_isa\_xemacs} (in your home directory)
|
|
132 |
that is executed after the \bt{.emacs} file.
|
|
133 |
\item \bt{isa\_gnu\_emacs} replaces \bt{emacs}. You may provide a
|
|
134 |
specific init file called
|
|
135 |
\bt{.emacs\_isa\_gnu\_emacs} (in your home
|
|
136 |
directory) that is executed after the
|
|
137 |
\bt{.emacs} file.
|
|
138 |
\item \bt{isaaxe} replaces \bt{axe}
|
|
139 |
\item \bt{isavim} replaces \bt{vim}
|
|
140 |
\end{itemize}
|
|
141 |
|
|
142 |
For example, as \bt{emacs} user you may type
|
|
143 |
\bt{isa\_xemacs doc/Set2g.thy \&} to view and edit
|
|
144 |
the above sample theory fragment.
|
|
145 |
|
|
146 |
\subsubsection{Display commands}
|
|
147 |
|
|
148 |
The next group of commands is used to display files using the graphical font.
|
|
149 |
With the terminal, of course also input is possible, using the same keystrokes
|
|
150 |
as with the editors.
|
|
151 |
|
|
152 |
\begin{itemize}
|
|
153 |
\item \bt{isaterm} replaces \bt{xterm}. This is used as terminal
|
|
154 |
for your ML interpreter running Isabelle with
|
|
155 |
theories and proofs containing graphical
|
|
156 |
characters. This terminal is also useful if
|
|
157 |
you want to \bt{cat} or \bt{grep} the Isabelle
|
|
158 |
files within your shell, and as
|
|
159 |
environment for commands like \bt{isapal}.
|
|
160 |
\item \bt{isapal} shows the palette of available graphical
|
|
161 |
characters. A man page is available.
|
|
162 |
\item \bt{codetable} prints all 8bit characters with their codes
|
|
163 |
\item \bt{isa\_xmosaic} replaces \bt{xmosaic}. This is useful for
|
|
164 |
browsing the index files of Isabelle theories
|
|
165 |
(with graphical operators) that are generated
|
|
166 |
if \I@make_html\I@ is set to \I@true\I@.
|
|
167 |
\end{itemize}
|
|
168 |
|
|
169 |
\subsubsection{Converters}
|
|
170 |
\label{conv}
|
|
171 |
|
|
172 |
The last group of commands is built to enable conversion between ASCII, 8bit
|
|
173 |
font and
|
|
174 |
\LaTeX\ representations of the graphical characters within papers, manuals,
|
|
175 |
and Isabelle theory and proof files. For the options of the converters, see
|
|
176 |
the corresponding man pages.
|
|
177 |
|
|
178 |
\begin{itemize}
|
|
179 |
\item \bt{isa2latex} converts a file with 8bit characters to a LaTeX
|
|
180 |
source. Pure ASCII input and conversion of 8bit
|
|
181 |
characters to their ASCII representations is also
|
|
182 |
possible.
|
|
183 |
\item \bt{a2isa} converts Isabelle files, from ASCII to 8bit characters.
|
|
184 |
It is used mainly to convert old files.
|
|
185 |
\end{itemize}
|
|
186 |
|
|
187 |
In order to output the first theory fragment (formulated without the 8bit
|
|
188 |
font) in subsection \ref{ex} as LaTeX\ source using suitable graphical
|
|
189 |
characters, type\\
|
|
190 |
\bt{isa2latex -s -A -o Set2.tex doc/Set2\_a.thy}.\\
|
|
191 |
(It was necessary to insert some blank characters in the file \bt{Set2\_a.thy}
|
|
192 |
that enable \bt{isa2latex} to recognize all the operators intended to be
|
|
193 |
printed with graphical characters, as discussed in subsection \ref{ambig}.)
|
|
194 |
|
|
195 |
For conversion of \bt{Set2.thy} to 8bit characters, type\\
|
|
196 |
\bt{a2isa -o Set2\_g.thy doc/Set2.thy}.
|
|
197 |
|
|
198 |
Further explanations of the use of the converter \bt{isa2latex} are given
|
|
199 |
in section \ref{latex}.
|
|
200 |
|
|
201 |
|
|
202 |
|
|
203 |
|
|
204 |
\section{\LaTeX\ output}
|
|
205 |
\label{latex}
|
|
206 |
|
|
207 |
Independently of whether Isabelle files are formulated with the graphical font
|
|
208 |
or not, they can be converted to \LaTeX\ source using \bt{isa2latex}
|
|
209 |
and in this way (pretty-)printed with the familiar symbols for quantification,
|
|
210 |
intersection, etc. The tool \bt{isa2latex} can also convert \LaTeX\ source
|
|
211 |
files containing Isabelle source to pure \LaTeX\
|
|
212 |
files, by converting the special character sequences of the Isabelle parts to
|
|
213 |
appropriate \LaTeX\ commands, and handing through the rest (almost) verbatim.
|
|
214 |
|
|
215 |
For example, this manual itself is converted to a \bt{.tex} file by \\
|
|
216 |
\bt{isa2latex -x -e -o manual.tex doc/manual.itex}
|
|
217 |
|
|
218 |
\subsection{Conversion modes}
|
|
219 |
|
|
220 |
To handle the different parts of an input file, \bt{isa2latex} has several
|
|
221 |
conversion modes, namely
|
|
222 |
\begin{itemize}
|
|
223 |
\item \bt{LATEX}: The input is is literally copied to the output,
|
|
224 |
without conversion of any characters. This mode is used for the \LaTeX\ parts
|
|
225 |
of the input document.
|
|
226 |
|
|
227 |
\item \bt{INLINE}: The conversion of characters and scanning for
|
|
228 |
multi character sequences is active, while newline and tab characters are
|
|
229 |
treated as single blank character.
|
|
230 |
Use this mode for inserting small parts of Isabelle source within
|
|
231 |
a line of text.
|
|
232 |
|
|
233 |
\item \bt{ISA}: The conversion of characters and scanning for
|
|
234 |
multi character sequences is active, while newline and tab characters are
|
|
235 |
treated according to an open tabbing environment.
|
|
236 |
This mode is used for displaying multiple lines of Isabelle source.
|
|
237 |
|
|
238 |
\item \bt{ESC}: In this mode the input is literally copied to the output.
|
|
239 |
This mode is intended as an escape mode from the \bt{INLINE} and \bt{ESC} modes.
|
|
240 |
\end{itemize}
|
|
241 |
|
|
242 |
Upon entrance of the conversion modes, \bt{isa2latex} generates the \LaTeX\
|
|
243 |
commands \bt{\mbox{$\backslash$}isamode} for \bt{ISA},
|
|
244 |
\bt{\mbox{$\backslash$}isainline} for \bt{INLINE},
|
|
245 |
and \bt{\mbox{$\backslash$}isaescape} for the \bt{ESC} mode. These act as
|
|
246 |
environment delimiters and may also set the appropriate fonts, styles etc. The
|
|
247 |
commands
|
|
248 |
are defined in the file \bt{latex/isa2latex.sty} and may be adapted as desired.
|
|
249 |
|
|
250 |
\subsection{Conversion mode switching}
|
|
251 |
|
|
252 |
The initial conversion mode of \bt{isa2latex} and the set of available modes
|
|
253 |
depend on the options given on the command line. Switching of the modes
|
|
254 |
relies on special toggles (like \I@\I\E@\E@@isa\I@, within the input
|
|
255 |
file) that indicate the beginning and end of the different parts of the input.
|
|
256 |
|
|
257 |
The following diagrams show the initial mode (enclosed in sqare brackets),
|
|
258 |
the available mode switches (in the arrow symbols)
|
|
259 |
and the modes reachable with them.
|
|
260 |
|
|
261 |
If the \bt{-x} option is not given:
|
|
262 |
|
|
263 |
\I@isa
|
|
264 |
[ISA] <-- \E\E@\E@@ --> ESC
|
|
265 |
\I@isa
|
|
266 |
|
|
267 |
If the \bt{-x} option is given:
|
|
268 |
|
|
269 |
\I@isa
|
|
270 |
[LATEX] <-- \I\E@\E@@ --> INLINE <-- \E\E@\E@@ --> ESC
|
|
271 |
^
|
|
272 |
|------ \I\E@\E@@isa --> ISA <-- \E\E@\E@@ --> ESC
|
|
273 |
\I@isa
|
|
274 |
|
|
275 |
|
|
276 |
\subsection{Ambiguity problems}
|
|
277 |
\label{ambig}
|
|
278 |
|
|
279 |
As \bt{isa2latex} converts its input files on a lexical level, it has limited
|
|
280 |
capability of dealing with ambiguities that are caused by using the same
|
|
281 |
characters for different operators. A typical examle
|
|
282 |
is the `\I@|\I@' character, which is used within the object logic \bt{HOL} both
|
|
283 |
as disjunction operator and as separator within \I@case\I@ expressions. In the
|
|
284 |
former case, it should be converted to `\I@Á\I@', and in the latter case
|
|
285 |
retained as `\I@|\I@'.
|
|
286 |
|
|
287 |
As a workaround, in the current version of \bt{isa2latex},
|
|
288 |
such ``dangerous'' characters are converted only if followed by a blank
|
|
289 |
character. Thus to enforce a conversion, append a blank character behind it, and
|
|
290 |
to prohibit it even if a blank character follows, you may insert a double
|
|
291 |
\I@\E\E@\E@@\I@, i.e. the string becomes `\I@|\E\E@\E@@\E\E@\E@@ \I@'.
|
|
292 |
|
|
293 |
You may also redefine the critical entries of the conversion tables in the file
|
|
294 |
\bt{config/conv-tables.inp}. The entry for the `\I@|\I@' character
|
|
295 |
looks like
|
|
296 |
\I@isa
|
|
297 |
> "\|\ " "|" "\mbox{$\vee$}"
|
|
298 |
\I@isa
|
|
299 |
The first string, which (as described by the verbose comments in that file)
|
|
300 |
is the lex expression for the ASCII input, could be adapted to require an
|
|
301 |
additional blank character before the `\I@|\I@', for example.
|
|
302 |
|
|
303 |
Most of these amibiguity problems can be avoided if you decide to employ the
|
|
304 |
graphical font for your Isabelle source files. In this case, we recommend
|
|
305 |
using this font as early as possible, in order to avoid later conversions.
|
|
306 |
For the conversion of old files, the tool \bt{a2isa} is provided. It
|
|
307 |
normally requires no changes of the original files and only minor corrections
|
|
308 |
of the files it produces. Thus the preferred way is to apply \bt{a2isa} once and
|
|
309 |
for all on the source files, correct all conversion mistakes, and then use the
|
|
310 |
new files with the graphical font. With these files, the ambiguity problems
|
|
311 |
should have gone.
|
|
312 |
|
|
313 |
As the converter \bt{a2isa} is a bit smarter than \bt{isa2latex} in converting
|
|
314 |
ASCII input, it is also useful if you do not employ the 8bit font directly. To
|
|
315 |
convert a problematic ASCII file containing Isabelle source, first apply
|
|
316 |
\bt{a2isa} and then \bt{isa2latex} without option \bt{-A}. For example, type\\
|
|
317 |
\bt{a2isa Set2.thy | isa2latex -s -o doc/Set2a.tex}\\
|
|
318 |
to generate a better output than in the example conversion given in subsection
|
|
319 |
\ref{conv}.
|
|
320 |
|
|
321 |
|
|
322 |
\section{Technical issues}
|
|
323 |
|
|
324 |
\subsection{Preparations}
|
|
325 |
|
|
326 |
To use the 8bit package, you have to set resp. extend the content of the
|
|
327 |
following environment variables:
|
|
328 |
|
|
329 |
\begin{itemize}
|
|
330 |
\item \bt{ISABELLE8BIT}: set the directory of the Isabelle 8bit package,\\
|
|
331 |
e.g. \bt{/usr/proj/isabelle/src/Tools/8bit}
|
|
332 |
|
|
333 |
\item \bt{PATH}: add the absolute path of the executables,\\
|
|
334 |
e.g. \bt{\$ISABELLE8BIT/bin}
|
|
335 |
|
|
336 |
\item \bt{MANPATH}: add the absolute path of the manual pages,\\
|
|
337 |
e.g. \bt{\$ISABELLE8BIT/man}
|
|
338 |
|
|
339 |
\item \bt{TEXINPUTS}: add the absolute path of special LaTeX style files
|
|
340 |
used by the 8bit package (if necessary),
|
|
341 |
e.g. \bt{\$ISABELLE8BIT/latex:}\\
|
|
342 |
the trailing `\bt{:}' makes latex search subdirectories!\\
|
|
343 |
The 8bit package uses
|
|
344 |
\begin{itemize}
|
|
345 |
\item the AMSFONT package
|
|
346 |
\item the supertab style (clarkson)
|
|
347 |
\item the special style \bt{isa2latex.sty}
|
|
348 |
\end{itemize}
|
|
349 |
Some of them are contained in that directory.
|
|
350 |
\end{itemize}
|
|
351 |
|
|
352 |
Before the first use of any executable of subdirectory {\tt bin}, call
|
|
353 |
the scripts \bt{fonts/install} and \bt{keyboard/install}. This is done best
|
|
354 |
in your \bt{.login} file.
|
|
355 |
|
|
356 |
\subsection{Installation and Configuration}
|
|
357 |
|
|
358 |
To install the 8bit package, change directory to \bt{\$ISABELLE8BIT} and
|
|
359 |
run \bt{gmake} (the gnu version of \bt{make}) on the \bt{Makefile} there.
|
|
360 |
|
|
361 |
If you want to adapt the configuration of the font (keyboard bindings or
|
|
362 |
conversion tables used by \bt{isa2latex}), change directory to\\
|
|
363 |
\bt{\$ISABELLE8BIT/config} ,
|
|
364 |
edit the files \bt{key-table.inp} resp. \bt{conv-tables.inp},
|
|
365 |
and run \bt{gmake} in this directory to generate new versions of
|
|
366 |
\bt{isa2latex}, editor support, and documentation.
|
|
367 |
|
|
368 |
For adapting the conversion table of \bt{a2isa}, change directory to \\
|
|
369 |
\bt{\$ISABELLE8BIT/c-sources/a2isa}, edit the file \bt{lex.x}
|
|
370 |
accordingly, and run \bt{gmake} there.
|
|
371 |
|
|
372 |
\subsection{Management of alternative sources}
|
|
373 |
|
|
374 |
If you retain ASCII versions of logical operators for compatibility reasons,
|
|
375 |
as described in subsection \ref{compat}, you may want to export versions of your
|
|
376 |
Isabelle theories that contain no 8bit characters. To support this, a patching
|
|
377 |
mechanism is provided as follows. Encapsulate each section of your files dealing
|
|
378 |
solely with the 8bit font with suitable begin and end pragmas (some pair of
|
|
379 |
unique comment lines) and configure three configuration files analogously to\\
|
|
380 |
\bt{\$ISABELLE8BIT/isa-patches/HOL/\{extract|clean|add\}-HOL.cfg}.
|
|
381 |
Then you can call the \bt{patcher} with the first file to extract and store to
|
|
382 |
a file, the second to remove, and the third to re-add the 8bit section of the
|
|
383 |
Isabelle files. See also the man page of \bt{patcher}.
|
|
384 |
|
|
385 |
|
|
386 |
\end{document}
|
|
387 |
|
|
388 |
|