\documentclass[runningheads]{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}\titlerunning{Myhill-Nerode using Regular Expressions}\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 themintroduce the subject by describing finite automata and only mentioning on theside a connection with regular expressions. Unfortunately, automata are difficultto formalise in HOL-based theorem provers. The reason is thatthey need to be represented as graphs, matrices or functions, none of whichare inductive datatypes. Also convenient operations for disjoint unions ofgraphs and functions are not easily formalisiable in HOL. In contrast, regularexpressions can be defined conveniently as datatype and a correspondingreasoning infrastructure comes for free. We show in this paper that a centralresult from formal language theory---the Myhill-Nerode theorem---can berecreated using only regular expressions.\end{abstract}\input{session}\bibliographystyle{plain}\bibliography{root}\end{document}%%% Local Variables:%%% mode: latex%%% TeX-master: t%%% End: