# HG changeset patch
# User urbanc
# Date 1297110610 0
# Node ID d63baacbdb165d1f38f0fb4ce679e0f3a60382a5
# Parent  2335fcb96052e43ebc3bd6098cae1e6cabc6125e
parts of the 3 section

diff -r 2335fcb96052 -r d63baacbdb16 Myhill_1.thy
--- a/Myhill_1.thy	Mon Feb 07 13:17:01 2011 +0000
+++ b/Myhill_1.thy	Mon Feb 07 20:30:10 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill_1
-  imports Main List_Prefix Prefix_subtract Prelude
+  imports Main 
 begin
 
 (*
@@ -334,7 +334,7 @@
 lemma folds_alt_simp [simp]:
   assumes a: "finite rs"
   shows "L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply(rule set_eq_intro)
+apply(rule set_eqI)
 apply(simp add: folds_def)
 apply(rule someI2_ex)
 apply(rule_tac finite_imp_fold_graph[OF a])
@@ -345,7 +345,7 @@
 
 text {* Just a technical lemma for collections and pairs *}
 
-lemma [simp]:
+lemma Pair_Collect[simp]:
   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 by simp
 
@@ -471,16 +471,16 @@
 *}
 
 definition 
-  transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
+  transition :: "lang \<Rightarrow> rexp \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
 where
-  "Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X"
+  "Y \<Turnstile>r\<Rightarrow> X \<equiv> Y ;; (L r) \<subseteq> X"
 
 definition
   "init_rhs CS X \<equiv>  
       if ([] \<in> X) then 
-          {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
+          {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}
       else 
-          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
+          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"
 
 text {*
   In the definition of @{text "init_rhs"}, the term 
@@ -496,6 +496,9 @@
 
 
 definition "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
+
+
+
 (************ arden's lemma variation ********************)
 
 text {* 
@@ -516,7 +519,7 @@
 
 text {* 
   The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}.
-  *}
+*}
 
 definition
   "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
@@ -526,7 +529,7 @@
   using @{text "ALT"} to form a single regular expression. 
   When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"}
   is used to compute compute the regular expression corresponds to @{text "rhs"}.
-  *}
+*}
 
 definition
   "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)"
@@ -535,7 +538,7 @@
   The following @{text "attach_rexp rexp' itm"} attach 
   the regular expression @{text "rexp'"} to
   the right of right hand side item @{text "itm"}.
-  *}
+*}
 
 fun 
   attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
@@ -546,7 +549,7 @@
 text {* 
   The following @{text "append_rhs_rexp rhs rexp"} attaches 
   @{text "rexp"} to every item in @{text "rhs"}.
-  *}
+*}
 
 definition
   "append_rhs_rexp rhs rexp \<equiv> (attach_rexp rexp) ` rhs"
@@ -622,7 +625,7 @@
 qed
 
 text {*
-  The @{text "P"} in lemma @{text "wf_iter"} is an invaiant kept throughout the iteration procedure.
+  The @{text "P"} in lemma @{text "wf_iter"} is an invariant kept throughout the iteration procedure.
   The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"},
   an invariant over equal system @{text "ES"}.
   Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}.
@@ -631,6 +634,7 @@
 text {* 
   Every variable is defined at most onece in @{text "ES"}.
   *}
+
 definition 
   "distinct_equas ES \<equiv> 
             \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
@@ -834,7 +838,7 @@
         and "clist \<in> Y"
         using decom "(1)" every_eqclass_has_transition by blast
       hence 
-        "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
+        "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"
         unfolding transition_def
 	using "(1)" decom
         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
diff -r 2335fcb96052 -r d63baacbdb16 Myhill_2.thy
--- a/Myhill_2.thy	Mon Feb 07 13:17:01 2011 +0000
+++ b/Myhill_2.thy	Mon Feb 07 20:30:10 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill_2
-  imports Myhill_1
+  imports Myhill_1 List_Prefix Prefix_subtract
 begin
 
 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
