diff -r 09e6f3719cbc -r 5d724fe0e096 Journal/Paper.thy --- 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 \ Timess" abbreviation "STAR \ Star" +definition + Delta :: "'a lang \ 'a lang" +where + "Delta A = (if [] \ A then {[]} else {})" notation (latex output) str_eq ("\\<^bsub>_\<^esub>") and @@ -71,12 +75,32 @@ nullable ("\'(_')") 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 \ 'a lang \ 'a lang" +where + "Der c A \ {s. [c] @ s \ A}" + +definition + Ders :: "'a list \ 'a lang \ 'a lang" +where + "Ders s A \ {s'. s @ s' \ A}" + lemma meta_eq_app: shows "f \ \x. g x \ f x \ g x" @@ -133,6 +157,27 @@ "_asms" :: "prop \ asms \ asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") "_asm" :: "prop \ asms" ("_") +lemma pow_length: + assumes a: "[] \ A" + and b: "s \ A \ Suc n" + shows "n < length s" +using b +proof (induct n arbitrary: s) + case 0 + have "s \ A \ Suc 0" by fact + with a have "s \ []" by auto + then show "0 < length s" by auto +next + case (Suc n) + have ih: "\s. s \ A \ Suc n \ n < length s" by fact + have "s \ A \ Suc (Suc n)" by fact + then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \ A" and **: "s2 \ A \ 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 \ 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\ = A \ A\ \ {[]}"}, which is equal to @{term "A\ = A\ \ A \ {[]}"}. Adding @{text B} to both sides gives @{term "B \ A\ = B \ (A\ \ A \ {[]})"}, whose right-hand side is equal to @{term "(B \ A\) \ A \ 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 \ A\ \ X"} using the definition of @{text "\"}. 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 \ X \ (A \ Suc k)"} since its length is only @{text k} (the strings in @{term "X \ (A \ Suc k)"} are all longer). From @{text "(*)"} it follows then that - @{term s} must be an element in @{term "(\m\{0..k}. B \ (A \ m))"}. This in turn + @{term s} must be an element in @{term "(\m\k. B \ (A \ m))"}. This in turn implies that @{term s} is in @{term "(\n. B \ (A \ n))"}. Using Property~\ref{langprops}@{text "(iii)"} this is equal to @{term "B \ A\"}, 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 "= \ (\ ` rs)"}} + \mbox{@{thm (lhs) folds_plus_simp} @{text "= \ (\ ` 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 \A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"} + @{term "x \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\"} where we use Property~\ref{langprops}@{text "(i)"} in order to infer that - @{term "Der c (A\) = Der c (A \ A\)"}. We can then complete the proof by - using the fifth equation and noting that @{term "Delta A \ Der c (A\) \ (Der + @{term "Deriv c (A\) = Deriv c (A \ A\)"}. We can then complete the proof by + using the fifth equation and noting that @{term "Delta A \ Deriv c (A\) \ (Deriv c A) \ A\"}. 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 "\"} & @{thm (rhs) der.simps(1)}\\ - @{thm (lhs) der.simps(2)} & @{text "\"} & @{thm (rhs) der.simps(2)}\\ - @{thm (lhs) der.simps(3)[where c'="d"]} & @{text "\"} & @{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 "\"} & @{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 "\"} & @{thm (rhs) deriv.simps(1)}\\ + @{thm (lhs) deriv.simps(2)} & @{text "\"} & @{thm (rhs) deriv.simps(2)}\\ + @{thm (lhs) deriv.simps(3)[where c'="d"]} & @{text "\"} & @{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 "\"} & @{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 "\"} & @{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 "\"} & @{thm (rhs) der.simps(6)}\smallskip\\ - @{thm (lhs) ders.simps(1)} & @{text "\"} & @{thm (rhs) ders.simps(1)}\\ - @{thm (lhs) ders.simps(2)} & @{text "\"} & @{thm (rhs) ders.simps(2)}\\ + @{term "Times (deriv c r\<^isub>1) r\<^isub>2"}\\ + @{thm (lhs) deriv.simps(6)} & @{text "\"} & @{thm (rhs) deriv.simps(6)}\smallskip\\ + @{thm (lhs) derivs.simps(1)} & @{text "\"} & @{thm (rhs) derivs.simps(1)}\\ + @{thm (lhs) derivs.simps(2)} & @{text "\"} & @{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 \(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 \(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"} + @{term "x \(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 "\"} & @{thm (rhs) pder.simps(1)}\\ - @{thm (lhs) pder.simps(2)} & @{text "\"} & @{thm (rhs) pder.simps(2)}\\ - @{thm (lhs) pder.simps(3)[where c'="d"]} & @{text "\"} & @{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 "\"} & @{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 "\"} & @{thm (rhs) pderiv.simps(1)}\\ + @{thm (lhs) pderiv.simps(2)} & @{text "\"} & @{thm (rhs) pderiv.simps(2)}\\ + @{thm (lhs) pderiv.simps(3)[where c'="d"]} & @{text "\"} & @{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 "\"} & @{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 "\"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~% - @{term "(Timess (pder c r\<^isub>1) r\<^isub>2) \ (pder c r\<^isub>2)"}\\ + @{term "(Timess (pderiv c r\<^isub>1) r\<^isub>2) \ (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 "\"} & @{thm (rhs) pder.simps(6)}\smallskip\\ - @{thm (lhs) pders.simps(1)} & @{text "\"} & @{thm (rhs) pders.simps(1)}\\ - @{thm (lhs) pders.simps(2)} & @{text "\"} & @{text "\ (pders s) ` (pder c r)"}\\ + @{term "Timess (pderiv c r\<^isub>1) r\<^isub>2"}\\ + @{thm (lhs) pderiv.simps(6)} & @{text "\"} & @{thm (rhs) pderiv.simps(6)}\smallskip\\ + @{thm (lhs) pderivs.simps(1)} & @{text "\"} & @{thm (rhs) pderivs.simps(1)}\\ + @{thm (lhs) pderivs.simps(2)} & @{text "\"} & @{text "\ (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 "\"} & @{thm (rhs) pders.simps(2)}\\ + @{thm (lhs) pderivs.simps(2)} & @{text "\"} & @{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 "\r. Ders s (lang r) = \ lang ` (pders s r)"} + @{text "(IH)"}\hspace{3mm}@{term "\r. Derivs s (lang r) = \ 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 (\ lang ` (pder c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\ - & @{text "="} & @{term "\ (Ders s) ` (lang ` (pder c r))"} & by def.~of @{text "Ders"}\\ - & @{text "="} & @{term "\ lang ` (\ pders s ` (pder c r))"} & by IH\\ - & @{text "="} & @{term "\ 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 (\ lang ` (pderiv c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\ + & @{text "="} & @{term "\ (Derivs s) ` (lang ` (pderiv c r))"} & by def.~of @{text "Ders"}\\ + & @{text "="} & @{term "\ lang ` (\ pderivs s ` (pderiv c r))"} & by IH\\ + & @{text "="} & @{term "\ 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 \(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pders x r = pders y r"} + @{term "x \(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>(\x. pders x r)\<^esub>"} refines @{term "\(lang r)"}. So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\(lang r)))"}} - holds if @{term "finite (UNIV // (=(\x. pders x r)=))"}. In order to establish + holds if @{term "finite (UNIV // (=(\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 "\x. pders x r"}} is finite. For this recall Definition + tagging-function \mbox{@{term "\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 "\x. pders x r"} is a subset of @{term "Pow (pders_lang UNIV r)"}, + Now the range of @{term "\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>(\x. pders x r)\<^esub>"}, which refines @{term "\(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) = (\ lang ` (pders_lang B r))"} + @{term "Deriv_lang B (lang r) = (\ 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 (\(pders_lang B - r))"}}. Thus the regular expression @{term "\(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 (\(pderivs_lang B + r))"}}. Thus the regular expression @{term "\(pderivs_lang B r)"} verifies that + @{term "Deriv_lang B A"} is regular. *}