src/HOL/Lex/README.html
author paulson
Wed, 07 Oct 1998 10:31:30 +0200
changeset 5619 76a8c72e3fd4
parent 5327 39a81cd9f942
permissions -rw-r--r--
new theorems

<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Lex/README</TITLE></HEAD>
<BODY>

<H1>A Simplified Scanner Generator</H1>

This directory contains the theories for the functional scanner generator
described
<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html">
here</A>. In contrast to the paper, the latest version of the theories
provides a fully executable scanner generator. The non-executable bits
(transitive closure) have been eliminated by going from regular expressions
directly to nondeterministic automata, thus bypassing epsilon-moves.
<br>
<br>
Overview:
<dl>
<dt>Automata</dt>
<dd>AutoProj, NA, NAe, DA, Automata</dd>
<dt>Regular expressions and their conversion to automata</dt>
<dd>RegSet, RegExp, RegExp2NA, RegExp2NAe</dd>
<dt>Scanning</dt>
<dd>Prefix, MaxPrefix, MaxChop, AutoMaxChop, Scanner</dd>
</dl>
In addition there are some bits and pieces:
<ul>
<li> Regset_of_nat_DA describes the translation of deterministic automata
     into regular sets. Should be completed to translate finite automata
     into regular expressions.
<li> Chopper, AutoChopper and AutoChopper1 are old versions of the scanner
     (excluding regular expressions). Mainly of historic interest.
</ul>

</BODY>
</HTML>