@@ -7,15 +7,15 @@
 subsection {* The scheme*}
 
 text {* 
-  The following convenient notation @{text "x \<approx>Lang y"} means:
+  The following convenient notation @{text "x \<approx>A y"} means:
   string @{text "x"} and @{text "y"} are equivalent with respect to 
-  language @{text "Lang"}.
+  language @{text "A"}.
   *}
 
 definition
   str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
 where
-  "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"
+  "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
 
 text {*
   The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions.
diff -r 2335fcb96052 -r d63baacbdb16 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Feb 07 13:17:01 2011 +0000
+++ b/Paper/Paper.thy	Mon Feb 07 20:30:10 2011 +0000
@@ -14,6 +14,7 @@
 
 notation (latex output)
   str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
+  str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
   Seq (infixr "\<cdot>" 100) and
   Star ("_\<^bsup>\<star>\<^esup>") and
   pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
@@ -21,9 +22,11 @@
   quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
   REL ("\<approx>") and
   UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
-  L ("L '(_')" [0] 101) and
+  L ("L'(_')" [0] 101) and
+  Lam ("\<lambda>'(_')" [100] 100) and 
+  Trn ("_, _" [100, 100] 100) and 
   EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
-  transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longrightarrow}}> _" [100, 100, 100] 100)
+  transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100)
 (*>*)
 
 
@@ -213,12 +216,12 @@
 
 
   Central to our proof will be the solution of equational systems
-  involving regular expressions. For this we will use Arden's lemma \cite{}
+  involving regular expressions. 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.
 
-  \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\
+  \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
   If @{thm (prem 1) ardens_revised} then
   @{thm (lhs) ardens_revised} has the unique solution
   @{thm (rhs) ardens_revised}.
@@ -226,7 +229,7 @@
 
   \begin{proof}
   For the right-to-left direction we assume @{thm (rhs) ardens_revised} and show
-  that @{thm (lhs) ardens_revised} holds. From Prop.~\ref{langprops}$(i)$ 
+  that @{thm (lhs) ardens_revised} holds. From Prop.~\ref{langprops}@{text "(i)"} 
   we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
   which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both 
   sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
@@ -245,12 +248,12 @@
   of @{text "\<star>"}.
   For the inclusion in the other direction we assume a string @{text s}
   with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}
-  we know by Prop.~\ref{langprops}$(ii)$ that 
+  we know by Prop.~\ref{langprops}@{text "(ii)"} that 
   @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
   (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 
   From @{text "(*)"} it follows then that
   @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
-  implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}$(iii)$ 
+  implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} 
   this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
   \end{proof}
 
