diff -r fa8d33d13cb6 -r cf1c17431dab Journal/Paper.thy --- a/Journal/Paper.thy Mon Aug 15 21:09:08 2011 +0000 +++ b/Journal/Paper.thy Mon Aug 15 22:36:26 2011 +0000 @@ -1568,7 +1568,7 @@ show that there are only finitely many equivalence classes. So far we showed this directly by induction on @{text "r"} using tagging-functions. However, there is also an indirect method to come up with such a refined - relation by using derivatives of regular expressions \cite{Brzozowski64}. + relation by using derivatives of regular expressions~\cite{Brzozowski64}. Assume the following two definitions for the \emph{left-quotient} of a language, which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c} @@ -1618,7 +1618,7 @@ \noindent where @{text "\"} in the fifth line is a function that tests whether the empty string is in the language and returns @{term "{[]}"} or @{term "{}"}, accordingly. - The only interesting case above is the last one where we use Prop.~\ref{langprops}@{text "(i)"} + The only interesting case is the last one where we use Prop.~\ref{langprops}@{text "(i)"} in order to infer that @{term "Der c (A\) = Der c (A \ A\)"}. We can then complete the proof by noting that @{term "Delta A \ Der c (A\) \ (Der c A) \ A\"}. @@ -1649,7 +1649,8 @@ The last two clauses extend derivatives from characters to strings---i.e.~list of characters. The list-cons operator is written \mbox{@{text "_ :: _"}}. The boolean function @{term "nullable r"} needed in the @{const Times}-case tests - whether a regular expression can recognise the empty string: + whether a regular expression can recognise the empty string. It can be defined as + follows. \begin{center} \begin{tabular}{c@ {\hspace{10mm}}c} @@ -1670,8 +1671,8 @@ \noindent By induction on the regular expression @{text r}, respectively on the string @{text s}, - one can easily show that left-quotients and derivatives relate as follows - \cite{Sakarovitch09}: + one can easily show that left-quotients and derivatives of regular expressions + relate as follows (for example \cite{Sakarovitch09}): \begin{equation}\label{Dersders} \mbox{\begin{tabular}{c} @@ -1681,10 +1682,10 @@ \end{equation} \noindent - The importance in the context of the Myhill-Nerode theorem is that + The importance of this fact in the context of the Myhill-Nerode theorem is that we can use \eqref{mhders} and \eqref{Dersders} in order to establish that @{term "x \(lang r) y"} is equivalent to - @{term "lang (ders x r) = lang (ders y r)"}. Hence + \mbox{@{term "lang (ders x r) = lang (ders y r)"}}. Hence \begin{equation} @{term "x \(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"} @@ -1692,20 +1693,21 @@ \noindent - which means the right-hand side (seen as relation) refines the - Myhill-Nerode relation. Consequently, we can use - @{text "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"} as a tagging-relation - for the regular expression @{text r}. However, in - order to be useful for the second part of the Myhill-Nerode theorem, we also have to show that - for the corresponding language there are only finitely many derivatives---thus ensuring - that there are only finitely many equivalence classes. Unfortunately, this - is not true in general. Sakarovitch gives an example where a regular - expression has infinitely many derivatives w.r.t.~the language - \mbox{@{term "({a} \ {b})\ \ ({a} \ {b})\ \ {a}"}} - \cite[Page~141]{Sakarovitch09}. + which means the right-hand side (seen as relation) refines the Myhill-Nerode + relation. Consequently, we can use @{text + "\<^raw:$\threesim$>\<^bsub>(\x. ders x r)\<^esub>"} as a + tagging-relation. However, in order to be useful for the second part of the + Myhill-Nerode theorem, we have to be able to establish that for the + corresponding language there are only finitely many derivatives---thus + ensuring that there are only finitely many equivalence + classes. Unfortunately, this is not true in general. Sakarovitch gives an + example where a regular expression has infinitely many derivatives + w.r.t.~the language \mbox{@{term "({a} \ {b})\ \ ({a} \ {b})\ \ {a}"}} + \cite[Page~141]{Sakarovitch09}. + What Brzozowski \cite{Brzozowski64} established is that for every language there - \emph{are} only finitely `dissimilar' derivatives for a regular + \emph{are} only finitely `dissimilar' derivatives of a regular expression. Two regular expressions are said to be \emph{similar} provided they can be identified using the using the @{text "ACI"}-identities: @@ -2050,12 +2052,11 @@ HOLlight and Isabelle/HOL are based. In order to guarantee consistency, formalisations can only extend HOL by definitions that introduce a notion in terms of already existing concepts. A convenient definition for automata - (based on graphs) use a polymorphic type for the state nodes. This allows us - to use the standard operation of disjoint union in order to compose two - automata. But we cannot use such a polymorphic definition of automata in HOL - as part of the definition for regularity of a language (a set of strings). - Consider the following attempt - + (based on graphs) uses a polymorphic type for the state nodes. This allows + us to use the standard operation of disjoint union in order to compose two + automata. Unfortunately, we cannot use such a polymorphic definition of + in HOL as part of the definition for regularity of a language (a + set of strings). Consider the following attempt \begin{center} @{text "is_regular A \ \M(\). is_finite_automata (M) \ \(M) = A"}