--- a/Paper/Paper.thy Mon Feb 21 02:33:05 2011 +0000
+++ b/Paper/Paper.thy Mon Feb 21 03:30:38 2011 +0000
@@ -143,7 +143,7 @@
\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
@@ -228,7 +228,7 @@
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.
*}
@@ -587,7 +587,7 @@
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
@@ -868,7 +868,7 @@
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
@@ -896,13 +896,13 @@
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
- \emph{tagging functions} defined over strings. Given the inductive hypothesis, it will
- be easy to prove that the range of these tagging functions is finite
+ Our proof will rely on some
+ \emph{taggingfunctions} defined over strings. Given the inductive hypothesis, it will
+ 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.
@@ -953,14 +953,14 @@
\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}"}
- and @{text "x \<in> X"}. From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
+ 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"},
@@ -969,12 +969,12 @@
\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]}
@@ -1016,13 +1016,13 @@
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}
@@ -1160,7 +1160,7 @@
\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:
@@ -1204,23 +1204,23 @@
\end{center}
%
\noindent
- We can find a strict prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"},
- @{text "x' < x"} and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string
+ We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
+ @{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
- this string into two parts, say @{text "a"} and @{text "b"}, such @{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"},
+ 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 that @{text "a \<in> A"}
+ 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}
@@ -1240,9 +1240,9 @@
\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>})"}
@@ -1256,11 +1256,11 @@
\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>"}.
- Therefore, finally, @{text "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
+ 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
complete the proof.\qed
\end{proof}
*}