# HG changeset patch
# User urbanc
# Date 1297371640 0
# Node ID 3b9deda4f45960f65a94f3fa0836758aa2054b99
# Parent  9540c2f2ea778ac8efffc43e382e9d234980e918
simplified a bit the proof

diff -r 9540c2f2ea77 -r 3b9deda4f459 Myhill_1.thy
--- a/Myhill_1.thy	Thu Feb 10 13:10:16 2011 +0000
+++ b/Myhill_1.thy	Thu Feb 10 21:00:40 2011 +0000
@@ -402,6 +402,13 @@
      "L_rhs rhs = \<Union> (L ` rhs)"
 end
 
+lemma L_rhs_union_distrib:
+  fixes A B::"rhs_item set"
+  shows "L A \<union> L B = L (A \<union> B)"
+by simp
+
+
+
 text {* Transitions between equivalence classes *}
 
 definition 
@@ -412,14 +419,14 @@
 text {* Initial equational system *}
 
 definition
-  "init_rhs CS X \<equiv>  
+  "Init_rhs CS X \<equiv>  
       if ([] \<in> X) then 
           {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
       else 
           {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
 definition 
-  "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
+  "Init CS \<equiv> {(X, Init_rhs CS X) | X.  X \<in> CS}"
 
 
 
@@ -464,9 +471,6 @@
 definition
   "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
-
-section {* While-combinator *}
-
 text {*
   The following term @{text "remove ES Y yrhs"} removes the equation
   @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
@@ -476,30 +480,33 @@
   *}
 
 definition
-  "Remove ES Y yrhs \<equiv> 
-      Subst_all  (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"
+  "Remove ES X xrhs \<equiv> 
+      Subst_all  (ES - {(X, xrhs)}) X (Arden X xrhs)"
+
+
+section {* While-combinator *}
 
 text {*
-  The following term @{text "iterm X ES"} represents one iteration in the while loop.
+  The following term @{text "Iter X ES"} represents one iteration in the while loop.
   It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
 *}
 
 definition 
-  "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)
+  "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
                 in Remove ES Y yrhs)"
 
 text {*
-  The following term @{text "reduce X ES"} repeatedly removes characteriztion equations
+  The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
   for unknowns other than @{text "X"} until one is left.
 *}
 
 definition 
-  "reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (iter X) ES"
+  "Reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (Iter X) ES"
 
 text {*
-  Since the @{text "while"} combinator from HOL library is used to implement @{text "reduce X ES"},
+  Since the @{text "while"} combinator from HOL library is used to implement @{text "Reduce X ES"},
   the induction principle @{thm [source] while_rule} is used to proved the desired properties
-  of @{text "reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
+  of @{text "Reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
   in terms of a series of auxilliary predicates:
 *}
 
@@ -573,6 +580,13 @@
   "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
                   finite_rhs ES \<and> self_contained ES"
 
+
+lemma invariantI:
+  assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES" 
+          "finite_rhs ES" "self_contained ES"
+  shows "invariant ES"
+using assms by (simp add: invariant_def)
+
 subsection {* The proof of this direction *}
 
 subsubsection {* Basic properties *}
@@ -581,10 +595,6 @@
   The following are some basic properties of the above definitions.
 *}
 
-lemma L_rhs_union_distrib:
-  fixes A B::"rhs_item set"
-  shows "L A \<union> L B = L (A \<union> B)"
-by simp
 
 lemma finite_Trn:
   assumes fin: "finite rhs"
@@ -601,7 +611,7 @@
 qed
 
 lemma finite_Lam:
-  assumes fin:"finite rhs"
+  assumes fin: "finite rhs"
   shows "finite {r. Lam r \<in> rhs}"
 proof -
   have "finite {Lam r | r. Lam r \<in> rhs}"
@@ -614,16 +624,13 @@
 qed
 
 lemma rexp_of_empty:
-  assumes finite:"finite rhs"
-  and nonempty:"rhs_nonempty rhs"
+  assumes finite: "finite rhs"
+  and nonempty: "rhs_nonempty rhs"
   shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
 using finite nonempty rhs_nonempty_def
 using finite_Trn[OF finite]
 by (auto)
 
-lemma [intro!]:
-  "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto
-
 lemma lang_of_rexp_of:
   assumes finite:"finite rhs"
   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
@@ -632,41 +639,30 @@
     by (rule finite_Trn[OF finite]) 
   then show ?thesis
     apply(auto simp add: Seq_def)
-    apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
+    apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI)
+    apply(auto)
     apply(rule_tac x= "Trn X xa" in exI)
-    apply(auto simp: Seq_def)
+    apply(auto simp add: Seq_def)
     done
 qed
 
-lemma rexp_of_lam_eq_lam_set:
-  assumes fin: "finite rhs"
-  shows "L (\<Uplus>{r. Lam r \<in> rhs}) = L ({Lam r | r. Lam r \<in> rhs})"
-proof -
-  have "finite ({r. Lam r \<in> rhs})" using fin by (rule finite_Lam)
-  then show ?thesis by auto
-qed
-
-lemma [simp]:
-  "L (append_rexp r xb) = L xb ;; L r"
-apply (cases xb, auto simp: Seq_def)
-apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)
-apply(auto simp: Seq_def)
-done
+lemma lang_of_append:
+  "L (append_rexp r rhs_item) = L rhs_item ;; L r"
+by (induct rule: append_rexp.induct)
+   (auto simp add: seq_assoc)
 
 lemma lang_of_append_rhs:
   "L (append_rhs_rexp rhs r) = L rhs ;; L r"
-apply (auto simp:append_rhs_rexp_def image_def)
-apply (auto simp:Seq_def)
-apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def)
-by (rule_tac x = "append_rexp r xb" in exI, auto simp:Seq_def)
+unfolding append_rhs_rexp_def
+by (auto simp add: Seq_def lang_of_append)
 
 lemma classes_of_union_distrib:
-  "classes_of A \<union> classes_of B = classes_of (A \<union> B)"
-by (auto simp add:classes_of_def)
+  shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
+by (auto simp add: classes_of_def)
 
 lemma lefts_of_union_distrib:
-  "lefts_of A \<union> lefts_of B = lefts_of (A \<union> B)"
-by (auto simp:lefts_of_def)
+  shows "lefts_of (A \<union> B) = lefts_of A \<union> lefts_of B"
+by (auto simp add: lefts_of_def)
 
 
 subsubsection {* Intialization *}
@@ -702,7 +698,7 @@
 qed
 
 lemma l_eq_r_in_eqs:
-  assumes X_in_eqs: "(X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"
+  assumes X_in_eqs: "(X, xrhs) \<in> (Init (UNIV // (\<approx>Lang)))"
   shows "X = L xrhs"
 proof 
   show "X \<subseteq> L xrhs"
@@ -713,12 +709,12 @@
     proof (cases "x = []")
       assume empty: "x = []"
       thus ?thesis using X_in_eqs "(1)"
-        by (auto simp:eqs_def init_rhs_def)
+        by (auto simp: Init_def Init_rhs_def)
     next
       assume not_empty: "x \<noteq> []"
       then obtain clist c where decom: "x = clist @ [c]"
         by (case_tac x rule:rev_cases, auto)
-      have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:eqs_def)
+      have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:Init_def)
       then obtain Y 
         where "Y \<in> UNIV // (\<approx>Lang)" 
         and "Y ;; {[c]} \<subseteq> X"
@@ -730,17 +726,17 @@
 	using "(1)" decom
         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
       thus ?thesis using X_in_eqs "(1)"	
-        by (simp add: eqs_def init_rhs_def)
+        by (simp add: Init_def Init_rhs_def)
     qed
   qed
 next
   show "L xrhs \<subseteq> X" using X_in_eqs
-    by (auto simp:eqs_def init_rhs_def transition_def) 
+    by (auto simp:Init_def Init_rhs_def transition_def) 
 qed
 
-lemma finite_init_rhs: 
+lemma finite_Init_rhs: 
   assumes finite: "finite CS"
-  shows "finite (init_rhs CS X)"
+  shows "finite (Init_rhs CS X)"
 proof-
   have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A")
   proof -
@@ -753,34 +749,36 @@
     ultimately show ?thesis 
       by auto
   qed
-  thus ?thesis by (simp add:init_rhs_def transition_def)
+  thus ?thesis by (simp add:Init_rhs_def transition_def)
 qed
 
