--- a/Journal/Paper.thy Thu Jul 11 16:46:05 2013 +0100
+++ b/Journal/Paper.thy Thu Sep 12 10:34:11 2013 +0200
@@ -96,7 +96,7 @@
ONE ("ONE" 999) and
ZERO ("ZERO" 999) and
pderivs_lang ("pdersl") and
- UNIV1 ("UNIV\<^isup>+") and
+ UNIV1 ("UNIV\<^sup>+") and
Deriv_lang ("Dersl") and
Derivss ("Derss") and
deriv ("der") and
@@ -132,7 +132,7 @@
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}"
+ "A \<cdot> B = {s\<^sub>1 @ s\<^sub>2 | s\<^sub>1 s\<^sub>2. s\<^sub>1 \<in> A \<and> s\<^sub>2 \<in> B}"
unfolding conc_def by simp
lemma conc_Union_left:
@@ -327,7 +327,7 @@
union, namely
%
\begin{equation}\label{disjointunion}
- @{text "A\<^isub>1 \<uplus> A\<^isub>2 \<equiv> {(1, x) | x \<in> A\<^isub>1} \<union> {(2, y) | y \<in> A\<^isub>2}"}
+ @{text "A\<^sub>1 \<uplus> A\<^sub>2 \<equiv> {(1, x) | x \<in> A\<^sub>1} \<union> {(2, y) | y \<in> A\<^sub>2}"}
\end{equation}
\noindent
@@ -484,7 +484,7 @@
establish the usual closure properties, including complementation, for
regular languages. We use the Continuation Lemma, which is also a corollary
of the Myhill-Nerode Theorem, for establishing
- the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip
+ the non-regularity of the language @{text "a\<^sup>nb\<^sup>n"}.\medskip
\noindent
{\bf Contributions:} There is an extensive literature on regular languages.
@@ -541,8 +541,8 @@
(ii) & @{thm[mode=IfThen] pow_length}\\
(iii) & @{thm conc_Union_left} \\
(iv) & If @{thm (prem 1) star_decom} and @{thm (prem 2) star_decom} then
- there exists an @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{text "x = x\<^isub>p @ x\<^isub>s"}
- and \mbox{@{term "x\<^isub>p \<noteq> []"}} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.
+ there exists an @{text "x\<^sub>p"} and @{text "x\<^sub>s"} with @{text "x = x\<^sub>p @ x\<^sub>s"}
+ and \mbox{@{term "x\<^sub>p \<noteq> []"}} such that @{term "x\<^sub>p \<in> A"} and @{term "x\<^sub>s \<in> A\<star>"}.
\end{tabular}
\end{proposition}
@@ -559,9 +559,9 @@
The notation in Isabelle/HOL for the quotient of a language @{text A}
according to an equivalence relation @{term REL} is @{term "A // REL"}. We
- will write @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined as
+ will write @{text "\<lbrakk>x\<rbrakk>\<^sub>\<approx>"} for the equivalence class defined as
\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>"}.
+ "\<lbrakk>x\<rbrakk>\<^sub>\<approx> = \<lbrakk>y\<rbrakk>\<^sub>\<approx>"}.
Central to our proof will be the solution of equational systems
@@ -604,10 +604,10 @@
@{thm (lhs) lang.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(1)}\\
@{thm (lhs) lang.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(2)}\\
@{thm (lhs) lang.simps(3)[where a="c"]} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(3)[where a="c"]}\\
- @{thm (lhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
- @{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
- @{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
- @{thm (rhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+ @{thm (lhs) lang.simps(4)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]} & @{text "\<equiv>"} &
+ @{thm (rhs) lang.simps(4)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]}\\
+ @{thm (lhs) lang.simps(5)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]} & @{text "\<equiv>"} &
+ @{thm (rhs) lang.simps(5)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]}\\
@{thm (lhs) lang.simps(6)[where r="r"]} & @{text "\<equiv>"} &
@{thm (rhs) lang.simps(6)[where r="r"]}\\
\end{tabular}
@@ -665,15 +665,15 @@
example: consider the regular language built up over the alphabet @{term "{a, b}"} and
containing just the string two strings @{text "[a]"} and @{text "[a, b]"}. The
relation @{term "\<approx>({[a], [a, b]})"} partitions @{text UNIV}
- into four equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"}, @{text "X\<^isub>3"} and @{text "X\<^isub>4"}
+ into four equivalence classes @{text "X\<^sub>1"}, @{text "X\<^sub>2"}, @{text "X\<^sub>3"} and @{text "X\<^sub>4"}
as follows
\begin{center}
\begin{tabular}{l}
- @{text "X\<^isub>1 = {[]}"}\\
- @{text "X\<^isub>2 = {[a]}"}\\
- @{text "X\<^isub>3 = {[a, b]}"}\\
- @{text "X\<^isub>4 = UNIV - {[], [a], [a, b]}"}
+ @{text "X\<^sub>1 = {[]}"}\\
+ @{text "X\<^sub>2 = {[a]}"}\\
+ @{text "X\<^sub>3 = {[a, b]}"}\\
+ @{text "X\<^sub>4 = UNIV - {[], [a], [a, b]}"}
\end{tabular}
\end{center}
@@ -694,7 +694,7 @@
\end{equation}
\noindent
- In our running example, @{text "X\<^isub>2"} and @{text "X\<^isub>3"} are the only
+ In our running example, @{text "X\<^sub>2"} and @{text "X\<^sub>3"} are the only
equivalence classes in @{term "finals {[a], [a, b]}"}.
It is straightforward to show that in general
%
@@ -732,41 +732,41 @@
\begin{center}
\begin{tabular}{l}
- @{term "X\<^isub>1 \<Turnstile>a\<Rightarrow> X\<^isub>2"},\; @{term "X\<^isub>1 \<Turnstile>b\<Rightarrow> X\<^isub>4"};\\
- @{term "X\<^isub>2 \<Turnstile>b\<Rightarrow> X\<^isub>3"},\; @{term "X\<^isub>2 \<Turnstile>a\<Rightarrow> X\<^isub>4"};\\
- @{term "X\<^isub>3 \<Turnstile>a\<Rightarrow> X\<^isub>4"},\; @{term "X\<^isub>3 \<Turnstile>b\<Rightarrow> X\<^isub>4"} and\\
- @{term "X\<^isub>4 \<Turnstile>a\<Rightarrow> X\<^isub>4"},\; @{term "X\<^isub>4 \<Turnstile>b\<Rightarrow> X\<^isub>4"}.
+ @{term "X\<^sub>1 \<Turnstile>a\<Rightarrow> X\<^sub>2"},\; @{term "X\<^sub>1 \<Turnstile>b\<Rightarrow> X\<^sub>4"};\\
+ @{term "X\<^sub>2 \<Turnstile>b\<Rightarrow> X\<^sub>3"},\; @{term "X\<^sub>2 \<Turnstile>a\<Rightarrow> X\<^sub>4"};\\
+ @{term "X\<^sub>3 \<Turnstile>a\<Rightarrow> X\<^sub>4"},\; @{term "X\<^sub>3 \<Turnstile>b\<Rightarrow> X\<^sub>4"} and\\
+ @{term "X\<^sub>4 \<Turnstile>a\<Rightarrow> X\<^sub>4"},\; @{term "X\<^sub>4 \<Turnstile>b\<Rightarrow> X\<^sub>4"}.
\end{tabular}
\end{center}
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
+ the equivalence classes @{text "X\<^sub>1,\<dots>,X\<^sub>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 initial equational system
+ Let us assume @{text "[] \<in> X\<^sub>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\<^sub>1"} & @{text "="} & @{text "(Y\<^sub>1\<^sub>1, ATOM c\<^sub>1\<^sub>1) + \<dots> + (Y\<^sub>1\<^sub>p, ATOM c\<^sub>1\<^sub>p) + \<lambda>(ONE)"} \\
+ @{text "X\<^sub>2"} & @{text "="} & @{text "(Y\<^sub>2\<^sub>1, ATOM c\<^sub>2\<^sub>1) + \<dots> + (Y\<^sub>2\<^sub>o, ATOM c\<^sub>2\<^sub>o)"} \\
& $\vdots$ \\
- @{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)"}\\
+ @{text "X\<^sub>n"} & @{text "="} & @{text "(Y\<^sub>n\<^sub>1, ATOM c\<^sub>n\<^sub>1) + \<dots> + (Y\<^sub>n\<^sub>q, ATOM c\<^sub>n\<^sub>q)"}\\
\end{tabular}
\end{center}
\noindent
- where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} are pairs consisting of an equivalence class and
+ where the terms @{text "(Y\<^sub>i\<^sub>j, ATOM c\<^sub>i\<^sub>j)"} are pairs consisting 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"}.
+ stand for all transitions @{term "Y\<^sub>i\<^sub>j \<Turnstile>c\<^sub>i\<^sub>j\<Rightarrow>
+ X\<^sub>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
- %are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these
- %predecessor states to @{text X\<^isub>i}.
+ %equation @{text "X\<^sub>i = rhs\<^sub>i"} in this system
+ %corresponds roughly to a state of an automaton whose name is @{text X\<^sub>i} and its predecessor states
+ %are the @{text "Y\<^sub>i\<^sub>j"}; the @{text "c\<^sub>i\<^sub>j"} are the labels of the transitions from these
+ %predecessor states to @{text X\<^sub>i}.
There can only be
- finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} in a right-hand side
+ finitely many terms of the form @{text "(Y\<^sub>i\<^sub>j, ATOM c\<^sub>i\<^sub>j)"} in a right-hand side
since by assumption there are only finitely many
equivalence classes and only finitely many characters.
The term @{text "\<lambda>(ONE)"} in the first equation acts as a marker for the initial state, that
@@ -783,11 +783,11 @@
%
\begin{equation}\label{exmpcs}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{term "X\<^isub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
- @{term "X\<^isub>2"} & @{text "="} & @{text "(X\<^isub>1, ATOM a)"}\\
- @{term "X\<^isub>3"} & @{text "="} & @{text "(X\<^isub>2, ATOM b)"}\\
- @{term "X\<^isub>4"} & @{text "="} & @{text "(X\<^isub>1, ATOM b) + (X\<^isub>2, ATOM a) + (X\<^isub>3, ATOM a)"}\\
- & & \mbox{}\hspace{0mm}@{text "+ (X\<^isub>3, ATOM b) + (X\<^isub>4, ATOM a) + (X\<^isub>4, ATOM b)"}\\
+ @{term "X\<^sub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
+ @{term "X\<^sub>2"} & @{text "="} & @{text "(X\<^sub>1, ATOM a)"}\\
+ @{term "X\<^sub>3"} & @{text "="} & @{text "(X\<^sub>2, ATOM b)"}\\
+ @{term "X\<^sub>4"} & @{text "="} & @{text "(X\<^sub>1, ATOM b) + (X\<^sub>2, ATOM a) + (X\<^sub>3, ATOM a)"}\\
+ & & \mbox{}\hspace{0mm}@{text "+ (X\<^sub>3, ATOM b) + (X\<^sub>4, ATOM a) + (X\<^sub>4, ATOM b)"}\\
\end{tabular}}
\end{equation}
@@ -802,17 +802,17 @@
\end{center}
\noindent
- and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
+ and we can prove for @{text "X\<^sub>2\<^sub>.\<^sub>.\<^sub>n"} that the following equations
%
\begin{equation}\label{inv1}
- @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, ATOM c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, ATOM c\<^isub>i\<^isub>q)"}.
+ @{text "X\<^sub>i = \<calL>(Y\<^sub>i\<^sub>1, ATOM c\<^sub>i\<^sub>1) \<union> \<dots> \<union> \<calL>(Y\<^sub>i\<^sub>q, ATOM c\<^sub>i\<^sub>q)"}.
\end{equation}
\noindent
- hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+ hold. Similarly for @{text "X\<^sub>1"} we can show the following equation
%
\begin{equation}\label{inv2}
- @{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, ATOM c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, ATOM c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(ONE))"}.
+ @{text "X\<^sub>1 = \<calL>(Y\<^sub>1\<^sub>1, ATOM c\<^sub>1\<^sub>1) \<union> \<dots> \<union> \<calL>(Y\<^sub>1\<^sub>p, ATOM c\<^sub>1\<^sub>p) \<union> \<calL>(\<lambda>(ONE))"}.
\end{equation}
\noindent
@@ -863,12 +863,12 @@
\begin{center}
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{thm (lhs) Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ @{thm (lhs) Append_rexp.simps(2)[where X="Y" and r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}
& @{text "\<equiv>"} &
- @{thm (rhs) Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\\
- @{thm (lhs) Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ @{thm (rhs) Append_rexp.simps(2)[where X="Y" and r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}\\
+ @{thm (lhs) Append_rexp.simps(1)[where r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}
& @{text "\<equiv>"} &
- @{thm (rhs) Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ @{thm (rhs) Append_rexp.simps(1)[where r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}
\end{tabular}
\end{center}
@@ -891,22 +891,22 @@
then we calculate the combined regular expressions for all @{text r} coming
from the deleted @{text "(X, r)"}, and take the @{const Star} of it;
finally we append this regular expression to @{text rhs'}. If we apply this
- operation to the right-hand side of @{text "X\<^isub>4"} in \eqref{exmpcs}, we obtain
+ operation to the right-hand side of @{text "X\<^sub>4"} in \eqref{exmpcs}, we obtain
the equation:
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{term "X\<^isub>4"} & @{text "="} &
- @{text "(X\<^isub>1, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
- & & @{text "(X\<^isub>2, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
- & & @{text "(X\<^isub>3, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
- & & @{text "(X\<^isub>3, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b}))"}
+ @{term "X\<^sub>4"} & @{text "="} &
+ @{text "(X\<^sub>1, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+ & & @{text "(X\<^sub>2, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+ & & @{text "(X\<^sub>3, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+ & & @{text "(X\<^sub>3, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b}))"}
\end{tabular}
\end{center}
\noindent
- That means we eliminated the recursive occurrence of @{text "X\<^isub>4"} on the
+ That means we eliminated the recursive occurrence of @{text "X\<^sub>4"} on the
right-hand side.
It can be easily seen that the @{text "Arden"}-operation mimics Arden's
@@ -952,11 +952,11 @@
the substitution operation we will arrange it so that @{text "xrhs"} does not contain
any occurrence of @{text X}. For example substituting the first equation in
\eqref{exmpcs} into the right-hand side of the second, thus eliminating the equivalence
- class @{text "X\<^isub>1"}, gives us the equation
+ class @{text "X\<^sub>1"}, gives us the equation
%
\begin{equation}\label{exmpresult}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{term "X\<^isub>2"} & @{text "="} & @{text "\<lambda>(TIMES ONE (ATOM a))"}
+ @{term "X\<^sub>2"} & @{text "="} & @{text "\<lambda>(TIMES ONE (ATOM a))"}
\end{tabular}}
\end{equation}
@@ -1223,8 +1223,8 @@
\begin{center}
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{text "X\<^isub>2"} & @{text "="} & @{text "TIMES ONE (ATOM a)"}\\
- @{text "X\<^isub>3"} & @{text "="} & @{text "TIMES (TIMES ONE (ATOM a)) (ATOM b)"}
+ @{text "X\<^sub>2"} & @{text "="} & @{text "TIMES ONE (ATOM a)"}\\
+ @{text "X\<^sub>3"} & @{text "="} & @{text "TIMES (TIMES ONE (ATOM a)) (ATOM b)"}
\end{tabular}
\end{center}
@@ -1235,7 +1235,7 @@
calculating a regular expression for the complement of a regular language:
if we combine all regular
expressions corresponding to equivalence classes not in @{term "finals A"}
- (in the running example @{text "X\<^isub>1"} and @{text "X\<^isub>4"}),
+ (in the running example @{text "X\<^sub>1"} and @{text "X\<^sub>4"}),
then we obtain a regular expression for the complement language @{term "- A"}.
This is similar to the usual construction of a `complement automaton'.
@@ -1318,8 +1318,8 @@
R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}.
\begin{definition}
- A relation @{text "R\<^isub>1"} \emph{refines} @{text "R\<^isub>2"}
- provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
+ A relation @{text "R\<^sub>1"} \emph{refines} @{text "R\<^sub>2"}
+ provided @{text "R\<^sub>1 \<subseteq> R\<^sub>2"}.
\end{definition}
\noindent
@@ -1373,9 +1373,9 @@
@{text "\<equiv>"} &
@{thm (rhs) tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]} \\
@{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}\;@{text "x"} & @{text "\<equiv>"} &
- @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}\\
+ @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^sub>p \<in> A \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x})"}\\
@{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>p, x\<^isub>s) \<in> Partitions x}"}
+ @{text "{\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^sub>p < x \<and> x\<^sub>p \<in> A\<^sup>\<star> \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x}"}
\end{tabular}
\caption{Three tagging functions used the cases for @{term "PLUS"}, @{term "TIMES"} and @{term "STAR"}
regular expressions. The sets @{text A} and @{text B} are arbitrary languages instantiated
@@ -1402,27 +1402,27 @@
\end{proof}
\begin{lemma}\label{fintwo}
- Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
- @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
- If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
- then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
+ Given two equivalence relations @{text "R\<^sub>1"} and @{text "R\<^sub>2"}, whereby
+ @{text "R\<^sub>1"} refines @{text "R\<^sub>2"}.
+ If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^sub>1" and ?R2.0="R\<^sub>2"]}
+ then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^sub>1" and ?R2.0="R\<^sub>2"]}.
\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
- @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
+ be @{text "X \<mapsto>"}~@{term "{R\<^sub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
+ @{term "finite (f ` (UNIV // R\<^sub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^sub>1)"},
which must be 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
+ on @{term "UNIV // R\<^sub>2"}. This is equivalent to showing that two equivalence
+ classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^sub>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 \<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"},
- they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
+ @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^sub>2} related.
+ We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^sub>2 `` {x}"}}.
+ From the latter fact we can infer that @{term "R\<^sub>1 ``{x} \<in> f X"}
+ and further @{term "R\<^sub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
+ such that @{term "R\<^sub>1 `` {x} = R\<^sub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
+ are @{text "R\<^sub>1"}-related. Since by assumption @{text "R\<^sub>1"} refines @{text "R\<^sub>2"},
+ they must also be @{text "R\<^sub>2"}-related, as we need to show.\qed
\end{proof}
\noindent
@@ -1450,7 +1450,7 @@
"(\<approx>A `` {x}, \<approx>B `` {x}) = (\<approx>A `` {y}, \<approx>B `` {y})"} holds by assumption. Then
clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"}, as we needed to
show. Finally we can discharge this case by setting @{text A} to @{term
- "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.\qed
+ "lang r\<^sub>1"} and @{text B} to @{term "lang r\<^sub>2"}.\qed
\end{proof}
\noindent
@@ -1475,9 +1475,9 @@
\end{equation}
\noindent
- If we know that @{text "(x\<^isub>p, x\<^isub>s) \<in> Partitions x"}, we will
- refer to @{text "x\<^isub>p"} as the \emph{prefix} of the string @{text x},
- and respectively to @{text "x\<^isub>s"} as the \emph{suffix}.
+ If we know that @{text "(x\<^sub>p, x\<^sub>s) \<in> Partitions x"}, we will
+ refer to @{text "x\<^sub>p"} as the \emph{prefix} of the string @{text x},
+ and respectively to @{text "x\<^sub>s"} as the \emph{suffix}.
*}
@@ -1490,8 +1490,8 @@
\scalebox{1}{
\begin{tikzpicture}[scale=0.8,fill=gray!20]
\node[draw,minimum height=3.8ex, fill] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of x, fill] (za) { $\hspace{0.6em}@{text "z\<^isub>p"}\hspace{0.6em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zza) { $\hspace{2.6em}@{text "z\<^isub>s"}\hspace{2.6em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of x, fill] (za) { $\hspace{0.6em}@{text "z\<^sub>p"}\hspace{0.6em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zza) { $\hspace{2.6em}@{text "z\<^sub>s"}\hspace{2.6em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(x.north west) -- ($(za.north west)+(0em,0em)$)
@@ -1507,17 +1507,17 @@
\draw[decoration={brace,transform={yscale=3}},decorate]
($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{@{text "x @ z\<^isub>p \<in> A"}};
+ node[midway, below=0.5em]{@{text "x @ z\<^sub>p \<in> A"}};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
- node[midway, below=0.5em]{@{text "z\<^isub>s \<in> B"}};
+ node[midway, below=0.5em]{@{text "z\<^sub>s \<in> B"}};
\end{tikzpicture}}
\\[2mm]
\scalebox{1}{
\begin{tikzpicture}[scale=0.8,fill=gray!20]
- \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{3em}@{text "x\<^isub>p"}\hspace{3em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.2em}@{text "x\<^isub>s"}\hspace{0.2em}$ };
+ \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{3em}@{text "x\<^sub>p"}\hspace{3em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.2em}@{text "x\<^sub>s"}\hspace{0.2em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
@@ -1534,11 +1534,11 @@
\draw[decoration={brace,transform={yscale=3}},decorate]
($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> B"}};
+ node[midway, below=0.5em]{@{term "x\<^sub>s @ z \<in> B"}};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{@{term "x\<^isub>p \<in> A"}};
+ node[midway, below=0.5em]{@{term "x\<^sub>p \<in> A"}};
\end{tikzpicture}}
\end{tabular}
\end{center}
@@ -1550,22 +1550,22 @@
(second picture). In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. The first case
we will only go through if we know that @{term "x \<approx>A y"} holds @{text "("}@{text "*"}@{text ")"}.
Because then
- we can infer from @{term "x @ z\<^isub>p \<in> A"} that @{term "y @ z\<^isub>p \<in> A"} holds for all @{text "z\<^isub>p"}.
- In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is one possible partition
- of the string @{text x}. We have to know that both @{text "x\<^isub>p"} and the
- corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related'
- to @{text "y\<^isub>s"} @{text "("}@{text "**"}@{text ")"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
+ we can infer from @{term "x @ z\<^sub>p \<in> A"} that @{term "y @ z\<^sub>p \<in> A"} holds for all @{text "z\<^sub>p"}.
+ In the second case we only know that @{text "x\<^sub>p"} and @{text "x\<^sub>s"} is one possible partition
+ of the string @{text x}. We have to know that both @{text "x\<^sub>p"} and the
+ corresponding partition @{text "y\<^sub>p"} are in @{text "A"}, and that @{text "x\<^sub>s"} is `@{text B}-related'
+ to @{text "y\<^sub>s"} @{text "("}@{text "**"}@{text ")"}. From the latter fact we can infer that @{text "y\<^sub>s @ z \<in> B"}.
This will solve the second case.
Taking the two requirements, @{text "("}@{text "*"}@{text ")"} and @{text "(**)"}, together we define the
tagging-function in the @{const Times}-case as (see Fig.~\ref{tagfig}):
\begin{center}
@{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}\;@{text "x"}~@{text "\<equiv>"}~
- @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}
+ @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^sub>p \<in> A \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x})"}
\end{center}
\noindent
- Note that we have to make the assumption for all suffixes @{text "x\<^isub>s"}, since we do
+ Note that we have to make the assumption for all suffixes @{text "x\<^sub>s"}, since we do
not know anything about how the string @{term x} is partitioned.
With this definition in place, let us prove the @{const "Times"}-case.
@@ -1583,36 +1583,36 @@
\noindent
and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot>
B"}. As shown in the pictures above, there are two cases to be
- considered. First, there exists a @{text "z\<^isub>p"} and @{text
- "z\<^isub>s"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s
+ considered. First, there exists a @{text "z\<^sub>p"} and @{text
+ "z\<^sub>s"} such that @{term "x @ z\<^sub>p \<in> A"} and @{text "z\<^sub>s
\<in> B"}. 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"}. Hence by the Myhill-Nerode
- Relation @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"},
+ Relation @{term "y @ z\<^sub>p \<in> A"} holds. Using @{text "z\<^sub>s \<in> B"},
we can conclude in this case with @{term "y @ z \<in> A \<cdot> B"} (recall @{text
- "z\<^isub>p @ z\<^isub>s = z"}).
+ "z\<^sub>p @ z\<^sub>s = z"}).
- Second there exists a partition @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with
- @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have
+ Second there exists a partition @{text "x\<^sub>p"} and @{text "x\<^sub>s"} with
+ @{text "x\<^sub>p \<in> A"} and @{text "x\<^sub>s @ z \<in> B"}. We therefore have
\begin{center}
- @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
+ @{text "\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^sub>p \<in> A \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x}"}
\end{center}
\noindent
and by the assumption about @{term "tag_Times A B"} also
\begin{center}
- @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | y\<^isub>p \<in> A \<and> (y\<^isub>p, y\<^isub>s) \<in> Partitions y}"}
+ @{text "\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>y\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | y\<^sub>p \<in> A \<and> (y\<^sub>p, y\<^sub>s) \<in> Partitions y}"}
\end{center}
\noindent
- This means there must be a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"}
- such that @{term "y\<^isub>p \<in> A"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``
- {y\<^isub>s}"}. Unfolding the Myhill-Nerode Relation and together with the
- facts that @{text "x\<^isub>p \<in> A"} and \mbox{@{text "x\<^isub>s @ z \<in> B"}}, we
- obtain @{term "y\<^isub>p \<in> A"} and @{text "y\<^isub>s @ z \<in> B"}, as needed in
+ This means there must be a partition @{text "y\<^sub>p"} and @{text "y\<^sub>s"}
+ such that @{term "y\<^sub>p \<in> A"} and @{term "\<approx>B `` {x\<^sub>s} = \<approx>B ``
+ {y\<^sub>s}"}. Unfolding the Myhill-Nerode Relation and together with the
+ facts that @{text "x\<^sub>p \<in> A"} and \mbox{@{text "x\<^sub>s @ z \<in> B"}}, we
+ obtain @{term "y\<^sub>p \<in> A"} and @{text "y\<^sub>s @ z \<in> B"}, as needed in
this case. 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"}.\qed
+ A} to @{term "lang r\<^sub>1"} and @{text B} to @{term "lang r\<^sub>2"}.\qed
\end{proof}
\noindent
@@ -1635,8 +1635,8 @@
\begin{tikzpicture}[scale=0.8,fill=gray!20]
\node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{4em}@{text "x\<^bsub>pmax\<^esub>"}\hspace{4em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.5em}@{text "x\<^bsub>s\<^esub>"}\hspace{0.5em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
- \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (za) { $\hspace{2em}@{text "z\<^sub>a"}\hspace{2em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zb) { $\hspace{7em}@{text "z\<^sub>b"}\hspace{7em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
@@ -1652,46 +1652,46 @@
\draw[decoration={brace,transform={yscale=3}},decorate]
($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{@{term "x\<^isub>s @ z\<^isub>a \<in> A"}};
+ node[midway, below=0.5em]{@{term "x\<^sub>s @ z\<^sub>a \<in> A"}};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"}};
+ node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<^sup>\<star>"}};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
- node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
+ node[midway, below=0.5em]{@{term "z\<^sub>b \<in> A\<star>"}};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
- node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> A\<star>"}};
+ node[midway, below=0.5em]{@{term "x\<^sub>s @ z \<in> A\<star>"}};
\end{tikzpicture}}
\end{center}
%
\noindent
- We can find a strict prefix @{text "x\<^isub>p"} of @{text x} such that @{term "x\<^isub>p \<in> A\<star>"},
- @{text "x\<^isub>p < x"} and the rest @{term "x\<^isub>s @ z \<in> A\<star>"}. For example the empty string
+ We can find a strict prefix @{text "x\<^sub>p"} of @{text x} such that @{term "x\<^sub>p \<in> A\<star>"},
+ @{text "x\<^sub>p < x"} and the rest @{term "x\<^sub>s @ z \<in> A\<star>"}. For example the empty string
@{text "[]"} would do (recall @{term "x \<noteq> []"}).
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\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we
+ @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^sub>s @ z"} we
know it is in @{term "A\<star>"} and cannot be the empty string. By Property~\ref{langprops}@{text "(iv)"},
we can separate
this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<noteq> []"}, @{text "a \<in> A"}
- and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},
+ and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^sub>s"},
otherwise @{text "x\<^bsub>pmax\<^esub>"} 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\<^isub>s @ z\<^isub>a \<in> A"} and
- @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
+ `overlaps' with @{text z}, splitting it into two components @{text "z\<^sub>a"} and
+ @{text "z\<^sub>b"}. For this we know that @{text "x\<^sub>s @ z\<^sub>a \<in> A"} and
+ @{term "z\<^sub>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\<^isub>s @ z\<^isub>a"}.
+ `border' of @{text x} and @{text z}. This string is @{text "x\<^sub>s @ z\<^sub>a"}.
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>p, x\<^isub>s) \<in> Partitions x}"}
+ @{text "{\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^sub>p < x \<and> x\<^sub>p \<in> A\<^sup>\<star> \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x}"}
\end{center}
\begin{proof}[@{const Star}-Case]
@@ -1706,26 +1706,26 @@
can infer @{text y} is the empty string and
then 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 and the facts @{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"} and @{text "x\<^bsub>pmax\<^esub> < x"},
+ above. By the tagging-function and the facts @{text "x\<^bsub>pmax\<^esub> \<in> A\<^sup>\<star>"} and @{text "x\<^bsub>pmax\<^esub> < x"},
we have
\begin{center}
- @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^bsub>pmax\<^esub> < x \<and> x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star> \<and> (x\<^bsub>pmax\<^esub>, x\<^isub>s) \<in> Partitions x}"}
+ @{text "\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^bsub>pmax\<^esub> < x \<and> x\<^bsub>pmax\<^esub> \<in> A\<^sup>\<star> \<and> (x\<^bsub>pmax\<^esub>, x\<^sub>s) \<in> Partitions x}"}
\end{center}
\noindent
which by assumption is equal to
\begin{center}
- @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | y\<^bsub>p\<^esub> < y \<and> y\<^bsub>p\<^esub> \<in> A\<^isup>\<star> \<and> (y\<^bsub>p\<^esub>, y\<^isub>s) \<in> Partitions y}"}
+ @{text "\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>y\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | y\<^bsub>p\<^esub> < y \<and> y\<^bsub>p\<^esub> \<in> A\<^sup>\<star> \<and> (y\<^bsub>p\<^esub>, y\<^sub>s) \<in> Partitions y}"}
\end{center}
\noindent
- From this we know there exist a partition @{text "y\<^isub>p"} and @{text
- "y\<^isub>s"} with @{term "y\<^isub>p \<in> A\<star>"} and also @{term "x\<^isub>s \<approx>A
- y\<^isub>s"}. Unfolding the Myhill-Nerode Relation we know @{term
- "y\<^isub>s @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
- Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \<in>
+ From this we know there exist a partition @{text "y\<^sub>p"} and @{text
+ "y\<^sub>s"} with @{term "y\<^sub>p \<in> A\<star>"} and also @{term "x\<^sub>s \<approx>A
+ y\<^sub>s"}. Unfolding the Myhill-Nerode Relation we know @{term
+ "y\<^sub>s @ z\<^sub>a \<in> A"}. We also know that @{term "z\<^sub>b \<in> A\<star>"}.
+ Therefore @{term "y\<^sub>p @ (y\<^sub>s @ z\<^sub>a) @ z\<^sub>b \<in>
A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. The last step is to set
@{text "A"} to @{term "lang r"} and thus complete the proof.\qed
\end{proof}
@@ -1775,7 +1775,7 @@
component is accepting and at least one state in the set is also accepting.
The idea behind the @{text "STAR"}-case is similar to the @{text "TIMES"}-case.
- We assume some automaton has consumed some strictly smaller part of the input in @{text "A\<^isup>\<star>"};
+ We assume some automaton has consumed some strictly smaller part of the input in @{text "A\<^sup>\<star>"};
we need to check that from the state we ended up in a terminal state in the
automaton @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>"} can be reached. Since we do not know from which state this will
succeed, we need to run the automaton from all possible states we could have
@@ -1840,8 +1840,8 @@
@{thm (lhs) Deriv_star} & $=$ & @{thm (rhs) Deriv_star}\\
@{thm (lhs) Derivs_simps(1)} & $=$ & @{thm (rhs) Derivs_simps(1)}\\
@{thm (lhs) Derivs_simps(2)} & $=$ & @{thm (rhs) Derivs_simps(2)}\\
- %@{thm (lhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
- % & @{thm (rhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
+ %@{thm (lhs) Derivs_simps(3)[where ?s1.0="s\<^sub>1" and ?s2.0="s\<^sub>2"]} & $=$
+ % & @{thm (rhs) Derivs_simps(3)[where ?s1.0="s\<^sub>1" and ?s2.0="s\<^sub>2"]}\\
\end{tabular}}
\end{equation}
@@ -1863,13 +1863,13 @@
@{thm (lhs) deriv.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(1)}\\
@{thm (lhs) deriv.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(2)}\\
@{thm (lhs) deriv.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(3)[where c'="d"]}\\
- @{thm (lhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm (lhs) deriv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
- @{term "Plus (Times (deriv c r\<^isub>1) r\<^isub>2) (deriv c r\<^isub>2)"}\\
- & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
- @{term "Times (deriv c r\<^isub>1) r\<^isub>2"}\\
+ @{thm (lhs) deriv.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}
+ & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+ @{thm (lhs) deriv.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}
+ & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^sub>1"}~@{text "then"}~%
+ @{term "Plus (Times (deriv c r\<^sub>1) r\<^sub>2) (deriv c r\<^sub>2)"}\\
+ & & \phantom{@{text "if"}~@{term "nullable r\<^sub>1"}~}@{text "else"}~%
+ @{term "Times (deriv c r\<^sub>1) r\<^sub>2"}\\
@{thm (lhs) deriv.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(6)}\smallskip\\
@{thm (lhs) derivs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(1)}\\
@{thm (lhs) derivs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(2)}
@@ -1887,10 +1887,10 @@
@{thm (lhs) nullable.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(1)}\\
@{thm (lhs) nullable.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(2)}\\
@{thm (lhs) nullable.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(3)}\\
- @{thm (lhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm (lhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm (lhs) nullable.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}
+ & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+ @{thm (lhs) nullable.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}
+ & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
@{thm (lhs) nullable.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(6)}
\end{longtable}
\end{center}
@@ -1935,8 +1935,8 @@
ensuring that there are only finitely many equivalence
classes. Unfortunately, this is not true in general. Sakarovitch gives an
example where a regular expression has infinitely many derivatives
- w.r.t.~the language @{text "(ab)\<^isup>\<star> \<union> (ab)\<^isup>\<star>a"}, which is formally
- written in our notation as \mbox{@{text "{[a,b]}\<^isup>\<star> \<union> ({[a,b]}\<^isup>\<star> \<cdot> {[a]})"}}
+ w.r.t.~the language @{text "(ab)\<^sup>\<star> \<union> (ab)\<^sup>\<star>a"}, which is formally
+ written in our notation as \mbox{@{text "{[a,b]}\<^sup>\<star> \<union> ({[a,b]}\<^sup>\<star> \<cdot> {[a]})"}}
(see \cite[Page~141]{Sakarovitch09}).
@@ -1947,8 +1947,8 @@
%
\begin{equation}\label{ACI}
\mbox{\begin{tabular}{cl}
- (@{text A}) & @{term "Plus (Plus r\<^isub>1 r\<^isub>2) r\<^isub>3"} $\equiv$ @{term "Plus r\<^isub>1 (Plus r\<^isub>2 r\<^isub>3)"}\\
- (@{text C}) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
+ (@{text A}) & @{term "Plus (Plus r\<^sub>1 r\<^sub>2) r\<^sub>3"} $\equiv$ @{term "Plus r\<^sub>1 (Plus r\<^sub>2 r\<^sub>3)"}\\
+ (@{text C}) & @{term "Plus r\<^sub>1 r\<^sub>2"} $\equiv$ @{term "Plus r\<^sub>2 r\<^sub>1"}\\
(@{text I}) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
\end{tabular}}
\end{equation}
@@ -1969,13 +1969,13 @@
@{thm (lhs) pderiv.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(1)}\\
@{thm (lhs) pderiv.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(2)}\\
@{thm (lhs) pderiv.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(3)[where c'="d"]}\\
- @{thm (lhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm (lhs) pderiv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
- @{term "(Timess (pderiv c r\<^isub>1) r\<^isub>2) \<union> (pderiv c r\<^isub>2)"}\\
- & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
- @{term "Timess (pderiv c r\<^isub>1) r\<^isub>2"}\\
+ @{thm (lhs) pderiv.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}
+ & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+ @{thm (lhs) pderiv.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}
+ & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^sub>1"}~@{text "then"}~%
+ @{term "(Timess (pderiv c r\<^sub>1) r\<^sub>2) \<union> (pderiv c r\<^sub>2)"}\\
+ & & \phantom{@{text "if"}~@{term "nullable r\<^sub>1"}~}@{text "else"}~%
+ @{term "Timess (pderiv c r\<^sub>1) r\<^sub>2"}\\
@{thm (lhs) pderiv.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(6)}\smallskip\\
@{thm (lhs) pderivs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(1)}\\
@{thm (lhs) pderivs.simps(2)} & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}
@@ -2093,8 +2093,8 @@
@{thm pderivs_lang_Zero}\\
@{thm pderivs_lang_One}\\
@{thm pderivs_lang_Atom}\\
- @{thm pderivs_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm pderivs_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm pderivs_lang_Plus[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+ @{thm pderivs_lang_Times[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
@{thm pderivs_lang_Star}\\
\end{tabular}}
\end{equation}
@@ -2168,12 +2168,12 @@
proved using both parts of 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"}
+ @{term "s\<^sub>1 \<approx>A s\<^sub>2"} if and only if @{term "s\<^sub>1 \<approx>(-A) s\<^sub>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"}
+ holds for any strings @{text "s\<^sub>1"} and @{text
+ "s\<^sub>2"}. Therefore @{text A} and the complement language @{term "-A"}
give rise to the same partitions. So if one is finite, the other is too, and
vice versa. As noted earlier, our algorithm for solving equational systems
actually calculates a regular expression for the complement language.
@@ -2213,10 +2213,10 @@
%@{thm (lhs) Rev.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(1)}\\
%@{thm (lhs) Rev.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(2)}\\
%@{thm (lhs) Rev.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(3)}\\
- %@{thm (lhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
- % @{thm (rhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- %@{thm (lhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
- % @{thm (rhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ %@{thm (lhs) Rev.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]} & @{text "\<equiv>"} &
+ % @{thm (rhs) Rev.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+ %@{thm (lhs) Rev.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]} & @{text "\<equiv>"} &
+ % @{thm (rhs) Rev.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
%@{thm (lhs) Rev.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(6)}\\
%\end{tabular}
%\end{center}
@@ -2344,10 +2344,10 @@
@{thm (lhs) UP.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(1)}\\
@{thm (lhs) UP.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(2)}\\
@{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(3)}\\
- @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} &
- @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} &
- @{text "\<equiv>"} & @{thm (rhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]} &
+ @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+ @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]} &
+ @{text "\<equiv>"} & @{thm (rhs) UP.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
@{thm (lhs) UP.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(6)}
\end{tabular}
\end{center}
@@ -2437,9 +2437,9 @@
they need to be related by the Myhill-Nerode Relation.
Using this lemma, it is straightforward to establish that the language
- \mbox{@{text "A \<equiv> \<Union>\<^isub>n a\<^sup>n @ b\<^sup>n"}} is not regular (@{text "a\<^sup>n"} stands
+ \mbox{@{text "A \<equiv> \<Union>\<^sub>n a\<^sup>n @ b\<^sup>n"}} is not regular (@{text "a\<^sup>n"} stands
for the strings consisting of @{text n} times the character a; similarly for
- @{text "b\<^isup>n"}). For this consider the infinite set @{text "B \<equiv> \<Union>\<^isub>n a\<^sup>n"}.
+ @{text "b\<^sup>n"}). For this consider the infinite set @{text "B \<equiv> \<Union>\<^sub>n a\<^sup>n"}.
\begin{lemma}
No two distinct strings in set @{text "B"} are Myhill-Nerode related by language @{text A}.