regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:b755090d0f3d
+:97090fc7aa9f
 abbreviation "TIMESS \<equiv> Times_set"
 abbreviation "STAR \<equiv> Star"
 notation (latex output)
-str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
+str_eq ("\<approx>\<^bsub>_\<^esub>") and
-str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
+str_eq_applied ("_ \<approx>\<^bsub>_\<^esub> _") and
 conc (infixr "\<cdot>" 100) and
 star ("_\<^bsup>\<star>\<^esup>") and
 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
 Suc ("_+1" [100] 100) and
 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) 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\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
+tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
-tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
+tag_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_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_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_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) and
+tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
-tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
+tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
 Delta ("\<Delta>'(_')") and
 nullable ("\<delta>'(_')") and
 Cons ("_ :: _" [100, 100] 100)
 lemma meta_eq_app:
 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
 by auto
+lemma str_eq_def':
+shows "x \<approx>A y \<equiv> (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)"
+unfolding str_eq_def by simp
 lemma conc_def':
 "A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
 unfolding conc_def by simp
 connecting the accepting states of $A_1$ to the initial state of $A_2$:
 %
 \begin{center}
 \begin{tabular}{ccc}
-\begin{tikzpicture}[scale=0.9]
+\begin{tikzpicture}[scale=1]
 %\draw[step=2mm] (-1,-1) grid (1,1);
 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
 \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
 \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
-\draw (-0.6,0.0) node {\footnotesize$A_1$};
+\draw (-0.6,0.0) node {\small$A_1$};
-\draw ( 0.6,0.0) node {\footnotesize$A_2$};
+\draw ( 0.6,0.0) node {\small$A_2$};
 \end{tikzpicture}
 &
 \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
 &
-\begin{tikzpicture}[scale=0.9]
+\begin{tikzpicture}[scale=1]
 %\draw[step=2mm] (-1,-1) grid (1,1);
 \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
 \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
 \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
 \draw (C) to [very thick, bend left=45] (B);
 \draw (D) to [very thick, bend right=45] (B);
-\draw (-0.6,0.0) node {\footnotesize$A_1$};
+\draw (-0.6,0.0) node {\small$A_1$};
-\draw ( 0.6,0.0) node {\footnotesize$A_2$};
+\draw ( 0.6,0.0) node {\small$A_2$};
 \end{tikzpicture}
 \end{tabular}
 \end{center}
 Also one might consider automata theory as a well-worn stock subject where
 everything is crystal clear. However, paper proofs about automata often
 involve subtle side-conditions which are easily overlooked, but which make
 formal reasoning rather painful. For example Kozen's proof of the
