31 Trn ("'(_, _')" [100, 100] 100) and |
31 Trn ("'(_, _')" [100, 100] 100) and |
32 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and |
32 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and |
33 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and |
33 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and |
34 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and |
34 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and |
35 append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and |
35 append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and |
36 append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) |
36 append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) |
37 |
37 |
38 (*>*) |
38 (*>*) |
39 |
39 |
40 |
40 |
41 section {* Introduction *} |
41 section {* Introduction *} |
513 \noindent |
513 \noindent |
514 We first delete all terms of the form @{text "(X, r)"} from @{text rhs}; |
514 We first delete all terms of the form @{text "(X, r)"} from @{text rhs}; |
515 then we calculate the combinded regular expressions for all @{text r} coming |
515 then we calculate the combinded regular expressions for all @{text r} coming |
516 from the deleted @{text "(X, r)"}, and take the @{const STAR} of it; |
516 from the deleted @{text "(X, r)"}, and take the @{const STAR} of it; |
517 finally we append this regular expression to @{text rhs'}. It can be easily seen |
517 finally we append this regular expression to @{text rhs'}. It can be easily seen |
518 that this operation mimics Arden's lemma on the level of equations. |
518 that this operation mimics Arden's lemma on the level of equations. |
519 |
519 The \emph{substituion-operation} takes an equation |
520 |
520 of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}. |
521 \begin{center} |
521 |
522 @{thm Subst_def} |
522 \begin{center} |
523 \end{center} |
523 \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l} |
|
524 @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ |
|
525 & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\ |
|
526 & & @{text "r' ="} & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\ |
|
527 & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\ |
|
528 \end{tabular} |
|
529 \end{center} |
|
530 |
|
531 \noindent |
|
532 We again delete first all occurence of @{text "(X, r)"} in @{text rhs}; we then calculate |
|
533 the regular expression corresponding to the deleted terms; finally we append this |
|
534 regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use |
|
535 the substitution operation we will arrange it so that @{text "xrhs"} does not contain |
|
536 any occurence of @{text X}. |
524 *} |
537 *} |
525 |
538 |
526 section {* Regular Expressions Generate Finitely Many Partitions *} |
539 section {* Regular Expressions Generate Finitely Many Partitions *} |
527 |
540 |
528 text {* |
541 text {* |