-lemma init_ES_satisfy_invariant:
-  assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
-  shows "invariant (eqs (UNIV // (\<approx>Lang)))"
-proof -
-  have "finite (eqs (UNIV // (\<approx>Lang)))" using finite_CS
-    by (simp add:eqs_def)
-  moreover have "distinct_equas (eqs (UNIV // (\<approx>Lang)))"     
-    by (simp add:distinct_equas_def eqs_def)
-  moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))"
-    by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps)
-  moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))"
-    using l_eq_r_in_eqs by (simp add:valid_eqns_def)
-  moreover have "finite_rhs (eqs (UNIV // (\<approx>Lang)))"
-    using finite_init_rhs[OF finite_CS] 
-    by (auto simp:finite_rhs_def eqs_def)
-  moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))"
-    by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)
-  ultimately show ?thesis by (simp add:invariant_def)
+lemma Init_ES_satisfies_invariant:
+  assumes finite_CS: "finite (UNIV // \<approx>A)"
+  shows "invariant (Init (UNIV // \<approx>A))"
+proof (rule invariantI)
+  show "valid_eqns (Init (UNIV // \<approx>A))"
+    unfolding valid_eqns_def 
+    using l_eq_r_in_eqs by simp
+  show "finite (Init (UNIV // \<approx>A))" using finite_CS
+    unfolding Init_def by simp
+  show "distinct_equas (Init (UNIV // \<approx>A))"     
+    unfolding distinct_equas_def Init_def by simp
+  show "ardenable (Init (UNIV // \<approx>A))"
+    unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def
+    by auto
+  show "finite_rhs (Init (UNIV // \<approx>A))"
+    using finite_Init_rhs[OF finite_CS]
+    unfolding finite_rhs_def Init_def by auto
+  show "self_contained (Init (UNIV // \<approx>A))"
+    unfolding self_contained_def Init_def Init_rhs_def classes_of_def lefts_of_def
+    by auto
 qed
 
 subsubsection {* Interation step *}
 
 text {*
   From this point until @{text "iteration_step"}, 
-  the correctness of the iteration step @{text "iter X ES"} is proved.
+  the correctness of the iteration step @{text "Iter X ES"} is proved.
 *}
 
 lemma Arden_keeps_eq:
@@ -906,8 +904,7 @@
 lemma Subst_updates_cls:
   "X \<notin> classes_of xrhs \<Longrightarrow> 
       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])
+apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib)
 by (auto simp:classes_of_def)
 
 lemma Subst_all_keeps_self_contained:
@@ -933,7 +930,7 @@
           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])
+          apply (simp only:self_contained_def lefts_of_union_distrib)
           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
         moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" 
           using sc 
@@ -945,22 +942,44 @@
   } thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
 qed
 
-lemma Subst_all_satisfy_invariant:
+lemma Subst_all_satisfies_invariant:
   assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
   shows "invariant (Subst_all ES Y (Arden Y yrhs))"
-proof -  
-  have finite_yrhs: "finite yrhs" 
+proof (rule invariantI)
+  have Y_eq_yrhs: "Y = L yrhs" 
+    using invariant_ES by (simp only:invariant_def valid_eqns_def, blast)
+   have finite_yrhs: "finite yrhs" 
     using invariant_ES by (auto simp:invariant_def finite_rhs_def)
   have nonempty_yrhs: "rhs_nonempty yrhs" 
     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_all ES Y (Arden Y yrhs))" 
+  show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
+  proof-
+    have "Y = L (Arden Y yrhs)" 
+      using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
+      by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
+    thus ?thesis using invariant_ES 
+      by (clarsimp simp add:valid_eqns_def 
+        Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
+        simp del:L_rhs.simps)
+  qed
+  show "finite (Subst_all ES Y (Arden Y yrhs))" 
+    using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
+  show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" 
     using invariant_ES
     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))"
+  show "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 rhs Y (Arden Y yrhs))"
+        by (simp add:nonempty_yrhs 
+               Subst_keeps_nonempty Arden_keeps_nonempty)
+    } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
+  qed
+  show "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)
@@ -973,32 +992,8 @@
     ultimately show ?thesis 
       by (simp add:Subst_all_keeps_finite_rhs)
   qed
-  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 rhs Y (Arden Y yrhs))"
-        by (simp add:nonempty_yrhs 
-               Subst_keeps_nonempty Arden_keeps_nonempty)
-    } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
-  qed
-  moreover have "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
-  proof-
-    have "Y = L (Arden Y yrhs)" 
-      using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs      
-      by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
-    thus ?thesis using invariant_ES 
-      by (clarsimp simp add:valid_eqns_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_all ES Y (Arden Y yrhs))"
+  show "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_all_card_le: 
@@ -1036,16 +1031,16 @@
   assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
   and    not_T: "card ES \<noteq> 1"
-  shows "(invariant (iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (iter X ES)) \<and> 
-                (iter X ES, ES) \<in> measure card)"
+  shows "(invariant (Iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (Iter X ES)) \<and> 
+                (Iter X ES, ES) \<in> measure card)"
 proof -
   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
   then obtain Y yrhs 
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
     using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto)
-  let ?ES' = "iter X ES"
+  let ?ES' = "Iter X ES"
   show ?thesis
