\documentclass[acmtocl]{acmtrans2m}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{tikz}
\usepackage{pgf}
\usetikzlibrary{arrows,automata,decorations,fit,calc}
\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
\usetikzlibrary{matrix}
%%\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
\usepackage{stmaryrd}
\usepackage{mathpartir}
\usepackage{longtable}

\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%

\newcommand*{\threesim}{%
  \mathrel{\vcenter{\offinterlineskip
  \hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}}}}

\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

\newcommand{\bigplus}{\mbox{\Large\bf$+$}}

\newtheorem{thrm}{Theorem}[section]
\newtheorem{lmm}{Lemma}[section]
\newtheorem{dfntn}{Definition}[section]
\newtheorem{prpstn}{Proposition}[section]


\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
  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}

\begin{abstract} 
There are numerous textbooks on regular languages. Nearly all of them
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.
\end{abstract}
\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}
\maketitle


\input{session}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: