# HG changeset patch
# User wu
# Date 1293803273 0
# Node ID cef2893f353b5656ffea858629a33013d9f6c836
# Parent  90a57a533b0c51740bef95012fb486396fb1f235
Rewritten of hard direction once more. To make it looking better.

diff -r 90a57a533b0c -r cef2893f353b Myhill.thy
--- a/Myhill.thy	Tue Dec 14 14:31:31 2010 +0000
+++ b/Myhill.thy	Fri Dec 31 13:47:53 2010 +0000
@@ -15,6 +15,23 @@
   start[intro]: "[] \<in> L\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" 
 
+lemma seq_union_distrib:
+  "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
+by (auto simp:Seq_def)
+
+lemma seq_assoc:
+  "(A ;; B) ;; C = A ;; (B ;; C)"
+unfolding Seq_def
+apply(auto)
+apply(metis)
+by (metis append_assoc)
+
+lemma union_seq:
+  "\<Union> {f x y ;; z| x y. P x y } = (\<Union> {f x y|x y. P x y });; z"
+apply (auto simp add:Seq_def)
+apply metis
+done
+
 theorem ardens_revised:
   assumes nemp: "[] \<notin> A"
   shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)"
@@ -61,14 +78,11 @@
 where
   "folds f z S \<equiv> SOME x. fold_graph f z S x"
 
-lemma folds_simp_null [simp]:
-  "finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> L r)"
-apply (simp add: folds_def)
-apply (rule someI2_ex)
-apply (erule finite_imp_fold_graph)
-apply (erule fold_graph.induct)
-apply (auto)
-done
+lemma folds_alt_simp [simp]:
+  "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
+apply (rule set_ext, simp add:folds_def)
+apply (rule someI2_ex, erule finite_imp_fold_graph)
+by (erule fold_graph.induct, auto)
 
 lemma [simp]:
   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
@@ -84,71 +98,94 @@
 where
   "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"
 
+definition
+  final :: "string set \<Rightarrow> string set \<Rightarrow> bool"
+where
+  "final X Lang \<equiv> (X \<in> UNIV // \<approx>Lang) \<and> (\<forall>s \<in> X. s \<in> Lang)"
 
+lemma lang_is_union_of_finals: 
+  "Lang = \<Union> {X. final X Lang}"
+proof 
+  show "Lang \<subseteq> \<Union> {X. final X Lang}"
+  proof
+    fix x
+    assume "x \<in> Lang"   
+    thus "x \<in> \<Union> {X. final X Lang}"
+      apply (simp, rule_tac x = "(\<approx>Lang) `` {x}" in exI)      
+      apply (auto simp:final_def quotient_def Image_def str_eq_rel_def str_eq_def)
+      by (drule_tac x = "[]" in spec, simp)
+  qed
+next
+  show "\<Union>{X. final X Lang} \<subseteq> Lang"
+    by (auto simp:final_def)
+qed
 
 section {* finite \<Rightarrow> regular *}
 
-definition
-  transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
-where
-  "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"
+datatype rhs_item = 
+   Lam "rexp"                           (* Lambda *)
+ | Trn "string set" "rexp"              (* Transition *)
 
-definition
-  transitions_rexp ("_ \<turnstile>\<rightarrow> _")
-where
-  "Y \<turnstile>\<rightarrow> X \<equiv> folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"
+fun the_Trn:: "rhs_item \<Rightarrow> (string set \<times> rexp)"
+where "the_Trn (Trn Y r) = (Y, r)"
+
+fun the_r :: "rhs_item \<Rightarrow> rexp"
+where "the_r (Lam r) = r"
 
-definition
-  "init_rhs CS X \<equiv> if X = {[]} 
-                   then {({[]}, EMPTY)} 
-                   else if ([] \<in> X)
-                        then insert ({[]}, EMPTY) {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}
-                        else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"
+overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> string set"
+begin
+fun L_rhs_e:: "rhs_item \<Rightarrow> string set"
+where
+  "L_rhs_e (Lam r) = L r" |
+  "L_rhs_e (Trn X r) = X ;; L r"
+end
 
-overloading L_rhs \<equiv> "L:: (string set \<times> rexp) set \<Rightarrow> string set"
+overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> string set"
 begin
-fun L_rhs:: "(string set \<times> rexp) set \<Rightarrow> string set"
+fun L_rhs:: "rhs_item set \<Rightarrow> string set"
 where
-  "L_rhs rhs = \<Union> {(Y;; L r) | Y r . (Y, r) \<in> rhs}"
+  "L_rhs rhs = \<Union> (L ` rhs)"
 end
 
 definition
-  "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, init_rhs CS X)})"
-
-lemma [simp]:
-  shows "finite (Y \<Turnstile>\<Rightarrow> X)"
-unfolding transitions_def
-by auto
+  "init_rhs CS X \<equiv>  if ([] \<in> X)
+                    then {Lam EMPTY} \<union> {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}
+                    else {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"
 
-lemma defined_by_str:
-  assumes "s \<in> X" 
-  and "X \<in> UNIV // (\<approx>Lang)"
-  shows "X = (\<approx>Lang) `` {s}"
-using assms
-unfolding quotient_def Image_def
-unfolding str_eq_rel_def str_eq_def
-by auto
-
-
+definition
+  "eqs CS \<equiv> {(X, init_rhs CS X)|X.  X \<in> CS}"
 
 (************ arden's lemma variation ********************)
-definition 
-  "rexp_of rhs X \<equiv> folds ALT NULL {r. (X, r) \<in> rhs}"
+
+definition
+  "items_of rhs X \<equiv> {Trn X r | r. (Trn X r) \<in> rhs}"
+
+definition
+  "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
 
 definition 
-  "arden_variate X rhs \<equiv> {(Y, SEQ r (STAR (rexp_of rhs X)))| Y r. (Y, r) \<in> rhs \<and> Y \<noteq> X}"
+  "rexp_of rhs X \<equiv> folds ALT NULL ((snd o the_Trn) ` items_of rhs X)"
+
+definition
+  "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)"
 
-(************* rhs/equations property **************)
+fun attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
+where
+  "attach_rexp r' (Lam r)   = Lam (SEQ r r')"
+| "attach_rexp r' (Trn X r) = Trn X (SEQ r r')"
+
+definition
+  "append_rhs_rexp rhs r \<equiv> (attach_rexp r) ` rhs"
 
 definition 
-  "distinct_equas ES \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
+  "arden_variate X rhs \<equiv> append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"
+
 
 (*********** substitution of ES *************)
 
 text {* rhs_subst rhs X xrhs: substitude all occurence of X in rhs with xrhs *}
 definition 
-  "rhs_subst rhs X xrhs \<equiv> {(Y, r) | Y r. Y \<noteq> X \<and> (Y, r) \<in> rhs} \<union> 
-                          {(X, SEQ r\<^isub>1 r\<^isub>2 ) | r\<^isub>1 r\<^isub>2. (X, r\<^isub>1) \<in> xrhs \<and> (X, r\<^isub>2) \<in> rhs}"
+  "rhs_subst rhs X xrhs \<equiv> (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"
 
 definition
   "eqs_subst ES X xrhs \<equiv> {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
@@ -158,17 +195,35 @@
 *}
 
 definition 
-  "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> ([] \<notin> L (rexp_of rhs X)) \<and> X = L rhs"
+  "distinct_equas ES \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
+
+definition 
+  "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"
+
+definition 
+  "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
+
+definition 
+  "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
 
 definition 
   "non_empty ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> X \<noteq> {}"
 
-definition 
-  "self_contained ES \<equiv> \<forall> X xrhs. (X, xrhs) \<in> ES 
-                             \<longrightarrow> (\<forall> Y r.(Y, r) \<in> xrhs \<and> Y \<noteq> {[]} \<longrightarrow> (\<exists> yrhs. (Y, yrhs) \<in> ES))"
+definition
+  "finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"
 
 definition 
-  "Inv ES \<equiv> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> non_empty ES \<and> self_contained ES"
+  "classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"
+
+definition
+  "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
+
+definition 
+  "self_contained ES \<equiv> \<forall> (X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"
+
+definition 
+  "Inv ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
+            non_empty ES \<and> finite_rhs ES \<and> self_contained ES"
 
 lemma wf_iter [rule_format]: 
   fixes f
@@ -197,63 +252,574 @@
   qed
 qed
 
+text {* ************* basic properties of definitions above ************************ *}
+
+lemma L_rhs_union_distrib:
+  " L (A::rhs_item set) \<union> L B = L (A \<union> B)"
+by simp
+
+lemma finite_snd_Trn:
+  assumes finite:"finite rhs"
+  shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \<in> rhs}" (is "finite ?B")
+proof-
+  def rhs' \<equiv> "{e \<in> rhs. \<exists> r. e = Trn Y r}"
+  have "?B = (snd o the_Trn) ` rhs'" using rhs'_def by (auto simp:image_def)
+  moreover have "finite rhs'" using finite rhs'_def by auto
+  ultimately show ?thesis by simp
+qed
+
+lemma rexp_of_empty:
+  assumes finite:"finite rhs"
+  and nonempty:"rhs_nonempty rhs"
+  shows "[] \<notin> L (rexp_of rhs X)"
+using finite nonempty rhs_nonempty_def
+by (drule_tac finite_snd_Trn[where Y = X], auto simp:rexp_of_def items_of_def)
+
+lemma [intro!]:
+  "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto
+
+lemma finite_items_of:
+  "finite rhs \<Longrightarrow> finite (items_of rhs X)"
+by (auto simp:items_of_def intro:finite_subset)
+
+lemma lang_of_rexp_of:
+  assumes finite:"finite rhs"
+  shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))"
+proof -
+  have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto
+  thus ?thesis
+    apply (auto simp:rexp_of_def Seq_def items_of_def)
+    apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto)
+    by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def)
+qed
+
+lemma rexp_of_lam_eq_lam_set:
+  assumes finite: "finite rhs"
+  shows "L (rexp_of_lam rhs) = L (lam_of rhs)"
+proof -
+  have "finite (the_r ` {Lam r |r. Lam r \<in> rhs})" using finite
+    by (rule_tac finite_imageI, auto intro:finite_subset)
+  thus ?thesis by (auto simp:rexp_of_lam_def lam_of_def)
+qed
+
+lemma [simp]:
+  " L (attach_rexp r xb) = L xb ;; L r"
+apply (cases xb, auto simp:Seq_def)
+by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def)
+
+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 = "attach_rexp r xb" in exI, auto simp:Seq_def)
+
+lemma classes_of_union_distrib:
+  "classes_of A \<union> classes_of B = classes_of (A \<union> 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)
+
+
 text {* ******BEGIN: proving the initial equation-system satisfies Inv ****** *}
 