-  proof(unfold iter_def Remove_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)
@@ -1062,7 +1057,7 @@
              card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
       proof -
         have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))" 
-        proof(rule Subst_all_satisfy_invariant)
+        proof(rule Subst_all_satisfies_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
@@ -1104,11 +1099,11 @@
 lemma reduce_x:
   assumes inv: "invariant ES"
   and contain_x: "(X, xrhs) \<in> ES" 
-  shows "\<exists> xrhs'. reduce X ES = {(X, xrhs')} \<and> invariant(reduce X ES)"
+  shows "\<exists> xrhs'. Reduce X ES = {(X, xrhs')} \<and> invariant(Reduce X ES)"
 proof -
   let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
   show ?thesis
-  proof (unfold reduce_def, 
+  proof (unfold Reduce_def, 
          rule while_rule [where P = ?Inv and r = "measure card"])
     from inv and contain_x show "?Inv ES" by auto
   next
@@ -1116,7 +1111,7 @@
   next
     fix ES
     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
-    show "(iter X ES, ES) \<in> measure card"
+    show "(Iter X ES, ES) \<in> measure card"
     proof -
       from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
       from inv have "invariant ES" by simp
@@ -1126,7 +1121,7 @@
   next
     fix ES
     assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
-    thus "?Inv (iter X ES)" 
+    thus "?Inv (Iter X ES)" 
     proof -
       from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
       from inv have "invariant ES" by simp
@@ -1144,91 +1139,89 @@
 
 lemma last_cl_exists_rexp:
   assumes Inv_ES: "invariant {(X, xrhs)}"
-  shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
+  shows "\<exists>r::rexp. L r = X" 
 proof-
   def A \<equiv> "Arden X xrhs"
-  have "?P (\<Uplus>{r. Lam r \<in> A})"
+  have eq: "{Lam r | r. Lam r \<in> A} = A"
   proof -
-    have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
-    proof(rule rexp_of_lam_eq_lam_set)
-      show "finite A" 
-	unfolding A_def
-	using Inv_ES
-        by (rule_tac Arden_keeps_finite) 
-           (auto simp add: invariant_def finite_rhs_def)
-    qed
-    also have "\<dots> = L A"
-    proof-
-      have "{Lam r | r. Lam r \<in> A} = A"
-      proof-
-        have "classes_of A = {}" using Inv_ES 
-	  unfolding A_def
-          by (simp add:Arden_removes_cl 
-                       self_contained_def invariant_def lefts_of_def) 
-        thus ?thesis
-	  unfolding A_def
-          by (auto simp only: classes_of_def, case_tac x, auto)
-      qed
-      thus ?thesis by simp
-    qed
-    also have "\<dots> = X"
-    unfolding A_def
-    proof(rule Arden_keeps_eq [THEN sym])
-      show "X = L xrhs" using Inv_ES 
-        by (auto simp only: invariant_def valid_eqns_def)  
-    next
-      from Inv_ES show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
-        by(simp add: invariant_def ardenable_def rexp_of_empty finite_rhs_def)
-    next
-      from Inv_ES show "finite xrhs" 
-        by (simp add: invariant_def finite_rhs_def)
-    qed
-    finally show ?thesis by simp
+    have "classes_of A = {}" using Inv_ES 
+      unfolding A_def self_contained_def invariant_def lefts_of_def
+      by (simp add: Arden_removes_cl) 
+    thus ?thesis unfolding A_def classes_of_def
+      apply(auto simp only:)
+      apply(case_tac x)
+      apply(auto)
+      done
   qed
-  thus ?thesis by auto
+  have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
+    using Arden_keeps_finite by auto
+  then have "finite {r. Lam r \<in> A}" by (rule finite_Lam)
+  then have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
+    by auto
+  also have "\<dots> = L A" by (simp add: eq)
+  also have "\<dots> = X" 
+  proof -
+    have "X = L xrhs" using Inv_ES unfolding invariant_def valid_eqns_def
+      by auto
+    moreover
+    from Inv_ES have "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
+      unfolding invariant_def ardenable_def finite_rhs_def
+      by(simp add: rexp_of_empty)
+    moreover
+    from Inv_ES have "finite xrhs"  unfolding invariant_def finite_rhs_def
+      by simp
+    ultimately show "L A = X" unfolding A_def
+      by (rule  Arden_keeps_eq[symmetric])
+  qed
+  finally have "L (\<Uplus>{r. Lam r \<in> A}) = X" .
+  then show "\<exists>r::rexp. L r = X" by blast
 qed
 
 lemma every_eqcl_has_reg: 
-  assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
-  and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))"
-  shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")
+  assumes finite_CS: "finite (UNIV // \<approx>A)"
+  and X_in_CS: "X \<in> (UNIV // \<approx>A)"
+  shows "\<exists>r::rexp. L r = X"
 proof -
-  let ?ES = " eqs (UNIV // \<approx>Lang)"
-  from X_in_CS 
-  obtain xrhs where "(X, xrhs) \<in> ?ES"
-    by (auto simp:eqs_def init_rhs_def)
-  from reduce_x [OF init_ES_satisfy_invariant [OF finite_CS] this]
-  have "\<exists>xrhs'. reduce X ?ES = {(X, xrhs')} \<and> invariant (reduce X ?ES)" .
-  then obtain xrhs' where "invariant {(X, xrhs')}" by auto
-  from last_cl_exists_rexp [OF this]
-  show ?thesis .
+  def ES \<equiv> "Init (UNIV // \<approx>A)"
+  have "invariant ES" using finite_CS unfolding ES_def
+    by (rule Init_ES_satisfies_invariant)
+  moreover
+  from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def
+    unfolding Init_def Init_rhs_def by auto
+  ultimately
+  obtain xrhs' where "Reduce X ES = {(X, xrhs')}" "invariant (Reduce X ES)"
+    using reduce_x by blast
+  then show "\<exists>r::rexp. L r = X"
+  using last_cl_exists_rexp by auto
 qed
 
 
-theorem hard_direction: 
+lemma bchoice_finite_set:
+  assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" 
+  and     b: "finite S"
+  shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys"
+using bchoice[OF a] b
+apply(erule_tac exE)
+apply(rule_tac x="fa ` S" in exI)
+apply(auto)
+done
+
+theorem Myhill_Nerode1:
   assumes finite_CS: "finite (UNIV // \<approx>A)"
   shows   "\<exists>r::rexp. A = L r"
 proof -
-  have "\<forall> X \<in> (UNIV // \<approx>A). \<exists>reg::rexp. X = L reg" 
+  have f: "finite (finals A)" 
+    using finals_in_partitions finite_CS by (rule finite_subset)
+  have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r" 
     using finite_CS every_eqcl_has_reg by blast
-  then obtain f 
-    where f_prop: "\<forall> X \<in> (UNIV // \<approx>A). X = L ((f X)::rexp)"
-    by (auto dest: bchoice)
-  def rs \<equiv> "f ` (finals A)"  
-  have "A = \<Union> (finals A)" using lang_is_union_of_finals by auto
-  also have "\<dots> = L (\<Uplus>rs)" 
-  proof -
-    have "finite rs"
-    proof -
-      have "finite (finals A)" 
-        using finite_CS finals_in_partitions[of "A"]   
-        by (erule_tac finite_subset, simp)
-      thus ?thesis using rs_def by auto
-    qed
-    thus ?thesis 
-      using f_prop rs_def finals_in_partitions[of "A"] by auto
-  qed
-  finally show ?thesis by blast
+  then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r"
+    using finals_in_partitions by auto
+  then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs"
+    using f by (auto dest: bchoice_finite_set)
+  then have "A = L (\<Uplus>rs)" 
+    unfolding lang_is_union_of_finals[symmetric] by simp
+  then show "\<exists>r::rexp. A = L r" by blast
 qed 
 
+
 end
\ No newline at end of file
diff -r 9540c2f2ea77 -r 3b9deda4f459 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 10 13:10:16 2011 +0000
+++ b/Paper/Paper.thy	Thu Feb 10 21:00:40 2011 +0000
@@ -373,7 +373,7 @@
   the language is regular. In our setting we therefore have to show:
   
   \begin{theorem}\label{myhillnerodeone}
-  @{thm[mode=IfThen] hard_direction}
+  @{thm[mode=IfThen] Myhill_Nerode1}
   \end{theorem}
 
   \noindent
@@ -534,6 +534,19 @@
   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}.
+
+  We lift these two operation to work over equational systems @{text ES}: @{const Subst_all}
+  substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES}; 
+  @{const Remove} completely removes such an equaution from @{text ES} by substituting 
+  it to the rest of the equational system, but first removing all recursive occurences
+  of @{text X} by applying @{const Arden} to @{text "xrhs"}.
+
+  \begin{center}
+  \begin{tabular}{rcl}
+  @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
+  @{thm (lhs) Remove_def}    & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
+  \end{tabular}
+  \end{center}
 *}
 
 section {* Regular Expressions Generate Finitely Many Partitions *}