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)

section {* Preliminaries *}

text {*

  A central technique in our proof is 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 right-to-left direction we assume @{thm (rhs) ardens_revised} and show

  @{thm (lhs) ardens_revised}. 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 @{term "B \<union> (B ;; A\<star>) ;; A"}. This completes this direction. 

  For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction

  on @{text n}, we can show 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 ???.

  The inclusion in the other direction we establishing by assuming 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)"} as its length is only @{text k}. 

  From @{text "(*)"} it follows 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}

*}

  and @{const CHAR} are straightforward, because we can easily establish