\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{$\_\!\_$}}\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-basedtheorem provers. The reason is that they need to be represented as graphs or matrices, neither of which can be defined as inductive datatype. Also operations, such as disjoint unions of graphs, are not easily formalisiable in HOL. In contrast, regular expressions can be defined easily 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: