\documentclass{ita}
\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{proof}
%%\usepackage{mathabx}
\usepackage{stmaryrd}
\usepackage{mathpartir}

\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$+$}}
\begin{document}

\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
  Expressions}
\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.}
\author{Chunhan Wu}\address{PLA University of Science and Technology, China}
\author{Xingyuan Zhang}\sameaddress{1}
\author{Christian Urban}\address{King's College London, United Kingdom}\secondaddress{corresponding author}
\subjclass{68Q45}
\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}

\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 difficult
to formalise in HOL-based theorem provers. The reason is that
they need to be represented as 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 HOL. 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}
\maketitle

\input{session}

%%\mbox{}\\[-10mm]
\bibliographystyle{plain}
\bibliography{root}

\end{document}

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