\documentclass[final,natbib]{svjour3} 
%\documentclass[acmtocl,final]{acmtrans2m}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
%%\usepackage{amsthm}
\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$+$}}

%\spnewtheorem{thrm}{Theorem}[section]{\bf}{\it}
%\spnewtheorem{lmm}{Lemma}[section]{\bf}{\it}
%\spnewtheorem{dfntn}{Definition}[section]{\bf}{\it}
%\spnewtheorem{prpstn}{Proposition}[section]{\bf}{\it}

\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}.}}
\titlerunning{A Formalisation of the Myhill-Nerode Theorem based on Regular
  Expressions}
%\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
Chunhan Wu \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: