# HG changeset patch
# User urbanc
# Date 1298111031 0
# Node ID 342983676c8f95d211721510af647d6066958c06
# Parent  c5f138b5fc88f40cd340ee8ec5746d1065a208c9
included comments by Chunhan

diff -r c5f138b5fc88 -r 342983676c8f Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Feb 18 15:06:06 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 10:23:51 2011 +0000
@@ -271,7 +271,7 @@
   involving equivalence classes of languages. For this we will use Arden's lemma \cite{Brzozowski64},
   which solves equations of the form @{term "X = A ;; X \<union> B"} provided
   @{term "[] \<notin> A"}. However we will need the following `reverse' 
-  version of Arden's lemma.
+  version of Arden's lemma (`reverse' in the sense of changing the order of @{text "\<cdot>"}).
 
   \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
   If @{thm (prem 1) arden} then
@@ -738,7 +738,7 @@
 
   \noindent
   Finiteness is straightforward, as @{const Subst} and @{const Arden} operations 
-  keep the equational system finite. These operation also preserve soundness 
+  keep the equational system finite. These operations also preserve soundness 
   and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
   The property ardenable is clearly preserved because the append-operation
   cannot make a regular expression to match the empty string. Validity is
@@ -848,14 +848,21 @@
 section {* Myhill-Nerode, Second Part *}
 
 text {*
+  We will prove in this section the second part of the Myhill-Nerode
+  theorem. It can be formulated in our setting as follows.
 
   \begin{theorem}
   Given @{text "r"} is a regular expressions, then @{thm Myhill_Nerode2}.
   \end{theorem}  
 
-  \begin{proof}
-  By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
-  and @{const CHAR} are straightforward, because we can easily establish
+  \noindent
+  The proof will be by induction on the structure of @{text r}. It turns out
+  the base cases are straightforward.
+
+
+  \begin{proof}[Base Cases]
+  The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because 
+  we can easily establish
 
   \begin{center}
   \begin{tabular}{l}
@@ -865,8 +872,15 @@
   \end{tabular}
   \end{center}
 
+  \noindent
+  hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed
   \end{proof}
 
+  \noindent
+  Much more interesting are the inductive cases, which seem hard to be solved 
+  directly. The reader is invited to try. Our method will rely on some
+  \emph{tagging} functions of strings. Given the inductive hypothesis, it will 
+  be easy to prove that the range of these tagging functions is finite.
 
   @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]}
 
@@ -909,6 +923,13 @@
   "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
   regular expression.
 
+  While regular expressions are convenient in formalisations, they have some
+  limitations. One is that there seems to be no notion of a minimal regular
+  expression, like there is for automata. For an implementation of a simple
+  regular expression matcher, whose correctness has been formally
+  established, we refer the reader to Owens and Slind \cite{OwensSlind08}.
+
+
   Our formalisation consists of ??? lines of Isabelle/Isar code for the first
   direction and ??? for the second. While this might be seen as too large to
   count as a concise proof pearl, this should be seen in the context of the
@@ -960,12 +981,6 @@
   as stated in the Introduction is not so convenient to formalise in a 
   HOL-based theorem prover.
 
-  While regular expressions are convenient in formalisations, they have some
-  limitations. One is that there seems to be no notion of a minimal regular
-  expression, like there is for automata. For an implementation of a simple
-  regular expression matcher, whose correctness has been formally
-  established, we refer the reader to Owens and Slind \cite{OwensSlind08}.
-
 *}
 
 
diff -r c5f138b5fc88 -r 342983676c8f Paper/document/root.tex
--- a/Paper/document/root.tex	Fri Feb 18 15:06:06 2011 +0000
+++ b/Paper/document/root.tex	Sat Feb 19 10:23:51 2011 +0000
@@ -31,7 +31,7 @@
 
 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
   Expressions (Proof Pearl)}
-\author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}}
+\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
 
diff -r c5f138b5fc88 -r 342983676c8f tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed