(*<*)+ −
theory Paper+ −
imports "../Myhill" "LaTeXsugar"+ −
begin+ −
+ −
declare [[show_question_marks = false]]+ −
+ −
notation (latex output)+ −
str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and+ −
Seq (infixr "\<cdot>" 100) and+ −
Star ("_\<^bsup>\<star>\<^esup>") and+ −
pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and+ −
Suc ("_+1" [100] 100) and+ −
quotient ("_ \<^raw:\ensuremath{\sslash}> _ " [90, 90] 90)+ −
+ −
+ −
(*>*)+ −
+ −
section {* Introduction *}+ −
+ −
text {*+ −
+ −
*}+ −
+ −
section {* Preliminaries *}+ −
+ −
text {*+ −
Central to our proof will be the solution of equational systems+ −
involving regular expressions. For this we will use the following ``reverse'' + −
version of Arden's lemma.+ −
+ −
\begin{lemma}[Reverse Arden's Lemma]\mbox{}\\+ −
If @{thm (prem 1) ardens_revised} then+ −
@{thm (lhs) ardens_revised} has the unique solution+ −
@{thm (rhs) ardens_revised}.+ −
\end{lemma}+ −
+ −
\begin{proof}+ −
For the right-to-left direction we assume @{thm (rhs) ardens_revised} and show+ −
that @{thm (lhs) ardens_revised} holds. From Lemma ??? we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},+ −
which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both + −
sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side+ −
is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction. + −
+ −
For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction+ −
on @{text n}, we can establish the property+ −
+ −
\begin{center}+ −
@{text "(*)"}\hspace{5mm} @{thm (concl) ardens_helper}+ −
\end{center}+ −
+ −
\noindent+ −
Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for+ −
all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using Lemma ???.+ −
For the inclusion in the other direction we assume a string @{text s}+ −
with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}+ −
we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}+ −
(the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). + −
From @{text "(*)"} it follows then that+ −
@{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn+ −
implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this+ −
is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed+ −
\end{proof}+ −
*}+ −
+ −
section {* Regular expressions have finitely many partitions *}+ −
+ −
text {*+ −
+ −
\begin{lemma}+ −
Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.+ −
\end{lemma} + −
+ −
\begin{proof}+ −
By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}+ −
and @{const CHAR} are straightforward, because we can easily establish+ −
+ −
\begin{center}+ −
\begin{tabular}{l}+ −
@{thm quot_null_eq}\\+ −
@{thm quot_empty_subset}\\+ −
@{thm quot_char_subset}+ −
\end{tabular}+ −
\end{center}+ −
+ −
+ −
+ −
\end{proof}+ −
+ −
*}+ −
+ −
+ −
(*<*)+ −
end+ −
(*>*)+ −