\documentclass[acmtocl,final]{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}

\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular
  Expressions}

\begin{abstract} 
There are numerous textbooks on regular languages. Many of them focus
on finite automata for proving properties.  Unfortunately, automata
are not so straightforward to formalise in theorem provers. The reason
is that natural representations for automata are graphs, matrices or
functions, none of which are inductive datatypes. Regular
expressions can be defined straightforwardly as a datatype and a
corresponding reasoning infrastructure comes for free in theorem
provers. 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: