The Isabelle 8bit Package

David von Oheimb and Franz Regensburger Technical University of Munich, Germany

   E-mail: {oheimb|regensbu}@informatik.tu-muenchen.de

July 12, 1996

1 Introduction

The 8bit package enables you to view, edit and print Isabelle files and perform proofs in a quite pleasant form.

Instead of representing logical operators with ASCII character sequences, a special graphical character font, and alternatively a L^{A}TEX command format, is provided. There are editors and a terminal capable of inputting and displaying the graphical characters, and converters between the different representations. The graphical font extends the normal ASCII 7bit character coding with (nonstandard) character codes having the 8th bit set. All this is described in section 2 of this manual.

Even without employing the 8bit font, the L^{A}TEX output for Isabelle files can be used for manuals, papers etc. This is the focus of section 3.

2 Graphical Isabelle

This section describes the main purpose of the 8bit package, which is to provide an extension to the ASCII character set that allows to formulate and display many logical operators as graphical symbols.

2.1 Usage

To employ the graphical font within Isabelle, just (re-)formulate the logical operators of your Isabelle theory (and proof) files using this font. A graphical terminal and suitable editors are described in subsection 2.2.

As a typical example, consider the following fragment of an Isabelle theory, an alternative formulation of the bounded universal quantifier within the set theory of HOL.

Without graphical characters, the operator is defined as follows.

consts
        Ball    :: "'a set => ('a => bool) => bool"

syntax
        "@Ball" :: "pttrn => 'a set => bool => bool" ("(3! : ./  )" 10)
translations
                "!x:A. P" == "Ball A (%x. P)"
defs
     Ball def   "Ball A P == ! x. x:A −−> P x"

Using the graphical font (and assuming a corresponding re-formulation of HOL operators), the definition of the operator can be improved to the following.

consts
        Ball    :: "'a set ⇒ ('a ⇒ bool) ⇒ bool"
syntax
        "GBall" :: "pttrn ⇒ 'a set ⇒ bool ⇒ bool"    ("(3∀ ∈ ./  )" 10)
translations
                "∀x∈A. P" == "Ball A (λx. P)"
defs
     Ball def   "Ball A P ≡ ∀x. x∈A ⟶ P x"

Note the appearance of the graphical characters, which makes the code much more legible.

It is also possible to retain pure ASCII versions of the logical operators while offering the possibility of graphical input and output. This may be necessary for compatibility reasons or for providing graphical versions of the meta logic Pure or object logics already defined. In these cases, the graphical syntax can be supplied additionally with appropriate types, syntax, and translations sections, as done for example in the Isabelle distribution of HOL.

In the example given above, the ASCII formulation of the quantifier can be augmented with a graphical version by the following definition.

syntax
        "GBall" :: "pttrn => 'a set => bool => bool" ("(3∀ ∈ ./  )" 10)
translations

                "∀x∈A. P" == "!x:A. P"

With this approach, the operators can still be entered in ASCII form, which is important for the usability of old (pure ASCII) Isabelle files, while they are displayed in the new graphical form. The additional level of syntax translations introduced in this way may interfere with other translation rules and should therefore be designed carefully.

2.2 User commands

A number of commands for manipulating files with graphical characters are available, as described in this subsection.

2.2.1 Editors

The first group of commands includes versions of the most common editors that can handle the graphical font for both keyboard input and display input. See

the files doc/{fontindex|keyindex|fkmatrix}.dvi for the keystrokes defined

for inputting the special characters. The editors are

• isa xemacs replaces xemacs. You may provide a specific init file called .emacs isa xemacs (in your home directory) that is executed after the

     .emacs file.

• isa gnu emacs replaces emacs. You may provide a specific init file called .emacs isa gnu emacs (in your home directory) that is executed after the

     .emacs file.
   • isaaxe replaces axe
   • isavim replaces vim

For example, as emacs user you may type isa xemacs doc/Set2g.thy & to view and edit the above sample theory fragment.

2.2.2 Display commands

The next group of commands is used to display files using the graphical font. With the terminal, of course also input is possible, using the same keystrokes as with the editors.

• isaterm replaces xterm. This is used as terminal for your ML interpreter running Isabelle with theories and proofs containing graphical characters. This terminal is also useful if you want to cat or grep the Isabelle files within your shell, and as environment for commands like isapal.

• isapal shows the palette of available graphical characters. A man page is available.

• codetable prints all 8bit characters with their codes

• isa xmosaic replaces xmosaic. This is useful for browsing the index files of Isabelle theories (with graphical operators) that are generated if

     make html is set to true.

2.2.3 Converters

The last group of commands is built to enable conversion between ASCII, 8bit font and L^{A}TEX representations of the graphical characters within papers, manuals, and Isabelle theory and proof files. For the options of the converters, see the corresponding man pages.

• isa2latex converts a file with 8bit characters to a LaTeX source. Pure ASCII input and conversion of 8bit characters to their ASCII representations is also possible.

• a2isa converts Isabelle files, from ASCII to 8bit characters. It is used mainly to convert old files.

In order to output the first theory fragment (formulated without the 8bit font) in subsection 2.1 as LaTeX source using suitable graphical characters, type

isa2latex -s -A -o Set2.tex doc/Set2 a.thy.

(It was necessary to insert some blank characters in the file Set2 a.thy that enable isa2latex to recognize all the operators intended to be printed with graphical characters, as discussed in subsection 3.3.)

For conversion of Set2.thy to 8bit characters, type

a2isa -o Set2 g.thy doc/Set2.thy.

Further explanations of the use of the converter isa2latex are given in section 3.

3 L^{A}TEX output

Independently of whether Isabelle files are formulated with the graphical font or not, they can be converted to L^{A}TEX source using isa2latex and in this way (pretty-)printed with the familiar symbols for quantification, intersection, etc. The tool isa2latex can also convert L^{A}TEX source files containing Isabelle source to pure L^{A}TEX files, by converting the special character sequences of the Isabelle parts to appropriate L^{A}TEX commands, and handing through the rest (almost) verbatim.

For example, this manual itself is converted to a .tex file by

isa2latex -x -e -o manual.tex doc/manual.itex

3.1 Conversion modes

To handle the different parts of an input file, isa2latex has several conversion modes, namely

• LATEX: The input is is literally copied to the output, without conversion of any characters. This mode is used for the L^{A}TEX parts of the input document.

• INLINE: The conversion of characters and scanning for multi character sequences is active, while newline and tab characters are treated as single blank character. Use this mode for inserting small parts of Isabelle source within a line of text.

• ISA: The conversion of characters and scanning for multi character sequences is active, while newline and tab characters are treated according to an open tabbing environment. This mode is used for displaying multiple lines of Isabelle source.

• ESC: In this mode the input is literally copied to the output. This mode is intended as an escape mode from the INLINE and ESC modes.

Upon entrance of the conversion modes, isa2latex generates the L^{A}TEX

commands \isamode for ISA, \isainline for INLINE, and \isaescape for the

ESC mode. These act as environment delimiters and may also set the appropriate fonts, styles etc. The commands are defined in the file latex/isa2latex.sty and may be adapted as desired.

3.2 Conversion mode switching

The initial conversion mode of isa2latex and the set of available modes depend on the options given on the command line. Switching of the modes relies on special toggles (like \I@isa, within the input file) that indicate the beginning and end of the different parts of the input.

The following diagrams show the initial mode (enclosed in sqare brackets), the available mode switches (in the arrow symbols) and the modes reachable with them.

If the -x option is not given:

[ISA] <−− \E@ −−> ESC

If the -x option is given:

[LATEX] <−− \I@ −−> INLINE <−− \E@ −−> ESC
   ^

|−−−−−− \I@isa −−> ISA <−− \E@ −−> ESC

3.3 Ambiguity problems

