\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: