35 abbreviation "PLUS \<equiv> Plus"

    35 abbreviation "PLUS \<equiv> Plus"

    36 abbreviation "TIMES \<equiv> Times"

    36 abbreviation "TIMES \<equiv> Times"

    37 abbreviation "TIMESS \<equiv> Timess"

    37 abbreviation "TIMESS \<equiv> Timess"

    38 abbreviation "STAR \<equiv> Star"

    38 abbreviation "STAR \<equiv> Star"

    39 

    39 

    40 

    44 

    41 notation (latex output)

    45 notation (latex output)

    42   str_eq ("\<approx>\<^bsub>_\<^esub>") and

    46   str_eq ("\<approx>\<^bsub>_\<^esub>") and

    43   str_eq_applied ("_ \<approx>\<^bsub>_\<^esub> _") and

    47   str_eq_applied ("_ \<approx>\<^bsub>_\<^esub> _") and

    44   conc (infixr "\<cdot>" 100) and

    48   conc (infixr "\<cdot>" 100) and

    69   tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>" [100] 100) and

    73   tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>" [100] 100) and

    70   Delta ("\<Delta>'(_')") and

    74   Delta ("\<Delta>'(_')") and

    71   nullable ("\<delta>'(_')") and

    75   nullable ("\<delta>'(_')") and

    72   Cons ("_ :: _" [100, 100] 100) and

    76   Cons ("_ :: _" [100, 100] 100) and

    73   Rev ("Rev _" [1000] 100) and

    77   Rev ("Rev _" [1000] 100) and

    75   ONE ("ONE" 999) and

    80   ONE ("ONE" 999) and

    76   ZERO ("ZERO" 999) and

    81   ZERO ("ZERO" 999) and

    78   UNIV1 ("UNIV\<^isup>+") and

    83   UNIV1 ("UNIV\<^isup>+") and

    80 

   104 

    81 lemma meta_eq_app:

   105 lemma meta_eq_app:

    82   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"

   106   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"

    83   by auto

   107   by auto

    84 

   108 

   131   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

   155   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

   132   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

   156   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

   133   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

   157   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

   134   "_asm" :: "prop \<Rightarrow> asms" ("_")

   158   "_asm" :: "prop \<Rightarrow> asms" ("_")

   135 

   159 

   136 

   181 

   137 (*>*)

   182 (*>*)

   138 

   183 

   139 

   184 

   140 section {* Introduction *}

   185 section {* Introduction *}

   443   @{term "[] \<notin> A"}. However we will need the following `reversed' 

   488   @{term "[] \<notin> A"}. However we will need the following `reversed' 

   444   version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \<cdot> X"} to

   489   version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \<cdot> X"} to

   445   \mbox{@{term "X \<cdot> A"}}).

   490   \mbox{@{term "X \<cdot> A"}}).

   446 

   491 

   447   \begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\

   492   \begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\

   451   \end{lmm}

   496   \end{lmm}

   452 

   497 

   453   \begin{proof}

   498   \begin{proof}

   456   we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},

   501   we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},

   457   which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both 

   502   which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both 

   458   sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side

   503   sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side

   459   is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation 

   504   is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation 

   460   completes this direction. 

   505   completes this direction. 

   461 

   506 

   463   on @{text n}, we can establish the property

   508   on @{text n}, we can establish the property

   464 

   509 

   465   \begin{center}

   510   \begin{center}

   467   \end{center}

   512   \end{center}

   468   

   513   

   469   \noindent

   514   \noindent

   470   Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for

   515   Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for

   471   all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition

   516   all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition

   472   of @{text "\<star>"}.

   517   of @{text "\<star>"}.

   473   For the inclusion in the other direction we assume a string @{text s}

   518   For the inclusion in the other direction we assume a string @{text s}

   475   we know by Property~\ref{langprops}@{text "(ii)"} that 

   520   we know by Property~\ref{langprops}@{text "(ii)"} that 

   476   @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}

   521   @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}

   477   (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer). 

   522   (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer). 

   478   From @{text "(*)"} it follows then that

   523   From @{text "(*)"} it follows then that

   480   implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"} 

   525   implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"} 

   481   this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.

   526   this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.

   482   \end{proof}

   527   \end{proof}

   483 

   528 

   484   \noindent

   529   \noindent

   518   of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's

   563   of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's

   519   @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const PLUS} over the 

   564   @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const PLUS} over the 

   520   set @{text rs} with @{const ZERO} for the empty set. We can prove that for a finite set @{text rs}

   565   set @{text rs} with @{const ZERO} for the empty set. We can prove that for a finite set @{text rs}

   521   %

   566   %

   522   \begin{equation}\label{uplus}

   567   \begin{equation}\label{uplus}

   524   \end{equation}

   569   \end{equation}

   525 

   570 

   526   \noindent

   571   \noindent

   527   holds, whereby @{text "\<calL> ` rs"} stands for the 

   572   holds, whereby @{text "\<calL> ` rs"} stands for the 

   528   image of the set @{text rs} under function @{text "\<calL>"} defined as

   573   image of the set @{text rs} under function @{text "\<calL>"} defined as

  1572   showed this directly by induction on @{text "r"} using tagging-functions. 

  1617   showed this directly by induction on @{text "r"} using tagging-functions. 

  1573   However, there is also  an indirect method to come up with such a refined 

  1618   However, there is also  an indirect method to come up with such a refined 

  1574   relation by using derivatives of regular expressions~\cite{Brzozowski64}. 

  1619   relation by using derivatives of regular expressions~\cite{Brzozowski64}. 

  1575 

  1620 

  1576   Assume the following two definitions for the \emph{left-quotient} of a language,

  1621   Assume the following two definitions for the \emph{left-quotient} of a language,

  1578   is a character and @{text s} a string, respectively:

  1623   is a character and @{text s} a string, respectively:

  1579 

  1624 

  1580   \begin{center}

  1625   \begin{center}

  1581   \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l}

  1626   \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l}

  1582   @{thm (lhs) Der_def}  & @{text "\<equiv>"} & @{thm (rhs) Der_def}\\

  1627   @{thm (lhs) Der_def}  & @{text "\<equiv>"} & @{thm (rhs) Der_def}\\

  1586 

  1631 

  1587   \noindent

  1632   \noindent

  1588   In order to aid readability, we shall make use of the following abbreviation

  1633   In order to aid readability, we shall make use of the following abbreviation

  1589 

  1634 

  1590   \begin{center}

  1635   \begin{center}

  1592   \end{center}

  1637   \end{center}

  1593   

  1638   

  1594   \noindent

  1639   \noindent

  1595   where we apply the left-quotient to a set of languages and then combine the results.

  1640   where we apply the left-quotient to a set of languages and then combine the results.

  1596   Clearly we have the following equivalence between the Myhill-Nerode relation

  1641   Clearly we have the following equivalence between the Myhill-Nerode relation

  1597   (Definition~\ref{myhillneroderel}) and left-quotients

  1642   (Definition~\ref{myhillneroderel}) and left-quotients

  1598 

  1643 

  1599   \begin{equation}\label{mhders}

  1644   \begin{equation}\label{mhders}

  1601   \end{equation}

  1646   \end{equation}

  1602 

  1647 

  1603   \noindent

  1648   \noindent

  1604   It is also straightforward to establish the following properties of left-quotients

  1649   It is also straightforward to establish the following properties of left-quotients

  1605   

  1650   

  1606   \begin{equation}

  1651   \begin{equation}

  1607   \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}

  1652   \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}

  1612   @{thm (lhs) Der_conc}  & $=$ & @{thm (rhs) Der_conc}\\

  1657   @{thm (lhs) Der_conc}  & $=$ & @{thm (rhs) Der_conc}\\

  1618   \end{tabular}}

  1663   \end{tabular}}

  1619   \end{equation}

  1664   \end{equation}

  1620 

  1665 

  1621   \noindent

  1666   \noindent

  1622   where @{text "\<Delta>"} in the fifth line is a function that tests whether the

  1667   where @{text "\<Delta>"} in the fifth line is a function that tests whether the

  1623   empty string is in the language and returns @{term "{[]}"} or @{term "{}"},

  1668   empty string is in the language and returns @{term "{[]}"} or @{term "{}"},

  1624   accordingly.  Note also that in the last equation we use the list-cons operator written

  1669   accordingly.  Note also that in the last equation we use the list-cons operator written

  1625   \mbox{@{text "_ :: _"}}.  The only interesting case is the case of @{term "A\<star>"}

  1670   \mbox{@{text "_ :: _"}}.  The only interesting case is the case of @{term "A\<star>"}

  1626   where we use Property~\ref{langprops}@{text "(i)"} in order to infer that

  1671   where we use Property~\ref{langprops}@{text "(i)"} in order to infer that

  1629   c A) \<cdot> A\<star>"}. 

  1674   c A) \<cdot> A\<star>"}. 

  1630 

  1675 

  1631   Brzozowski observed that the left-quotients for languages of

  1676   Brzozowski observed that the left-quotients for languages of

  1632   regular expressions can be calculated directly using the notion of

  1677   regular expressions can be calculated directly using the notion of

  1633   \emph{derivatives of a regular expression} \cite{Brzozowski64}. We define

  1678   \emph{derivatives of a regular expression} \cite{Brzozowski64}. We define

  1634   this notion in Isabelle/HOL as follows:

  1679   this notion in Isabelle/HOL as follows:

  1635 

  1680 

  1636   \begin{center}

  1681   \begin{center}

  1637   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}

  1682   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}

  1644      & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%

  1689      & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%

  1646      &             & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%  

  1691      &             & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%  

  1651   \end{tabular}

  1696   \end{tabular}

  1652   \end{center}

  1697   \end{center}

  1653 

  1698 

  1654   \noindent

  1699   \noindent

  1655   The last two clauses extend derivatives from characters to strings. The

  1700   The last two clauses extend derivatives from characters to strings. The

  1677   one can easily show that left-quotients and derivatives of regular expressions 

  1722   one can easily show that left-quotients and derivatives of regular expressions 

  1678   relate as follows (see for example~\cite{Sakarovitch09}):

  1723   relate as follows (see for example~\cite{Sakarovitch09}):

  1679 

  1724 

  1680   \begin{equation}\label{Dersders}

  1725   \begin{equation}\label{Dersders}

  1681   \mbox{\begin{tabular}{c}

  1726   \mbox{\begin{tabular}{c}

  1684   \end{tabular}}

  1729   \end{tabular}}

  1685   \end{equation}

  1730   \end{equation}

  1686 

  1731 

  1687   \noindent

  1732   \noindent

  1688   The importance of this fact in the context of the Myhill-Nerode theorem is that 

  1733   The importance of this fact in the context of the Myhill-Nerode theorem is that 

  1689   we can use \eqref{mhders} and \eqref{Dersders} in order to 

  1734   we can use \eqref{mhders} and \eqref{Dersders} in order to 

  1690   establish that 

  1735   establish that 

  1691 

  1736 

  1692   \begin{center}

  1737   \begin{center}

  1693   @{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm}

  1738   @{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm}

  1695   \end{center}

  1740   \end{center}

  1696 

  1741 

  1697   \noindent

  1742   \noindent

  1698   holds and hence

  1743   holds and hence

  1699 

  1744 

  1700   \begin{equation}

  1745   \begin{equation}

  1702   \end{equation}

  1747   \end{equation}

  1703 

  1748 

  1704 

  1749 

  1705   \noindent

  1750   \noindent

  1706   This means the right-hand side (seen as a relation) refines the Myhill-Nerode

  1751   This means the right-hand side (seen as a relation) refines the Myhill-Nerode

  1741   derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined

  1786   derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined

  1742   in Isabelle/HOL as follows:

  1787   in Isabelle/HOL as follows:

  1743 

  1788 

  1744   \begin{center}

  1789   \begin{center}

  1745   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}

  1790   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}

  1752      & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%

  1797      & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%

  1754      & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%  

  1799      & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%  

  1759   \end{tabular}

  1804   \end{tabular}

  1760   \end{center}

  1805   \end{center}

  1761 

  1806 

  1762   \noindent

  1807   \noindent

  1763   Again the last two clauses extend partial derivatives from characters to strings. 

  1808   Again the last two clauses extend partial derivatives from characters to strings. 

  1771 

  1816 

  1772   \noindent

  1817   \noindent

  1773   in order to `sequence' a regular expression with a set of regular

  1818   in order to `sequence' a regular expression with a set of regular

  1774   expressions. Note that in the last clause we first build the set of partial

  1819   expressions. Note that in the last clause we first build the set of partial

  1775   derivatives w.r.t~the character @{text c}, then build the image of this set under the

  1820   derivatives w.r.t~the character @{text c}, then build the image of this set under the

  1777   convenient to introduce for this the following abbreviation

  1822   convenient to introduce for this the following abbreviation

  1778 

  1823 

  1779   \begin{center}

  1824   \begin{center}

  1785 

  1830 

  1786   \begin{center}

  1831   \begin{center}

  1787   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}

  1832   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}

  1789   \end{tabular}

  1834   \end{tabular}

  1790   \end{center}

  1835   \end{center}

  1791 

  1836 

  1792   Partial derivatives can be seen as having the @{text "ACI"}-identities already built in: 

  1837   Partial derivatives can be seen as having the @{text "ACI"}-identities already built in: 

  1793   taking the partial derivatives of the

  1838   taking the partial derivatives of the

  1795   equal sets.  Antimirov \cite{Antimirov95} showed a similar result to

  1840   equal sets.  Antimirov \cite{Antimirov95} showed a similar result to

  1796   \eqref{Dersders} for partial derivatives, namely

  1841   \eqref{Dersders} for partial derivatives, namely

  1797 

  1842 

  1798   \begin{equation}\label{Derspders}

  1843   \begin{equation}\label{Derspders}

  1799   \mbox{\begin{tabular}{lc}

  1844   \mbox{\begin{tabular}{lc}

  1802   \end{tabular}}

  1847   \end{tabular}}

  1803   \end{equation} 

  1848   \end{equation} 

  1804 

  1849 

  1805   \begin{proof}

  1850   \begin{proof}

  1806   The first fact is by a simple induction on @{text r}. For the second we slightly

  1851   The first fact is by a simple induction on @{text r}. For the second we slightly

  1807   modify Antimirov's proof by performing an induction on @{text s} where we

  1852   modify Antimirov's proof by performing an induction on @{text s} where we

  1808   generalise over all @{text r}. That means in the @{text "cons"}-case the 

  1853   generalise over all @{text r}. That means in the @{text "cons"}-case the 

  1809   induction hypothesis is

  1854   induction hypothesis is

  1810 

  1855 

  1811   \begin{center}

  1856   \begin{center}

  1813   \end{center}

  1858   \end{center}

  1814 

  1859 

  1815   \noindent

  1860   \noindent

  1816   With this we can establish

  1861   With this we can establish

  1817 

  1862 

  1818   \begin{center}

  1863   \begin{center}

  1819   \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll}

  1864   \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll}

  1826   \end{tabular}

  1871   \end{tabular}

  1827   \end{center}

  1872   \end{center}

  1828   

  1873   

  1829   \noindent

  1874   \noindent

  1830   Note that in order to apply the induction hypothesis in the fourth equation, we

  1875   Note that in order to apply the induction hypothesis in the fourth equation, we

  1836   Taking \eqref{Dersders} and \eqref{Derspders} together gives the relationship 

  1881   Taking \eqref{Dersders} and \eqref{Derspders} together gives the relationship 

  1837   between languages of derivatives and partial derivatives

  1882   between languages of derivatives and partial derivatives

  1838 

  1883 

  1839   \begin{equation}

  1884   \begin{equation}

  1840   \mbox{\begin{tabular}{lc}

  1885   \mbox{\begin{tabular}{lc}

  1843   \end{tabular}}

  1888   \end{tabular}}

  1844   \end{equation} 

  1889   \end{equation} 

  1845 

  1890 

  1846   \noindent

  1891   \noindent

  1847   These two properties confirm the observation made earlier 

  1892   These two properties confirm the observation made earlier 

  1851   Antimirov also proved that for every language and regular expression 

  1896   Antimirov also proved that for every language and regular expression 

  1852   there are only finitely many partial derivatives, whereby the set of partial

  1897   there are only finitely many partial derivatives, whereby the set of partial

  1853   derivatives of @{text r} w.r.t.~a language @{text A} is defined as

  1898   derivatives of @{text r} w.r.t.~a language @{text A} is defined as

  1854 

  1899 

  1855   \begin{equation}\label{Pdersdef}

  1900   \begin{equation}\label{Pdersdef}

  1857   \end{equation}

  1902   \end{equation}

  1858 

  1903 

  1859   \begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov}

  1904   \begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov}

  1860   For every language @{text A} and every regular expression @{text r}, 

  1905   For every language @{text A} and every regular expression @{text r}, 

  1862   \end{thrm}

  1907   \end{thrm}

  1863 

  1908 

  1864   \noindent

  1909   \noindent

  1865   Antimirov's proof first establishes this theorem for the language @{term UNIV1}, 

  1910   Antimirov's proof first establishes this theorem for the language @{term UNIV1}, 

  1866   which is the set of all non-empty strings. For this he proves:

  1911   which is the set of all non-empty strings. For this he proves:

  1867 

  1912 

  1868   \begin{equation}\label{pdersunivone}

  1913   \begin{equation}\label{pdersunivone}

  1869   \mbox{\begin{tabular}{l}

  1914   \mbox{\begin{tabular}{l}

  1876   \end{tabular}}

  1921   \end{tabular}}

  1877   \end{equation}

  1922   \end{equation}

  1878 

  1923 

  1879   \noindent

  1924   \noindent

  1880   from which one can deduce by induction on @{text r} that

  1925   from which one can deduce by induction on @{text r} that

  1881 

  1926 

  1882   \begin{center}

  1927   \begin{center}

  1884   \end{center}

  1929   \end{center}

  1885 

  1930 

  1886   \noindent

  1931   \noindent

  1887   holds. Now Antimirov's theorem follows because

  1932   holds. Now Antimirov's theorem follows because

  1888 

  1933 

  1889   \begin{center}

  1934   \begin{center}

  1896   closely in our formalisation (only the last two cases of

  1941   closely in our formalisation (only the last two cases of

  1897   \eqref{pdersunivone} involve some non-routine induction arguments), we omit

  1942   \eqref{pdersunivone} involve some non-routine induction arguments), we omit

  1898   the details.

  1943   the details.

  1899 

  1944 

  1900   Let us now return to our proof for the second direction in the Myhill-Nerode

  1945   Let us now return to our proof for the second direction in the Myhill-Nerode

  1905   \begin{proof}[Proof of Theorem~\ref{myhillnerodetwo} (second version)]

  1950   \begin{proof}[Proof of Theorem~\ref{myhillnerodetwo} (second version)]

  1906   Using \eqref{mhders}

  1951   Using \eqref{mhders}

  1907   and \eqref{Derspders} we can easily infer that

  1952   and \eqref{Derspders} we can easily infer that

  1908 

  1953 

  1909   \begin{center}

  1954   \begin{center}

  1911   \end{center}

  1956   \end{center}

  1912 

  1957 

  1913   \noindent

  1958   \noindent

  1914   which means the tagging-relation @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"} refines @{term "\<approx>(lang r)"}.

  1959   which means the tagging-relation @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"} refines @{term "\<approx>(lang r)"}.

  1915   So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\<approx>(lang r)))"}} 

  1960   So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\<approx>(lang r)))"}} 

  1917   the latter, we can use Lemma~\ref{finone} and show that the range of the 

  1962   the latter, we can use Lemma~\ref{finone} and show that the range of the 

  1919   \ref{Pdersdef}, which gives us that 

  1964   \ref{Pdersdef}, which gives us that 

  1920 

  1965 

  1921   \begin{center}

  1966   \begin{center}

  1927   which we know is finite by Theorem~\ref{antimirov}. Consequently there 

  1972   which we know is finite by Theorem~\ref{antimirov}. Consequently there 

  1928   are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"},

  1973   are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"},

  1929   which refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the 

  1974   which refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the 

  1930   second part of the Myhill-Nerode theorem.

  1975   second part of the Myhill-Nerode theorem.

  1931   \end{proof}

  1976   \end{proof}

  2005 

  2050 

  2006   A perhaps surprising fact is that regular languages are closed under any

  2051   A perhaps surprising fact is that regular languages are closed under any

  2007   left-quotient. Define

  2052   left-quotient. Define

  2008 

  2053 

  2009   \begin{center}

  2054   \begin{center}

  2011   \end{center}

  2056   \end{center}

  2012 

  2057 

  2013   \noindent

  2058   \noindent

  2014   and assume @{text B} is any language and @{text A} is regular, then @{term

  2059   and assume @{text B} is any language and @{text A} is regular, then @{term

  2016   using partial derivatives: From @{text A} being regular we know there exists

  2061   using partial derivatives: From @{text A} being regular we know there exists

  2017   a regular expression @{text r} such that @{term "A = lang r"}. We also know

  2062   a regular expression @{text r} such that @{term "A = lang r"}. We also know

  2019   regular expression @{text r} (recall Theorem~\ref{antimirov}). By definition 

  2064   regular expression @{text r} (recall Theorem~\ref{antimirov}). By definition 

  2020   and \eqref{Derspders} therefore

  2065   and \eqref{Derspders} therefore

  2021 

  2066 

  2022   

  2067   

  2023   \begin{equation}\label{eqq}

  2068   \begin{equation}\label{eqq}

  2025   \end{equation}

  2070   \end{equation}

  2026 

  2071 

  2027   \noindent

  2072   \noindent

  2029   B r"}, we know by \eqref{uplus} that there exists a regular expression so that

  2074   B r"}, we know by \eqref{uplus} that there exists a regular expression so that

  2033 *}

  2078 *}

  2034 

  2079 

  2035 

  2080 

  2036 section {* Conclusion and Related Work *}

  2081 section {* Conclusion and Related Work *}

  2037 

  2082