(*<*)
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)

(*>*)

section {* Introduction *}

text {*
  
*}

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}
*}

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
(*>*)