@@ -294,36 +297,108 @@
 section {* Finite Partitions Imply Regularity of a Language *}
 
 text {*
+  The central definition in the Myhill-Nerode theorem is the
+  \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two 
+  strings are related, provided there is no distinguishing extension in this
+  language. This can be defined as:
+
   \begin{definition}[Myhill-Nerode Relation]\mbox{}\\
-  @{thm str_eq_rel_def[simplified]}
+  @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
   \end{definition}
 
   \noindent
-  It is easy to see that @{term "\<approx>A"} is an equivalence relation, which partitions
-  the set of all string, @{text "UNIV"}, into a set of equivalence classed. We define
-  the set @{term "finals A"} as those equivalence classes that contain strings of 
-  @{text A}, namely
+  It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
+  partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
+  equivalence classes. One direction of the Myhill-Nerode theorem establishes 
+  that if there are finitely many equivalence classes, then the language is 
+  regular. In our setting we have therefore
+  
+  \begin{theorem}\label{myhillnerodeone}
+  @{thm[mode=IfThen] hard_direction}
+  \end{theorem}
 
+  \noindent
+  To prove this theorem, we define the set @{term "finals A"} as those equivalence
+  classes that contain strings of @{text A}, namely
+  %
   \begin{equation} 
   @{thm finals_def}
   \end{equation}
 
   \noindent
-  It is easy to show that @{thm lang_is_union_of_finals} holds. We can also define 
-  a notion of \emph{transition} between equivalence classes as
+  It is straightforward to show that @{thm lang_is_union_of_finals} holds. 
+  Therefore if we know that there exists a regular expression for every
+  equivalence class in @{term "finals A"} (which by assumption must be
+  a finite set), then we can just combine these regular expressions with @{const ALT}
+  and obtain a regular expression that matches every string in @{text A}.
 
+
+  We prove Thm.~\ref{myhillnerodeone} by calculating a regular expression for
+  \emph{all} equivalence classes, not just the ones in @{term "finals A"}. We
+  first define a notion of \emph{transition} between equivalence classes
+  %
   \begin{equation} 
   @{thm transition_def}
   \end{equation}
 
   \noindent
-  which means if we add the character @{text c} to all strings in the equivalence
-  class @{text Y} HERE
+  which means that if we concatenate all strings matching the regular expression @{text r} 
+  to the end of all strings in the equivalence class @{text Y}, we obtain a subset of 
+  @{text X}. Note that we do not define any automaton here, we merely relate two sets
+  w.r.t.~a regular expression. 
+  
+  Next we build an equational system that
+  contains an equation for each equivalence class. Suppose we have 
+  the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+  contains the empty string @{text "[]"} (since equivalence classes are disjoint).
+  Let us assume @{text "[] \<in> X\<^isub>1"}. We can build the following equational system
+  
+  \begin{center}
+  \begin{tabular}{rcl}
+  @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\
+  @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\
+  & $\vdots$ \\
+  @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
+  \end{tabular}
+  \end{center}
 
-  \begin{theorem}
-  Given a language @{text A}.
-  @{thm[mode=IfThen] hard_direction}
-  \end{theorem}
+  \noindent
+  where the pairs @{text "(Y\<^isub>i\<^isub>j, r\<^isub>i\<^isub>j)"} stand for all transitions 
+  @{term "Y\<^isub>i\<^isub>j \<Turnstile>r\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}.  The term @{text "\<lambda>(EMPTY)"} acts as a marker for the equivalence
+  class containing @{text "[]"}. (Note that we mark, roughly speaking, the
+  single ``initial'' state in the equational system, which is different from
+  the method by Brzozowski \cite{Brzozowski64}, which marks the ``terminal''
+  states.) Overloading the function @{text L} for the two kinds of terms in the 
+  equational system as follows
+  
+  \begin{center}
+  @{thm L_rhs_e.simps(1)[where r="r", THEN eq_reflection]}\hspace{20mm}
+  @{thm L_rhs_e.simps(2)[where X="X" and r="r", THEN eq_reflection]}
+  \end{center}
+
+  \noindent
+  we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
+  %
+  \begin{equation}\label{inv1}
+  @{text "X\<^isub>i = L(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> L(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
+  \end{equation}
+
+  \noindent
+  hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+  %
+  \begin{equation}\label{inv2}
+  @{text "X\<^isub>1 = L(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> L(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> L(\<lambda>(EMPTY))"}.
+  \end{equation}
+
+  \noindent
+  hold. The reason for adding the @{text \<lambda>}-marker to our equational system is 
+  to obtain this equations, which only holds in this form since none of 
+  the other terms contain the empty string. Our proof of Thm.~\ref{myhillnerodeone}
+  will be by transforming the equational system into a \emph{solved form}
+  maintaining the invariants \eqref{inv1} and \eqref{inv2}. From the solved
+  form we will be able to read off the regular expressions using our 
+  variant of Arden's Lemma (Lem.~\ref{arden}).
+
 *}
 
 section {* Regular Expressions Generate Finitely Many Partitions *}
diff -r 2335fcb96052 -r d63baacbdb16 Paper/document/root.tex
--- a/Paper/document/root.tex	Mon Feb 07 13:17:01 2011 +0000
+++ b/Paper/document/root.tex	Mon Feb 07 20:30:10 2011 +0000
@@ -22,6 +22,7 @@
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 
+
 \begin{document}
 
 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
@@ -45,6 +46,7 @@
 using only regular expressions. 
 \end{abstract}
 
+
 \input{session}
 
 \bibliographystyle{plain}