\documentclass[acmtocl]{acmtrans2m}

%%\usepackage{pdfsetup}

\usepackage{longtable}

\newtheorem{thrm}{Theorem}[section]

\newtheorem{lmm}{Lemma}[section]

\newtheorem{dfntn}{Definition}[section]

\newtheorem{prpstn}{Proposition}[section]

  Expressions$^\star$}

%%\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.}

\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and

Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and

Christian Urban\\ King's College London, United Kingdom}

introduce the subject by describing finite automata and only

mentioning on the side a connection with regular

expressions. Unfortunately, automata are not so straightforward to

formalise in theorem provers. The reason is that a natural

representation for automata are graphs, matrices or functions, none of

which are inductive datatypes. Also convenient operations for disjoint

unions of graphs, matrices and functions are not easily formalisiable

in Isabelle/HOL, the theorem prover we are using. In contrast, regular

expressions can be defined conveniently as a datatype and a

corresponding reasoning infrastructure comes for free. We show in this

paper that a central result from formal language theory---the

Myhill-Nerode Theorem---can be recreated using only regular

expressions. From this theorem many closure properties of regular

languages follow.

\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving}

\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages}

\terms{Interactive theorem proving, regular languages}

\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}

\begin{document}

\begin{bottomstuff}

Corresponding Author: Christian Urban, Department of Informatics, King's College London, 

Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\

$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}.

\end{bottomstuff}