24   L ("L '(_')" [0] 101) and

    25   L ("L'(_')" [0] 101) and

    26   Lam ("\<lambda>'(_')" [100] 100) and 

    27   Trn ("_, _" [100, 100] 100) and 

    26   transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longrightarrow}}> _" [100, 100, 100] 100)

    29   transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100)

   216   involving regular expressions. For this we will use Arden's lemma \cite{}

   219   involving regular expressions. For this we will use Arden's lemma \cite{Brzozowski64}

   221   \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\

   224   \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\

   229   that @{thm (lhs) ardens_revised} holds. From Prop.~\ref{langprops}$(i)$ 

   232   that @{thm (lhs) ardens_revised} holds. From Prop.~\ref{langprops}@{text "(i)"} 

   248   we know by Prop.~\ref{langprops}$(ii)$ that 

   251   we know by Prop.~\ref{langprops}@{text "(ii)"} that 

   253   implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}$(iii)$ 

   256   implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"} 

   298   @{thm str_eq_rel_def[simplified]}

   306   @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}

   302   It is easy to see that @{term "\<approx>A"} is an equivalence relation, which partitions

   310   It is easy to see that @{term "\<approx>A"} is an equivalence relation, which

   303   the set of all string, @{text "UNIV"}, into a set of equivalence classed. We define

   311   partitions the set of all strings, @{text "UNIV"}, into a set of disjoint

   304   the set @{term "finals A"} as those equivalence classes that contain strings of 

   312   equivalence classes. One direction of the Myhill-Nerode theorem establishes 

   305   @{text A}, namely

   313   that if there are finitely many equivalence classes, then the language is 

   306 

   314   regular. In our setting we have therefore

   315   

   316   \begin{theorem}\label{myhillnerodeone}

   317   @{thm[mode=IfThen] hard_direction}

   318   \end{theorem}

   319 

   320   \noindent

   321   To prove this theorem, we define the set @{term "finals A"} as those equivalence

   322   classes that contain strings of @{text A}, namely

   323   %

   312   It is easy to show that @{thm lang_is_union_of_finals} holds. We can also define 

   329   It is straightforward to show that @{thm lang_is_union_of_finals} holds. 

   313   a notion of \emph{transition} between equivalence classes as

   330   Therefore if we know that there exists a regular expression for every

   314 

   331   equivalence class in @{term "finals A"} (which by assumption must be

   332   a finite set), then we can just combine these regular expressions with @{const ALT}

   333   and obtain a regular expression that matches every string in @{text A}.

   334 

   335 

   336   We prove Thm.~\ref{myhillnerodeone} by calculating a regular expression for

   337   \emph{all} equivalence classes, not just the ones in @{term "finals A"}. We

   338   first define a notion of \emph{transition} between equivalence classes

   339   %

   320   which means if we add the character @{text c} to all strings in the equivalence

   345   which means that if we concatenate all strings matching the regular expression @{text r} 

   321   class @{text Y} HERE

   346   to the end of all strings in the equivalence class @{text Y}, we obtain a subset of 

   322 

   347   @{text X}. Note that we do not define any automaton here, we merely relate two sets

   323   \begin{theorem}

   348   w.r.t.~a regular expression. 

   324   Given a language @{text A}.

   349   

   325   @{thm[mode=IfThen] hard_direction}

   350   Next we build an equational system that

   326   \end{theorem}

   351   contains an equation for each equivalence class. Suppose we have 

   352   the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that

   353   contains the empty string @{text "[]"} (since equivalence classes are disjoint).

   354   Let us assume @{text "[] \<in> X\<^isub>1"}. We can build the following equational system

   355   

   356   \begin{center}

   357   \begin{tabular}{rcl}

   358   @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\

   359   @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\

   360   & $\vdots$ \\

   361   @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\

   362   \end{tabular}

   363   \end{center}

   364 

   365   \noindent

   366   where the pairs @{text "(Y\<^isub>i\<^isub>j, r\<^isub>i\<^isub>j)"} stand for all transitions 

   367   @{term "Y\<^isub>i\<^isub>j \<Turnstile>r\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}.  The term @{text "\<lambda>(EMPTY)"} acts as a marker for the equivalence

   368   class containing @{text "[]"}. (Note that we mark, roughly speaking, the

   369   single ``initial'' state in the equational system, which is different from

   370   the method by Brzozowski \cite{Brzozowski64}, which marks the ``terminal''

   371   states.) Overloading the function @{text L} for the two kinds of terms in the 

   372   equational system as follows

   373   

   374   \begin{center}

   375   @{thm L_rhs_e.simps(1)[where r="r", THEN eq_reflection]}\hspace{20mm}

   376   @{thm L_rhs_e.simps(2)[where X="X" and r="r", THEN eq_reflection]}

   377   \end{center}

   378 

   379   \noindent

   380   we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations

   381   %

   382   \begin{equation}\label{inv1}

   383   @{text "X\<^isub>i = L(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> L(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.

   384   \end{equation}

   385 

   386   \noindent

   387   hold. Similarly for @{text "X\<^isub>1"} we can show the following equation

   388   %

   389   \begin{equation}\label{inv2}

   390   @{text "X\<^isub>1 = L(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> L(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> L(\<lambda>(EMPTY))"}.

   391   \end{equation}

   392 

   393   \noindent

   394   hold. The reason for adding the @{text \<lambda>}-marker to our equational system is 

   395   to obtain this equations, which only holds in this form since none of 

   396   the other terms contain the empty string. Our proof of Thm.~\ref{myhillnerodeone}

   397   will be by transforming the equational system into a \emph{solved form}

   398   maintaining the invariants \eqref{inv1} and \eqref{inv2}. From the solved

   399   form we will be able to read off the regular expressions using our 

   400   variant of Arden's Lemma (Lem.~\ref{arden}).

   401