\documentclass{llncs}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage{amsmath}

\usepackage{amssymb}

\usepackage{tikz}

\usepackage{pgf}

\usepackage{pdfsetup}

\usepackage{ot1patch}

\usepackage{times}

\usepackage{proof}

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

\begin{document}

\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular

  Expressions (Proof Pearl)}

\author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}}

\institute{PLA University, 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 a

hassle for formalisations 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: