--- a/Myhill_1.thy	Thu Feb 10 08:40:38 2011 +0000
+++ b/Myhill_1.thy	Thu Feb 10 12:32:45 2011 +0000
@@ -249,6 +249,33 @@
   show "X = B ;; A\<star>" by simp
 qed
 
+(*
+corollary arden_eq:
+  assumes nemp: "[] \<notin> A"
+  shows "(X ;; A \<union> B) = (B ;; A\<star>)"
+proof -
+  { assume "X = X ;; A \<union> B"
+    then have "X = B ;; A\<star>"
+    then have ?thesis
+      thm arden[THEN iffD1]
+apply(rule set_eqI)
+thm arden[THEN iffD1]
+apply(rule iffI)
+apply(rule trans)
+apply(rule arden[THEN iffD2, symmetric])
+apply(rule arden[OF iffD1, symmetric])
+thm trans
+proof -
+  { assume "X = X ;; A \<union> B"
+    then have "X = B ;; A\<star>" using arden[OF nemp] by blast
+    moreover 
+  
+    
+using arden[of "A" "X" "B", OF nemp]
+apply(erule_tac iffE)
+apply(blast)
+*)
+
 
 section {* Regular Expressions *}
 
@@ -287,7 +314,7 @@
 abbreviation
   Setalt  ("\<Uplus>_" [1000] 999) 
 where
-  "\<Uplus>A == folds ALT NULL A"
+  "\<Uplus>A \<equiv> folds ALT NULL A"
 
 text {* 
   For finite sets, @{term Setalt} is preserved under @{term L}.
@@ -297,8 +324,8 @@
   fixes rs::"rexp set"
   assumes a: "finite rs"
   shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
+unfolding folds_def
 apply(rule set_eqI)
-apply(simp add: folds_def)
 apply(rule someI2_ex)
 apply(rule_tac finite_imp_fold_graph[OF a])
 apply(erule fold_graph.induct)
@@ -346,8 +373,7 @@
 
 lemma finals_in_partitions:
   shows "finals A \<subseteq> (UNIV // \<approx>A)"
-unfolding finals_def
-unfolding quotient_def
+unfolding finals_def quotient_def
 by auto
 
 
@@ -376,9 +402,6 @@
      "L_rhs rhs = \<Union> (L ` rhs)"
 end
 
-definition
-  "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}"
-
 text {* Transitions between equivalence classes *}
 
 definition 
@@ -418,8 +441,8 @@
   "append_rhs_rexp rhs rexp \<equiv> (append_rexp rexp) ` rhs"
 
 definition 
-  "arden_op X rhs \<equiv> 
-     append_rhs_rexp (rhs - trns_of rhs X) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
+  "Arden X rhs \<equiv> 
+     append_rhs_rexp (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
 
 
 section {* Substitution Operation on equations *}
@@ -430,8 +453,8 @@
 *}
 
 definition 
-  "subst_op rhs X xrhs \<equiv> 
-        (rhs - (trns_of rhs X)) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
+  "Subst rhs X xrhs \<equiv> 
+        (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
 
 text {*
   @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every 
@@ -439,7 +462,7 @@
 *}
 
 definition
-  "subst_op_all ES X xrhs \<equiv> {(Y, subst_op yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
+  "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
 
 section {* While-combinator *}
@@ -454,7 +477,7 @@
 
 definition
   "remove_op ES Y yrhs \<equiv> 
-      subst_op_all  (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)"
+      Subst_all  (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"
 
 text {*
   The following term @{text "iterm X ES"} represents one iteration in the while loop.
@@ -760,20 +783,19 @@
   the correctness of the iteration step @{text "iter X ES"} is proved.
 *}
 
-lemma arden_op_keeps_eq:
+lemma Arden_keeps_eq:
   assumes l_eq_r: "X = L rhs"
   and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
   and finite: "finite rhs"
-  shows "X = L (arden_op X rhs)"
+  shows "X = L (Arden X rhs)"
 proof -
   def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
-  def b \<equiv> "rhs - trns_of rhs X"
+  def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"
   def B \<equiv> "L b" 
   have "X = B ;; A\<star>"
   proof-
-    have "L rhs = L(trns_of rhs X \<union> b)" by (auto simp: b_def trns_of_def)
+    have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
     also have "\<dots> = X ;; A \<union> B"
-      unfolding trns_of_def
       unfolding L_rhs_union_distrib[symmetric]
       by (simp only: lang_of_rexp_of finite B_def A_def)
     finally show ?thesis
@@ -783,8 +805,8 @@
       apply(simp)
       done
   qed
-  moreover have "L (arden_op X rhs) = (B ;; A\<star>)"
-    by (simp only:arden_op_def L_rhs_union_distrib lang_of_append_rhs 
+  moreover have "L (Arden X rhs) = B ;; A\<star>"
+    by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs 
                   B_def A_def b_def L_rexp.simps seq_union_distrib_left)
    ultimately show ?thesis by simp
 qed 
@@ -793,9 +815,9 @@
   "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
 by (auto simp:append_rhs_rexp_def)
 
-lemma arden_op_keeps_finite:
-  "finite rhs \<Longrightarrow> finite (arden_op X rhs)"
-by (auto simp:arden_op_def append_keeps_finite)
+lemma Arden_keeps_finite:
+  "finite rhs \<Longrightarrow> finite (Arden X rhs)"
+by (auto simp:Arden_def append_keeps_finite)
 
 lemma append_keeps_nonempty:
   "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)"
@@ -810,32 +832,31 @@
   "\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')"
 by (auto simp:rhs_nonempty_def)
 
-lemma arden_op_keeps_nonempty:
-  "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (arden_op X rhs)"
-by (simp only:arden_op_def append_keeps_nonempty nonempty_set_sub)
+lemma Arden_keeps_nonempty:
+  "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (Arden X rhs)"
+by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub)
 
 
-lemma subst_op_keeps_nonempty:
-  "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (subst_op rhs X xrhs)"
-by (simp only:subst_op_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)
+lemma Subst_keeps_nonempty:
+  "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (Subst rhs X xrhs)"
+by (simp only:Subst_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)
 
-lemma subst_op_keeps_eq:
+lemma Subst_keeps_eq:
   assumes substor: "X = L xrhs"
   and finite: "finite rhs"
-  shows "L (subst_op rhs X xrhs) = L rhs" (is "?Left = ?Right")
+  shows "L (Subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
 proof-
-  def A \<equiv> "L (rhs - trns_of rhs X)"
+  def A \<equiv> "L (rhs - {Trn X r | r. Trn X r \<in> rhs})"
   have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
-    unfolding subst_op_def
+    unfolding Subst_def
     unfolding L_rhs_union_distrib[symmetric]
     by (simp add: A_def)
   moreover have "?Right = A \<union> L ({Trn X r | r. Trn X r \<in> rhs})"
   proof-
-    have "rhs = (rhs - trns_of rhs X) \<union> (trns_of rhs X)" by (auto simp add: trns_of_def)
+    have "rhs = (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> ({Trn X r | r. Trn X r \<in> rhs})" by auto
     thus ?thesis 
       unfolding A_def
       unfolding L_rhs_union_distrib
-      unfolding trns_of_def
       by simp
   qed
   moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" 
@@ -843,29 +864,29 @@
   ultimately show ?thesis by simp
 qed
 
-lemma subst_op_keeps_finite_rhs:
-  "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (subst_op rhs Y yrhs)"
-by (auto simp:subst_op_def append_keeps_finite)
+lemma Subst_keeps_finite_rhs:
+  "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
+by (auto simp:Subst_def append_keeps_finite)
 
-lemma subst_op_all_keeps_finite:
+lemma Subst_all_keeps_finite:
   assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)"
-  shows "finite (subst_op_all ES Y yrhs)"
+  shows "finite (Subst_all ES Y yrhs)"
 proof -
-  have "finite {(Ya, subst_op yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" 
+  have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" 
                                                                   (is "finite ?A")
   proof-
     def eqns' \<equiv> "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \<in> ES}"
-    def h \<equiv> "\<lambda> ((Ya::string set), yrhsa). (Ya, subst_op yrhsa Y yrhs)"
+    def h \<equiv> "\<lambda> ((Ya::string set), yrhsa). (Ya, Subst yrhsa Y yrhs)"
     have "finite (h ` eqns')" using finite h_def eqns'_def by auto
     moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def)
     ultimately show ?thesis by auto      
   qed
-  thus ?thesis by (simp add:subst_op_all_def)
+  thus ?thesis by (simp add:Subst_all_def)
 qed
 
-lemma subst_op_all_keeps_finite_rhs:
-  "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (subst_op_all ES Y yrhs)"
-by (auto intro:subst_op_keeps_finite_rhs simp add:subst_op_all_def finite_rhs_def)
+lemma Subst_all_keeps_finite_rhs:
+  "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
+by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
 
 lemma append_rhs_keeps_cls:
   "classes_of (append_rhs_rexp rhs r) = classes_of rhs"
@@ -873,61 +894,61 @@
 apply (case_tac xa, auto simp:image_def)
 by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
 
-lemma arden_op_removes_cl:
-  "classes_of (arden_op Y yrhs) = classes_of yrhs - {Y}"
-apply (simp add:arden_op_def append_rhs_keeps_cls trns_of_def)
+lemma Arden_removes_cl:
+  "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}"
+apply (simp add:Arden_def append_rhs_keeps_cls)
 by (auto simp:classes_of_def)
 
 lemma lefts_of_keeps_cls:
-  "lefts_of (subst_op_all ES Y yrhs) = lefts_of ES"
-by (auto simp:lefts_of_def subst_op_all_def)
+  "lefts_of (Subst_all ES Y yrhs) = lefts_of ES"
+by (auto simp:lefts_of_def Subst_all_def)
 
-lemma subst_op_updates_cls:
+lemma Subst_updates_cls:
   "X \<notin> classes_of xrhs \<Longrightarrow> 
-      classes_of (subst_op rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
-apply (simp only:subst_op_def append_rhs_keeps_cls 
+      classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
+apply (simp only:Subst_def append_rhs_keeps_cls 
                               classes_of_union_distrib[THEN sym])
-by (auto simp:classes_of_def trns_of_def)
+by (auto simp:classes_of_def)
 
-lemma subst_op_all_keeps_self_contained:
+lemma Subst_all_keeps_self_contained:
   fixes Y
   assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
-  shows "self_contained (subst_op_all ES Y (arden_op Y yrhs))" 
+  shows "self_contained (Subst_all ES Y (Arden Y yrhs))" 
                                                    (is "self_contained ?B")
 proof-
   { fix X xrhs'
     assume "(X, xrhs') \<in> ?B"
     then obtain xrhs 
-      where xrhs_xrhs': "xrhs' = subst_op xrhs Y (arden_op Y yrhs)"
-      and X_in: "(X, xrhs) \<in> ES" by (simp add:subst_op_all_def, blast)    
+      where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
+      and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast)    
     have "classes_of xrhs' \<subseteq> lefts_of ?B"
     proof-
-      have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def subst_op_all_def)
+      have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def Subst_all_def)
       moreover have "classes_of xrhs' \<subseteq> lefts_of ES"
       proof-
         have "classes_of xrhs' \<subseteq> 
-                        classes_of xrhs \<union> classes_of (arden_op Y yrhs) - {Y}"
+                        classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
         proof-
-          have "Y \<notin> classes_of (arden_op Y yrhs)" 
-            using arden_op_removes_cl by simp
-          thus ?thesis using xrhs_xrhs' by (auto simp:subst_op_updates_cls)
+          have "Y \<notin> classes_of (Arden Y yrhs)" 
+            using Arden_removes_cl by simp
+          thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
         qed
         moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc
           apply (simp only:self_contained_def lefts_of_union_distrib[THEN sym])
           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
-        moreover have "classes_of (arden_op Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" 
+        moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" 
           using sc 
-          by (auto simp add:arden_op_removes_cl self_contained_def lefts_of_def)
+          by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def)
         ultimately show ?thesis by auto
       qed
       ultimately show ?thesis by simp
     qed
-  } thus ?thesis by (auto simp only:subst_op_all_def self_contained_def)
+  } thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
 qed
 
