\documentclass{llncs}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
\usepackage{proof}
%%\usepackage{mathabx}
\usepackage{stmaryrd}

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


\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 (Proof Pearl)}
\author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
\institute{PLA University of Science and Technology, China \and TU Munich, Germany}
\maketitle

\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 and functions are not easily formalisiable in HOL. In contrast, regular
expressions can be defined conveniently as 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.

\end{abstract}


\input{session}

\bibliographystyle{plain}
\bibliography{root}

\end{document}

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