--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/root.tex	Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,73 @@
+\documentclass[runningheads]{llncs}
+\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}
+
+\titlerunning{Myhill-Nerode using Regular Expressions}
+
+
+\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}}}
+\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
+
+\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
+\begin{document}
+
+\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
+  Expressions (Proof Pearl)}
+\author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
+\institute{PLA University of Science and Technology, China \and TU Munich, Germany}
+\maketitle
+
+%\mbox{}\\[-10mm]
+\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 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}
+
+
+\input{session}
+
+%%\mbox{}\\[-10mm]
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: