
diff -r 8749db46d5e6 -r 07a269d9642b Journal/Paper.thy
--- a/Journal/Paper.thy	Wed Aug 03 13:56:01 2011 +0000
+++ b/Journal/Paper.thy	Wed Aug 03 17:08:31 2011 +0000
@@ -48,6 +48,7 @@
   quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
   REL ("\<approx>") and
   UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
+  lang ("\<^raw:\ensuremath{\cal{L}}>" 101) and
   lang ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
   lang_trm ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
   Lam ("\<lambda>'(_')" [100] 100) and 
@@ -68,7 +69,11 @@
   tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
   Delta ("\<Delta>'(_')") and
   nullable ("\<delta>'(_')") and
-  Cons ("_ :: _" [100, 100] 100)
+  Cons ("_ :: _" [100, 100] 100) and
+  Rev ("Rev _" [1000] 100) and
+  Der ("Der _ _" [1000, 1000] 100) and
+  ONE ("ONE" 999) and
+  ZERO ("ZERO" 999)
 
 lemma meta_eq_app:
   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
@@ -307,9 +312,9 @@
   Myhill-Nerode theorem requires that automata do not have inaccessible
   states \cite{Kozen97}. Another subtle side-condition is completeness of
   automata, that is automata need to have total transition functions and at most one
-  `sink' state from which there is no connection to a final state (Brozowski
+  `sink' state from which there is no connection to a final state (Brzozowski
   mentions this side-condition in the context of state complexity
-  of automata \cite{Brozowski10}). Such side-conditions mean that if we define a regular
+  of automata \cite{Brzozowski10}). Such side-conditions mean that if we define a regular
   language as one for which there exists \emph{a} finite automaton that
   recognises all its strings (see Def.~\ref{baddef}), then we need a lemma which
   ensures that another equivalent can be found satisfying the
@@ -324,9 +329,9 @@
   exists an automaton that recognises all its strings, we define a
   regular language as:
 
-  \begin{dfntn}
-  A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
-  strings of @{text "A"}.
+  \begin{dfntn}\label{regular}
+  A language @{text A} is \emph{regular}, provided there is a regular expression 
+  that matches all strings of @{text "A"}.
   \end{dfntn}
   
   \noindent
@@ -1465,7 +1470,7 @@
   There are potentially many such prefixes, but there can only be finitely many of them (the 
   string @{text x} is finite). Let us therefore choose the longest one and call it 
   @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we
-  know it is in @{term "A\<star>"} and it is not the empty string. By Lemma~\ref{langprops}@{text "(i)"}, 
+  know it is in @{term "A\<star>"} and it is not the empty string. By Prop.~\ref{langprops}@{text "(i)"}, 
   we can separate
   this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
   and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},
@@ -1542,8 +1547,8 @@
   \end{center}
 
   \noindent
-  Now clearly we have the following relation between the Myhill-Nerode relation
-  (Definition~\ref{myhillneroderel}) and left-quotients
+  Clearly we have the following relation between the Myhill-Nerode relation
+  (Def.~\ref{myhillneroderel}) and left-quotients
 
   \begin{equation}\label{mhders}
   @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"}
@@ -1552,16 +1557,20 @@
   \noindent
   It is realtively easy to establish the following properties for left-quotients:
   
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
+  \begin{equation}
+  \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
   @{thm (lhs) Der_zero}  & $=$ & @{thm (rhs) Der_zero}\\
   @{thm (lhs) Der_one}   & $=$ & @{thm (rhs) Der_one}\\
   @{thm (lhs) Der_atom}  & $=$ & @{thm (rhs) Der_atom}\\
   @{thm (lhs) Der_union} & $=$ & @{thm (rhs) Der_union}\\
   @{thm (lhs) Der_conc}  & $=$ & @{thm (rhs) Der_conc}\\
   @{thm (lhs) Der_star}  & $=$ & @{thm (rhs) Der_star}\\
-  \end{tabular}
-  \end{center}
+  @{thm (lhs) Ders_nil}  & $=$ & @{thm (rhs) Ders_nil}\\
+  @{thm (lhs) Ders_cons} & $=$ & @{thm (rhs) Ders_cons}\\
+  %@{thm (lhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}  & $=$ 
+  %   & @{thm (rhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
+  \end{tabular}}
+  \end{equation}
 
   \noindent
   where @{text "\<Delta>"} is a function that tests whether the empty string
@@ -1572,7 +1581,7 @@
   
   Brzozowski observed that the left-quotients for languages of regular
   expressions can be calculated directly via the notion of \emph{derivatives
-  of a regular expressions} \cite{Brzozowski64} which we define in Isabelle/HOL as 
+  of a regular expression} \cite{Brzozowski64}, which we define in Isabelle/HOL as 
   follows:
 
   \begin{center}
@@ -1594,8 +1603,10 @@
   \end{center}
 
   \noindent
-  The function @{term "nullable r"} tests whether the regular expression
-  can recognise the empty string:
+  The last two lines extend @{const der} to strings (list of characters) where
+  list-cons is written \mbox{@{text "_ :: _"}}. The function @{term "nullable r"} needed 
+  in the @{const Times}-case tests whether a regular expression can recognise 
+  the empty string:
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{10mm}}c}
@@ -1615,52 +1626,56 @@
   \end{center}
 
   \noindent
