regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:d371536861bc
+:2b414a8a7132
 Suc ("_+1" [100] 100) and
 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
 REL ("\<approx>") and
 UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
 lang ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
+lang_trm ("\<^raw:\ensuremath{\cal{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:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
 Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
 Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
-tag_str_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
+tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
-tag_str_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
+tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
 tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
 tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
-tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
+tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
+tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
+Delta ("\<Delta>'(_')") and
+nullable ("\<delta>'(_')")
 lemma meta_eq_app:
 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
 by auto
 \noindent
 changes the type---the disjoint union is not a set, but a set of
 pairs. Using this definition for disjoint union means we do not have a
 single type for automata. As a result we will not be able to define a regular
 language as one for which there exists an automaton that recognises all its
-strings. Similarly, we cannot state properties about \emph{all} automata,
+strings, since there is no type quantification available in HOL (unlike in Coq, for
-since there is no type quantification available in HOL (unlike in Coq, for
 example).
 An alternative, which provides us with a single type for automata, is to give every
 state node an identity, for example a natural
 number, and then be careful to rename these identities apart whenever
 will be needed for regular expressions. Moreover, a reasoning infrastructure
 (like induction and recursion) comes for free in HOL-based theorem provers.
 This has recently been exploited in HOL4 with a formalisation of
 regular expression matching based on derivatives \cite{OwensSlind08} and
 with an equivalence checker for regular expressions in Isabelle/HOL
-\cite{KraussNipkow11}.  The purpose of this paper is to show that a central
+\cite{KraussNipkow11}.  The main purpose of this paper is to show that a central
 result about regular languages---the Myhill-Nerode theorem---can be
 recreated by only using regular expressions. This theorem gives necessary
 and sufficient conditions for when a language is regular. As a corollary of
 this theorem we can easily establish the usual closure properties, including
 complementation, for regular languages.\medskip
 \noindent
-{\bf Contributions:} There is an extensive literature on regular languages.
+{\bf Contributions:} There is an extensive literature on regular
-To our best knowledge, our proof of the Myhill-Nerode theorem is the first
+languages.  To our best knowledge, our proof of the Myhill-Nerode theorem is
-that is based on regular expressions, only. The part of this theorem stating
+the first that is based on regular expressions, only. The part of this
-that finitely many partitions imply regularity of the language is proved by
+theorem stating that finitely many partitions imply regularity of the
-an argument about solving equational sytems.  This argument seems to be folklore.
+language is proved by an argument about solving equational sytems.  This
-For the other part, we give two proofs: a
+argument appears to be folklore. For the other part, we give two proofs: one
-direct proof using certain tagging-functions, and an indirect proof using
+direct proof using certain tagging-functions, and another indirect proof
-Antimirov's partial derivatives \cite{Antimirov95} (also earlier russion work).
+using Antimirov's partial derivatives \cite{Antimirov95}. Again to our best
-Again to our best knowledge, the tagging-functions have not been used before to
+knowledge, the tagging-functions have not been used before to establish the
-establish the Myhill-Nerode theorem.
+Myhill-Nerode theorem. Derivatives of regular expressions have been used
+extensively in the literature, unlike partial derivatives. However, partial
+derivatives are more suitable in the context of the Myhill-Nerode theorem,
+since it is easier to establish formally their finiteness result.
 *}
 section {* Preliminaries *}
 text {*
 @{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
 (the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
 From @{text "(*)"} it follows then that
 @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn
 implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
-this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.\qed
+this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
 \end{proof}
 \noindent
 Regular expressions are defined as the inductive datatype
 section {* The Myhill-Nerode Theorem, First Part *}
 text {*
-Folklore: Henzinger (arden-DFA-regexp.pdf)
+\footnote{Folklore: Henzinger (arden-DFA-regexp.pdf); Hofmann}
 \noindent
 The key 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 a tertiary relation.
-\begin{dfntn}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
+\begin{dfntn}[Myhill-Nerode Relation]\label{myhillneroderel}
+Given a language @{text A}, two strings @{text x} and
 @{text y} are Myhill-Nerode related provided
 \begin{center}
 @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
 \end{center}
 \end{dfntn}
 \end{equation}
 \noindent
 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
+It is straightforward to show that in general
-@{thm finals_in_partitions} hold.
+\begin{center}
+@{thm lang_is_union_of_finals}\hspace{15mm}
+@{thm finals_in_partitions}
+\end{center}
+\noindent
+hold.
 Therefore if we know that there exists a regular expression for every
 equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
 a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression
 that matches every string in @{text A}.
 \begin{proof}
 Finiteness is given by the assumption and the way how we set up the
 initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
 follows from the fact that the equivalence classes are disjoint. The @{text ardenable}
 property also follows from the setup of the initial equational system, as does
-validity.\qed
+validity.
 \end{proof}
 \noindent
 Next we show that @{text Iter} preserves the invariant.
 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 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 the assumption
-to complete the proof.\qed
+to complete the proof.
 \end{proof}
 \noindent
 We also need the fact that @{text Iter} decreases the termination measure.
 By assumption we know that @{text "ES"} is finite and has more than one element.
 Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
 @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
 that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
 removes the equation @{text "Y = yrhs"} from the system, and therefore
-the cardinality of @{const Iter} strictly decreases.\qed
+the cardinality of @{const Iter} strictly decreases.
 \end{proof}
 \noindent
 This brings us to our property we want to establish for @{text Solve}.
 does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
 with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
 of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
 for which the invariant holds. This allows us to conclude that
 @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
-as needed.\qed
+as needed.
 \end{proof}
 \noindent
 With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
 there exists a regular expression.
 invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
 we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
 removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
 This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
 So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\<Uplus>rs)"}.
-With this we can conclude the proof.\qed
+With this we can conclude the proof.
 \end{proof}
 \noindent
 Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
 of the Myhill-Nerode theorem.
 in @{term "finals A"} there exists a regular expression. Moreover by assumption
 we know that @{term "finals A"} must be finite, and therefore there must be a finite
 set of regular expressions @{text "rs"} such that
 @{term "\<Union>(finals A) = L (\<Uplus>rs)"}.
 Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
-as the regular expression that is needed in the theorem.\qed
+as the regular expression that is needed in the theorem.
 \end{proof}
 *}
 section {* Myhill-Nerode, Second Part *}
 text {*
 \noindent
-We will prove in this section the second part of the Myhill-Nerode
+In this section and the next we will give two proofs for establishing the second
-theorem. It can be formulated in our setting as follows:
+part of the Myhill-Nerode theorem. It can be formulated in our setting as follows:
 \begin{thrm}
 Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
 \end{thrm}
 \noindent
-The proof will be by induction on the structure of @{text r}. It turns out
+The first proof will be by induction on the structure of @{text r}. It turns out
 the base cases are straightforward.
 \begin{proof}[Base Cases]
 The cases for @{const ZERO}, @{const ONE} and @{const ATOM} are routine, because
 @{thm quot_atom_subset}
 \end{tabular}
 \end{center}
 \noindent
-hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed
+hold, which shows that @{term "UNIV // \<approx>(lang r)"} must be finite.
 \end{proof}
 \noindent
 Much more interesting, however, are the inductive cases. They seem hard to solve
 directly. The reader is invited to try.
-Our proof will rely on some
+Our first proof will rely on some
 \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will
-be easy to prove that the \emph{range} of these tagging-functions is finite
+be easy to prove that the \emph{range} of these tagging-functions is finite.
-(the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
+The range of a function @{text f} is defined as
+\begin{center}
+@{text "range f \<equiv> f ` UNIV"}
+\end{center}
+\noindent
+that means we take the image of @{text f} w.r.t.~all elements in the domain.
 With this we will be able to infer that the tagging-functions, seen as relations,
 give rise to finitely many equivalence classes of @{const UNIV}. Finally we
-will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which
+will show that the tagging-relations are more refined than @{term "\<approx>(lang r)"}, which
-implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^isub>1"}
+implies that @{term "UNIV // \<approx>(lang r)"} must also be finite---a relation @{text "R\<^isub>1"}
-is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}).
+is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
 We formally define the notion of a \emph{tagging-relation} as follows.
 \begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
 and @{text y} are \emph{tag-related} provided
 \begin{center}
-@{text "x =tag= y \<equiv> tag x = tag y"}\;.
+@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \<equiv> tag x = tag y"}\;.
 \end{center}
 \end{dfntn}
 In order to establish finiteness of a set @{text A}, we shall use the following powerful
 and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
 assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
 From the assumptions we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with
 @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in
 turn means that the equivalence classes @{text X}
-and @{text Y} must be equal.\qed
+and @{text Y} must be equal.
 \end{proof}
 \begin{lmm}\label{fintwo}
 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
 \begin{proof}
 We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
 be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
 @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
-which is finite by assumption. What remains to be shown is that @{text f} is injective
+which must be finite by assumption. What remains to be shown is that @{text f} is injective
 on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence
 classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
 @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
 @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
 We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}.
 From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
 and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
 such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
 are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
-they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
+they must also be @{text "R\<^isub>2"}-related, as we need to show.
 \end{proof}
 \noindent
 Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
-that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging-function whose
+that @{term "UNIV // \<approx>(lang r)"} is finite, we have to find a tagging-function whose
-range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(lang r)"}.
 Let us attempt the @{const PLUS}-case first.
 \begin{proof}[@{const "PLUS"}-Case]
 We take as tagging-function
 %
 \noindent
 where @{text "A"} and @{text "B"} are some arbitrary languages.
 We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
 then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
-@{term "tag_str_PLUS A B"} is a subset of this product set---so finite. It remains to be shown
+@{term "tag_str_Plus A B"} is a subset of this product set---so finite. It remains to be shown
 that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to
 showing
 %
 \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"}
 \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse
 in which set, @{text A} or @{text B}, the string @{term "x @ z"} is.
 The definition of the tagging-function will give us in each case the
 information to infer that @{text "y @ z \<in> A \<union> B"}.
 Finally we
-can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
+can discharge this case by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
 \end{proof}
 \noindent
 The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
 Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
 By the assumption about @{term "tag_str_TIMES A B"} we have
 @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
 relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
 with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const TIMES}-case
-by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
+by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
 \end{proof}
 \noindent
 The case for @{const STAR} is similar to @{const TIMES}, but poses a few extra challenges. When
 we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the
 \noindent
 and we know that we have a @{term "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 @{term "z\<^isub>b \<in> A\<star>"}.
 Therefore @{term "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 @{term "L r"} and
+@{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "lang r"} and
-complete the proof.\qed
+complete the proof.
 \end{proof}
 *}
 section {* Second Part based on Partial Derivatives *}
 text {*
 \noindent
 As we have seen in the previous section, in order to establish
 the second direction of the Myhill-Nerode theorem, we need to find
-a more refined relation (more refined than ??) for which we can
+a more refined relation than @{term "\<approx>(lang r)"} for which we can
-show that there are only finitely many equivalence classes.
+show that there are only finitely many equivalence classes. So far we
-Brzozowski presented in the Appendix of~\cite{Brzozowski64}
+showed this by induction on @{text "r"}. However, there is also
+an indirect method to come up with such a refined relation. Assume
+the following two definitions for a left-quotient of a language, which
+we write as @{term "Der c A"} and @{term "Ders s A"} where
+@{text c} is a character and @{text s} a string:
+\begin{center}
+\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
+@{thm (lhs) Der_def}  & @{text "\<equiv>"} & @{thm (rhs) Der_def}\\
+@{thm (lhs) Ders_def} & @{text "\<equiv>"} & @{thm (rhs) Ders_def}\\
+\end{tabular}
+\end{center}
+\noindent
+Now clearly we have the following relation between the Myhill-Nerode relation
+(Definition~\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"}
+\end{equation}
+\noindent
+It is realtively easy to establish the following identidies for left-quotients:
+\begin{center}
+\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}
+\noindent
+where @{text "\<Delta>"} is a function that tests whether the empty string
+is in the language and returns @{term "{[]}"} or @{term "{}"}, respectively.
+The only interesting case above is the last one where we use Prop.~\ref{langprops}
+in order to infer that @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can
+then complete the proof by observing that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"}.
+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
+follows:
+\begin{center}
+\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+@{thm (lhs) der.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(1)}\\
+@{thm (lhs) der.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(2)}\\
+@{thm (lhs) der.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(3)[where c'="d"]}\\
+@{thm (lhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+& @{text "\<equiv>"} & @{thm (rhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+@{thm (lhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+& @{text "\<equiv>"}\\
+\multicolumn{3}{@ {\hspace{5mm}}l@ {}}{@{thm (rhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}}\\
+@{thm (lhs) der.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) der.simps(6)}\smallskip\\
+@{thm (lhs) ders.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) ders.simps(1)}\\
+@{thm (lhs) ders.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) ders.simps(2)}\\
+\end{tabular}
+\end{center}
+\noindent
+The function @{term "nullable r"} tests whether the regular expression
+can recognise the empty string:
+\begin{center}
+\begin{tabular}{cc}
+\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+@{thm (lhs) nullable.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(1)}\\
+@{thm (lhs) nullable.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(2)}\\
+@{thm (lhs) nullable.simps(3)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(3)}\\
+\end{tabular} &
+\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+@{thm (lhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+& @{text "\<equiv>"} & @{thm (rhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+@{thm (lhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+& @{text "\<equiv>"} & @{thm (rhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+@{thm (lhs) nullable.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(6)}\\
+\end{tabular}
+\end{tabular}
+\end{center}
+\noindent
+Brzozowski proved
+\begin{equation}\label{Dersders}
+\mbox{\begin{tabular}{l}
+@{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 \eqref{Dersders} in order to derive
+\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
+\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"}\\
+\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.
 in order to prove the second
 direction of the Myhill-Nerode theorem. There he calculates the
 derivatives for regular expressions and shows that for every
 language there can be only finitely many of them %derivations (if

changeset 174	2b414a8a7132
parent 173	d371536861bc
child 175	edc642266a82