-lemma subst_op_all_satisfy_invariant:
+lemma Subst_all_satisfy_invariant:
   assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
-  shows "invariant (subst_op_all ES Y (arden_op Y yrhs))"
+  shows "invariant (Subst_all ES Y (Arden Y yrhs))"
 proof -  
   have finite_yrhs: "finite yrhs" 
     using invariant_ES by (auto simp:invariant_def finite_rhs_def)
@@ -935,66 +956,66 @@
     using invariant_ES by (auto simp:invariant_def ardenable_def)
   have Y_eq_yrhs: "Y = L yrhs" 
     using invariant_ES by (simp only:invariant_def valid_eqns_def, blast)
-  have "distinct_equas (subst_op_all ES Y (arden_op Y yrhs))" 
+  have "distinct_equas (Subst_all ES Y (Arden Y yrhs))" 
     using invariant_ES
-    by (auto simp:distinct_equas_def subst_op_all_def invariant_def)
-  moreover have "finite (subst_op_all ES Y (arden_op Y yrhs))" 
-    using invariant_ES by (simp add:invariant_def subst_op_all_keeps_finite)
-  moreover have "finite_rhs (subst_op_all ES Y (arden_op Y yrhs))"
+    by (auto simp:distinct_equas_def Subst_all_def invariant_def)
+  moreover have "finite (Subst_all ES Y (Arden Y yrhs))" 
+    using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
+  moreover have "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
   proof-
     have "finite_rhs ES" using invariant_ES 
       by (simp add:invariant_def finite_rhs_def)