+lemma defined_by_str:
+  "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"
+by (auto simp:quotient_def Image_def str_eq_rel_def str_eq_def)
+
+lemma every_eqclass_has_transition:
+  assumes has_str: "s @ [c] \<in> X"
+  and     in_CS:   "X \<in> UNIV // (\<approx>Lang)"
+  obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
+proof -
+  def Y \<equiv> "(\<approx>Lang) `` {s}"
+  have "Y \<in> UNIV // (\<approx>Lang)" 
+    unfolding Y_def quotient_def by auto
+  moreover
+  have "X = (\<approx>Lang) `` {s @ [c]}" 
+    using has_str in_CS defined_by_str by blast
+  then have "Y ;; {[c]} \<subseteq> X" 
+    unfolding Y_def Image_def Seq_def
+    unfolding str_eq_rel_def
+    by (auto) (simp add: str_eq_def)
+  moreover
+  have "s \<in> Y" unfolding Y_def 
+    unfolding Image_def str_eq_rel_def str_eq_def by simp
+  ultimately show thesis by (blast intro: that)
+qed
+
+lemma l_eq_r_in_eqs:
+  assumes X_in_eqs: "(X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"
+  shows "X = L xrhs"
+proof 
+  show "X \<subseteq> L xrhs"
+  proof
+    fix x
+    assume "(1)": "x \<in> X"
+    show "x \<in> L xrhs"          
+    proof (cases "x = []")
+      assume empty: "x = []"
+      thus ?thesis using X_in_eqs "(1)"
+        by (auto simp:eqs_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)
+      then obtain Y 
+        where "Y \<in> UNIV // (\<approx>Lang)" 
+        and "Y ;; {[c]} \<subseteq> X"
+        and "clist \<in> Y"
+        using decom "(1)" every_eqclass_has_transition by blast
+      hence "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y ;; {[c]} \<subseteq> X}"
+        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)
+    qed
+  qed
+next
+  show "L xrhs \<subseteq> X" using X_in_eqs
+    by (auto simp:eqs_def init_rhs_def) 
+qed
+
+lemma finite_init_rhs: 
+  assumes finite: "finite CS"
+  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 -
+    def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" 
+    def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
+    have "finite (CS \<times> (UNIV::char set))" using finite by auto
+    hence "finite S" using S_def 
+      by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto)
+    moreover have "?A = h ` S" by (auto simp: S_def h_def image_def)
+    ultimately show ?thesis 
+      by auto
+  qed
+  thus ?thesis by (simp add:init_rhs_def)
+qed
+
 lemma init_ES_satisfy_Inv:
   assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
-  and X_in_eq_cls: "X \<in> (UNIV // (\<approx>Lang))"
   shows "Inv (eqs (UNIV // (\<approx>Lang)))"
 proof -
   have "finite (eqs (UNIV // (\<approx>Lang)))" using finite_CS
-    by (auto simp add:eqs_def)
+    by (simp add:eqs_def)
   moreover have "distinct_equas (eqs (UNIV // (\<approx>Lang)))"     
-    by (auto simp:distinct_equas_def eqs_def)
+    by (simp add:distinct_equas_def eqs_def)
   moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))"
-  proof-
-    have "\<And> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<Longrightarrow> ([] \<notin> L (rexp_of rhs X))"
-    proof 
-      apply (auto simp:eqs_def rexp_of_def)
-      sorry
-    moreover have "\<forall> X rhs. (X, rhs) \<in> (eqs (UNIV // (\<approx>Lang))) \<longrightarrow> X = L rhs"
-      sorry
-    ultimately show ?thesis by (simp add:ardenable_def)
-  qed
+    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 "non_empty (eqs (UNIV // (\<approx>Lang)))"
     by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def str_eq_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)
+    by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)
   ultimately show ?thesis by (simp add:Inv_def)
 qed
 
+text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}
 
