--- a/Derivatives.thy Wed Aug 03 17:08:31 2011 +0000
+++ b/Derivatives.thy Fri Aug 05 05:34:11 2011 +0000
@@ -21,35 +21,15 @@
where
"Ders s A \<equiv> {s'. s @ s' \<in> A}"
-definition
- Ders_set :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where
- "Ders_set A B \<equiv> {s' | s s'. s @ s' \<in> B \<and> s \<in> A}"
-
-lemma Ders_set_Ders:
- shows "Ders_set A B = (\<Union>s \<in> A. Ders s B)"
-unfolding Ders_set_def Ders_def
-by auto
-
-lemma Der_zero [simp]:
- shows "Der c {} = {}"
-unfolding Der_def
-by auto
+abbreviation
+ "Derss s A \<equiv> \<Union> (Ders s) ` A"
-lemma Der_one [simp]:
- shows "Der c {[]} = {}"
-unfolding Der_def
-by auto
-
-lemma Der_atom [simp]:
- shows "Der c {[d]} = (if c = d then {[]} else {})"
-unfolding Der_def
-by auto
-
-lemma Der_union [simp]:
- shows "Der c (A \<union> B) = Der c A \<union> Der c B"
-unfolding Der_def
-by auto
+lemma Der_simps [simp]:
+ shows "Der c {} = {}"
+ and "Der c {[]} = {}"
+ and "Der c {[d]} = (if c = d then {[]} else {})"
+ and "Der c (A \<union> B) = Der c A \<union> Der c B"
+unfolding Der_def by auto
lemma Der_conc [simp]:
shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)"
@@ -60,7 +40,7 @@
shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"
proof -
have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"
- unfolding Der_def Delta_def
+ unfolding Der_def Delta_def conc_def
apply(auto)
apply(drule star_decom)
apply(auto simp add: Cons_eq_append_conv)
@@ -69,7 +49,7 @@
have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})"
by (simp only: star_unfold_left[symmetric])
also have "... = Der c (A \<cdot> A\<star>)"
- by (simp only: Der_union Der_one) (simp)
+ by (simp only: Der_simps) (simp)
also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
by simp
also have "... = (Der c A) \<cdot> A\<star>"
@@ -77,19 +57,12 @@
finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" .
qed
-lemma Ders_nil [simp]:
+lemma Ders_simps [simp]:
shows "Ders [] A = A"
-unfolding Ders_def by simp
-
-lemma Ders_cons [simp]:
- shows "Ders (c # s) A = Ders s (Der c A)"
+ and "Ders (c # s) A = Ders s (Der c A)"
+ and "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
unfolding Ders_def Der_def by auto
-lemma Ders_append [simp]:
- shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
-unfolding Ders_def by simp
-
-
subsection {* Brozowsky's derivatives of regular expressions *}
fun
@@ -137,7 +110,7 @@
subsection {* Antimirov's Partial Derivatives *}
abbreviation
- "Times_set rs r \<equiv> {Times r' r | r'. r' \<in> rs}"
+ "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}"
fun
pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
@@ -147,11 +120,11 @@
| "pder c (Atom c') = (if c = c' then {One} else {Zero})"
| "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"
| "pder c (Times r1 r2) =
- (if nullable r1 then Times_set (pder c r1) r2 \<union> pder c r2 else Times_set (pder c r1) r2)"
-| "pder c (Star r) = Times_set (pder c r) (Star r)"
+ (if nullable r1 then Timess (pder c r1) r2 \<union> pder c r2 else Timess (pder c r1) r2)"
+| "pder c (Star r) = Timess (pder c r) (Star r)"
abbreviation
- "pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r"
+ "pder_set c rs \<equiv> \<Union> pder c ` rs"
fun
pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
@@ -160,7 +133,7 @@
| "pders (c # s) r = \<Union> (pders s) ` (pder c r)"
abbreviation
- "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
+ "pderss s A \<equiv> \<Union> (pders s) ` A"
lemma pders_append:
"pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
@@ -170,85 +143,113 @@
shows "pders (s @ [c]) r = pder_set c (pders s r)"
by (simp add: pders_append)
-lemma pders_set_lang:
- shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))"
-unfolding image_def
-by auto
-
-lemma pders_Zero [simp]:
+lemma pders_simps [simp]:
shows "pders s Zero = {Zero}"
-by (induct s) (simp_all)
-
-lemma pders_One [simp]:
- shows "pders s One = (if s = [] then {One} else {Zero})"
+ and "pders s One = (if s = [] then {One} else {Zero})"
+ and "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
+ and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
by (induct s) (auto)
-lemma pders_Atom [simp]:
- shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
-by (induct s) (auto)
+subsection {* Relating left-quotients and partial derivatives *}
+
+lemma Der_pder:
+ shows "Der c (lang r) = \<Union> lang ` (pder c r)"
+by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib)
-lemma pders_Plus [simp]:
- shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
-by (induct s) (auto)
+lemma Ders_pders:
+ shows "Ders s (lang r) = \<Union> lang ` (pders s r)"
+proof (induct s arbitrary: r)
+ case (Cons c s)
+ have ih: "\<And>r. Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
+ have "Ders (c # s) (lang r) = Ders s (Der c (lang r))" by simp
+ also have "\<dots> = Ders s (\<Union> lang ` (pder c r))" by (simp add: Der_pder)
+ also have "\<dots> = Derss s (lang ` (pder c r))"
+ by (auto simp add: Ders_def)
+ also have "\<dots> = \<Union> lang ` (pderss s (pder c r))"
+ using ih by auto
+ also have "\<dots> = \<Union> lang ` (pders (c # s) r)" by simp
+ finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" .
+qed (simp add: Ders_def)
+
+subsection {* Relating derivatives and partial derivatives *}
+
+lemma
+ shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
+unfolding Der_der[symmetric] Der_pder by simp
+
+lemma
+ shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
+unfolding Ders_ders[symmetric] Ders_pders by simp
+
+
+subsection {* There are only finitely many partial derivatives for a language *}
+
+abbreviation
+ "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
text {* Non-empty suffixes of a string *}
definition
"Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
-lemma Suf:
+lemma Suf_snoc:
shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}"
unfolding Suf_def conc_def
by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
lemma Suf_Union:
- shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"
+ shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
by (auto simp add: conc_def)
+lemma pders_set_snoc:
+ shows "pders_set (Suf s \<cdot> {[c]}) r = (pder_set c (pders_set (Suf s) r))"
+by (simp add: Suf_Union pders_snoc)
+
lemma pders_Times:
- shows "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
+ shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)"
proof (induct s rule: rev_induct)
case (snoc c s)
- have ih: "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
+ have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)"
by fact
have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))"
by (simp add: pders_snoc)
- also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
+ also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2))"
using ih by (auto) (blast)
- also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
- by (simp)
- also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"
+ also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_set (Suf s) r2)"
by (simp)
- also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
- by (auto simp add: pders_snoc)
- also have "\<dots> \<subseteq> Times_set (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
- by (auto simp add: if_splits) (blast)
- also have "\<dots> = Times_set (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"
- by (auto simp add: pders_snoc Suf Suf_Union)
+ also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_set (Suf s \<cdot> {[c]}) r2"
+ by (simp add: pders_set_snoc)
+ also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2"
+ by auto
+ also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2"
+ by (auto simp add: if_splits pders_snoc) (blast)
+ also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_set (Suf (s @ [c])) r2"
+ by (auto simp add: Suf_snoc)
finally show ?case .
-qed (simp)
+qed (simp)
+
lemma pders_Star:
assumes a: "s \<noteq> []"
- shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Times_set (pders v r) (Star r))"
+ shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Timess (pders v r) (Star r))"
using a
proof (induct s rule: rev_induct)
case (snoc c s)
- have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r))" by fact
+ have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Timess (pders v r) (Star r))" by fact
{ assume asm: "s \<noteq> []"
have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)
- also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r)))"
- using ih[OF asm] by blast
- also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Times_set (pders v r) (Star r)))"
+ also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Timess (pders v r) (Star r)))"
+ using ih[OF asm] by (auto) (blast)
+ also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Timess (pders v r) (Star r)))"
by simp
- also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"
+ also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"
by (auto split: if_splits)
- also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
+ also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
using asm by (auto simp add: Suf_def)
- also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \<union> (Times_set (pder c r) (Star r))"
+ also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pders (v @ [c]) r) (Star r))) \<union> (Timess (pder c r) (Star r))"
by (simp add: pders_snoc)
- also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))"
- by (auto simp add: Suf Suf_Union pders_snoc)
+ also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Timess (pders v r) (Star r)))"
+ by (auto simp add: Suf_snoc Suf_Union pders_snoc)
finally have ?case .
}
moreover
@@ -284,7 +285,7 @@
using a unfolding UNIV1_def Suf_def by (auto)
lemma pders_set_Times:
- shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Times_set (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
+ shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Timess (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
unfolding UNIV1_def
apply(rule UN_least)
apply(rule subset_trans)
@@ -298,7 +299,7 @@
done
lemma pders_set_Star:
- shows "pders_set UNIV1 (Star r) \<subseteq> Times_set (pders_set UNIV1 r) (Star r)"
+ shows "pders_set UNIV1 (Star r) \<subseteq> Timess (pders_set UNIV1 r) (Star r)"
unfolding UNIV1_def
apply(rule UN_least)
apply(rule subset_trans)
@@ -308,9 +309,9 @@
apply(auto)
done
-lemma finite_Times_set:
+lemma finite_Timess:
assumes a: "finite A"
- shows "finite (Times_set A r)"
+ shows "finite (Timess A r)"
using a by (auto)
lemma finite_pders_set_UNIV1:
@@ -326,11 +327,11 @@
apply(simp)
apply(rule finite_subset)
apply(rule pders_set_Times)
-apply(simp only: finite_Times_set finite_Un)
+apply(simp only: finite_Timess finite_Un)
apply(simp)
apply(rule finite_subset)
apply(rule pders_set_Star)
-apply(simp only: finite_Times_set)
+apply(simp only: finite_Timess)
done
lemma pders_set_UNIV_UNIV1:
@@ -371,48 +372,6 @@
qed
-subsection {* Relating left-quotients and partial derivatives *}
-
-lemma Der_pder:
- shows "Der c (lang r) = \<Union> lang ` (pder c r)"
-by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib)
-
-lemma Ders_pders:
- shows "Ders s (lang r) = \<Union> lang ` (pders s r)"
-proof (induct s rule: rev_induct)
- case (snoc c s)
- have ih: "Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
- have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))"
- by (simp add: Ders_append)
- also have "\<dots> = Der c (\<Union> lang ` (pders s r))" using ih
- by (simp)
- also have "\<dots> = (\<Union>r\<in>pders s r. Der c (lang r))"
- unfolding Der_def image_def by auto
- also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> lang ` (pder c r)))"
- by (simp add: Der_pder)
- also have "\<dots> = (\<Union>lang ` (pder_set c (pders s r)))"
- by (simp add: pders_set_lang)
- also have "\<dots> = (\<Union>lang ` (pders (s @ [c]) r))"
- by (simp add: pders_snoc)
- finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .
-qed (simp add: Ders_def)
-
-lemma Ders_set_pders_set:
- shows "Ders_set A (lang r) = (\<Union> lang ` (pders_set A r))"
-by (simp add: Ders_set_Ders Ders_pders)
-
-
-subsection {* Relating derivatives and partial derivatives *}
-
-lemma
- shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
-unfolding Der_der[symmetric] Der_pder by simp
-
-lemma
- shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
-unfolding Ders_ders[symmetric] Ders_pders by simp
-
-
text {* Relating the Myhill-Nerode relation with left-quotients. *}
lemma MN_Rel_Ders:
--- a/Journal/Paper.thy Wed Aug 03 17:08:31 2011 +0000
+++ b/Journal/Paper.thy Fri Aug 05 05:34:11 2011 +0000
@@ -34,7 +34,7 @@
abbreviation "ATOM \<equiv> Atom"
abbreviation "PLUS \<equiv> Plus"
abbreviation "TIMES \<equiv> Times"
-abbreviation "TIMESS \<equiv> Times_set"
+abbreviation "TIMESS \<equiv> Timess"
abbreviation "STAR \<equiv> Star"
@@ -143,19 +143,18 @@
wide range of textbooks on this subject, many of which are aimed at students
and contain very detailed `pencil-and-paper' proofs (e.g.~\cite{Kozen97,
HopcroftUllman69}). It seems natural to exercise theorem provers by
- formalising the theorems and by verifying formally the algorithms. A
- popular choice for a theorem prover would be one based on Higher-Order Logic
- (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development
+ formalising the theorems and by verifying formally the algorithms.
+
+ A popular choice for a theorem prover would be one based on Higher-Order
+ Logic (HOL), for example HOL4, HOLlight or Isabelle/HOL. For the development
presented in this paper we will use the latter. HOL is a predicate calculus
that allows quantification over predicate variables. Its type system is
- based on Church's Simple Theory of Types \cite{Church40}. Although
- many mathematical concepts can be conveniently expressed in HOL, there are some
+ based on Church's Simple Theory of Types \cite{Church40}. Although many
+ mathematical concepts can be conveniently expressed in HOL, there are some
limitations that hurt badly, if one attempts a simple-minded formalisation
- of regular languages in it.
-
- The typical approach to regular languages is to introduce finite automata
- and then define everything in terms of them \cite{Kozen97}. For example,
- a regular language is normally defined as:
+ of regular languages in it. The typical approach to regular languages is to
+ introduce finite automata and then define everything in terms of them
+ \cite{Kozen97}. For example, a regular language is normally defined as:
\begin{dfntn}\label{baddef}
A language @{text A} is \emph{regular}, provided there is a
@@ -252,7 +251,8 @@
language as one for which there exists an automaton that recognises all its
strings. This is because we cannot make a definition in HOL that is polymorphic in
the state type and there is no type quantification available in HOL (unlike
- in Coq, for example).
+ in Coq, for example).\footnote{Slind already pointed out this problem in an email
+ to the HOL4 mailing list on 21st April 2005.}
An alternative, which provides us with a single type for automata, is to give every
state node an identity, for example a natural
@@ -266,8 +266,8 @@
problems as with graphs. Composing, for example, two non-deterministic automata in parallel
requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
dismisses for this the option of using identities, because it leads according to
- him to ``messy proofs''. Since he does not need to define what a regular
- language is, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes
+ him to ``messy proofs''. Since he does not need to define what regular
+ languages are, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes
\begin{quote}
\it%
@@ -317,7 +317,7 @@
of automata \cite{Brzozowski10}). Such side-conditions mean that if we define a regular
language as one for which there exists \emph{a} finite automaton that
recognises all its strings (see Def.~\ref{baddef}), then we need a lemma which
- ensures that another equivalent can be found satisfying the
+ ensures that another equivalent one can be found satisfying the
side-condition. Unfortunately, such `little' and `obvious' lemmas make
a formalisation of automata theory a hair-pulling experience.
@@ -360,11 +360,12 @@
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
- widely in the literature about regular expressions. However, partial
- derivatives are more suitable in the context of the Myhill-Nerode theorem,
- since it is easier to establish formally their finiteness result.
-
+ theorem. Derivatives of regular expressions have been used recently quite
+ widely in the literature; partial derivatives, in contrast, attracted much
+ less attention. However, partial derivatives are more suitable in the
+ context of the Myhill-Nerode theorem, since it is easier to establish
+ formally their finiteness result. We have not found any proof that uses
+ either of them in order to prove the Myhill-Nerode theorem.
*}
section {* Preliminaries *}
@@ -398,10 +399,13 @@
we will make use of the following properties of these constructions.
\begin{prpstn}\label{langprops}\mbox{}\\
- \begin{tabular}{@ {}ll}
+ \begin{tabular}{@ {}lp{10cm}}
(i) & @{thm star_unfold_left} \\
(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 @{term "x\<^isub>p \<noteq> []"} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.
\end{tabular}
\end{prpstn}
@@ -1167,8 +1171,8 @@
\noindent
that means we take the image of @{text f} w.r.t.~all elements in the
domain. 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-relations are more refined than
+ as relations, give rise to finitely many equivalence classes.
+ Finally we will show that the tagging-relations are more refined than
@{term "\<approx>(lang r)"}, which implies that @{term "UNIV // \<approx>(lang r)"} must
also be finite. We formally define the notion of a \emph{tagging-relation}
as follows.
@@ -1249,7 +1253,7 @@
is that we need to establish that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}.
This amounts to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
@{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. As we shall see, this definition will
- provide us just the right assumptions in order to get the proof through.
+ provide us with just the right assumptions in order to get the proof through.
\begin{proof}[@{const "PLUS"}-Case]
We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite
@@ -1264,7 +1268,7 @@
\noindent
The @{const TIMES}-case is slightly more complicated. We first prove the
- following lemma, which will aid the refinement-proofs.
+ following lemma, which will aid the proof about refinement.
\begin{lmm}\label{refinement}
The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\<approx>A"}, provided for
@@ -1274,15 +1278,21 @@
\noindent
- We therefore can clean information from how the strings @{text "x @ z"} are in @{text A}
- and construct appropriate tagging-functions to infer that @{term "y @ z \<in> A"}.
- For the @{const Times}-case we additionally need the notion of the set of all
- possible partitions of a string
+ We therefore can analyse how the strings @{text "x @ z"} are in the language
+ @{text A} and then construct an appropriate tagging-function to infer that
+ @{term "y @ z"} are also in @{text A}. For this we sill need the notion of
+ the set of all possible \emph{partitions} of a string
\begin{equation}
@{thm Partitions_def}
\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},
+ respectively to @{text "x\<^isub>s"} as the \emph{suffix}.
+
+
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"}:
%
@@ -1350,12 +1360,13 @@
(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 "(*)"}. 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 a possible partition
- of the string @{text x}. So we have to know that both @{text "x\<^isub>p"} and the
+ 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 "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
+ This will solve the second case.
Taking the two requirements, @{text "(*)"} and @{text "(**)"}, together we define the
- tagging-function as:
+ tagging-function in the @{const Times}-case as:
\begin{center}
@{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~
@@ -1363,27 +1374,32 @@
\end{center}
\noindent
- With this definition in place, we can discharge the @{const "Times"}-case as follows.
+ We have to make the assumption for all suffixes @{text "x\<^isub>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.
\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_Times A B"} is a subset of this product set, and therefore finite.
- By Lemma \ref{refinement} we know
+ For the refinement of @{term "\<approx>(A \<cdot> B)"} and @{text "\<^raw:$\threesim$>\<^bsub>\<times>tag A B\<^esub>"},
+ we have by Lemma \ref{refinement}
\begin{center}
@{term "tag_Times A B x = tag_Times A B y"}
\end{center}
\noindent
- and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot> B"}. As shown
- above, there are two cases to be considered (see pictures above). 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 \<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"}. Which means by the Myhill-Nerode
- relation that @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"}, we can conclude in this case
- with @{term "y @ z \<in> A \<cdot> B"}.
+ 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
+ \<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"},
+ we can conclude in this case with @{term "y @ z \<in> A \<cdot> B"} (recall @{text
+ "z\<^isub>p @ z\<^isub>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
@@ -1403,7 +1419,7 @@
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 @{text "x\<^isub>s @ z \<in> B"}, we
+ 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 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"}.
@@ -1411,7 +1427,7 @@
\noindent
The case for @{const Star} is similar to @{const TIMES}, but poses a few
- extra challenges. To deal with them we define first the notion of a \emph{string
+ extra challenges. To deal with them, we define first the notion of a \emph{string
prefix} and a \emph{strict string prefix}:
\begin{center}
@@ -1421,8 +1437,7 @@
\end{tabular}
\end{center}
- \noindent
- When we analyse the case of @{text "x @ z"} being an element in @{term "A\<star>"}
+ When analysing the case of @{text "x @ z"} being an element in @{term "A\<star>"}
and @{text x} is not the empty string, we have the following picture:
\begin{center}
@@ -1466,13 +1481,13 @@
\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
- @{text "[]"} would do.
+ @{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
- know it is in @{term "A\<star>"} and it is not the empty string. By Prop.~\ref{langprops}@{text "(i)"},
+ know it is in @{term "A\<star>"} and cannot be the empty string. By Prop.~\ref{langprops}@{text "(iv)"},
we can separate
- this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
+ 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"},
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
@@ -1497,8 +1512,9 @@
that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}.
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 @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
+ From the assumption about strict prefixes in @{text "\<^raw:$\threesim$>\<^bsub>\<star>tag A\<^esub>"}, we
+ 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"},
we have
@@ -1515,17 +1531,17 @@
\end{center}
\noindent
- and we know there exist partitions @{text "y\<^isub>p"} and @{text
+ From this we know there exist partitions @{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>
A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. As the last step we have to set
- @{text "A"} to @{term "lang r"} and complete the proof.
+ @{text "A"} to @{term "lang r"} and thus complete the proof.
\end{proof}
*}
-section {* Second Part based on Partial Derivatives *}
+section {* Second Part proved using Partial Derivatives *}
text {*
\noindent
@@ -1534,10 +1550,12 @@
a more refined relation than @{term "\<approx>(lang r)"} for which we can
show that there are only finitely many equivalence classes. So far we
showed this by induction on @{text "r"}. However, there is also
- an indirect method to come up with such a refined relation. Assume
- the following two definitions for a left-quotient of a language, which
- we write as @{term "Der c A"} and @{term "Ders s A"} where
- @{text c} is a character and @{text s} a string:
+ an indirect method to come up with such a refined relation based on
+ derivatives of regular expressions \cite{Brzozowski64}.
+
+ Assume the following two definitions for a \emph{left-quotient} of a language,
+ which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c}
+ is a character and @{text s} a string:
\begin{center}
\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
@@ -1547,6 +1565,14 @@
\end{center}
\noindent
+ In order to aid readability, we shall also make use of the following abbreviation:
+
+ \begin{center}
+ @{abbrev "Derss s A"}
+ \end{center}
+
+
+ \noindent
Clearly we have the following relation between the Myhill-Nerode relation
(Def.~\ref{myhillneroderel}) and left-quotients
@@ -1555,20 +1581,20 @@
\end{equation}
\noindent
- It is realtively easy to establish the following properties for left-quotients:
+ It is straightforward to establish the following properties for left-quotients:
\begin{equation}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
- @{thm (lhs) Der_zero} & $=$ & @{thm (rhs) Der_zero}\\
- @{thm (lhs) Der_one} & $=$ & @{thm (rhs) Der_one}\\
- @{thm (lhs) Der_atom} & $=$ & @{thm (rhs) Der_atom}\\
- @{thm (lhs) Der_union} & $=$ & @{thm (rhs) Der_union}\\
+ @{thm (lhs) Der_simps(1)} & $=$ & @{thm (rhs) Der_simps(1)}\\
+ @{thm (lhs) Der_simps(2)} & $=$ & @{thm (rhs) Der_simps(2)}\\
+ @{thm (lhs) Der_simps(3)} & $=$ & @{thm (rhs) Der_simps(3)}\\
+ @{thm (lhs) Der_simps(4)} & $=$ & @{thm (rhs) Der_simps(4)}\\
@{thm (lhs) Der_conc} & $=$ & @{thm (rhs) Der_conc}\\
@{thm (lhs) Der_star} & $=$ & @{thm (rhs) Der_star}\\
- @{thm (lhs) Ders_nil} & $=$ & @{thm (rhs) Ders_nil}\\
- @{thm (lhs) Ders_cons} & $=$ & @{thm (rhs) Ders_cons}\\
- %@{thm (lhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
- % & @{thm (rhs) Ders_append[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
+ @{thm (lhs) Ders_simps(1)} & $=$ & @{thm (rhs) Ders_simps(1)}\\
+ @{thm (lhs) Ders_simps(2)} & $=$ & @{thm (rhs) Ders_simps(2)}\\
+ %@{thm (lhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
+ % & @{thm (rhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
\end{tabular}}
\end{equation}
@@ -1603,10 +1629,10 @@
\end{center}
\noindent
- The last two lines extend @{const der} to strings (list of characters) where
- list-cons is written \mbox{@{text "_ :: _"}}. The function @{term "nullable r"} needed
- in the @{const Times}-case tests whether a regular expression can recognise
- the empty string:
+ The last two clauses extend derivatives for characters to strings (list of
+ characters). The list-cons operator is written \mbox{@{text "_ :: _"}}. The
+ function @{term "nullable r"} needed in the @{const Times}-case tests
+ whether a regular expression can recognise the empty string:
\begin{center}
\begin{tabular}{c@ {\hspace{10mm}}c}
@@ -1639,8 +1665,8 @@
\noindent
The importance in the context of the Myhill-Nerode theorem is that
- we can use \eqref{mhders} and the equations above in order to
- establish that @{term "x \<approx>(lang r) y"} if and only if
+ we can use \eqref{mhders} and \eqref{Dersders} in order to
+ establish that @{term "x \<approx>(lang r) y"} is equivalent to
@{term "lang (ders x r) = lang (ders y r)"}. From this we obtain
\begin{equation}
@@ -1649,29 +1675,35 @@
\noindent
- Consequently, we can use as the tagging relation @{text
- "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"}, since it refines
- @{term "\<approx>(lang r)"}. However, in order to be useful in the Myhill-Nerode
- theorem, we have to show that for a language there are only finitely many
- derivatives. Unfortunately, this is not true in general: Sakarovitch gives
- an example with infinitely many derivatives
- \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved is
- that for every language there \emph{are} finitely `dissimilar' derivatives for a
- regular expression. Two regular expressions are said to be \emph{similar}
- provided they can be identified using the using the @{text "ACI"}-identities:
+ which means the right-hand side (seen as relation) refines the
+ Myhill-Nerode relation. Consequently, we can use
+ @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a potential tagging-relation
+ for the regular expression @{text r}. However, in
+ order to be useful in the Myhill-Nerode theorem, we also have to show that
+ for the corresponding language there are only finitely many derivatives---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.~a language
+ \cite[Page~141]{Sakarovitch09}. What Brzozowski \cite{Brzozowski64} proved
+ is that for every language there \emph{are} only finitely `dissimilar'
+ derivatives for a regular expression. Two regular expressions are said to be
+ \emph{similar} provided they can be identified using the using the @{text
+ "ACI"}-identities:
- \begin{center}
- \begin{tabular}{cl}
+ \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 I}) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
- Carrying this idea through menas we now have to reasoning modulo @{text "ACI"}.
- This can be done, but it is very painful in a theorem prover (since there is
- no direct characterisation of the set of dissimlar derivatives).
+ Carrying this idea through, we must not consider the set of all derivatives,
+ but the ones modulo @{text "ACI"}. In principle, this can be formally
+ defined, but it is very painful in a theorem prover (since there is no
+ direct characterisation of the set of dissimlar derivatives).
+
Fortunately, there is a much simpler approach using \emph{partial
derivatives}. They were introduced by Antimirov \cite{Antimirov95} and can be defined
@@ -1686,49 +1718,97 @@
& @{text "\<equiv>"} & @{thm (rhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
@{thm (lhs) pder.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 "(Times_set (pder c r\<^isub>1) r\<^isub>2) \<union> (pder c r\<^isub>2)"}\\
+ @{term "(Timess (pder c r\<^isub>1) r\<^isub>2) \<union> (pder c r\<^isub>2)"}\\
& & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
- @{term "Times_set (pder c r\<^isub>1) r\<^isub>2"}\\
+ @{term "Timess (pder c r\<^isub>1) r\<^isub>2"}\\
@{thm (lhs) pder.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(6)}\smallskip\\
@{thm (lhs) pders.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(1)}\\
- @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(2)}\\
+ @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}\\
\end{tabular}
\end{center}
\noindent
- Unlike `simple' derivatives, these functions return a set of regular
- expressions. In the @{const Times} and @{const Star} cases we use
+ Again the last two clauses extend partial derivatives from characters to strings.
+ Unlike `simple' derivatives, the functions for partial derivatives return sets of regular
+ expressions. In the @{const Times} and @{const Star} cases we therefore use the
+ auxiliary definition
\begin{center}
@{text "TIMESS rs r \<equiv> {TIMES r' r | r' \<in> rs}"}
\end{center}
\noindent
- in order to `sequence' a regular expressions with respect to a set of regular
- expresions. Note that in the last case we first build the set of partial derivatives
- w.r.t~@{text c}, then build the image of this set under the function @{term "pders s"}
- and finally `union up' all resulting sets. Note also that in some sense, partial
- derivatives have the @{text "ACI"}-identities already build in. Antimirov
- \cite{Antimirov95}
- showed
+ in order to `sequence' a regular expression with a set of regular
+ expressions. Note that in the last clause we first build the set of partial
+ derivatives w.r.t~the character @{text c}, then build the image of this set under the
+ function @{term "pders s"} and finally `union up' all resulting sets. It will be
+ convenient to introduce the following abbreviation
+
+ \begin{center}
+ @{abbrev "pderss s A"}
+ \end{center}
+
+ \noindent
+ which simplifies the last clause of @{const "pders"} to
+
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
+ @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(2)}\\
+ \end{tabular}
+ \end{center}
+
+ Partial derivatives can be seen as having the @{text "ACI"}-identities already built in:
+ taking the partial derivatives of the
+ regular expressions in \eqref{ACI} gives us in each case
+ equal sets. Antimirov \cite{Antimirov95} showed a similar result to
+ \eqref{Dersders} for partial derivatives:
\begin{equation}
- \mbox{\begin{tabular}{c}
- @{thm Der_pder}\\
- @{thm Ders_pders}
+ \mbox{\begin{tabular}{lc}
+ @{text "(i)"} & @{thm Der_pder}\\
+ @{text "(ii)"} & @{thm Ders_pders}
\end{tabular}}
- \end{equation}
+ \end{equation}
+
+ \begin{proof}
+ The first fact is by a simple induction on @{text r}. For the second we slightly
+ modify Antimirov's proof by performing an induction on @{text s} where we
+ genaralise over all @{text r}. That means in the @{text "cons"}-case the
+ induction hypothesis is
+
+ \begin{center}
+ @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Ders s (lang r) = \<Union> lang ` (pders s r)"}
+ \end{center}
\noindent
- and proved that for every language and regular expression there are only finitely
+ With this we can establish
+
+ \begin{center}
+ \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll}
+ @{term "Ders (c # s) (lang r)"}
+ & @{text "="} & @{term "Ders s (Der c (lang r))"} & by def.\\
+ & @{text "="} & @{term "Ders s (\<Union> lang ` (pder c r))"} & by @{text "(i)"}\\
+ & @{text "="} & @{term "\<Union> (Ders s) ` (lang ` (pder c r))"} & by def.~of @{text "Ders"}\\
+ & @{text "="} & @{term "\<Union> lang ` (\<Union> pders s ` (pder c r))"} & by IH\\
+ & @{text "="} & @{term "\<Union> lang ` (pders (c # s) r)"} & by def.\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ In order to apply the induction hypothesis in the fourth step, we need the generalisation
+ over all regular expressions @{text r}. The case for the empty string is routine and omitted.
+ \end{proof}
+
+ Antimirov also proved that for every language and regular expression there are only finitely
many partial derivatives.
*}
section {* Closure Properties *}
text {*
- The beautiful characteristics of regular languages is that they are closed
- under many operations. Closure under union, sequencencing and Kleene-star
+ \noindent
+ The real beauty of regular languages is that they are closed
+ under almost all set operations. Closure under union, concatenation and Kleene-star
are trivial to establish given our definition of regularity (Def.~\ref{regular}).
More interesting is the closure under complement, because
it seems difficult to construct a regular expression for the complement