regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:6b4c20714b4f
+:f77a7138f791
 \end{tabular}
 \end{tabular}
 \end{center}
 Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
-a regular expression that matches all languages of @{text rs}. We only need to know the existence
+a regular expression that matches the union of all languages of @{text rs}. We only need to know the
+existence
 of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
 @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the
 set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
 %
 \begin{equation}\label{uplus}
 \noindent
 holds, whereby @{text "\<calL> ` rs"} stands for the
 image of the set @{text rs} under function @{text "\<calL>"}.
 *}
-section {* The Myhill-Nerode Theorem, First Part *}
+section {* The Myhill-Nerode Theorem *}
 text {*
 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
 \begin{equation}
 @{thm finals_def}
 \end{equation}
 \noindent
-In our running example, @{text "X\<^isub>2"} is the only equivalence class in @{term "finals {[c]}"}.
+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
 @{thm finals_in_partitions} 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
 \begin{center}
 @{thm ardenable_def}
 \end{center}
 \noindent
-This allows us to prove
+This allows us to prove a version of Arden's lemma on the level of equations.
 \begin{lemma}\label{ardenable}
 Given an equation @{text "X = rhs"}.
 If @{text "X = \<Union>\<calL> ` rhs"},
 @{thm (prem 2) Arden_keeps_eq}, and
 and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
 The property ardenable is clearly preserved because the append-operation
 cannot make a regular expression to match the empty string. Validity is
 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 replace @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+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 our assumption
+\mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption
 to complete the proof.\qed
 \end{proof}
 \noindent
 We also need the fact that @{text Iter} decreases the termination measure.
 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
+%
 \begin{center}
 @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
 \end{center}
 \noindent
 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"}
 \end{center}
+%
 \noindent
 which by unfolding the Myhill-Nerode relation is identical to
 %
 \begin{equation}\label{pattern}
 @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
 \end{equation}
+%
 \noindent
 since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
 \eqref{pattern} we just have to unfold the definition of the tagging-relation 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
 \noindent
 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"}
 \end{center}
+%
 \noindent
 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
 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"}
 \end{center}
+%
 \noindent
 and \emph{string subtraction}:
+%
 \begin{center}
 \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
 @{text "x - []"} & @{text "\<equiv>"} & @{text x}\\
 @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\
 \end{tabular}
 \end{center}
+%
 \noindent
 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
 Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split'
 this string to be in @{term "A ;; B"}:
+%
 \begin{center}
 \scalebox{0.7}{
 \begin{tikzpicture}
 \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'"}\hspace{4em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'"}\hspace{0.5em}$ };
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
 node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
 \end{tikzpicture}}
 \end{center}
+%
 \noindent
 Either there is a prefix of @{text x} in @{text A} and the rest in @{text B},
 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}.
 In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the
 following tagging-function
+%
 \begin{center}
 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
 \end{center}
 \noindent
-with the idea that in the first split we have to make sure that @{text "x - x'"}
+with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
 is in the language @{text B}.
 \begin{proof}[@{const SEQ}-Case]
 If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
 then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
 @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
 We have to show injectivity of this tagging-function as
+%
 \begin{center}
 @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
 \end{center}
+%
 \noindent
 There are two cases to be considered (see pictures above). First, there exists
 a @{text "x'"} such that
 @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
+%
 \begin{center}
 @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
 \end{center}
+%
 \noindent
 and by the assumption about @{term "tag_str_SEQ A B"} also
+%
 \begin{center}
 @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
 \end{center}
+%
 \noindent
 That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and
 @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
 @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
 relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
 \noindent
 The case for @{const STAR} is similar as @{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}
 \scalebox{0.7}{
 \begin{tikzpicture}
 \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ };
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
 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>"},
 @{text "x' < x"} and the rest @{text "(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
 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
 the following tagging-function:
+%
 \begin{center}
-@{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}
+@{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
 \end{center}
 \begin{proof}[@{const STAR}-Case]
 If @{term "finite (UNIV // \<approx>A)"}
 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
 @{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
 Again we have to show injectivity of this tagging-function as
+%
 \begin{center}
 @{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
 \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
 string, we can devide the string @{text "x @ z"} as shown in the picture
 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}
+%
 \noindent
 which by assumption is equal to
+%
 \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'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"} and @{text "y'\<^isub>m\<^isub>a\<^isub>x < y"}
+and we know that we have a @{text "y' \<in> A\<star>"} and @{text "y' < y"}
-and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y'\<^isub>m\<^isub>a\<^isub>x)"}. Unfolding the Myhill-Nerode
+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'\<^isub>m\<^isub>a\<^isub>x) @ 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 @{text "z\<^isub>b \<in> A\<star>"}.
-Therefore, finally, @{text "y'\<^isub>m\<^isub>a\<^isub>x @ ((y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
+Therefore, finally, @{text "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
-@{term "y @ z \<in> A\<star>"}. As a 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 @{text "L r"} and
-complete the proof.
+complete the proof.\qed
 \end{proof}
 *}
 text {*
 In this paper we took the view that a regular language is one where there
 exists a regular expression that matches all of its strings. Regular
 expressions can conveniently be defined as a datatype in a HOL-based theorem
 prover. For us it was therefore interesting to find out how far we can push
-this point of view.
+this point of view. We have establised both directions of the Myhill-Nerode
+theorem.
-Having formalised the Myhill-Nerode theorem means we
+%
-pushed quite far. Using this theorem we can obviously prove when a language
+\begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\
+A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
+\end{theorem}
+%
+\noindent
+Having formalised this theorem means we
+pushed our point of view quite far. Using this theorem we can obviously prove when a language
 is \emph{not} regular---by establishing that it has infinitely many
 equivalence classes generated by the Myhill-Nerode relation (this is usually
 the purpose of the pumping lemma \cite{Kozen97}).  We can also use it to
 establish the standard textbook results about closure properties of regular
 languages. Interesting is the case of closure under complement, because
 it seems difficult to construct a regular expression for the complement
 language by direct means. However the existence of such a regular expression
 can be easily proved using the Myhill-Nerode theorem since
+%
 \begin{center}
 @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
 \end{center}
+%
 \noindent
 holds for any strings @{text "s\<^isub>1"} and @{text
 "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
 partitions.  Proving the existence of such a regular expression via automata would
 be quite involved. It includes the
 find our own arguments.  So for us the formalisation was not the
 bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but
 from what is shown in the Nuprl Math Library about their development it
 seems substantially larger than ours. The code of ours can be found in the
 Mercurial Repository at
+\mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
-\begin{center}
-\url{http://www4.in.tum.de/~urbanc/regexp.html}
-\end{center}
 Our proof of the first direction is very much inspired by \emph{Brzozowski's
 algebraic mehod} used to convert a finite automaton to a regular
 expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence

changeset 132	f77a7138f791
parent 131	6b4c20714b4f
child 133	3ab755a96cef