regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:f9d54f49c808
+:e7504bfdbd50
 text {*
 \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.
+language. This can be defined as a ternary relation.
 \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}
 \begin{equation}
 @{thm transition_def}
 \end{equation}
 \noindent
-which means that if we concatenate the character @{text c} to the end of all
+which means that if we append the character @{text c} 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 an automaton here, we merely relate two sets
 (with the help of a character). In our concrete example we have
 @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<^isub>i\<Rightarrow> X\<^isub>3"} with @{text "d\<^isub>i"} being any
 other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>c\<^isub>j\<Rightarrow> X\<^isub>3"} for any
 Next we construct an \emph{initial equational system} that
 contains an equation for each equivalence class. We first give
 an informal description of this construction. 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 build the following equational system
+Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following initial equational system
 \begin{center}
 \begin{tabular}{rcl}
 @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, ATOM c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, ATOM c\<^isub>1\<^isub>p) + \<lambda>(ONE)"} \\
 @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, ATOM c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, ATOM c\<^isub>2\<^isub>o)"} \\
 @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, ATOM c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, ATOM c\<^isub>n\<^isub>q)"}\\
 \end{tabular}
 \end{center}
 \noindent
-where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"}
+where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} are pairs consiting of an equivalence class and
+a regular expression. In the initial equational system, they
 stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
 X\<^isub>i"}.
 %The intuition behind the equational system is that every
 %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
 %corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states
 \end{lmm}
 \noindent
 Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
 but we can still ensure that it holds throughout our algorithm of transforming equations
-into solved form. The \emph{substitution-operation} takes an equation
+into solved form.
+The \emph{substitution-operation} takes an equation
 of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
 \begin{center}
 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
 @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
 In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
 the following tagging-function:
 %
 \begin{center}
 @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]}~@{text "\<equiv>"}~
-@{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>s, x\<^isub>p) \<in> Partitions x}"}
+@{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
 \end{center}
 \begin{proof}[@{const Star}-Case]
 If @{term "finite (UNIV // \<approx>A)"}
 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of

changeset 338	e7504bfdbd50
parent 334	d47c2143ab8a
child 348	bea94f1e6771