-Myhill-Nerode theorem requires that the automata do not have inaccessible
+Myhill-Nerode theorem requires that automata do not have inaccessible
 states \cite{Kozen97}. Another subtle side-condition is completeness of
 automata, that is automata need to have total transition functions and at most one
 `sink' state from which there is no connection to a final state (Brozowski
 mentions this side-condition in the context of state complexity
 of automata \cite{Brozowski10}). Such side-conditions mean that if we define a regular
 \noindent
 {\bf Contributions:} There is an extensive literature on regular languages.
 To our best knowledge, our proof of the Myhill-Nerode theorem is the first
 that is based on regular expressions, only. The part of this theorem stating
 that finitely many partitions imply regularity of the language is proved by
-an argument about solving equational sytems.  This argument appears to be
+an argument about solving equational systems.  This argument appears to be
 folklore. For the other part, we give two proofs: one direct proof using
 certain tagging-functions, and another indirect proof using Antimirov's
 partial derivatives \cite{Antimirov95}. Again to our best knowledge, the
 tagging-functions have not been used before to establish the Myhill-Nerode
 theorem. Derivatives of regular expressions have been recently used quite
 string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of
 the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}.  We omit
 the proofs for these properties, but invite the reader to consult our
 formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
-The notation in Isabelle/HOL for the quotient of a language @{text A} according to an
+The notation in Isabelle/HOL for the quotient of a language @{text A}
-equivalence relation @{term REL} is @{term "A // REL"}. We will write
+according to an equivalence relation @{term REL} is @{term "A // REL"}. We
-@{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined
+will write @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined as
-as \mbox{@{text "{y | y \<approx> x}"}}.
+\mbox{@{text "{y | y \<approx> x}"}}, and have @{text "x \<approx> y"} if and only if @{text
+"\<lbrakk>x\<rbrakk>\<^isub>\<approx> = \<lbrakk>y\<rbrakk>\<^isub>\<approx>"}.
 Central to our proof will be the solution of equational systems
 involving equivalence classes of languages. For this we will use Arden's Lemma
 (see \cite[Page 100]{Sakarovitch09}),
 \end{lmm}
 \begin{proof}
 For the right-to-left direction we assume @{thm (rhs) arden} and show
 that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"}
-we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"},
+we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
-which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both
+which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both
-sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side
+sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
 is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. This completes this direction.
 For the other direction we assume @{thm (lhs) arden}. By a simple induction
 on @{text n}, we can establish the property
 \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]}
+@{thm str_eq_def'}
 \end{center}
 \end{dfntn}
 \noindent
 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
 \end{tabular}}
 \end{equation}
 \noindent
 where @{text "d\<^isub>1\<dots>d\<^isub>n"} is the sequence of all characters
-except @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
+but not containing @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
 characters.
 Overloading the function @{text \<calL>} for the two kinds of terms in the
 equational system, we have
 section {* Myhill-Nerode, Second Part *}
 text {*
 \noindent
-In this section and the next we will give two proofs for establishing the second
+In this section we will give a proof for establishing the second
 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 first proof will be by induction on the structure of @{text r}. It turns out
+The 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
 \noindent
 Much more interesting, however, are the inductive cases. They seem hard to solve
 directly. The reader is invited to try.
-In order how to see how our first proof proceeds we use the following suggestive picture
+In order to see how our proof proceeds consider the following suggestive picture
-from Constable et al \cite{Constable00}:
+taken from Constable et al \cite{Constable00}:
-\begin{center}
+\begin{equation}\label{pics}
-\begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
+\mbox{\begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
 \begin{tikzpicture}[scale=1]
 %Circle
 \draw[thick] (0,0) circle (1.1);
 \end{tikzpicture}
 &
 \draw[very thick] (0, 0) -- (\a:1.1);
 \foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2}
 \draw (\a: 0.77) node {$a_{\l}$};
 \end{tikzpicture}\\
 @{term UNIV} & @{term "UNIV // (\<approx>(lang r))"} & @{term "UNIV // R"}
-\end{tabular}
+\end{tabular}}
-\end{center}
+\end{equation}
-Our first proof will rely on some
+\noindent
+The relation @{term "\<approx>(lang r)"} partitions the set of all strings into some
+equivalence classes. To show that there are only finitely many of
+them, it suffices to show in each induction step the existence of another
+relation, say @{text R}, for which we can show that there are finitely many
+equivalence classes and which refines @{term "\<approx>(lang r)"}. A relation @{text
+"R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text
+"R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} 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.
 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.
+that means we take the image of @{text f} w.r.t.~all elements in the
-With this we will be able to infer that the tagging-functions, seen as relations,
+domain. With this we will be able to infer that the tagging-functions, seen
-give rise to finitely many equivalence classes of @{const UNIV}. Finally we
+as relations, give rise to finitely many equivalence classes of @{const
-will show that the tagging-relations are more refined than @{term "\<approx>(lang r)"}, which
+UNIV}. Finally we will show that the tagging-relations are more refined than
-implies that @{term "UNIV // \<approx>(lang r)"} must also be finite---a relation @{text "R\<^isub>1"}
+@{term "\<approx>(lang r)"}, which implies that @{term "UNIV // \<approx>(lang r)"} must
-is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
+also be finite.  We formally define the notion of a \emph{tagging-relation}
-We formally define the notion of a \emph{tagging-relation} as follows.
+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 \<^raw:$\threesim$>\<^bsub>tag\<^esub> y \<equiv> tag x = tag y"}\;.
 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>(lang r)"} is finite, we have to find a tagging-function whose
+that @{term "UNIV // \<approx>(lang r)"} is finite, we have to construct a tagging-function whose
 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
 %
 \begin{center}
-@{thm tag_str_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
+@{thm tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
 \end{center}
 \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_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"}
 is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A \<cdot> B"}
 (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}
+\begin{tabular}{l}
+@{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\
 @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+\end{tabular}
 \end{center}
 %
 \noindent
 and \emph{string subtraction}:
 %
 \begin{center}
-@{text "[] - y \<equiv> []"}\hspace{10mm}
+\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-@{text "x - [] \<equiv> x"}\hspace{10mm}
+@{text "[] - y"}  & @{text "\<equiv>"} & @{text "[]"}\\
-@{text "cx - dy \<equiv> if c = d then x - y else cx"}
+@{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 \<cdot> B"} there are only two possible ways of how to `split'
 this string to be in @{term "A \<cdot> B"}:
 %
 \begin{center}
-\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+\begin{tabular}{c}
-\scalebox{0.7}{
+\scalebox{0.9}{
 \begin{tikzpicture}
 \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
 node[midway, below=0.5em]{@{term "x' \<in> A"}};
 \end{tikzpicture}}
-&
+\\
-\scalebox{0.7}{
+\scalebox{0.9}{
 \begin{tikzpicture}
 \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
 \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$  };
 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
 In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. For this we use the
 following tagging-function
 %
 \begin{center}
-@{thm tag_str_Times_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+@{thm tag_Times_def[where ?A="A" and ?B="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') @ z"}
 is in the language @{text B}.
 \begin{proof}[@{const TIMES}-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_TIMES A B"} is a subset of this product set, and therefore finite.
+@{term "tag_Times 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_TIMES A B x = tag_str_TIMES A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
+@{term "\<forall>z. tag_Times A B x = tag_Times A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
 \end{center}
 %
 \noindent
 There are two cases to be considered (see pictures above). First, there exists
 a @{text "x'"} such that
 \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_TIMES A B"} also
+and by the assumption about @{term "tag_Times 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}
 %
 relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
 have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
 @{term "y @ z \<in> A \<cdot> B"}, as needed in this case.
 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
+By the assumption about @{term "tag_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 "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
 \end{proof}
 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
+@{thm tag_Star_def[where ?A="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.
+@{term "tag_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>"}
+@{term "\<forall>z. tag_Star A x = tag_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

changeset 181	97090fc7aa9f
parent 180	b755090d0f3d
child 182	560712a29a36