1 \documentclass[runningheads]{llncs}

     2 \usepackage{isabelle}

     3 \usepackage{isabellesym}

     4 \usepackage{amsmath}

     5 \usepackage{amssymb}

     6 \usepackage{tikz}

     7 \usepackage{pgf}

     8 \usetikzlibrary{arrows,automata,decorations,fit,calc}

     9 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning}

    10 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf

    11 \usetikzlibrary{matrix}

    12 \usepackage{pdfsetup}

    13 \usepackage{ot1patch}

    14 \usepackage{times}

    15 %%\usepackage{proof}

    16 %%\usepackage{mathabx}

    17 \usepackage{stmaryrd}

    18 

    19 \titlerunning{Myhill-Nerode using Regular Expressions}

    20 

    21 

    22 \urlstyle{rm}

    23 \isabellestyle{it}

    24 \renewcommand{\isastyleminor}{\it}%

    25 \renewcommand{\isastyle}{\normalsize\it}%

    26 

    27 

    28 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    29 \renewcommand{\isasymequiv}{$\dn$}

    30 \renewcommand{\isasymemptyset}{$\varnothing$}

    31 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    32 

    33 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}}

    34 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

    35 

    36 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}

    37 \begin{document}

    38 

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

    40   Expressions (Proof Pearl)}

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

    42 \institute{PLA University of Science and Technology, China \and TU Munich, Germany}

    43 \maketitle

    44 

    45 %\mbox{}\\[-10mm]

    46 \begin{abstract} 

    47 There are numerous textbooks on regular languages. Nearly all of them

    48 introduce the subject by describing finite automata and only mentioning on the

    49 side a connection with regular expressions. Unfortunately, automata are difficult

    50 to formalise in HOL-based theorem provers. The reason is that

    51 they need to be represented as graphs, matrices or functions, none of which

    52 are inductive datatypes. Also convenient operations for disjoint unions of

    53 graphs and functions are not easily formalisiable in HOL. In contrast, regular

    54 expressions can be defined conveniently as a datatype and a corresponding

    55 reasoning infrastructure comes for free. We show in this paper that a central

    56 result from formal language theory---the Myhill-Nerode theorem---can be

    57 recreated using only regular expressions.

    58 

    59 \end{abstract}

    60 

    61 

    62 \input{session}

    63 

    64 %%\mbox{}\\[-10mm]

    65 \bibliographystyle{plain}

    66 \bibliography{root}

    67 

    68 \end{document}

    69 

    70 %%% Local Variables:

    71 %%% mode: latex

    72 %%% TeX-master: t

    73 %%% End: