regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:08afbed1c8c7
+:604518f0127f
 @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"}
 \end{equation}
 \noindent
 changes the type---the disjoint union is not a set, but a set of pairs.
-Using this definition for disjoint unions means we do not have a single type for automata
+Using this definition for disjoint union means we do not have a single type for automata
 and hence will not be able to state certain properties about \emph{all}
 automata, since there is no type quantification available in HOL. 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
 {\bf Contributions:}
 There is an extensive literature on regular languages.
 To our knowledge, our proof of the Myhill-Nerode theorem is the
 first that is based on regular expressions, only. We prove the part of this theorem
 stating that a regular expression has only finitely many partitions using certain
-tagging-functions. Again to our best knowledge, these tagging functions have
+tagging-functions. Again to our best knowledge, these tagging-functions have
 not been used before to establish the Myhill-Nerode theorem.
 *}
 section {* Preliminaries *}
 \begin{lemma}\label{ardenable}
 Given an equation @{text "X = rhs"}.
 If @{text "X = \<Union>\<calL> ` rhs"},
 @{thm (prem 2) Arden_keeps_eq}, and
 @{thm (prem 3) Arden_keeps_eq}, then
-@{text "X = \<Union>\<calL> ` (Arden X rhs)"}
+@{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
 \end{lemma}
 \noindent
 The \emph{substitution-operation} takes an equation
 of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
 text {*
 We will prove in this section the second part of the Myhill-Nerode
 theorem. It can be formulated in our setting as follows.
 \begin{theorem}
-Given @{text "r"} is a regular expressions, then @{thm Myhill_Nerode2}.
+Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
 \end{theorem}
 \noindent
 The proof will be by induction on the structure of @{text r}. It turns out
 the base cases are straightforward.
 \noindent
 Much more interesting, however, are the inductive cases. They seem hard to be solved
 directly. The reader is invited to try.
-Our method will rely on some
+Our proof will rely on some
-\emph{tagging functions} defined over strings. Given the inductive hypothesis, it will
+\emph{taggingfunctions} defined over strings. Given the inductive hypothesis, it will
-be easy to prove that the 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"}).
-With this we will be able to infer that the tagging functions, seen as relations,
+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 relation is more refined than @{term "\<approx>(L r)"}, which
+will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which
 implies that @{term "UNIV // \<approx>(L 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"}).
 We formally define the notion of a \emph{tagging-relation} as follows.
 \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
 \end{lemma}
 \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
-@{text "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{text "Pow (UNIV // R\<^isub>1)"},
+@{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
 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} with @{term "X = R\<^isub>2 `` {x}"}
+We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}.
-and @{text "x \<in> X"}. From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f 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
 \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>(L 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)"}.
 Let us attempt the @{const ALT}-case first.
 \begin{proof}[@{const "ALT"}-Case]
-We take as tagging function
+We take as tagging-function
 %
 \begin{center}
 @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
 \end{center}
 The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
 they are slightly more complicated. In the @{const SEQ}-case we essentially have
 to be able to infer that
 %
 \begin{center}
-@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+@{text "\<dots>"}@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
 \end{center}
 %
 \noindent
-using the information given by the appropriate tagging function. The complication
+using the information given by the appropriate tagging-function. The complication
 is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
-(this was easy in case of @{term "A \<union> B"}). For this we define the
+(this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
 notions of \emph{string prefixes}
 %
 \begin{center}
 @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
 @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
 with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case
 by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
 \end{proof}
 \noindent
-The case for @{const STAR} is similar as @{const SEQ}, but poses a few extra challenges. When
+The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When
 we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the
 empty string, we
 have the following picture:
 %
 \begin{center}
 node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
 \end{tikzpicture}}
 \end{center}
 %
 \noindent
-We can find a strict prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"},
+We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
-@{text "x' < x"} and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string
+@{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string
 @{text "[]"} would do.
-There are many such prefixes, but there can only be finitely many of them (the
+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'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we
-know it is in @{text "A\<star>"}. By definition of @{text "A\<star>"}, we can separate
+know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate
-this string into two parts, say @{text "a"} and @{text "b"}, such @{text "a \<in> A"}
+this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
-and @{text "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
+and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
 otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}
 `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
 @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
-@{text "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{text "x @ z \<in> A\<star>"}
+@{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
 such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
 `border' of @{text x} and @{text z}. This string is @{text "(x - x') @ z\<^isub>a"}.
-In order to show that @{text "x @ z \<in> A\<star>"} implies @{text "y @ z \<in> A\<star>"}, we use
+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 tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
 \end{center}
 \end{center}
 %
 \noindent
 We first need to consider the case that @{text x} is the empty string.
 From the assumption we can infer @{text y} is the empty string and
-clearly have @{text "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
+clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
 string, we can divide the string @{text "x @ z"} as shown in the picture
-above. By the tagging function we have
+above. By the tagging-function we have
 %
 \begin{center}
 @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
 \end{center}
 %
 \begin{center}
 @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
 \end{center}
 %
 \noindent
-and we know that we have a @{text "y' \<in> A\<star>"} and @{text "y' < y"}
+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 @{text "z\<^isub>b \<in> A\<star>"}.
+relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
-Therefore, finally, @{text "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
+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 @{text "L r"} and
+@{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "L r"} and
 complete the proof.\qed
 \end{proof}
 *}

changeset 135	604518f0127f
parent 134	08afbed1c8c7
child 136	13b0f3dac9a2