# HG changeset patch
# User urbanc
# Date 1298228071 0
# Node ID f77a7138f791a786551cd9230eae651bb7d24731
# Parent  6b4c20714b4f6ab7dc4cb3f45b323fb887b66046
comments by Xingyuan

diff -r 6b4c20714b4f -r f77a7138f791 Myhill_2.thy
--- a/Myhill_2.thy	Sun Feb 20 17:47:54 2011 +0000
+++ b/Myhill_2.thy	Sun Feb 20 18:54:31 2011 +0000
@@ -801,6 +801,9 @@
   shows "finite (UNIV // \<approx>(L r))"
 by (induct r) (auto)
 
+theorem Myhill_Nerode:
+  shows "(\<exists>r::rexp. A = L r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
+using Myhill_Nerode1 Myhill_Nerode2 by metis
 
 (*
 section {* Closure properties *}
@@ -811,9 +814,6 @@
   "reg A \<equiv> \<exists>r::rexp. A = L r"
 
 
-theorem Myhill_Nerode:
-  shows "reg A \<longleftrightarrow> finite (UNIV // \<approx>A)"
-using Myhill_Nerode1 Myhill_Nerode2 by auto
 
 lemma closure_union[intro]:
   assumes "reg A" "reg B" 
diff -r 6b4c20714b4f -r f77a7138f791 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 20 17:47:54 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 18:54:31 2011 +0000
@@ -355,7 +355,8 @@
   \end{center}
 
   Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating 
-  a regular expression that matches all languages of @{text rs}. We only need to know the existence
+  a regular expression that matches the union of all languages of @{text rs}. We only need to know the 
+  existence
   of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
   @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the 
   set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
@@ -369,7 +370,8 @@
   image of the set @{text rs} under function @{text "\<calL>"}.
 *}
 
