Contents

This is a library of constructions on regular expressions and lan-guages. It provides the operations of concatenation, Kleene star and left-quotients of languages. A theory of derivatives and partial deriva-tives is provided. Arden’s lemma and finiteness of partial derivatives is established. A simple regular expression matcher based on Bro-zowski’s derivatives is proved to be correct. An executable equivalence checker for regular expressions is verified; it does not need automata but works directly on regular expressions. By mapping regular expres-sions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, concatenation and (reflex-ive) transitive closure is obtained. For an exposition of the equivalence checker for regular and relation algebraic expressions see the paper by Krauss and Nipkow [3]. Extended regular expressions with complement and intersection ar