-text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}
+lemma arden_variate_keeps_eq:
+  assumes l_eq_r: "X = L rhs"
+  and not_empty: "[] \<notin> L (rexp_of rhs X)"
+  and finite: "finite rhs"
+  shows "X = L (arden_variate X rhs)"
+proof -
+  def A \<equiv> "L (rexp_of rhs X)"
+  def b \<equiv> "rhs - items_of rhs X"
+  def B \<equiv> "L b" 
+  have "X = B ;; A\<star>"
+  proof-
+    have "rhs = items_of rhs X \<union> b" by (auto simp:b_def items_of_def)
+    hence "L rhs = L(items_of rhs X \<union> b)" by simp
+    hence "L rhs = L(items_of rhs X) \<union> B" by (simp only:L_rhs_union_distrib B_def)
+    with lang_of_rexp_of
+    have "L rhs = X ;; A \<union> B " using finite by (simp only:B_def b_def A_def)
+    thus ?thesis
+      using l_eq_r not_empty
+      apply (drule_tac B = B and X = X in ardens_revised)
+      by (auto simp:A_def simp del:L_rhs.simps)
+  qed
+  moreover have "L (arden_variate X rhs) = (B ;; A\<star>)" (is "?L = ?R")
+    by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs 
+                  B_def A_def b_def L_rexp.simps seq_union_distrib)
+   ultimately show ?thesis by simp
+qed 
+
+lemma append_keeps_finite:
+  "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
+by (auto simp:append_rhs_rexp_def)
+
+lemma arden_variate_keeps_finite:
+  "finite rhs \<Longrightarrow> finite (arden_variate X rhs)"
+by (auto simp:arden_variate_def append_keeps_finite)
+
+lemma append_keeps_nonempty:
+  "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)"
+apply (auto simp:rhs_nonempty_def append_rhs_rexp_def)
+by (case_tac x, auto simp:Seq_def)
+
+lemma nonempty_set_sub:
+  "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (rhs - A)"
+by (auto simp:rhs_nonempty_def)
+
+lemma nonempty_set_union:
+  "\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')"
+by (auto simp:rhs_nonempty_def)
+
+lemma arden_variate_keeps_nonempty:
+  "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (arden_variate X rhs)"
+by (simp only:arden_variate_def append_keeps_nonempty nonempty_set_sub)
+
+
+lemma rhs_subst_keeps_nonempty:
+  "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs_subst rhs X xrhs)"
+by (simp only:rhs_subst_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)
+
+lemma rhs_subst_keeps_eq:
+  assumes substor: "X = L xrhs"
+  and finite: "finite rhs"
+  shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
+proof-
+  def A \<equiv> "L (rhs - items_of rhs X)"
+  have "?Left = A \<union> L (append_rhs_rexp xrhs (rexp_of rhs X))"
+    by (simp only:rhs_subst_def L_rhs_union_distrib A_def)
+  moreover have "?Right = A \<union> L (items_of rhs X)"
+  proof-
+    have "rhs = (rhs - items_of rhs X) \<union> (items_of rhs X)" by (auto simp:items_of_def)
+    thus ?thesis by (simp only:L_rhs_union_distrib A_def)
+  qed
+  moreover have "L (append_rhs_rexp xrhs (rexp_of rhs X)) = L (items_of rhs X)" 
+    using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)
+  ultimately show ?thesis by simp
+qed
+
+lemma rhs_subst_keeps_finite_rhs:
+  "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (rhs_subst rhs Y yrhs)"
+by (auto simp:rhs_subst_def append_keeps_finite)
+
+lemma eqs_subst_keeps_finite:
+  assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)"
+  shows "finite (eqs_subst ES Y yrhs)"
+proof -
+  have "finite {(Ya, rhs_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, rhs_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:eqs_subst_def)
+qed
+
+lemma eqs_subst_keeps_finite_rhs:
+  "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (eqs_subst ES Y yrhs)"
+by (auto intro:rhs_subst_keeps_finite_rhs simp add:eqs_subst_def finite_rhs_def)
+
+lemma append_rhs_keeps_cls:
+  "classes_of (append_rhs_rexp rhs r) = classes_of rhs"
+apply (auto simp:classes_of_def append_rhs_rexp_def)
+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_variate_removes_cl:
+  "classes_of (arden_variate Y yrhs) = classes_of yrhs - {Y}"
+apply (simp add:arden_variate_def append_rhs_keeps_cls items_of_def)
+by (auto simp:classes_of_def)
+
+lemma lefts_of_keeps_cls:
+  "lefts_of (eqs_subst ES Y yrhs) = lefts_of ES"
+by (auto simp:lefts_of_def eqs_subst_def)
+
+lemma rhs_subst_updates_cls:
+  "X \<notin> classes_of xrhs \<Longrightarrow> classes_of (rhs_subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
+apply (simp only:rhs_subst_def append_rhs_keeps_cls classes_of_union_distrib[THEN sym])
+by (auto simp:classes_of_def items_of_def)
+
+lemma eqs_subst_keeps_self_contained:
+  fixes Y
+  assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
+  shows "self_contained (eqs_subst ES Y (arden_variate Y yrhs))" (is "self_contained ?B")
+proof-
+  { fix X xrhs'
+    assume "(X, xrhs') \<in> ?B"
+    then obtain xrhs 
+      where xrhs_xrhs': "xrhs' = rhs_subst xrhs Y (arden_variate Y yrhs)"
+      and X_in: "(X, xrhs) \<in> ES" by (simp add:eqs_subst_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 eqs_subst_def)
+      moreover have "classes_of xrhs' \<subseteq> lefts_of ES"
+      proof-
+        have "classes_of xrhs' \<subseteq> classes_of xrhs \<union> classes_of (arden_variate Y yrhs) - {Y}"
+        proof-
+          have "Y \<notin> classes_of (arden_variate Y yrhs)" using arden_variate_removes_cl by simp
+          thus ?thesis using xrhs_xrhs' by (auto simp:rhs_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_variate Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" using sc
+          by (auto simp add:arden_variate_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:eqs_subst_def self_contained_def)
+qed
+
+lemma eqs_subst_satisfy_Inv:
+  assumes Inv_ES: "Inv (ES \<union> {(Y, yrhs)})"
+  shows "Inv (eqs_subst ES Y (arden_variate Y yrhs))"
+proof -  
+  have finite_yrhs: "finite yrhs" using Inv_ES by (auto simp:Inv_def finite_rhs_def)
+  have nonempty_yrhs: "rhs_nonempty yrhs" using Inv_ES by (auto simp:Inv_def ardenable_def)
+  have Y_eq_yrhs: "Y = L yrhs" using Inv_ES by (simp only:Inv_def valid_eqns_def, blast)
+
+  have "distinct_equas (eqs_subst ES Y (arden_variate Y yrhs))" using Inv_ES
+    by (auto simp:distinct_equas_def eqs_subst_def Inv_def)
+  moreover have "finite (eqs_subst ES Y (arden_variate Y yrhs))" using Inv_ES 
+    by (simp add:Inv_def eqs_subst_keeps_finite)
+  moreover have "finite_rhs (eqs_subst ES Y (arden_variate Y yrhs))"
+  proof-
+    have "finite_rhs ES" using Inv_ES by (simp add:Inv_def finite_rhs_def)
+    moreover have "finite (arden_variate Y yrhs)"
+    proof -
+      have "finite yrhs" using Inv_ES by (auto simp:Inv_def finite_rhs_def)
+      thus ?thesis using arden_variate_keeps_finite by simp
+    qed
+    ultimately show ?thesis by (simp add:eqs_subst_keeps_finite_rhs)
+  qed
+  moreover have "ardenable (eqs_subst ES Y (arden_variate Y yrhs))"
+  proof - 
+    { fix X rhs
+      assume "(X, rhs) \<in> ES"
+      hence "rhs_nonempty rhs"  using prems Inv_ES  by (simp add:Inv_def ardenable_def)
+      with nonempty_yrhs have "rhs_nonempty (rhs_subst rhs Y (arden_variate Y yrhs))"
+        by (simp add:nonempty_yrhs rhs_subst_keeps_nonempty arden_variate_keeps_nonempty)
+    } thus ?thesis by (auto simp add:ardenable_def eqs_subst_def)
+  qed
+  moreover have "valid_eqns (eqs_subst ES Y (arden_variate Y yrhs))"
+  proof-
+    have "Y = L (arden_variate Y yrhs)" using Y_eq_yrhs Inv_ES finite_yrhs nonempty_yrhs      
+        by (rule_tac arden_variate_keeps_eq, (simp add:rexp_of_empty)+)
+    thus ?thesis using Inv_ES 
+      by (clarsimp simp add:valid_eqns_def eqs_subst_def rhs_subst_keeps_eq Inv_def finite_rhs_def
+                   simp del:L_rhs.simps)
+  qed
+  moreover have non_empty_subst: "non_empty (eqs_subst ES Y (arden_variate Y yrhs))"
+    using Inv_ES by (auto simp:Inv_def non_empty_def eqs_subst_def)
+  moreover have self_subst: "self_contained (eqs_subst ES Y (arden_variate Y yrhs))"
+    using Inv_ES eqs_subst_keeps_self_contained by (simp add:Inv_def)
+  ultimately show ?thesis using Inv_ES by (simp add:Inv_def)
+qed
+
+lemma eqs_subst_card_le: 
+  assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
+  shows "card (eqs_subst ES Y yrhs) <= card ES"
+proof-
+  def f \<equiv> "\<lambda> x. ((fst x)::string set, rhs_subst (snd x) Y yrhs)"
+  have "eqs_subst ES Y yrhs = f ` ES" 
+    apply (auto simp:eqs_subst_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 eqs_subst_cls_remains: 
+  "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (eqs_subst ES Y yrhs)"
+by (auto simp:eqs_subst_def)
+
+lemma card_noteq_1_has_more:
+  assumes card:"card S \<noteq> 1"
+  and e_in: "e \<in> S"
+  and finite: "finite S"
+  obtains e' where "e' \<in> S \<and> e \<noteq> e'" 
+proof-
+  have "card (S - {e}) > 0"
+  proof -
+    have "card S > 1" using card e_in finite  by (case_tac "card S", auto) 
+    thus ?thesis using finite e_in by auto
+  qed
+  hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp)
+  thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
+qed
 
 lemma iteration_step: 
   assumes Inv_ES: "Inv ES"
-  and    X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES"
-  and    not_T: "card ES > 1"
-  shows "(\<exists> ES' xrhs'. Inv ES' \<and> (card ES', card ES) \<in> less_than \<and> (X, xrhs') \<in> ES')" 
+  and    X_in_ES: "(X, xrhs) \<in> ES"
+  and    not_T: "card ES \<noteq> 1"
+  shows "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'.(X, xrhs') \<in> ES')) \<and> (card ES', card ES) \<in> less_than" (is "\<exists> ES'. ?P ES'")
 proof -
+  have finite_ES: "finite ES" using Inv_ES by (simp add:Inv_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)
+  def ES' == "ES - {(Y, yrhs)}"
+  let ?ES'' = "eqs_subst ES' Y (arden_variate Y yrhs)"
+  have "?P ?ES''"
+  proof -
+    have "Inv ?ES''" using Y_in_ES Inv_ES
+      by (rule_tac eqs_subst_satisfy_Inv, simp add:ES'_def insert_absorb)
+    moreover have "\<exists>xrhs'. (X, xrhs') \<in> ?ES''"  using not_eq X_in_ES
+      by (rule_tac ES = ES' in eqs_subst_cls_remains, auto simp add:ES'_def)
+    moreover have "(card ?ES'', card ES) \<in> less_than" 
+    proof -
+      have "finite ES'" using finite_ES ES'_def by auto
+      moreover have "card ES' < card ES" using finite_ES Y_in_ES
+        by (auto simp:ES'_def card_gt_0_iff intro:diff_Suc_less)
+      ultimately show ?thesis 
+        by (auto dest:eqs_subst_card_le elim:le_less_trans)
+    qed
+    ultimately show ?thesis by simp
+  qed
+  thus ?thesis by blast
+qed
+
+text {* ***** END: proving every equation-system's iteration step satisfies Inv ************** *}
 
- 
-
+lemma iteration_conc: 
+  assumes history: "Inv ES"
+  and    X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES"
+  shows "\<exists> ES'. (Inv ES' \<and> (\<exists> xrhs'. (X, xrhs') \<in> ES')) \<and> card ES' = 1" (is "\<exists> ES'. ?P ES'")
+proof (cases "card ES = 1")
+  case True
+  thus ?thesis using history X_in_ES
+    by blast
+next
+  case False  
+  thus ?thesis using history iteration_step X_in_ES
+    by (rule_tac f = card in wf_iter, auto)
+qed
+  
+lemma last_cl_exists_rexp:
+  assumes ES_single: "ES = {(X, xrhs)}" 
+  and Inv_ES: "Inv ES"
+  shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
+proof-
+  let ?A = "arden_variate X xrhs"
+  have "?P (rexp_of_lam ?A)"
+  proof -
+    have "L (rexp_of_lam ?A) = L (lam_of ?A)"
+    proof(rule rexp_of_lam_eq_lam_set)
+      show "finite (arden_variate X xrhs)" using Inv_ES ES_single 
+        by (rule_tac arden_variate_keeps_finite, auto simp add:Inv_def finite_rhs_def)
+    qed
+    also have "\<dots> = L ?A"
+    proof-
+      have "lam_of ?A = ?A"
+      proof-
+        have "classes_of ?A = {}" using Inv_ES ES_single
+          by (simp add:arden_variate_removes_cl self_contained_def Inv_def lefts_of_def) 
+        thus ?thesis by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)
+      qed
+      thus ?thesis by simp
+    qed
+    also have "\<dots> = X"
+    proof(rule arden_variate_keeps_eq [THEN sym])
+      show "X = L xrhs" using Inv_ES ES_single by (auto simp only:Inv_def valid_eqns_def)  
+    next
+      from Inv_ES ES_single show "[] \<notin> L (rexp_of xrhs X)"
+        by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def)
+    next
+      from Inv_ES ES_single show "finite xrhs" by (simp add:Inv_def finite_rhs_def)
+    qed
+    finally show ?thesis by simp
+  qed
+  thus ?thesis by auto
+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")
+proof -
+  from X_in_CS have "\<exists> xrhs. (X, xrhs) \<in> (eqs (UNIV  // (\<approx>Lang)))"
+    by (auto simp:eqs_def init_rhs_def)
+  then obtain ES xrhs where Inv_ES: "Inv ES" 
+    and X_in_ES: "(X, xrhs) \<in> ES"
+    and card_ES: "card ES = 1"
+    using finite_CS X_in_CS init_ES_satisfy_Inv iteration_conc
+    by blast
+  hence ES_single_equa: "ES = {(X, xrhs)}" 
+    by (auto simp:Inv_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) 
+  thus ?thesis using Inv_ES
+    by (rule last_cl_exists_rexp)
+qed
 
+theorem hard_direction: 
+  assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
+  shows   "\<exists> (reg::rexp). Lang = L reg"
+proof -
+  have "\<forall> X \<in> (UNIV // (\<approx>Lang)). \<exists> (reg::rexp). X = L reg" 
+    using finite_CS every_eqcl_has_reg by blast
+  then obtain f where f_prop: "\<forall> X \<in> (UNIV // (\<approx>Lang)). X = L ((f X)::rexp)" 
+    by (auto dest:bchoice)
+  def rs \<equiv> "f ` {X. final X Lang}"  
+  have "Lang = \<Union> {X. final X Lang}" using lang_is_union_of_finals by simp
+  also have "\<dots> = L (folds ALT NULL rs)" 
+  proof -
+    have "finite {X. final X Lang}" using finite_CS by (auto simp:final_def)
+    thus ?thesis  using f_prop by (auto simp:rs_def final_def)
+  qed
+  finally show ?thesis by blast
+qed 
 
+section {* regular \<Rightarrow> finite*}
+
+lemma quot_empty_subset:
+  "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
+proof
+  fix x
+  assume h: "x \<in> UNIV // \<approx>{[]}"
+  show "x \<in> {{[]}, UNIV - {[]}}"
+    
  
+  have "\<And> s. s \<approx>{[]} [] \<Longrightarrow> s = []"
+    apply (auto simp add:str_eq_def)
+    apply blast
+  
+  hence "False"
+    apply (simp add:quotient_def)
 
 
-
-  
-
-
-
+lemma other_direction:
+  "Lang = L (r::rexp) \<Longrightarrow> finite (UNIV // (\<approx>Lang))"
+proof (induct arbitrary:Lang rule:rexp.induct)
+  case NULL
+  have "UNIV // (\<approx>{}) \<subseteq> {UNIV} "
+    by (auto simp:quotient_def str_eq_rel_def str_eq_def)
+  with prems show "?case" by (auto intro:finite_subset)
+next
+  case EMPTY
+  have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
+    sorry
+  with prems show ?case by (auto intro:finite_subset)
+next
+  case (CHAR c)
+  have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
+    sorry
+  with prems show ?case by (auto intro:finite_subset)
+next
+  case (SEQ r1 r2)
+  show ?case sorry
+next
+  case (ALT r1 r1)
+  show ?case sorry
+next
+  case (STAR r)
+  show ?case sorry
+qed
+    
 
-
-
-
-
-
-
+      
 
 
 
@@ -271,645 +837,9 @@
 
 
 
-lemma distinct_rhs_equations:
-  "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs"
-by (auto simp: equations_def equation_rhs_def distinct_rhs_def empty_rhs_def dest:no_two_cls_inters)
-
-lemma every_nonempty_eqclass_has_strings:
-  "\<lbrakk>X \<in> (UNIV Quo Lang); X \<noteq> {[]}\<rbrakk> \<Longrightarrow> \<exists> clist. clist \<in> X \<and> clist \<noteq> []"
-by (auto simp:quot_def equiv_class_def equiv_str_def)
-
-lemma every_eqclass_is_derived_from_empty:
-  assumes not_empty: "X \<noteq> {[]}"
-  shows "X \<in> (UNIV Quo Lang) \<Longrightarrow> \<exists> clist. {[]};{clist} \<subseteq> X \<and> clist \<noteq> []"
-using not_empty
-apply (drule_tac every_nonempty_eqclass_has_strings, simp)
-by (auto intro:exI[where x = clist] simp:lang_seq_def)
-
-lemma equiv_str_in_CS:
-  "\<lbrakk>clist\<rbrakk>Lang \<in> (UNIV Quo Lang)"
-by (auto simp:quot_def)
-
-lemma has_str_imp_defined_by_str:
-  "\<lbrakk>str \<in> X; X \<in> UNIV Quo Lang\<rbrakk> \<Longrightarrow> X = \<lbrakk>str\<rbrakk>Lang"
-by (auto simp:quot_def equiv_class_def equiv_str_def)
-
-lemma every_eqclass_has_ascendent:
-  assumes has_str: "clist @ [c] \<in> X"
-  and     in_CS:   "X \<in> UNIV Quo Lang"
-  shows "\<exists> Y. Y \<in> UNIV Quo Lang \<and> Y-c\<rightarrow>X \<and> clist \<in> Y" (is "\<exists> Y. ?P Y")
-proof -
-  have "?P (\<lbrakk>clist\<rbrakk>Lang)" 
-  proof -
-    have "\<lbrakk>clist\<rbrakk>Lang \<in> UNIV Quo Lang"       
-      by (simp add:quot_def, rule_tac x = clist in exI, simp)
-    moreover have "\<lbrakk>clist\<rbrakk>Lang-c\<rightarrow>X" 
-    proof -
-      have "X = \<lbrakk>(clist @ [c])\<rbrakk>Lang" using has_str in_CS
-        by (auto intro!:has_str_imp_defined_by_str)
-      moreover have "\<forall> sl. sl \<in> \<lbrakk>clist\<rbrakk>Lang \<longrightarrow> sl @ [c] \<in> \<lbrakk>(clist @ [c])\<rbrakk>Lang"
-        by (auto simp:equiv_class_def equiv_str_def)
-      ultimately show ?thesis unfolding CT_def lang_seq_def
-        by auto
-    qed
-    moreover have "clist \<in> \<lbrakk>clist\<rbrakk>Lang" 
-      by (auto simp:equiv_str_def equiv_class_def)
-    ultimately show "?P (\<lbrakk>clist\<rbrakk>Lang)" by simp
-  qed
-  thus ?thesis by blast
-qed
-
-lemma finite_charset_rS:
-  "finite {CHAR c |c. Y-c\<rightarrow>X}"
-by (rule_tac A = UNIV and f = CHAR in finite_surj, auto)
-
-lemma l_eq_r_in_equations:
-  assumes X_in_equas: "(X, xrhs) \<in> equations (UNIV Quo Lang)"
-  shows "X = L xrhs"    
-proof (cases "X = {[]}")
-  case True
-  thus ?thesis using X_in_equas 
-    by (simp add:equations_def equation_rhs_def lang_seq_def)
-next
-  case False 
-  show ?thesis
-  proof 
-    show "X \<subseteq> L xrhs"
-    proof
-      fix x
-      assume "(1)": "x \<in> X"
-      show "x \<in> L xrhs"          
-      proof (cases "x = []")
-        assume empty: "x = []"
-        hence "x \<in> L (empty_rhs X)" using "(1)"
-          by (auto simp:empty_rhs_def lang_seq_def)
-        thus ?thesis using X_in_equas False empty "(1)" 
-          unfolding equations_def equation_rhs_def by auto
-      next
-        assume not_empty: "x \<noteq> []"
-        hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto)
-        then obtain clist c where decom: "x = clist @ [c]" by blast
-        moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk>
-          \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"
-        proof -
-          fix Y
-          assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang"
-            and Y_CT_X: "Y-c\<rightarrow>X"
-            and clist_in_Y: "clist \<in> Y"
-          with finite_charset_rS 
-          show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"
-            by (auto simp :fold_alt_null_eqs)
-        qed
-        hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" 
-          using X_in_equas False not_empty "(1)" decom
-          by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def)
-        then obtain Xa where 
-          "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast
-        hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" 
-          using X_in_equas "(1)" decom
-          by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa])
-        thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def
-          by auto
-      qed
-    qed
-  next
-    show "L xrhs \<subseteq> X"
-    proof
-      fix x 
-      assume "(2)": "x \<in> L xrhs"
-      have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"
-        using finite_charset_rS
-        by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)
-      have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"
-        by (simp add:empty_rhs_def split:if_splits)
-      show "x \<in> X" using X_in_equas False "(2)"         
-        by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def)
-    qed
-  qed
-qed
-
-
-
-lemma no_EMPTY_equations:
-  "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs"
-apply (clarsimp simp add:equations_def equation_rhs_def)
-apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto)
-apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+
-done
-
-lemma init_ES_satisfy_ardenable:
-  "(X, xrhs) \<in> equations (UNIV Quo Lang)  \<Longrightarrow> ardenable (X, xrhs)"  
-  unfolding ardenable_def
-  by (auto intro:distinct_rhs_equations no_EMPTY_equations simp:l_eq_r_in_equations simp del:L_rhs.simps)
-
-lemma init_ES_satisfy_Inv:
-  assumes finite_CS: "finite (UNIV Quo Lang)"
-  and X_in_eq_cls: "X \<in> UNIV Quo Lang"
-  shows "Inv X (equations (UNIV Quo Lang))"
-proof -
-  have "finite (equations (UNIV Quo Lang))" using finite_CS
-    by (auto simp:equations_def)    
-  moreover have "\<exists>rhs. (X, rhs) \<in> equations (UNIV Quo Lang)" using X_in_eq_cls 
-    by (simp add:equations_def)
-  moreover have "distinct_equas (equations (UNIV Quo Lang))" 
-    by (auto simp:distinct_equas_def equations_def)
-  moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow>
-                 rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equations (UNIV Quo Lang)))" 
-    apply (simp add:left_eq_cls_def equations_def rhs_eq_cls_def equation_rhs_def)
-    by (auto simp:empty_rhs_def split:if_splits)
-  moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> X \<noteq> {}"
-    by (clarsimp simp:equations_def empty_notin_CS intro:classical)
-  moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> ardenable (X, xrhs)"
-    by (auto intro!:init_ES_satisfy_ardenable)
-  ultimately show ?thesis by (simp add:Inv_def)
-qed
-
-
-text {* *********** END: proving the initial equation-system satisfies Inv ******* *}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}
-
-lemma not_T_aux: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk>
-       \<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> insert a A "
-apply (case_tac "insert a A = {a}")
-by (auto simp:TCon_def)
-
-lemma not_T_atleast_2[rule_format]:
-  "finite S \<Longrightarrow> \<forall> x. x \<in> S \<and> (\<not> TCon S)\<longrightarrow> (\<exists> y. x \<noteq> y \<and> y \<in> S)"
-apply (erule finite.induct, simp)
-apply (clarify, case_tac "x = a")
-by (erule not_T_aux, auto)
-
-lemma exist_another_equa: 
-  "\<lbrakk>\<not> TCon ES; finite ES; distinct_equas ES; (X, rhl) \<in> ES\<rbrakk> \<Longrightarrow> \<exists> Y yrhl. (Y, yrhl) \<in> ES \<and> X \<noteq> Y"
-apply (drule not_T_atleast_2, simp)
-apply (clarsimp simp:distinct_equas_def)
-apply (drule_tac x= X in spec, drule_tac x = rhl in spec, drule_tac x = b in spec)
-by auto
-
-lemma Inv_mono_with_lambda:
-  assumes Inv_ES: "Inv X ES"
-  and X_noteq_Y:  "X \<noteq> {[]}"
-  shows "Inv X (ES - {({[]}, yrhs)})"
-proof -
-  have "finite (ES - {({[]}, yrhs)})" using Inv_ES
-    by (simp add:Inv_def)
-  moreover have "\<exists>rhs. (X, rhs) \<in> ES - {({[]}, yrhs)}" using Inv_ES X_noteq_Y
-    by (simp add:Inv_def)
-  moreover have "distinct_equas (ES - {({[]}, yrhs)})" using Inv_ES X_noteq_Y
-    apply (clarsimp simp:Inv_def distinct_equas_def)
-    by (drule_tac x = Xa in spec, simp)    
-  moreover have "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>
-                          ardenable (X, xrhs) \<and> X \<noteq> {}" using Inv_ES
-    by (clarify, simp add:Inv_def)
-  moreover 
-  have "insert {[]} (left_eq_cls (ES - {({[]}, yrhs)})) = insert {[]} (left_eq_cls ES)"
-    by (auto simp:left_eq_cls_def)
-  hence "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>
-                          rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (ES - {({[]}, yrhs)}))"
-    using Inv_ES by (auto simp:Inv_def)
-  ultimately show ?thesis by (simp add:Inv_def)
-qed
-
-lemma non_empty_card_prop:
-  "finite ES \<Longrightarrow> \<forall>e. e \<in> ES \<longrightarrow> card ES - Suc 0 < card ES"
-apply (erule finite.induct, simp)
-apply (case_tac[!] "a \<in> A")
-by (auto simp:insert_absorb)
-
-lemma ardenable_prop:
-  assumes not_lambda: "Y \<noteq> {[]}"
-  and ardable: "ardenable (Y, yrhs)"
-  shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" (is "\<exists> yrhs'. ?P yrhs'")
-proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)")
-  case True
-  thus ?thesis 
-  proof 
-    fix reg
-    assume self_contained: "(Y, reg) \<in> yrhs"
-    show ?thesis 
-    proof -
-      have "?P (arden_variate Y reg yrhs)"
-      proof -
-        have "Y = L (arden_variate Y reg yrhs)" 
-          using self_contained not_lambda ardable
-          by (rule_tac arden_variate_valid, simp_all add:ardenable_def)
-        moreover have "distinct_rhs (arden_variate Y reg yrhs)" 
-          using ardable 
-          by (auto simp:distinct_rhs_def arden_variate_def seq_rhs_r_def del_x_paired_def ardenable_def)
-        moreover have "rhs_eq_cls (arden_variate Y reg yrhs) = rhs_eq_cls yrhs - {Y}"
-        proof -
-          have "\<And> rhs r. rhs_eq_cls (seq_rhs_r rhs r) = rhs_eq_cls rhs"
-            apply (auto simp:rhs_eq_cls_def seq_rhs_r_def image_def)
-            by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "(x, ra)" in bexI, simp+)
-          moreover have "\<And> rhs X. rhs_eq_cls (del_x_paired rhs X) = rhs_eq_cls rhs - {X}"
-            by (auto simp:rhs_eq_cls_def del_x_paired_def)
-          ultimately show ?thesis by (simp add:arden_variate_def)
-        qed
-        ultimately show ?thesis by simp
-      qed
-      thus ?thesis by (rule_tac x= "arden_variate Y reg yrhs" in exI, simp)
-    qed
-  qed
-next
-  case False
-  hence "(2)": "rhs_eq_cls yrhs - {Y} = rhs_eq_cls yrhs"
-    by (auto simp:rhs_eq_cls_def)
-  show ?thesis 
-  proof -
-    have "?P yrhs" using False ardable "(2)" 
-      by (simp add:ardenable_def)      
-    thus ?thesis by blast
-  qed
-qed
-
-lemma equas_subst_f_del_no_other:
-  assumes self_contained: "(Y, rhs) \<in> ES"
-  shows "\<exists> rhs'. (Y, rhs') \<in> (equas_subst_f X xrhs ` ES)" (is "\<exists> rhs'. ?P rhs'")
-proof -
-  have "\<exists> rhs'. equas_subst_f X xrhs (Y, rhs) = (Y, rhs')"
-    by (auto simp:equas_subst_f_def)
-  then obtain rhs' where "equas_subst_f X xrhs (Y, rhs) = (Y, rhs')" by blast
-  hence "?P rhs'" unfolding image_def using self_contained
-    by (auto intro:bexI[where x = "(Y, rhs)"])
-  thus ?thesis by blast
-qed
-
-lemma del_x_paired_del_only_x: 
-  "\<lbrakk>X \<noteq> Y; (X, rhs) \<in> ES\<rbrakk> \<Longrightarrow> (X, rhs) \<in> del_x_paired ES Y"
-by (auto simp:del_x_paired_def)
-
-lemma equas_subst_del_no_other:
- "\<lbrakk>(X, rhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> (\<exists>rhs. (X, rhs) \<in> equas_subst ES Y rhs')"
-unfolding equas_subst_def
-apply (drule_tac X = Y and xrhs = rhs' in equas_subst_f_del_no_other)
-by (erule exE, drule del_x_paired_del_only_x, auto)
-
-lemma equas_subst_holds_distinct:
-  "distinct_equas ES \<Longrightarrow> distinct_equas (equas_subst ES Y rhs')"
-apply (clarsimp simp add:equas_subst_def distinct_equas_def del_x_paired_def equas_subst_f_def)
-by (auto split:if_splits)
-
-lemma del_x_paired_dels: 
-  "(X, rhs) \<in> ES \<Longrightarrow> {Y. Y \<in> ES \<and> fst Y = X} \<inter> ES \<noteq> {}"
-by (auto)
-
-lemma del_x_paired_subset:
-  "(X, rhs) \<in> ES \<Longrightarrow> ES - {Y. Y \<in> ES \<and> fst Y = X} \<subset> ES"
-apply (drule del_x_paired_dels)
-by auto
-
-lemma del_x_paired_card_less: 
-  "\<lbrakk>finite ES; (X, rhs) \<in> ES\<rbrakk> \<Longrightarrow> card (del_x_paired ES X) < card ES"
-apply (simp add:del_x_paired_def)
-apply (drule del_x_paired_subset)
-by (auto intro:psubset_card_mono)
-
-lemma equas_subst_card_less:
-  "\<lbrakk>finite ES; (Y, yrhs) \<in> ES\<rbrakk> \<Longrightarrow> card (equas_subst ES Y rhs') < card ES"
-apply (simp add:equas_subst_def)
-apply (frule_tac h = "equas_subst_f Y rhs'" in finite_imageI)
-apply (drule_tac f = "equas_subst_f Y rhs'" in Finite_Set.card_image_le)
-apply (drule_tac X = Y and xrhs = rhs' in equas_subst_f_del_no_other,erule exE)
-by (drule del_x_paired_card_less, auto)
-
-lemma equas_subst_holds_distinct_rhs:
-  assumes   dist': "distinct_rhs yrhs'"
-  and     history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"
-  and     X_in :  "(X, xrhs) \<in> equas_subst ES Y yrhs'"
-  shows "distinct_rhs xrhs"
-using X_in history
-apply (clarsimp simp:equas_subst_def del_x_paired_def)
-apply (drule_tac x = a in spec, drule_tac x = b in spec)
-apply (simp add:ardenable_def equas_subst_f_def)
-by (auto intro:rhs_subst_holds_distinct_rhs simp:dist' split:if_splits)
-
-lemma r_no_EMPTY_imp_seq_rhs_r_no_EMPTY:
-  "[] \<notin> L r \<Longrightarrow> no_EMPTY_rhs (seq_rhs_r rhs r)"
-by (auto simp:no_EMPTY_rhs_def seq_rhs_r_def lang_seq_def)
-
-lemma del_x_paired_holds_no_EMPTY:
-  "no_EMPTY_rhs yrhs \<Longrightarrow> no_EMPTY_rhs (del_x_paired yrhs Y)"
-by (auto simp:no_EMPTY_rhs_def del_x_paired_def)
-
-lemma rhs_subst_holds_no_EMPTY:
-  "\<lbrakk>no_EMPTY_rhs yrhs; (Y, r) \<in> yrhs; Y \<noteq> {[]}\<rbrakk> \<Longrightarrow> no_EMPTY_rhs (rhs_subst yrhs Y rhs' r)"
-apply (auto simp:rhs_subst_def intro!:no_EMPTY_rhss_imp_merge_no_EMPTY r_no_EMPTY_imp_seq_rhs_r_no_EMPTY del_x_paired_holds_no_EMPTY)
-by (auto simp:no_EMPTY_rhs_def)
-
-lemma equas_subst_holds_no_EMPTY:
-  assumes substor: "Y \<noteq> {[]}"
-  and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"
-  and X_in:"(X, xrhs) \<in> equas_subst ES Y yrhs'"
-  shows "no_EMPTY_rhs xrhs"
-proof-
-  from X_in have "\<exists> (Z, zrhs) \<in> ES. (X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)"
-    by (auto simp add:equas_subst_def del_x_paired_def)
-  then obtain Z zrhs where Z_in: "(Z, zrhs) \<in> ES"
-                       and X_Z: "(X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)" by blast
-  hence dist_zrhs: "distinct_rhs zrhs" using history
-    by (auto simp:ardenable_def)
-  show ?thesis
-  proof (cases "\<exists> r. (Y, r) \<in> zrhs")
-    case True
-    then obtain r where Y_in_zrhs: "(Y, r) \<in> zrhs" ..
-    hence some: "(SOME r. (Y, r) \<in> zrhs) = r" using Z_in dist_zrhs
-      by (auto simp:distinct_rhs_def)
-    hence "no_EMPTY_rhs (rhs_subst zrhs Y yrhs' r)"
-      using substor Y_in_zrhs history Z_in
-      by (rule_tac rhs_subst_holds_no_EMPTY, auto simp:ardenable_def)
-    thus ?thesis using X_Z True some
-      by (simp add:equas_subst_def equas_subst_f_def)
-  next
-    case False
-    hence "(X, xrhs) = (Z, zrhs)" using Z_in X_Z
-      by (simp add:equas_subst_f_def)
-    thus ?thesis using history Z_in
-      by (auto simp:ardenable_def)
-  qed
-qed
-
-lemma equas_subst_f_holds_left_eq_right:
-  assumes substor: "Y = L rhs'"
-  and     history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> distinct_rhs xrhs \<and> X = L xrhs"
-  and       subst: "(X, xrhs) = equas_subst_f Y rhs' (Z, zrhs)"
-  and     self_contained: "(Z, zrhs) \<in> ES"
-  shows "X = L xrhs"
-proof (cases "\<exists> r. (Y, r) \<in> zrhs")
-  case True
-  from True obtain r where "(1)":"(Y, r) \<in> zrhs" ..
-  show ?thesis
-  proof -
-    from history self_contained
-    have dist: "distinct_rhs zrhs" by auto
-    hence "(SOME r. (Y, r) \<in> zrhs) = r" using self_contained "(1)"
-      using distinct_rhs_def by (auto intro:some_equality)
-    moreover have "L zrhs = L (rhs_subst zrhs Y rhs' r)" using substor dist "(1)" self_contained
-      by (rule_tac rhs_subst_prop1, auto simp:distinct_equas_rhs_def)
-    ultimately show ?thesis using subst history self_contained
-      by (auto simp:equas_subst_f_def split:if_splits)
-  qed
-next
-  case False
-  thus ?thesis using history subst self_contained
-    by (auto simp:equas_subst_f_def)
-qed
-
-lemma equas_subst_holds_left_eq_right:
-  assumes history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"
-  and     substor: "Y = L rhs'"
-  and     X_in :  "(X, xrhs) \<in> equas_subst ES Y yrhs'"
-  shows "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y rhs' \<longrightarrow> X = L xrhs"
-apply (clarsimp simp add:equas_subst_def del_x_paired_def)
-using substor
-apply (drule_tac equas_subst_f_holds_left_eq_right)
-using history
-by (auto simp:ardenable_def)
-
-lemma equas_subst_holds_ardenable:
-  assumes substor: "Y = L yrhs'"
-  and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"
-  and X_in:"(X, xrhs) \<in> equas_subst ES Y yrhs'"
-  and dist': "distinct_rhs yrhs'"
-  and not_lambda: "Y \<noteq> {[]}"
-  shows "ardenable (X, xrhs)"
-proof -
-  have "distinct_rhs xrhs" using history X_in dist' 
-    by (auto dest:equas_subst_holds_distinct_rhs)
-  moreover have "no_EMPTY_rhs xrhs" using history X_in not_lambda
-    by (auto intro:equas_subst_holds_no_EMPTY)
-  moreover have "X = L xrhs" using history substor X_in
-  by (auto dest: equas_subst_holds_left_eq_right simp del:L_rhs.simps)
-  ultimately show ?thesis using ardenable_def by simp
-qed
-
-lemma equas_subst_holds_cls_defined:
-  assumes         X_in: "(X, xrhs) \<in> equas_subst ES Y yrhs'"
-  and           Inv_ES: "Inv X' ES"
-  and            subst: "(Y, yrhs) \<in> ES"
-  and  cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}"
-  shows "rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equas_subst ES Y yrhs'))"
-proof-
-  have tac: "\<lbrakk> A \<subseteq> B; C \<subseteq> D; E \<subseteq> A \<union> B\<rbrakk> \<Longrightarrow> E \<subseteq> B \<union> D" by auto
-  from X_in have "\<exists> (Z, zrhs) \<in> ES. (X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)"
-    by (auto simp add:equas_subst_def del_x_paired_def)
-  then obtain Z zrhs where Z_in: "(Z, zrhs) \<in> ES"
-                       and X_Z: "(X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)" by blast
-  hence "rhs_eq_cls zrhs \<subseteq> insert {[]} (left_eq_cls ES)" using Inv_ES
-    by (auto simp:Inv_def)
-  moreover have "rhs_eq_cls yrhs' \<subseteq> insert {[]} (left_eq_cls ES) - {Y}" 
-    using Inv_ES subst cls_holds_but_Y
-    by (auto simp:Inv_def)
-  moreover have "rhs_eq_cls xrhs \<subseteq> rhs_eq_cls zrhs \<union> rhs_eq_cls yrhs' - {Y}"
-    using X_Z cls_holds_but_Y
-    apply (clarsimp simp add:equas_subst_f_def rhs_subst_def split:if_splits)
-    by (auto simp:rhs_eq_cls_def merge_rhs_def del_x_paired_def seq_rhs_r_def)
-  moreover have "left_eq_cls (equas_subst ES Y yrhs') = left_eq_cls ES - {Y}" using subst
-    by (auto simp: left_eq_cls_def equas_subst_def del_x_paired_def equas_subst_f_def
-             dest: equas_subst_f_del_no_other
-             split: if_splits)
-  ultimately show ?thesis by blast
-qed
-
-lemma iteration_step: 
-  assumes Inv_ES: "Inv X ES"
-  and    not_T: "\<not> TCon ES"
-  shows "(\<exists> ES'. Inv X ES' \<and> (card ES', card ES) \<in> less_than)" 
-proof -
-  from Inv_ES not_T have another: "\<exists>Y yrhs. (Y, yrhs) \<in> ES \<and> X \<noteq> Y" unfolding Inv_def
-    by (clarify, rule_tac exist_another_equa[where X = X], auto)
-  then obtain Y yrhs where subst: "(Y, yrhs) \<in> ES" and not_X: " X \<noteq> Y" by blast
-  show ?thesis (is "\<exists> ES'. ?P ES'")
-  proof (cases "Y = {[]}") 
-    case True
-      --"in this situation, we pick a \"\<lambda>\" equation, thus directly remove it from the equation-system"
-    have "?P (ES - {(Y, yrhs)})" 
-    proof 
-      show "Inv X (ES - {(Y, yrhs)})" using True not_X
-        by (simp add:Inv_ES Inv_mono_with_lambda)
-    next 
-      show "(card (ES - {(Y, yrhs)}), card ES) \<in> less_than" using Inv_ES subst
-        by (auto elim:non_empty_card_prop[rule_format] simp:Inv_def)
-    qed
-    thus ?thesis by blast
-  next
-    case False
-      --"in this situation, we pick a equation and using ardenable to get a 
-        rhs without itself in it, then use equas_subst to form a new equation-system"
-    hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" 
-      using subst Inv_ES
-      by (auto intro:ardenable_prop simp add:Inv_def simp del:L_rhs.simps)
-    then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'"
-      and dist_Y': "distinct_rhs yrhs'"
-      and cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" by blast
-    hence "?P (equas_subst ES Y yrhs')"
-    proof -
-      have finite_del: "\<And> S x. finite S \<Longrightarrow> finite (del_x_paired S x)" 
-        apply (rule_tac A = "del_x_paired S x" in finite_subset)
-        by (auto simp:del_x_paired_def)
-      have "finite (equas_subst ES Y yrhs')" using Inv_ES 
-        by (auto intro!:finite_del simp:equas_subst_def Inv_def)
-      moreover have "\<exists>rhs. (X, rhs) \<in> equas_subst ES Y yrhs'" using Inv_ES not_X
-        by (auto intro:equas_subst_del_no_other simp:Inv_def)
-      moreover have "distinct_equas (equas_subst ES Y yrhs')" using Inv_ES
-        by (auto intro:equas_subst_holds_distinct simp:Inv_def)
-      moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow> ardenable (X, xrhs)"
-        using Inv_ES dist_Y' False Y'_l_eq_r
-        apply (clarsimp simp:Inv_def)
-        by (rule equas_subst_holds_ardenable, simp_all)
-      moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow> X \<noteq> {}" using Inv_ES
-        by (clarsimp simp:equas_subst_def Inv_def del_x_paired_def equas_subst_f_def split:if_splits, auto)
-      moreover have "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y yrhs' \<longrightarrow>
-                               rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equas_subst ES Y yrhs'))"
-        using Inv_ES subst cls_holds_but_Y
-        apply (rule_tac impI | rule_tac allI)+
-        by (erule equas_subst_holds_cls_defined, auto)
-      moreover have "(card (equas_subst ES Y yrhs'), card ES) \<in> less_than"using Inv_ES subst
-        by (simp add:equas_subst_card_less Inv_def)
-      ultimately show "?P (equas_subst ES Y yrhs')" by (auto simp:Inv_def)      
-    qed
-    thus ?thesis by blast
-  qed
-qed
-
-text {* ***** END: proving every equation-system's iteration step satisfies Inv ************** *}
-
-lemma iteration_conc: 
-  assumes history: "Inv X ES"
-  shows "\<exists> ES'. Inv X ES' \<and> TCon ES'" (is "\<exists> ES'. ?P ES'")
-proof (cases "TCon ES")
-  case True
-  hence "?P ES" using history by simp
-  thus ?thesis by blast
-next
-  case False  
-  thus ?thesis using history iteration_step
-    by (rule_tac f = card in wf_iter, simp_all)
-qed
-
-lemma eqset_imp_iff': "A = B \<Longrightarrow> \<forall> x. x \<in> A \<longleftrightarrow> x \<in> B"
-apply (auto simp:mem_def)
-done
-
-lemma set_cases2:
-  "\<lbrakk>(A = {} \<Longrightarrow> R A); \<And> x. (A = {x}) \<Longrightarrow> R A; \<And> x y. \<lbrakk>x \<noteq> y; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> R A\<rbrakk> \<Longrightarrow> R A"
-apply (case_tac "A = {}", simp)
-by (case_tac "\<exists> x. A = {x}", clarsimp, blast)
-
-lemma rhs_aux:"\<lbrakk>distinct_rhs rhs; {Y. \<exists>r. (Y, r) \<in> rhs} = {X}\<rbrakk> \<Longrightarrow> (\<exists>r. rhs = {(X, r)})"
-apply (rule_tac A = rhs in set_cases2, simp)
-apply (drule_tac x = X in eqset_imp_iff, clarsimp)
-apply (drule eqset_imp_iff',clarsimp)
-apply (frule_tac x = a in spec, drule_tac x = aa in spec)
-by (auto simp:distinct_rhs_def)
-
-lemma every_eqcl_has_reg: 
-  assumes finite_CS: "finite (UNIV Quo Lang)"
-  and X_in_CS: "X \<in> (UNIV Quo Lang)"
-  shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")
-proof-
-  have "\<exists>ES'. Inv X ES' \<and> TCon ES'" using finite_CS X_in_CS
-    by (auto intro:init_ES_satisfy_Inv iteration_conc)
-  then obtain ES' where Inv_ES': "Inv X ES'" 
-                   and  TCon_ES': "TCon ES'" by blast
-  from Inv_ES' TCon_ES' 
-  have "\<exists> rhs. ES' = {(X, rhs)}"
-    apply (clarsimp simp:Inv_def TCon_def)
-    apply (rule_tac x = rhs in exI)
-    by (auto dest!:card_Suc_Diff1 simp:card_eq_0_iff)  
-  then obtain rhs where ES'_single_equa: "ES' = {(X, rhs)}" ..
-  hence X_ardenable: "ardenable (X, rhs)" using Inv_ES'
-    by (simp add:Inv_def)
-  
-  from X_ardenable have X_l_eq_r: "X = L rhs"
-    by (simp add:ardenable_def)
-  hence rhs_not_empty: "rhs \<noteq> {}" using Inv_ES' ES'_single_equa
-    by (auto simp:Inv_def ardenable_def)
-  have rhs_eq_cls: "rhs_eq_cls rhs \<subseteq> {X, {[]}}"
-    using Inv_ES' ES'_single_equa
-    by (auto simp:Inv_def ardenable_def left_eq_cls_def)
-  have X_not_empty: "X \<noteq> {}" using Inv_ES' ES'_single_equa
-    by (auto simp:Inv_def)    
-  show ?thesis
-  proof (cases "X = {[]}")
-    case True
-    hence "?E EMPTY" by (simp)
-    thus ?thesis by blast
-  next
-    case False with  X_ardenable
-    have "\<exists> rhs'. X = L rhs' \<and> rhs_eq_cls rhs' = rhs_eq_cls rhs - {X} \<and> distinct_rhs rhs'"
-      by (drule_tac ardenable_prop, auto)
-    then obtain rhs' where X_eq_rhs': "X = L rhs'"
-      and rhs'_eq_cls: "rhs_eq_cls rhs' = rhs_eq_cls rhs - {X}" 
-      and rhs'_dist : "distinct_rhs rhs'" by blast
-    have "rhs_eq_cls rhs' \<subseteq> {{[]}}" using rhs_eq_cls False rhs'_eq_cls rhs_not_empty 
-      by blast
-    hence "rhs_eq_cls rhs' = {{[]}}" using X_not_empty X_eq_rhs'
-      by (auto simp:rhs_eq_cls_def)
-    hence "\<exists> r. rhs' = {({[]}, r)}" using rhs'_dist
-      by (auto intro:rhs_aux simp:rhs_eq_cls_def)
-    then obtain r where "rhs' = {({[]}, r)}" ..
-    hence "?E r" using X_eq_rhs' by (auto simp add:lang_seq_def)
-    thus ?thesis by blast     
-  qed
-qed
-
-text {* definition of a regular language *}
-
-abbreviation
-  reg :: "string set => bool"
-where
-  "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)"
-
-theorem myhill_nerode: 
-  assumes finite_CS: "finite (UNIV Quo Lang)"
-  shows   "\<exists> (reg::rexp). Lang = L reg" (is "\<exists> r. ?P r")
-proof -
-  have has_r_each: "\<forall>C\<in>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists>(r::rexp). C = L r" using finite_CS
-    by (auto dest:every_eqcl_has_reg)  
-  have "\<exists> (rS::rexp set). finite rS \<and> 
-                          (\<forall> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists> r \<in> rS. C = L r) \<and> 
-                          (\<forall> r \<in> rS. \<exists> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. C = L r)" 
-       (is "\<exists> rS. ?Q rS")
-  proof-
-    have "\<And> C. C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang} \<Longrightarrow> C = L (SOME (ra::rexp). C = L ra)"
-      using has_r_each
-      apply (erule_tac x = C in ballE, erule_tac exE)
-      by (rule_tac a = r in someI2, simp+)
-    hence "?Q ((\<lambda> C. SOME r. C = L r) ` {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang})" using has_r_each
-      using finite_CS by auto
-    thus ?thesis by blast    
-  qed
-  then obtain rS where finite_rS : "finite rS"
-    and has_r_each': "\<forall> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists> r \<in> (rS::rexp set). C = L r"
-    and has_cl_each: "\<forall> r \<in> (rS::rexp set). \<exists> C \<in> {X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. C = L r" by blast
-  have "?P (folds ALT NULL rS)"
-  proof
-    show "Lang \<subseteq> L (folds ALT NULL rS)" using finite_rS lang_eqs_union_of_eqcls[of Lang] has_r_each'
-      apply (clarsimp simp:fold_alt_null_eqs) by blast
-  next 
-    show "L (folds ALT NULL rS) \<subseteq> Lang" using finite_rS lang_eqs_union_of_eqcls[of Lang] has_cl_each
-      by (clarsimp simp:fold_alt_null_eqs)
-  qed
-  thus ?thesis by blast
-qed 
-
-
-text {* tests by Christian *}
+apply (induct arbitrary:Lang rule:rexp.induct)
+apply (simp add:QUOT_def equiv_class_def equiv_str_def)
+by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star)  
 
 (* Alternative definition for Quo *)
 definition