\documentclass{ita}+
−
\usepackage{isabelle}+
−
\usepackage{isabellesym}+
−
\usepackage{amsmath}+
−
\usepackage{amssymb}+
−
\usepackage{tikz}+
−
\usepackage{pgf}+
−
\usetikzlibrary{arrows,automata,decorations,fit,calc}+
−
\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}+
−
\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf+
−
\usetikzlibrary{matrix}+
−
\usepackage{pdfsetup}+
−
\usepackage{ot1patch}+
−
\usepackage{times}+
−
%%\usepackage{proof}+
−
%%\usepackage{mathabx}+
−
\usepackage{stmaryrd}+
−
+
−
+
−
\urlstyle{rm}+
−
\isabellestyle{it}+
−
\renewcommand{\isastyleminor}{\it}%+
−
\renewcommand{\isastyle}{\normalsize\it}%+
−
+
−
\newcommand*{\threesim}{%+
−
  \mathrel{\vcenter{\offinterlineskip+
−
  \hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}\vskip-.35ex\hbox{$\sim$}}}}+
−
+
−
\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}+
−
\thanks{This is a revised and expanded version of \cite{WuZhangUrban11}.}+
−
\author{Chunhan Wu}\address{PLA University of Science and Technology, China}+
−
\author{Xingyuan Zhang}\sameaddress{1}+
−
\author{Christian Urban}\address{TU Munich,+
−
  Germany}\secondaddress{corresponding author}+
−
\subjclass{68Q45}+
−
\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}+
−
+
−
\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, matrices and functions are not easily formalisiable in HOL. In contrast, regular+
−
expressions can be defined conveniently as a 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}+
−
\maketitle+
−
+
−
\input{session}+
−
+
−
%%\mbox{}\\[-10mm]+
−
\bibliographystyle{plain}+
−
\bibliography{root}+
−
+
−
\end{document}+
−
+
−
%%% Local Variables:+
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End:+
−