-section {* The Myhill-Nerode Theorem, First Part *}
+
+section {* The Myhill-Nerode Theorem *}
 
 text {*
   The key definition in the Myhill-Nerode theorem is the
@@ -416,7 +418,8 @@
   \end{equation}
 
   \noindent
-  In our running example, @{text "X\<^isub>2"} is the only equivalence class in @{term "finals {[c]}"}.
+  In our running example, @{text "X\<^isub>2"} is the only 
+  equivalence class in @{term "finals {[c]}"}.
   It is straightforward to show that in general @{thm lang_is_union_of_finals} and 
   @{thm finals_in_partitions} hold. 
   Therefore if we know that there exists a regular expression for every
@@ -577,7 +580,7 @@
   \end{center}
 
   \noindent
-  This allows us to prove
+  This allows us to prove a version of Arden's lemma on the level of equations.
 
   \begin{lemma}\label{ardenable}
   Given an equation @{text "X = rhs"}.
@@ -757,9 +760,9 @@
   cannot make a regular expression to match the empty string. Validity is
   given because @{const Arden} removes an equivalence class from @{text yrhs}
   and then @{const Subst_all} removes @{text Y} from the equational system.
-  Having proved the implication above, we can replace @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+  Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
   which matches with our proof-obligation of @{const "Subst_all"}. Since
-  \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use our assumption 
+  \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption 
   to complete the proof.\qed 
   \end{proof}
 
@@ -972,7 +975,7 @@
 
   \begin{proof}[@{const "ALT"}-Case] 
   We take as tagging function 
-
+  %
   \begin{center}
   @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
   \end{center}
@@ -988,14 +991,14 @@
   \begin{center}
   @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
   \end{center}
-
+  %
   \noindent
   which by unfolding the Myhill-Nerode relation is identical to
   %
   \begin{equation}\label{pattern}
   @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
   \end{equation}
-
+  %
   \noindent
   since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
   \eqref{pattern} we just have to unfold the definition of the tagging-relation and analyse 
@@ -1011,25 +1014,25 @@
   The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
   they are slightly more complicated. In the @{const SEQ}-case we essentially have
   to be able to infer that 
-
+  %
   \begin{center}
   @{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
   \end{center}
-
+  %
   \noindent
   using the information given by the appropriate tagging function. The complication 
   is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
   (this was easy in case of @{term "A \<union> B"}). For this we define the
   notions of \emph{string prefixes} 
-
+  %
   \begin{center}
   @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
   @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
   \end{center}
-
+  %
   \noindent
   and \emph{string subtraction}:
-
+  %
   \begin{center}
   \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
   @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
@@ -1037,12 +1040,13 @@
   @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\
   \end{tabular}
   \end{center}
-
+  %
   \noindent
   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
+  
   Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split' 
   this string to be in @{term "A ;; B"}:
-
+  %
   \begin{center}
   \scalebox{0.7}{
   \begin{tikzpicture}
@@ -1098,19 +1102,19 @@
                node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
   \end{tikzpicture}}
   \end{center}
-
+  %
   \noindent
   Either there is a prefix of @{text x} in @{text A} and the rest in @{text B},
   or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.
   In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the 
   following tagging-function
-
+  %
   \begin{center}
   @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
   \end{center}
 
   \noindent
-  with the idea that in the first split we have to make sure that @{text "x - x'"}
+  with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
   is in the language @{text B}.
 
   \begin{proof}[@{const SEQ}-Case]
@@ -1118,27 +1122,27 @@
   then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
   @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
   We have to show injectivity of this tagging-function as
-
+  %
   \begin{center}
   @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
   \end{center}
-
+  %
   \noindent
   There are two cases to be considered (see pictures above). First, there exists 
   a @{text "x'"} such that
   @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
-  
+  %
   \begin{center}
   @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
   \end{center}
-
+  %
   \noindent
   and by the assumption about @{term "tag_str_SEQ A B"} also 
-
+  %
   \begin{center}
   @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
   \end{center}
-
+  %
   \noindent
   That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and 
   @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
@@ -1160,7 +1164,7 @@
   we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the 
   empty string, we 
   have the following picture:
-
+  %
   \begin{center}
   \scalebox{0.7}{
   \begin{tikzpicture}
@@ -1198,7 +1202,7 @@
                node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
   \end{tikzpicture}}
   \end{center}
-
+  %
   \noindent
   We can find a strict prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"},
   @{text "x' < x"} and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string 
@@ -1218,9 +1222,9 @@
 
   In order to show that @{text "x @ z \<in> A\<star>"} implies @{text "y @ z \<in> A\<star>"}, we use
   the following tagging-function:
-
+  %
   \begin{center}
-  @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}
+  @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
   \end{center}
 
   \begin{proof}[@{const STAR}-Case]
@@ -1228,36 +1232,36 @@
   then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
   @{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
   Again we have to show injectivity of this tagging-function as  
-
+  %
   \begin{center}
   @{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
   \end{center}  
-
+  %
   \noindent
   We first need to consider the case that @{text x} is the empty string.
   From the assumption we can infer @{text y} is the empty string and
   clearly have @{text "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
   string, we can devide the string @{text "x @ z"} as shown in the picture 
   above. By the tagging function we have
-
+  %
   \begin{center}
   @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
   \end{center}
-
+  %
   \noindent
   which by assumption is equal to
-  
+  %
   \begin{center}
   @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
   \end{center}
-
+  %
   \noindent 
-  and we know that we have a @{text "y'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"} and @{text "y'\<^isub>m\<^isub>a\<^isub>x < y"}
-  and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y'\<^isub>m\<^isub>a\<^isub>x)"}. Unfolding the Myhill-Nerode
-  relation we know @{term "(y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}. We also know that @{text "z\<^isub>b \<in> A\<star>"}.
-  Therefore, finally, @{text "y'\<^isub>m\<^isub>a\<^isub>x @ ((y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
-  @{term "y @ z \<in> A\<star>"}. As a last step we have to set @{text "A"} to @{text "L r"} and
-  complete the proof.
+  and we know that we have a @{text "y' \<in> A\<star>"} and @{text "y' < y"}
+  and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
+  relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{text "z\<^isub>b \<in> A\<star>"}.
+  Therefore, finally, @{text "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
+  @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{text "L r"} and
+  complete the proof.\qed
   \end{proof}
 *}
 
@@ -1270,10 +1274,16 @@
   exists a regular expression that matches all of its strings. Regular
   expressions can conveniently be defined as a datatype in a HOL-based theorem
   prover. For us it was therefore interesting to find out how far we can push
-  this point of view. 
-
-  Having formalised the Myhill-Nerode theorem means we
-  pushed quite far. Using this theorem we can obviously prove when a language
+  this point of view. We have establised both directions of the Myhill-Nerode
+  theorem.
+  %
+  \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\
+  A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
+  \end{theorem}
+  %
+  \noindent
+  Having formalised this theorem means we
+  pushed our point of view quite far. Using this theorem we can obviously prove when a language
   is \emph{not} regular---by establishing that it has infinitely many
   equivalence classes generated by the Myhill-Nerode relation (this is usually
   the purpose of the pumping lemma \cite{Kozen97}).  We can also use it to
@@ -1282,11 +1292,11 @@
   it seems difficult to construct a regular expression for the complement
   language by direct means. However the existence of such a regular expression
   can be easily proved using the Myhill-Nerode theorem since 
-
+  %
   \begin{center}
   @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
   \end{center}
- 
+  %
   \noindent
   holds for any strings @{text "s\<^isub>1"} and @{text
   "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
@@ -1322,10 +1332,7 @@
   from what is shown in the Nuprl Math Library about their development it
   seems substantially larger than ours. The code of ours can be found in the
   Mercurial Repository at
-
-  \begin{center}
-  \url{http://www4.in.tum.de/~urbanc/regexp.html}
-  \end{center}
+  \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
 
 
   Our proof of the first direction is very much inspired by \emph{Brzozowski's
diff -r 6b4c20714b4f -r f77a7138f791 Paper/document/root.tex
--- a/Paper/document/root.tex	Sun Feb 20 17:47:54 2011 +0000
+++ b/Paper/document/root.tex	Sun Feb 20 18:54:31 2011 +0000
@@ -60,6 +60,7 @@
 
 \input{session}
 
+\mbox{}\\[-10mm]
 \bibliographystyle{plain}
 \bibliography{root}