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