As isa2latex converts its input files on a lexical level, it has limited capability of dealing with ambiguities that are caused by using the same characters for different operators. A typical examle is the ‘|’ character, which is used within the object logic HOL both as disjunction operator and as separator within case expressions. In the former case, it should be converted to ‘∨’, and in the latter case retained as ‘|’.

As a workaround, in the current version of isa2latex, such “dangerous” characters are converted only if followed by a blank character. Thus to enforce a conversion, append a blank character behind it, and to prohibit it even if a blank character follows, you may insert a double \E@, i.e. the string becomes ‘|\E@\E@ ’.

You may also redefine the critical entries of the conversion tables in the file config/conv-tables.inp. The entry for the ‘|’ character looks like

> "\|\ "               "|"             "\mbox{$\vee$}"

The first string, which (as described by the verbose comments in that file) is the lex expression for the ASCII input, could be adapted to require an additional blank character before the ‘|’, for example.

Most of these amibiguity problems can be avoided if you decide to employ the graphical font for your Isabelle source files. In this case, we recommend using this font as early as possible, in order to avoid later conversions. For the conversion of old files, the tool a2isa is provided. It normally requires no changes of the original files and only minor corrections of the files it produces. Thus the preferred way is to apply a2isa once and for all on the source files, correct all conversion mistakes, and then use the new files with the graphical font. With these files, the ambiguity problems should have gone.

As the converter a2isa is a bit smarter than isa2latex in converting ASCII input, it is also useful if you do not employ the 8bit font directly. To convert a problematic ASCII file containing Isabelle source, first apply a2isa and then isa2latex without option -A. For example, type

a2isa Set2.thy | isa2latex -s -o doc/Set2a.tex

to generate a better output than in the example conversion given in subsection 2.2.3.

4 Technical issues

4.1 Preparations

To use the 8bit package, you have to set respectively extend the content of the following environment variables:

• ISABELLE8BIT: set the directory of the Isabelle 8bit package,

     e.g. /usr/proj/isabelle/src/Tools/8bit

• PATH: add the absolute path of the executables,

     e.g. $ISABELLE8BIT/bin

• MANPATH: add the absolute path of the manual pages,

     e.g. $ISABELLE8BIT/man

• TEXINPUTS: add the absolute path of special LaTeX style files used by the 8bit package (if necessary), e.g. $ISABELLE8BIT/latex: the trailing ‘:’ makes latex search subdirectories! The 8bit package uses

– the AMSFONT package

– the supertab style (clarkson)

– the special style isa2latex.sty

Some of them are contained in that directory.

Before the first use of any executable of subdirectory bin, call the scripts

fonts/install and keyboard/install. This is done best in your .login file.

4.2 Installation and Configuration

To install the 8bit package, change directory to $ISABELLE8BIT. Configure the Makefile there, then run gmake clean (gmake is the gnu version of make) and

then gmake.

If you want to adapt the configuration of the font (keyboard bindings or conversion tables used by isa2latex), change directory to

$ISABELLE8BIT/config , edit the files key-table.inp respectively conv-tables.inp,

and run gmake in this directory to generate new versions of isa2latex, editor support, and documentation.

For adapting the conversion table of a2isa, change directory to

$ISABELLE8BIT/c-sources/a2isa, edit the file lex.x accordingly, and run

gmake there.

4.3 Management of alternative sources

If you retain ASCII versions of logical operators for compatibility reasons, as described in subsection 2.1, you may want to export versions of your Isabelle theories that contain no 8bit characters. To support this, a patching mechanism is provided as follows. Encapsulate each section of your files dealing solely with the 8bit font with suitable begin and end pragmas (some pair of unique comment lines) and configure three configuration files analogously to

$ISABELLE8BIT/isa-patches/HOL/{extract|clean|add}-HOL.cfg. Then you

can call the patcher with the first file to extract and store to a file, the second to remove, and the third to re-add the 8bit section of the Isabelle files. See also the man page of patcher.