(*<*)

theory Paper

imports "../Myhill" "LaTeXsugar"

begin

declare [[show_question_marks = false]]

notation (latex output)

  str_eq_rel ("\<approx>\<^bsub>_\<^esub>")

(*>*)

section {* Introduction *}

text {*

*}

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 starightforward, 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

(*>*)