--- a/Paper/Paper.thy Thu Feb 10 12:32:45 2011 +0000
+++ b/Paper/Paper.thy Thu Feb 10 13:10:16 2011 +0000
@@ -33,7 +33,7 @@
transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
- append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100)
+ append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50)
(*>*)
@@ -515,12 +515,25 @@
then we calculate the combinded regular expressions for all @{text r} coming
from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
finally we append this regular expression to @{text rhs'}. It can be easily seen
- that this operation mimics Arden's lemma on the level of equations.
-
+ that this operation mimics Arden's lemma on the level of equations.
+ The \emph{substituion-operation} takes an equation
+ of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
\begin{center}
- @{thm Subst_def}
+ \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ & & @{text "r' ="} & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
+ & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\
+ \end{tabular}
\end{center}
+
+ \noindent
+ We again delete first all occurence of @{text "(X, r)"} in @{text rhs}; we then calculate
+ the regular expression corresponding to the deleted terms; finally we append this
+ regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
+ the substitution operation we will arrange it so that @{text "xrhs"} does not contain
+ any occurence of @{text X}.
*}
section {* Regular Expressions Generate Finitely Many Partitions *}