\documentclass[final, natbib]{svjour3} 

%\documentclass[acmtocl,final]{acmtrans2m}

\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{stmaryrd}

\usepackage{mathpartir}

\usepackage{longtable}

%%\usepackage{chicago}

\def\citeN{\citet}

%%\journalname{Journal of Automated Reasoning}

\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$+$}}

\newtheorem{thrm}{Theorem}[section]

\newtheorem{lmm}{Lemma}[section]

\newtheorem{dfntn}{Definition}[section]

\newtheorem{prpstn}{Proposition}[section]

\begin{document}

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

  Expressions$^\star$\thanks{$^\star$ This is a revised and much expanded version of \cite{WuZhangUrban11}.}}

%\author{Chunhan Wu\\PLA University of Science and Technology Nanjing, China \and

%Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and

%Christian Urban\\ King's College London, United Kingdom}

\author{Chunhan Wu \and Xingyuan Zhang \and Christian Urban}

\institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and

Christian Urban \at King's College London, United Kingdom}

\date{Received: date / Accepted: date}

%\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular

%  Expressions}

\maketitle

\begin{abstract} 

There are numerous textbooks on regular languages. Many of them focus

on finite automata for proving properties.  Unfortunately, automata

are not so straightforward to formalise in theorem provers. The reason

is that natural representations for automata are graphs, matrices or

functions, none of which are inductive datatypes. Regular

expressions can be defined straightforwardly as a datatype and a

corresponding reasoning infrastructure comes for free in theorem

provers. We show in this paper that a central result from formal

language theory---the Myhill-Nerode Theorem---can be recreated using

only regular expressions. From this theorem many closure properties of

regular languages follow.

\end{abstract}

%\category{F.4.1}{Mathematical Logic and Formal Languages}{Mechanical Theorem Proving}

%\category{F.4.3}{Mathematical Logic and Formal Languages}{Formal Languages}

%\terms{Interactive theorem proving, regular languages}

%\keywords{Myhill-Nerode theorem, regular expressions, Isabelle theorem prover}

%\begin{document}

%\begin{bottomstuff}

%Corresponding Author: Christian Urban, Department of Informatics, King's College London, 

%Strand, London WC2R 2LS, UK. Email: christian.urban@kcl.ac.uk.\\

%$^\star$This is a revised and expanded version of \cite{WuZhangUrban11}.

%\end{bottomstuff}

%%\maketitle

\input{session}

\end{document}

%%% Local Variables:

%%% mode: latex

%%% TeX-master: t

%%% End: