28   wide range of textbooks about this subject. Many of these textbooks, such as

    28   wide range of textbooks about this subject. Many of which, such as

    31   formalising these theorems and by verifying formally the algorithms. There

    31   formalising these theorems and by verifying formally the algorithms. 

    32   is however a problem: the typical approach to regular languages is to start

    32 

    33   with finite automata.

    33   There is however a problem: the typical approach to the subject of regular

    34   languages is to introduce finite automata and define everything in terms of

    35   automata.  For example, a regular language is nearly always defined as one

    36   where there is a finite deterministic automata that recognises all the

    37   strings of the language. One benefit of this approach is that it is easy

    38   to prove on paper that regular languages are closed under complementation: 

    39   one just has to exchange the accepting and non-accepting states in the corresponding 

    40   automata into non-accepting.  The problem with automata is that they need

    41   to be represented as graphs (nodes represent states and edges, transitions)

    42   or as matrices (recording the transitions between states). Both representations

    43   cannot be defined in terms of inductive datatypes, and a reasoning infrastructure

    44   must be established manually. To our knowledge neither 

    45   Isabelle nor HOL4 nor Coq have a readily usable reasoning library for graphs

    46   and matrices. Moreover, the reasoning about graphs can be quite cumbersome.

    47   Cosider for example the frequently used operation of combinding two automata

    48   into a new compound automaton. While on paper, this can be done by just forming

    49   the disjoint union of the nodes, this does not work in typed systems \dots

    50