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