\documentclass{llncs}+ −
\usepackage{isabelle}+ −
\usepackage{isabellesym}+ −
\usepackage{amsmath}+ −
\usepackage{amssymb}+ −
\usepackage{tikz}+ −
\usepackage{pgf}+ −
\usepackage{pdfsetup}+ −
\usepackage{ot1patch}+ −
\usepackage{times}+ −
\usepackage{proof}+ −
\usepackage{stmaryrd}+ −
\usepackage{mathabx}+ −
+ −
+ −
\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:+ −