22 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and |
22 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and |
23 REL ("\<approx>") and |
23 REL ("\<approx>") and |
24 UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and |
24 UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and |
25 L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and |
25 L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and |
26 Lam ("\<lambda>'(_')" [100] 100) and |
26 Lam ("\<lambda>'(_')" [100] 100) and |
27 Trn ("_, _" [100, 100] 100) and |
27 Trn ("'(_, _')" [100, 100] 100) and |
28 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and |
28 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and |
29 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and |
29 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and |
30 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) |
30 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) |
31 (*>*) |
31 (*>*) |
32 |
32 |
431 The reason for adding the @{text \<lambda>}-marker to our equational system is |
431 The reason for adding the @{text \<lambda>}-marker to our equational system is |
432 to obtain this equation, which only holds in this form since none of |
432 to obtain this equation, which only holds in this form since none of |
433 the other terms contain the empty string. |
433 the other terms contain the empty string. |
434 |
434 |
435 |
435 |
436 Our proof of Thm.~\ref{myhillnerodeone} |
436 Our proof of Thm.~\ref{myhillnerodeone} will be by transforming the |
437 will be by transforming the equational system into a \emph{solved form} |
437 equational system into a \emph{solved form} maintaining the invariants |
438 maintaining the invariants \eqref{inv1} and \eqref{inv2}. From the solved |
438 \eqref{inv1} and \eqref{inv2}. From the solved form we will be able to read |
439 form we will be able to read off the regular expressions using our |
439 off the regular expressions. |
440 variant of Arden's Lemma (Lem.~\ref{arden}). |
440 |
|
441 In order to transform an equational system into solved form, we have two main |
|
442 operations: one that takes an equation of the form @{text "X = rhs"} and removes |
|
443 the recursive occurences of @{text X} in @{text rhs} using our variant of Arden's |
|
444 Lemma (Lem.~\ref{arden}). The other operation takes an equation @{text "X = rhs"} |
|
445 and substitutes @{text X} throughout the rest of the equational system |
|
446 adjusting the regular expressions approriately. To define them we need the |
|
447 operation |
|
448 |
|
449 \begin{center} |
|
450 @{thm attach_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm} |
|
451 @{thm attach_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]} |
|
452 \end{center} |
|
453 |
441 |
454 |
442 *} |
455 *} |
443 |
456 |
444 section {* Regular Expressions Generate Finitely Many Partitions *} |
457 section {* Regular Expressions Generate Finitely Many Partitions *} |
445 |
458 |