34 \begin{abstract} |
34 \begin{abstract} |
35 There are numerous textbooks on regular languages. Nearly all of them |
35 There are numerous textbooks on regular languages. Nearly all of them |
36 introduce the subject by describing finite automata and |
36 introduce the subject by describing finite automata and |
37 only mentioning on the side a connection with regular expressions. |
37 only mentioning on the side a connection with regular expressions. |
38 Unfortunately, automata are a hassle for formalisations in HOL-based |
38 Unfortunately, automata are a hassle for formalisations in HOL-based |
39 theorem provers. The reason is that they need to be represented as graphs |
39 theorem provers. The reason is that they need to be represented as graphs, |
40 or matrices, neither of which can be defined as inductive datatype. Also |
40 matrices or functions, none of which are inductive datatypes. Also |
41 operations, such as disjoint unions of graphs, are not easily formalisiable |
41 operations, such as disjoint unions of graphs, are not easily formalisiable |
42 in HOL. In contrast, regular expressions can be defined conveniently |
42 in HOL. In contrast, regular expressions can be defined conveniently |
43 as datatype and a corresponding reasoning infrastructure comes for |
43 as datatype and a corresponding reasoning infrastructure comes for |
44 free. We show in this paper that a central result from formal |
44 free. We show in this paper that a central result from formal |
45 language theory---the Myhill-Nerode theorem---can be recreated |
45 language theory---the Myhill-Nerode theorem---can be recreated |