--- a/Journal/Paper.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Journal/Paper.thy Mon Aug 22 12:49:27 2011 +0000
@@ -37,6 +37,10 @@
abbreviation "TIMESS \<equiv> Timess"
abbreviation "STAR \<equiv> Star"
+definition
+ Delta :: "'a lang \<Rightarrow> 'a lang"
+where
+ "Delta A = (if [] \<in> A then {[]} else {})"
notation (latex output)
str_eq ("\<approx>\<^bsub>_\<^esub>") and
@@ -71,12 +75,32 @@
nullable ("\<delta>'(_')") and
Cons ("_ :: _" [100, 100] 100) and
Rev ("Rev _" [1000] 100) and
- Der ("Der _ _" [1000, 1000] 100) and
+ Deriv ("Der _ _" [1000, 1000] 100) and
+ Derivs ("Ders") and
ONE ("ONE" 999) and
ZERO ("ZERO" 999) and
- pders_lang ("pdersl") and
+ pderivs_lang ("pdersl") and
UNIV1 ("UNIV\<^isup>+") and
- Ders_lang ("Dersl")
+ Deriv_lang ("Dersl") and
+ deriv ("der") and
+ derivs ("ders") and
+ pderiv ("pder") and
+ pderivs ("pders") and
+ pderivs_set ("pderss")
+
+
+lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union
+
+definition
+ Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where
+ "Der c A \<equiv> {s. [c] @ s \<in> A}"
+
+definition
+ Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where
+ "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+
lemma meta_eq_app:
shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
@@ -133,6 +157,27 @@
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
+lemma pow_length:
+ assumes a: "[] \<notin> A"
+ and b: "s \<in> A \<up> Suc n"
+ shows "n < length s"
+using b
+proof (induct n arbitrary: s)
+ case 0
+ have "s \<in> A \<up> Suc 0" by fact
+ with a have "s \<noteq> []" by auto
+ then show "0 < length s" by auto
+next
+ case (Suc n)
+ have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact
+ have "s \<in> A \<up> Suc (Suc n)" by fact
+ then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"
+ by (auto simp add: Seq_def)
+ from ih ** have "n < length s2" by simp
+ moreover have "0 < length s1" using * a by auto
+ ultimately show "Suc n < length s" unfolding eq
+ by (simp only: length_append)
+qed
(*>*)
@@ -445,25 +490,25 @@
\mbox{@{term "X \<cdot> A"}}).
\begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\
- If @{thm (prem 1) arden} then
- @{thm (lhs) arden} if and only if
- @{thm (rhs) arden}.
+ If @{thm (prem 1) reversed_Arden} then
+ @{thm (lhs) reversed_Arden} if and only if
+ @{thm (rhs) reversed_Arden}.
\end{lmm}
\begin{proof}
- For the right-to-left direction we assume @{thm (rhs) arden} and show
- that @{thm (lhs) arden} holds. From Property~\ref{langprops}@{text "(i)"}
+ For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
+ that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"}
we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
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> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation
completes this direction.
- For the other direction we assume @{thm (lhs) arden}. By a simple induction
+ For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
on @{text n}, we can establish the property
\begin{center}
- @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
+ @{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
\end{center}
\noindent
@@ -471,12 +516,12 @@
all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
of @{text "\<star>"}.
For the inclusion in the other direction we assume a string @{text s}
- with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden}
+ with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
we know by Property~\ref{langprops}@{text "(ii)"} that
@{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
(the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
From @{text "(*)"} it follows then that
- @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn
+ @{term s} must be an element in @{term "(\<Union>m\<le>k. B \<cdot> (A \<up> m))"}. This in turn
implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"}
this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
\end{proof}
@@ -520,7 +565,7 @@
set @{text rs} with @{const ZERO} for the empty set. We can prove that for a finite set @{text rs}
%
\begin{equation}\label{uplus}
- \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+ \mbox{@{thm (lhs) folds_plus_simp} @{text "= \<Union> (\<calL> ` rs)"}}
\end{equation}
\noindent
@@ -1574,7 +1619,7 @@
relation by using derivatives of regular expressions~\cite{Brzozowski64}.
Assume the following two definitions for the \emph{left-quotient} of a language,
- which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c}
+ which we write as @{term "Deriv c A"} and @{term "Derivs s A"} where @{text c}
is a character and @{text s} a string, respectively:
\begin{center}
@@ -1588,7 +1633,7 @@
In order to aid readability, we shall make use of the following abbreviation
\begin{center}
- @{abbrev "Derss s As"}
+ @{abbrev "Derivss s As"}
\end{center}
\noindent
@@ -1597,7 +1642,7 @@
(Definition~\ref{myhillneroderel}) and left-quotients
\begin{equation}\label{mhders}
- @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"}
+ @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Derivs x A = Derivs y A"}
\end{equation}
\noindent
@@ -1605,16 +1650,16 @@
\begin{equation}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
- @{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) Deriv_simps(1)} & $=$ & @{thm (rhs) Deriv_simps(1)}\\
+ @{thm (lhs) Deriv_simps(2)} & $=$ & @{thm (rhs) Deriv_simps(2)}\\
+ @{thm (lhs) Deriv_simps(3)} & $=$ & @{thm (rhs) Deriv_simps(3)}\\
+ @{thm (lhs) Deriv_simps(4)} & $=$ & @{thm (rhs) Deriv_simps(4)}\\
@{thm (lhs) Der_conc} & $=$ & @{thm (rhs) Der_conc}\\
- @{thm (lhs) Der_star} & $=$ & @{thm (rhs) Der_star}\\
- @{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"]}\\
+ @{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"]}\\
\end{tabular}}
\end{equation}
@@ -1624,8 +1669,8 @@
accordingly. Note also that in the last equation we use the list-cons operator written
\mbox{@{text "_ :: _"}}. The only interesting case is the case of @{term "A\<star>"}
where we use Property~\ref{langprops}@{text "(i)"} in order to infer that
- @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can then complete the proof by
- using the fifth equation and noting that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der
+ @{term "Deriv c (A\<star>) = Deriv c (A \<cdot> A\<star>)"}. We can then complete the proof by
+ using the fifth equation and noting that @{term "Delta A \<cdot> Deriv c (A\<star>) \<subseteq> (Deriv
c A) \<cdot> A\<star>"}.
Brzozowski observed that the left-quotients for languages of
@@ -1635,19 +1680,19 @@
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
- @{thm (lhs) der.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(1)}\\
- @{thm (lhs) der.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(2)}\\
- @{thm (lhs) der.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) der.simps(3)[where c'="d"]}\\
- @{thm (lhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{thm (rhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm (lhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ @{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 (der c r\<^isub>1) r\<^isub>2) (der c r\<^isub>2)"}\\
+ @{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 (der c r\<^isub>1) r\<^isub>2"}\\
- @{thm (lhs) der.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(6)}\smallskip\\
- @{thm (lhs) ders.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) ders.simps(1)}\\
- @{thm (lhs) ders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) ders.simps(2)}\\
+ @{term "Times (deriv c r\<^isub>1) r\<^isub>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)}\\
\end{tabular}
\end{center}
@@ -1679,8 +1724,8 @@
\begin{equation}\label{Dersders}
\mbox{\begin{tabular}{c}
- @{thm Der_der}\\
- @{thm Ders_ders}
+ @{thm Deriv_deriv}\\
+ @{thm Derivs_derivs}
\end{tabular}}
\end{equation}
@@ -1691,14 +1736,14 @@
\begin{center}
@{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm}
- @{term "lang (ders x r) = lang (ders y r)"}.
+ @{term "lang (derivs x r) = lang (derivs y r)"}.
\end{center}
\noindent
holds and hence
\begin{equation}
- @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"}
+ @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "derivs x r = derivs y r"}
\end{equation}
@@ -1743,19 +1788,19 @@
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
- @{thm (lhs) pder.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(1)}\\
- @{thm (lhs) pder.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(2)}\\
- @{thm (lhs) pder.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(3)[where c'="d"]}\\
- @{thm (lhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{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"]}
+ @{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 (pder c r\<^isub>1) r\<^isub>2) \<union> (pder c r\<^isub>2)"}\\
+ @{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 (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>"} & @{text "\<Union> (pders s) ` (pder c r)"}\\
+ @{term "Timess (pderiv c r\<^isub>1) r\<^isub>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)"}\\
\end{tabular}
\end{center}
@@ -1773,19 +1818,19 @@
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
+ function @{term "pderivs s"} and finally `union up' all resulting sets. It will be
convenient to introduce for this the following abbreviation
\begin{center}
- @{abbrev "pderss s rs"}
+ @{abbrev "pderivs_set s rs"}
\end{center}
\noindent
- which simplifies the last clause of @{const "pders"} to
+ which simplifies the last clause of @{const "pderivs"} 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)}\\
+ @{thm (lhs) pderivs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(2)}\\
\end{tabular}
\end{center}
@@ -1797,8 +1842,8 @@
\begin{equation}\label{Derspders}
\mbox{\begin{tabular}{lc}
- @{text "(i)"} & @{thm Der_pder}\\
- @{text "(ii)"} & @{thm Ders_pders}
+ @{text "(i)"} & @{thm Deriv_pderiv}\\
+ @{text "(ii)"} & @{thm Derivs_pderivs}
\end{tabular}}
\end{equation}
@@ -1809,7 +1854,7 @@
induction hypothesis is
\begin{center}
- @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Ders s (lang r) = \<Union> lang ` (pders s r)"}
+ @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)"}
\end{center}
\noindent
@@ -1817,12 +1862,12 @@
\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 "("}\ref{Derspders}@{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.\\
+ @{term "Derivs (c # s) (lang r)"}
+ & @{text "="} & @{term "Derivs s (Deriv c (lang r))"} & by def.\\
+ & @{text "="} & @{term "Derivs s (\<Union> lang ` (pderiv c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\
+ & @{text "="} & @{term "\<Union> (Derivs s) ` (lang ` (pderiv c r))"} & by def.~of @{text "Ders"}\\
+ & @{text "="} & @{term "\<Union> lang ` (\<Union> pderivs s ` (pderiv c r))"} & by IH\\
+ & @{text "="} & @{term "\<Union> lang ` (pderivs (c # s) r)"} & by def.\\
\end{tabular}
\end{center}
@@ -1838,8 +1883,8 @@
\begin{equation}
\mbox{\begin{tabular}{lc}
- @{text "(i)"} & @{thm der_pder[symmetric]}\\
- @{text "(ii)"} & @{thm ders_pders[symmetric]}
+ @{text "(i)"} & @{thm deriv_pderiv[symmetric]}\\
+ @{text "(ii)"} & @{thm derivs_pderivs[symmetric]}
\end{tabular}}
\end{equation}
@@ -1853,12 +1898,12 @@
derivatives of @{text r} w.r.t.~a language @{text A} is defined as
\begin{equation}\label{Pdersdef}
- @{thm pders_lang_def}
+ @{thm pderivs_lang_def}
\end{equation}
\begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov}
For every language @{text A} and every regular expression @{text r},
- \mbox{@{thm finite_pders_lang}}.
+ \mbox{@{thm finite_pderivs_lang}}.
\end{thrm}
\noindent
@@ -1867,12 +1912,12 @@
\begin{equation}\label{pdersunivone}
\mbox{\begin{tabular}{l}
- @{thm pders_lang_Zero}\\
- @{thm pders_lang_One}\\
- @{thm pders_lang_Atom}\\
- @{thm pders_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm pders_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm pders_lang_Star}\\
+ @{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_Star}\\
\end{tabular}}
\end{equation}
@@ -1880,19 +1925,19 @@
from which one can deduce by induction on @{text r} that
\begin{center}
- @{thm finite_pders_lang_UNIV1}
+ @{thm finite_pderivs_lang_UNIV1}
\end{center}
\noindent
holds. Now Antimirov's theorem follows because
\begin{center}
- @{thm pders_lang_UNIV}\\
+ @{thm pderivs_lang_UNIV}\\
\end{center}
\noindent
- and for all languages @{text "A"}, @{term "pders_lang A r"} is a subset of
- @{term "pders_lang UNIV r"}. Since we follow Antimirov's proof quite
+ and for all languages @{text "A"}, @{term "pderivs_lang A r"} is a subset of
+ @{term "pderivs_lang UNIV r"}. Since we follow Antimirov's proof quite
closely in our formalisation (only the last two cases of
\eqref{pdersunivone} involve some non-routine induction arguments), we omit
the details.
@@ -1907,23 +1952,23 @@
and \eqref{Derspders} we can easily infer that
\begin{center}
- @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pders x r = pders y r"}
+ @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pderivs x r = pderivs y r"}
\end{center}
\noindent
which means the tagging-relation @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"} refines @{term "\<approx>(lang r)"}.
So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\<approx>(lang r)))"}}
- holds if @{term "finite (UNIV // (=(\<lambda>x. pders x r)=))"}. In order to establish
+ holds if @{term "finite (UNIV // (=(\<lambda>x. pderivs x r)=))"}. In order to establish
the latter, we can use Lemma~\ref{finone} and show that the range of the
- tagging-function \mbox{@{term "\<lambda>x. pders x r"}} is finite. For this recall Definition
+ tagging-function \mbox{@{term "\<lambda>x. pderivs x r"}} is finite. For this recall Definition
\ref{Pdersdef}, which gives us that
\begin{center}
- @{thm pders_lang_def[where A="UNIV", simplified]}
+ @{thm pderivs_lang_def[where A="UNIV", simplified]}
\end{center}
\noindent
- Now the range of @{term "\<lambda>x. pders x r"} is a subset of @{term "Pow (pders_lang UNIV r)"},
+ Now the range of @{term "\<lambda>x. pderivs x r"} is a subset of @{term "Pow (pderivs_lang UNIV r)"},
which we know is finite by Theorem~\ref{antimirov}. Consequently there
are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"},
which refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the
@@ -2007,29 +2052,29 @@
left-quotient. Define
\begin{center}
- @{abbrev "Ders_lang B A"}
+ @{abbrev "Deriv_lang B A"}
\end{center}
\noindent
and assume @{text B} is any language and @{text A} is regular, then @{term
- "Ders_lang B A"} is regular. To see this consider the following argument
+ "Deriv_lang B A"} is regular. To see this consider the following argument
using partial derivatives: From @{text A} being regular we know there exists
a regular expression @{text r} such that @{term "A = lang r"}. We also know
- that @{term "pders_lang B r"} is finite for every language @{text B} and
+ that @{term "pderivs_lang B r"} is finite for every language @{text B} and
regular expression @{text r} (recall Theorem~\ref{antimirov}). By definition
and \eqref{Derspders} therefore
\begin{equation}\label{eqq}
- @{term "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"}
+ @{term "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))"}
\end{equation}
\noindent
- Since there are only finitely many regular expressions in @{term "pders_lang
+ Since there are only finitely many regular expressions in @{term "pderivs_lang
B r"}, we know by \eqref{uplus} that there exists a regular expression so that
- the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pders_lang B
- r))"}}. Thus the regular expression @{term "\<Uplus>(pders_lang B r)"} verifies that
- @{term "Ders_lang B A"} is regular.
+ the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pderivs_lang B
+ r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that
+ @{term "Deriv_lang B A"} is regular.
*}