-  Brzozowski proved 
+  By induction on the regular expression @{text r}, respectively the string @{text s}, 
+  one can easily show that left-quotients and derivatives relate as follows 
+  \cite{Sakarovitch09}:
 
   \begin{equation}\label{Dersders}
-  \mbox{\begin{tabular}{l}
+  \mbox{\begin{tabular}{c}
   @{thm Der_der}\\
   @{thm Ders_ders}
   \end{tabular}}
   \end{equation}
 
   \noindent
-  where the first is by induction on @{text r} and the second by a simple
-  calculation.
+  The importance in the context of the Myhill-Nerode theorem is that 
+  we can use \eqref{mhders} and the equations above in order to 
+  establish that @{term "x \<approx>(lang r) y"} if and only if
+  @{term "lang (ders x r) = lang (ders y r)"}. From this we obtain
 
-  The importance in the context of the Myhill-Nerode theorem is that 
-  we can use \eqref{mhders} and \eqref{Dersders} in order to derive
+  \begin{equation}
+  @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"}
+  \end{equation}
 
-  \begin{center}
-  @{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm} 
-  @{term "lang (ders x r) = lang (ders y r)"}
-  \end{center}
 
   \noindent
-  which means @{term "x \<approx>(lang r) y"} provided @{term "ders x r = ders y r"}.
-  Consequently, we can use as the tagging relation 
-  @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"}, which we know refines @{term "\<approx>(lang r)"}. 
-  This almost helps us because Brozowski also proved that there for every 
-  language there are only 
-  finitely `dissimilar' derivatives for a regular expression. Two regulare
-  expressions are similar if they can be identified using the using the 
-  ACI-identities
+  Consequently, we can use as the tagging relation @{text
+  "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"}, since it refines
+  @{term "\<approx>(lang r)"}. However, in order to be useful in the Myhill-Nerode
+  theorem, we have to show that for a language there are only finitely many
+  derivatives. Unfortunately, this is not true in general: Sakarovitch gives
+  an example with infinitely many derivatives
+  \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved is 
+  that for every language there \emph{are} finitely `dissimilar' derivatives for a
+  regular expression. Two regular expressions are said to be \emph{similar} 
+  provided they can be identified using the using the @{text "ACI"}-identities:
 
   \begin{center}
   \begin{tabular}{cl}
-  (A) & @{term "Plus (Plus r\<^isub>1 r\<^isub>2) r\<^isub>3"} $\equiv$ @{term "Plus r\<^isub>1 (Plus r\<^isub>2 r\<^isub>3)"}\\
-  (C) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
-  (I) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
+  (@{text A}) & @{term "Plus (Plus r\<^isub>1 r\<^isub>2) r\<^isub>3"} $\equiv$ @{term "Plus r\<^isub>1 (Plus r\<^isub>2 r\<^isub>3)"}\\
+  (@{text C}) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
+  (@{text I}) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  Without the indentification, we unfortunately obtain infinitely many
-  derivations (an example is given in \cite[Page~141]{Sakarovitch09}).
-  Reasoning modulo ACI can be done, but it is very painful in a theorem prover.
+  Carrying this idea through menas we now have to reasoning modulo @{text "ACI"}.
+  This can be done, but it is very painful in a theorem prover (since there is
+  no direct characterisation of the set of dissimlar derivatives).
 
-  Fortunately, there is a much simpler approach using partial
-  derivatives introduced by Antimirov \cite{Antimirov95}.
+  Fortunately, there is a much simpler approach using \emph{partial
+  derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined
+  in Isabelle/HOL as follows:
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
@@ -1680,14 +1695,101 @@
   \end{tabular}
   \end{center}
 
+  \noindent
+  Unlike `simple' derivatives, these functions return a set of regular
+  expressions. In the @{const Times} and @{const Star} cases we use 
+
+  \begin{center}
+  @{text "TIMESS rs r \<equiv> {TIMES r' r | r' \<in> rs}"}
+  \end{center}
+
+  \noindent
+  in order to `sequence' a regular expressions with respect to a set of regular 
+  expresions. Note that in the last case we first build the set of partial derivatives
+  w.r.t~@{text c}, then build the image of this set under the function @{term "pders s"}
+  and finally `union up' all resulting sets. Note also that in some sense, partial 
+  derivatives have the @{text "ACI"}-identities already build in. Antimirov 
+  \cite{Antimirov95}
+  showed 
+
+  \begin{equation}
+  \mbox{\begin{tabular}{c}
+  @{thm Der_pder}\\
+  @{thm Ders_pders}
+  \end{tabular}}
+  \end{equation}
+
+  \noindent
+  and proved that for every language and regular expression there are only finitely
+  many partial derivatives.
 *}
 
 section {* Closure Properties *}
 
+text {*
+  The beautiful characteristics of regular languages is that they are closed
+  under many operations. Closure under union, sequencencing and Kleene-star
+  are trivial to establish given our definition of regularity (Def.~\ref{regular}).
+  More interesting is the closure under complement, because
+  it seems difficult to construct a regular expression for the complement
+  language by direct means. However the existence of such a regular expression
+  can now 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 partitions.
+
+  Once closure under complement is established, closure under intersection
+  and set difference is also easy, because
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{term "A \<inter> B = - (- A \<union> - B)"}\\
+  @{term "A - B = - (- A \<union> B)"}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  Closure of regular languages under reversal, which means 
+
+  \begin{center}
+  @{text "A\<^bsup>-1\<^esup> \<equiv> {s\<^bsup>-1\<^esup> | s \<in> A}"}
+  \end{center}
+
+  \noindent 
+  can be shown with the help of the following operation defined on regular
+  expressions
+
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  @{thm (lhs) Rev.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(1)}\\
+  @{thm (lhs) Rev.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(2)}\\
+  @{thm (lhs) Rev.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(3)}\\
+  @{thm (lhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} & 
+      @{thm (rhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} & 
+      @{thm (rhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) Rev.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(6)}\\
+  \end{tabular}
+  \end{center}
+
+
+  In connection with left-quotient, the perhaps surprising fact is that
+  regular languages are closed under any left-quotient.
+
+  
+*}
+
 
 section {* Conclusion and Related Work *}
 
 text {*
+  \noindent
   In this paper we took the view that a regular language is one where there
   exists a regular expression that matches all of its strings. Regular
   expressions can conveniently be defined as a datatype in HOL-based theorem
@@ -1698,32 +1800,23 @@
   \begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\
   A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
   \end{thrm}
-  %
+  
   \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
-  establish the standard textbook results about closure properties of regular
-  languages. Interesting is the case of closure under complement, because
-  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
-  partitions.  Proving the existence of such a regular expression via automata 
-  using the standard method would 
-  be quite involved. It includes the
-  steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
-  "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
-  regular expression.
+  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 establish the standard
+  textbook results about closure properties of regular languages. Interesting
+  is the case of closure under complement, because 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.  Proving the existence of such a
+  regular expression via automata using the standard method would be quite
+  involved. It includes the steps: regular expression @{text "\<Rightarrow>"}
+  non-deterministic automaton @{text "\<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 method of calculating a
@@ -1737,23 +1830,23 @@
 
 
   Our formalisation consists of 780 lines of Isabelle/Isar code for the first
-  direction and 460 for the second, plus around 300 lines of standard material about
-  regular languages. While this might be seen as too large to count as a
-  concise proof pearl, this should be seen in the context of the work done by
-  Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem
-  in Nuprl using automata. They write that their four-member team needed
-  something on the magnitude of 18 months for their formalisation. The
-  estimate for our formalisation is that we needed approximately 3 months and
-  this included the time to find our proof arguments. Unlike Constable et al,
-  who were able to follow the proofs from \cite{HopcroftUllman69}, we had to
-  find our own arguments.  So for us the formalisation was not the
-  bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but
-  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
+  direction and 460 for the second, plus around 300 lines of standard material
+  about regular languages. While this might be seen large, it should be seen
+  in the context of the work done by Constable at al \cite{Constable00} who
+  formalised the Myhill-Nerode theorem in Nuprl using automata. They write
+  that their four-member team needed something on the magnitude of 18 months
+  for their formalisation. The estimate for our formalisation is that we
+  needed approximately 3 months and this included the time to find our proof
+  arguments. Unlike Constable et al, who were able to follow the proofs from
+  \cite{HopcroftUllman69}, we had to find our own arguments.  So for us the
+  formalisation was not the bottleneck. It is hard to gauge the size of a
+  formalisation in Nurpl, but 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
   \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
 
 
+
   Our proof of the first direction is very much inspired by \emph{Brzozowski's
   algebraic method} used to convert a finite automaton to a regular
   expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence




