# HG changeset patch
# User urbanc
# Date 1297343416 0
# Node ID 9540c2f2ea778ac8efffc43e382e9d234980e918
# Parent  5b12cd0a3b3cb4b7e47ca56cade8e9752792cbea
more things

diff -r 5b12cd0a3b3c -r 9540c2f2ea77 Myhill_1.thy
--- a/Myhill_1.thy	Thu Feb 10 12:32:45 2011 +0000
+++ b/Myhill_1.thy	Thu Feb 10 13:10:16 2011 +0000
@@ -448,7 +448,7 @@
 section {* Substitution Operation on equations *}
 
 text {* 
-  Suppose and equation @{text "X = xrhs"}, @{text "subst_op"} substitutes 
+  Suppose and equation @{text "X = xrhs"}, @{text "Subst"} substitutes 
   all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}.
 *}
 
@@ -476,7 +476,7 @@
   *}
 
 definition
-  "remove_op ES Y yrhs \<equiv> 
+  "Remove ES Y yrhs \<equiv> 
       Subst_all  (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"
 
 text {*
@@ -486,7 +486,7 @@
 
 definition 
   "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)
-                in remove_op ES Y yrhs)"
+                in Remove ES Y yrhs)"
 
 text {*
   The following term @{text "reduce X ES"} repeatedly removes characteriztion equations
@@ -911,7 +911,6 @@
 by (auto simp:classes_of_def)
 
 lemma Subst_all_keeps_self_contained:
-  fixes Y
   assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
   shows "self_contained (Subst_all ES Y (Arden Y yrhs))" 
                                                    (is "self_contained ?B")
@@ -1046,7 +1045,7 @@
     using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto)
   let ?ES' = "iter X ES"
   show ?thesis
-  proof(unfold iter_def remove_op_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
+  proof(unfold iter_def Remove_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
     from X_in_ES Y_in_ES and not_eq and Inv_ES
     show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
       by (auto simp: invariant_def distinct_equas_def)
diff -r 5b12cd0a3b3c -r 9540c2f2ea77 Paper/Paper.thy
--- 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 *}