-    moreover have "finite (arden_op Y yrhs)"
+    moreover have "finite (Arden Y yrhs)"
     proof -
       have "finite yrhs" using invariant_ES 
         by (auto simp:invariant_def finite_rhs_def)
-      thus ?thesis using arden_op_keeps_finite by simp
+      thus ?thesis using Arden_keeps_finite by simp
     qed
     ultimately show ?thesis 
-      by (simp add:subst_op_all_keeps_finite_rhs)
+      by (simp add:Subst_all_keeps_finite_rhs)
   qed
-  moreover have "ardenable (subst_op_all ES Y (arden_op Y yrhs))"
+  moreover have "ardenable (Subst_all ES Y (Arden Y yrhs))"
   proof - 
     { fix X rhs
       assume "(X, rhs) \<in> ES"
       hence "rhs_nonempty rhs"  using prems invariant_ES  
         by (simp add:invariant_def ardenable_def)
       with nonempty_yrhs 
-      have "rhs_nonempty (subst_op rhs Y (arden_op Y yrhs))"
+      have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
         by (simp add:nonempty_yrhs 
-               subst_op_keeps_nonempty arden_op_keeps_nonempty)
-    } thus ?thesis by (auto simp add:ardenable_def subst_op_all_def)
+               Subst_keeps_nonempty Arden_keeps_nonempty)
+    } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
   qed
-  moreover have "valid_eqns (subst_op_all ES Y (arden_op Y yrhs))"
+  moreover have "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
   proof-
-    have "Y = L (arden_op Y yrhs)" 
+    have "Y = L (Arden Y yrhs)" 
       using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs      
-      by (rule_tac arden_op_keeps_eq, (simp add:rexp_of_empty)+)
+      by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
     thus ?thesis using invariant_ES 
       by (clarsimp simp add:valid_eqns_def 
-              subst_op_all_def subst_op_keeps_eq invariant_def finite_rhs_def
+              Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
                    simp del:L_rhs.simps)
   qed
   moreover 
-  have self_subst: "self_contained (subst_op_all ES Y (arden_op Y yrhs))"
-    using invariant_ES subst_op_all_keeps_self_contained by (simp add:invariant_def)
+  have self_subst: "self_contained (Subst_all ES Y (Arden Y yrhs))"
+    using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
   ultimately show ?thesis using invariant_ES by (simp add:invariant_def)
 qed
 
-lemma subst_op_all_card_le: 
+lemma Subst_all_card_le: 
   assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
-  shows "card (subst_op_all ES Y yrhs) <= card ES"
+  shows "card (Subst_all ES Y yrhs) <= card ES"
 proof-
-  def f \<equiv> "\<lambda> x. ((fst x)::string set, subst_op (snd x) Y yrhs)"
-  have "subst_op_all ES Y yrhs = f ` ES" 
-    apply (auto simp:subst_op_all_def f_def image_def)
+  def f \<equiv> "\<lambda> x. ((fst x)::string set, Subst (snd x) Y yrhs)"
+  have "Subst_all ES Y yrhs = f ` ES" 
+    apply (auto simp:Subst_all_def f_def image_def)
     by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+)
   thus ?thesis using finite by (auto intro:card_image_le)
 qed
 
-lemma subst_op_all_cls_remains: 
-  "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (subst_op_all ES Y yrhs)"
-by (auto simp:subst_op_all_def)
+lemma Subst_all_cls_remains: 
+  "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
+by (auto simp:Subst_all_def)
 
 lemma card_noteq_1_has_more:
   assumes card:"card S \<noteq> 1"
@@ -1031,35 +1052,35 @@
       by (auto simp: invariant_def distinct_equas_def)
   next
     fix x
-    let ?ES' = "let (Y, yrhs) = x in subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)"
+    let ?ES' = "let (Y, yrhs) = x in Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"
     assume prem: "case x of (Y, yrhs) \<Rightarrow> (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)"
     thus "invariant (?ES') \<and> (\<exists>xrhs'. (X, xrhs') \<in> ?ES') \<and> (?ES', ES) \<in> measure card"
     proof(cases "x", simp)
       fix Y yrhs
       assume h: "(Y, yrhs) \<in> ES \<and>  X \<noteq> Y" 
-      show "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and>
-             (\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and>
-             card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES"
+      show "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
+             (\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
+             card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
       proof -
-        have "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))" 
-        proof(rule subst_op_all_satisfy_invariant)
+        have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))" 
+        proof(rule Subst_all_satisfy_invariant)
           from h have "(Y, yrhs) \<in> ES" by simp
           hence "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
           with Inv_ES show "invariant (ES - {(Y, yrhs)} \<union> {(Y, yrhs)})" by auto
         qed
         moreover have 
-          "(\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))"
-        proof(rule subst_op_all_cls_remains)
+          "(\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))"
+        proof(rule Subst_all_cls_remains)
           from X_in_ES and h
           show "(X, xrhs) \<in> ES - {(Y, yrhs)}" by auto
         qed
         moreover have 
-          "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES"
+          "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
         proof(rule le_less_trans)
           show 
-            "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<le> 
+            "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<le> 
                                                                 card (ES - {(Y, yrhs)})"
-          proof(rule subst_op_all_card_le)
+          proof(rule Subst_all_card_le)
             show "finite (ES - {(Y, yrhs)})" using finite_ES by auto
           qed
         next
@@ -1067,7 +1088,7 @@
             by (auto simp:card_gt_0_iff intro:diff_Suc_less)
         qed
         ultimately show ?thesis 
-          by (auto dest: subst_op_all_card_le elim:le_less_trans)
+          by (auto dest: Subst_all_card_le elim:le_less_trans)
       qed
     qed
   qed
@@ -1126,7 +1147,7 @@
   assumes Inv_ES: "invariant {(X, xrhs)}"
   shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
 proof-
-  def A \<equiv> "arden_op X xrhs"
+  def A \<equiv> "Arden X xrhs"
   have "?P (\<Uplus>{r. Lam r \<in> A})"
   proof -
     have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
@@ -1134,7 +1155,7 @@
       show "finite A" 
 	unfolding A_def
 	using Inv_ES
-        by (rule_tac arden_op_keeps_finite) 
+        by (rule_tac Arden_keeps_finite) 
            (auto simp add: invariant_def finite_rhs_def)
     qed
     also have "\<dots> = L A"
@@ -1143,7 +1164,7 @@
       proof-
         have "classes_of A = {}" using Inv_ES 
 	  unfolding A_def
-          by (simp add:arden_op_removes_cl 
+          by (simp add:Arden_removes_cl 
                        self_contained_def invariant_def lefts_of_def) 
         thus ?thesis
 	  unfolding A_def
@@ -1153,7 +1174,7 @@
     qed
     also have "\<dots> = X"
     unfolding A_def
-    proof(rule arden_op_keeps_eq [THEN sym])
+    proof(rule Arden_keeps_eq [THEN sym])
       show "X = L xrhs" using Inv_ES 
         by (auto simp only: invariant_def valid_eqns_def)  
     next

--- a/Paper/Paper.thy	Thu Feb 10 08:40:38 2011 +0000
+++ b/Paper/Paper.thy	Thu Feb 10 12:32:45 2011 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Myhill" "LaTeXsugar"
+imports "../Myhill" "LaTeXsugar" 
 begin
 
 declare [[show_question_marks = false]]
@@ -499,20 +499,28 @@
   \noindent
   which we also lift to entire right-hand sides of equations, written as
   @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
-  the \emph{arden-operation}, which takes an equivalence class @{text X} and
-  a rhs of an equation.
-
+  the \emph{arden-operation} for an equation of the form @{text "X = rhs"}:
+  
   \begin{center}
-  @{thm arden_op_def}
+  \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+  @{thm (lhs) Arden_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 "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+   & &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\ 
+  \end{tabular}
   \end{center}
 
   \noindent
-  The term left of $\triangleright$ deletes all terms of the form @{text "(X, r)"};
-  the term on the right calculates first the combinded regular expressions for all
-  @{text r} in the @{text "(X, r)"}, forms the star and appends it to the remaining
-  terms in the @{text rhs}. It can be easily seen that this operation mimics Arden's
-  lemma on the level of equations.
+  We first delete all terms of the form @{text "(X, r)"} from @{text rhs};
+  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.
   
+
+  \begin{center}
+  @{thm Subst_def}
+  \end{center}
 *}
 
 section {* Regular Expressions Generate Finitely Many Partitions *}

--- a/Paper/document/root.tex	Thu Feb 10 08:40:38 2011 +0000
+++ b/Paper/document/root.tex	Thu Feb 10 12:32:45 2011 +0000
@@ -26,7 +26,7 @@
 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
 
-\newcommand{\bigplus}{\mbox{\large\bf$+$}}
+\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
 \begin{document}
 
 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular