diff -r 85fa86398d39 -r fbd62804f153 MyhillNerode.thy
--- a/MyhillNerode.thy	Wed Nov 03 22:08:50 2010 +0000
+++ b/MyhillNerode.thy	Sat Nov 06 23:31:53 2010 +0000
@@ -740,12 +740,8 @@
   shows "X = L xrhs"    
 proof (cases "X = {[]}")
   case True
-  thus ?thesis using X_in_equas
-    unfolding equations_def 
-    unfolding equation_rhs_def 
-    apply(simp del: L_rhs.simps)
-    apply(simp add: lang_seq_def)
-    done
+  thus ?thesis using X_in_equas 
+    by (simp add:equations_def equation_rhs_def lang_seq_def)
 next
   case False 
   show ?thesis
@@ -758,32 +754,33 @@
       proof (cases "x = []")
         assume empty: "x = []"
         hence "x \<in> L (empty_rhs X)" using "(1)"
-	  unfolding empty_rhs_def
-          by (simp add: lang_seq_def)
+          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> []"
-        then obtain clist c where decom: "x = clist @ [c]" 
-	  using rev_cases by blast
-        moreover have "\<And> Y. Y-c\<rightarrow>X \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"
+        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_CT_X: "Y-c\<rightarrow>X"
+          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)
+            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)
+          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" "clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast
+          "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
+        thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def
           by auto
       qed
     qed
@@ -794,14 +791,11 @@
       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
-	unfolding CT_def
-        by (simp add: lang_seq_def fold_alt_null_eqs) (auto)
+        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)"
-        unfolding equations_def
-	unfolding equation_rhs_def
-	by (auto intro:"(2_1)" "(2_2)" simp: lang_seq_def)
+        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
@@ -1318,252 +1312,42 @@
 
 text {* tests by Christian *}
 
-(* compatibility with stable Isabelle *)
 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)"
-  by(auto intro:set_eqI)
-
-lemma folds_simp_null [simp]:
-  "finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) = (\<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
+by(auto intro:set_eqI)
 
-lemma folds_simp_empty [simp]:
-  "finite rs \<Longrightarrow> x \<in> L (folds ALT EMPTY rs) = ((\<exists>r \<in> rs. x \<in> L r) \<or> x = [])"
-apply (simp add: folds_def)
-apply (rule someI2_ex)
-apply (erule finite_imp_fold_graph)
-apply (erule fold_graph.induct)
-apply (auto)
-done
-
-abbreviation
-  str_eq ("_ \<approx>_ _")
-where
-  "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
-
-abbreviation
-  lang_eq ("\<approx>_")
+fun
+  MNRel
 where
-  "\<approx>Lang \<equiv> (\<lambda>(x, y). x \<approx>Lang y)"
-
-lemma lang_eq_is_equiv:
-  "equiv UNIV (\<approx>Lang)"
-unfolding equiv_def
-unfolding refl_on_def sym_def trans_def
-by (simp add: mem_def equiv_str_def)
-
-text {*
-  equivalence classes of x can be written
-
-    UNIV // (\<approx>Lang)``{x}
-
-  the language quotient can be written
-
-    UNIV // (\<approx>Lang)
-*}
-
-lemma
-  "(\<approx>Lang)``{x} = \<lbrakk>x\<rbrakk>Lang"
-unfolding equiv_class_def equiv_str_def Image_def mem_def
-by (simp)
-
-lemma
-  "UNIV // (\<approx>Lang) = UNIV Quo Lang"
-unfolding quotient_def quot_def 
-unfolding equiv_class_def equiv_str_def
-unfolding Image_def mem_def
-by auto
+  "MNRel Lang (x, y) = (x \<equiv>Lang\<equiv> y)"
 
 lemma
-  "{} \<notin> UNIV // (\<approx>Lang)"
-unfolding quotient_def 
-unfolding Image_def 
-apply(auto)
-apply(rule_tac x="x" in exI)
-unfolding mem_def
-apply(simp)
-done
-
-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}"
-
-definition
-  transitions_rexp ("_ \<turnstile>\<rightarrow> _")
-where
-  "Y \<turnstile>\<rightarrow> X \<equiv> if [] \<in> X then folds ALT EMPTY (Y \<Turnstile>\<Rightarrow>X) else folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"
-
-definition
-  "rhs CS X \<equiv> { (Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS }"
-
-definition
-  "rhs_sem CS X \<equiv> { (Y; L (Y \<turnstile>\<rightarrow> X)) | Y. Y \<in> CS }"
-
-definition
-  "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})"
-
-definition
-  "eqs_sem CS \<equiv> (\<Union>X \<in> CS. {(X, rhs_sem CS X)})"
-
-(*
-lemma 
-  assumes X_in_equas: "(X, rhss) \<in> (eqs_sem (UNIV // (\<approx>Lang)))"
-  shows "X = \<Union>rhss"
-using assms
-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
-*)
-
-lemma finite_rhs:
-  assumes fin: "finite CS"
-  shows "finite (rhs CS X)"
-  using fin unfolding rhs_def by (auto)
-
-lemma finite_eqs:
-  assumes fin: "finite CS"
-  shows "finite (eqs CS)"
-unfolding eqs_def
-apply(rule finite_UN_I)
-apply(rule fin)
-apply(simp add: eq_def)
+  "equiv UNIV (MNRel Lang)"
+unfolding equiv_def
+unfolding refl_on_def sym_def trans_def
+apply(auto simp add: mem_def equiv_str_def)
 done
 
 lemma
-  shows "X ; L (folds ALT NULL (X \<Turnstile>\<Rightarrow> Y)) \<subseteq> Y" 
-by (auto simp add: transitions_def lang_seq_def)
-
-lemma
-  shows "X ; L (X \<turnstile>\<rightarrow> Y) \<subseteq> Y" 
-apply (auto simp add: transitions_rexp_def transitions_def lang_seq_def)
-oops
+  "(MNRel Lang)``{x} = \<lbrakk>x\<rbrakk>Lang"
+unfolding equiv_class_def Image_def mem_def
+by (simp)
 
-lemma 
-  "equation_rhs CS X = rhs CS X"
-apply(simp only: rhs_def empty_rhs_def CT_def transitions_rexp_def transitions_def equation_rhs_def)
-oops
-
-
-
-lemma
-  shows "X ; L (X \<turnstile>\<rightarrow> Y) \<subseteq> Y" 
-apply (auto simp add: transitions_rexp_def transitions_def lang_seq_def)
-oops
+lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp 
 
 lemma
-  assumes a: "X \<in> (UNIV // (\<approx>Lang))"
-  shows "X \<subseteq> \<Union> (rhs_sem (UNIV // (\<approx>Lang)) X)"
-unfolding rhs_sem_def 
-apply (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs)
-apply(rule_tac x="X" in exI)
+  "UNIV//(MNRel (L1 \<union> L2)) \<subseteq> (UNIV//(MNRel L1)) \<union> (UNIV//(MNRel L2))"
+unfolding quotient_def
+unfolding UNION_eq_Union_image
+apply(rule tt)
+apply(rule Un_Union_image[symmetric])
 apply(simp)
-apply(simp add: quotient_def Image_def)
-apply(subst (4) mem_def)
-oops
-
-
-lemma UNIV_eq_complement:
-  "UNIV // (\<approx>Lang) = UNIV // (\<approx>(- Lang))"
-by auto
-
-lemma eq_inter:
-  fixes x y::"string"
-  shows "\<lbrakk>x \<approx>L1 y; x \<approx>L2 y\<rbrakk> \<Longrightarrow> (x \<approx>(L1 \<inter> L2) y)"
-by auto
-
-lemma equ_union:
-  fixes x y::"string"
-  shows "\<lbrakk>x \<approx>L1 y; x \<approx>L2 y\<rbrakk> \<Longrightarrow> (x \<approx>(L1 \<union> L2) y)"
-by auto
-
-(* HERE *)
-
-lemma tt:
-  "R1 \<subseteq> R2 \<Longrightarrow> R1 `` {x} \<subseteq> R2 `` {x}"
+apply(rule UN_mono)
+apply(simp)
+apply(simp)
 unfolding Image_def
-by auto
-
-lemma tt_aux:
-  "(\<approx>Lang) `` {x} = \<lbrakk>x\<rbrakk>Lang"
-unfolding Image_def
-unfolding equiv_class_def
-unfolding equiv_str_def
 unfolding mem_def
+unfolding MNRel.simps
 apply(simp)
-done
-
-lemma tt_old:
-  "(\<approx>L1) \<subseteq> (\<approx>L2) \<Longrightarrow> \<lbrakk>x\<rbrakk>L1 \<subseteq> \<lbrakk>x\<rbrakk>L2"
-unfolding tt_aux[symmetric]
-apply(simp add: tt)
-done
-
-
-
-
-lemma
-  assumes a: "finite (A // R1)" "R1 \<subseteq> R2"
-  shows "card (A // R2) <= card (A // R1)"
-using assms
-apply(induct )
-unfolding quotient_def
-apply(drule_tac tt)
-sorry 
-
-lemma other_direction_cu:
-  fixes r::"rexp"
-  shows "finite (UNIV // (\<approx>(L r)))"
-apply(induct r)
-apply(simp_all)
 oops
 
 
@@ -1574,13 +1358,13 @@
 where
   "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})"
 
-
 lemma test_01:
   "Lang \<subseteq> (\<Union> QUOT Lang)"
 unfolding QUOT_def equiv_class_def equiv_str_def
 by (blast)
 
-text{* by chunhan *}
+
+(* by chunhan *)
 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"
 proof 
   show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}"
@@ -1759,4 +1543,244 @@
 
 
 
+
+(* by chunhan *)
+
+
+lemma finite_tag_image: 
+  "finite (range tag) \<Longrightarrow> finite (((op `) tag) ` S)"
+apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset)
+by (auto simp add:image_def Pow_def)
+
+lemma str_inj_imps:
+  assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<equiv>lang\<equiv> n"
+  shows "inj_on ((op `) tag) (QUOT lang)"
+proof (clarsimp simp add:inj_on_def QUOT_def)
+  fix x y
+  assume eq_tag: "tag ` \<lbrakk>x\<rbrakk>lang = tag ` \<lbrakk>y\<rbrakk>lang"
+  show "\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang"
+  proof -
+    have aux1:"\<And>a b. a \<in> (\<lbrakk>b\<rbrakk>lang) \<Longrightarrow> (a \<equiv>lang\<equiv> b)"
+      by (simp add:equiv_class_def equiv_str_def)
+    have aux2: "\<And> A B f. \<lbrakk>f ` A = f ` B; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> a b. a \<in> A \<and> b \<in> B \<and> f a = f b"
+      by auto
+    have aux3: "\<And> a l. \<lbrakk>a\<rbrakk>l \<noteq> {}" 
+      by (auto simp:equiv_class_def equiv_str_def)
+    show ?thesis using eq_tag
+      apply (drule_tac aux2, simp add:aux3, clarsimp)
+      apply (drule_tac str_inj, (drule_tac aux1)+)
+      by (simp add:equiv_str_def equiv_class_def)
+  qed
+qed
+
+definition tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
+where
+  "tag_str_ALT L\<^isub>1 L\<^isub>2 x \<equiv> (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)"
+
+lemma tag_str_alt_range_finite:
+  assumes finite1: "finite (QUOT L\<^isub>1)"
+  and finite2: "finite (QUOT L\<^isub>2)"
+  shows "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))"
+proof -
+  have "{y. \<exists>x. y = (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"
+    by (auto simp:QUOT_def)
+  thus ?thesis using finite1 finite2
+    by (auto simp: image_def tag_str_ALT_def UNION_def 
+            intro: finite_subset[where B = "(QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"])
+qed
+
+lemma tag_str_alt_inj:
+  "tag_str_ALT L\<^isub>1 L\<^isub>2 x = tag_str_ALT L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<equiv>(L\<^isub>1 \<union> L\<^isub>2)\<equiv> y"
+apply (simp add:tag_str_ALT_def equiv_class_def equiv_str_def)
+by blast
+  
+lemma quot_alt:
+  assumes finite1: "finite (QUOT L\<^isub>1)"
+  and finite2: "finite (QUOT L\<^isub>2)"
+  shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+proof (rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD)
+  show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+    using finite_tag_image tag_str_alt_range_finite finite1 finite2
+    by auto
+next
+  show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+    apply (rule_tac str_inj_imps)
+    by (erule_tac tag_str_alt_inj)
+qed
+
+(* list_diff:: list substract, once different return tailer *)
+fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)
+where
+  "list_diff []  xs = []" |
+  "list_diff (x#xs) [] = x#xs" |
+  "list_diff (x#xs) (y#ys) = (if x = y then list_diff xs ys else (x#xs))"
+
+definition tag_str_SEQ:: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set) set"
+where
+  "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> if (\<exists> y. y \<le> x \<and> y \<in> L\<^isub>1)
+                         then {(\<lbrakk>(x - y)\<rbrakk>L\<^isub>2) | y.  y \<le> x \<and> y \<in> L\<^isub>1}
+                         else { \<lbrakk>x\<rbrakk>L\<^isub>1 }"
+
+lemma tag_str_seq_range_finite:
+  assumes finite1: "finite (QUOT L\<^isub>1)"
+  and finite2: "finite (QUOT L\<^isub>2)"
+  shows "finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))"
+proof -
+  have "(range (tag_str_SEQ L\<^isub>1 L\<^isub>2)) \<subseteq> Pow ((QUOT L\<^isub>1) \<union> (QUOT L\<^isub>2))"
+    by (auto simp:image_def tag_str_SEQ_def QUOT_def)
+  thus ?thesis using finite1 finite2 
+    by (rule_tac B = "Pow ((QUOT L\<^isub>1) \<union> (QUOT L\<^isub>2))" in finite_subset, auto)
+qed
+  
+lemma tag_str_seq_inj:
+  assumes tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
+  shows "(x::string) \<equiv>(L\<^isub>1 ; L\<^isub>2)\<equiv> y"
+proof (cases "\<exists> xa. xa \<le> x \<and> xa \<in> L\<^isub>1")
+  have equiv_str_sym: "\<And> x y lang. (x::string) \<equiv>lang\<equiv> y \<Longrightarrow> y \<equiv>lang\<equiv> x"
+    by (auto simp:equiv_str_def)
+  have set_equ_D: "\<And> A a B b. \<lbrakk>A = B; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> a b. a \<in> A \<and> b \<in> B \<and> a = b " by auto
+  have eqset_equ_D: "\<And> x y lang. {y. x \<equiv>lang\<equiv> y} = {ya. y \<equiv>lang\<equiv> ya} \<Longrightarrow> x \<equiv>lang\<equiv> y"
+    by (drule set_equ_D, auto simp:equiv_str_def)
+  assume  x_left_l1: "\<exists>xa\<le>x. xa \<in> L\<^isub>1"
+  show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+  proof (cases "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1")
+    assume y_left_l1: "\<exists>ya\<le>y. ya \<in> L\<^isub>1"
+    with tag_eq x_left_l1
+    show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+      apply (simp add:tag_str_SEQ_def)
+      apply (drule set_equ_D)
+      apply (auto simp:equiv_class_def equiv_str_def)[1]
+      apply (clarsimp simp:equiv_str_def)
+      apply (rule iffI)
+      apply  
+      apply (
+  next
+    assume y_in_l1: "\<not> (\<exists>ya\<le>y. ya \<in> L\<^isub>1)"
+    show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+      sorry
+  qed
+next
+  assume x_in_l1: "\<not> (\<exists>xa\<le>x. xa \<in> L\<^isub>1)"
+  show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+  proof (cases "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1")
+    assume y_left_l1: "\<exists>ya\<le>y. ya \<in> L\<^isub>1"
+    show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+      sorry
+  next
+    assume y_in_l1: "\<not> (\<exists>ya\<le>y. ya \<in> L\<^isub>1)"
+    with tag_eq x_in_l1
+    have "\<lbrakk>x\<rbrakk>(L\<^isub>1;L\<^isub>2) = \<lbrakk>y\<rbrakk>(L\<^isub>1;L\<^isub>2)"
+      sorry
+    thus "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+      by (auto simp:equiv_class_def equiv_str_def)
+  qed
+qed
+  
+apply (simp add:tag_str_SEQ_def split:if_splits)
+prefer 4
+apply (clarsimp simp add:equiv_str_def)
+apply (rule iffI)
+apply (simp add:lang_seq_def equiv_class_def equiv_str_def)
+apply blast
+apply (
+sorry
+
+
+lemma quot_seq: 
+  assumes finite1: "finite (QUOT L\<^isub>1)"
+  and finite2: "finite (QUOT L\<^isub>2)"
+  shows "finite (QUOT (L\<^isub>1;L\<^isub>2))"
+proof (rule_tac f = "(op `) (tag_str_SEQ L\<^isub>1 L\<^isub>2)" in finite_imageD)
+  show "finite (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 ; L\<^isub>2))"
+    using finite_tag_image tag_str_seq_range_finite finite1 finite2
+    by auto
+next
+  show "inj_on (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 ; L\<^isub>2))"
+    apply (rule_tac str_inj_imps)
+    by (erule_tac tag_str_seq_inj)
+qed
+
+definition tag_str_STAR:: "string set \<Rightarrow> string \<Rightarrow> (string set) set"
+where
+  "tag_str_STAR L\<^isub>1 x = {\<lbrakk>y\<rbrakk>L\<^isub>1 | y. y \<le> x}"
+
+lemma tag_str_star_range_finite:
+  assumes finite1: "finite (QUOT L\<^isub>1)"
+  shows "finite (range (tag_str_STAR L\<^isub>1))"
+proof -
+  have "range (tag_str_STAR L\<^isub>1) \<subseteq> Pow (QUOT L\<^isub>1)"
+    by (auto simp:image_def tag_str_STAR_def QUOT_def)
+  thus ?thesis using finite1
+    by (rule_tac B = "Pow (QUOT L\<^isub>1)" in finite_subset, auto)
+qed
+
+lemma tag_str_star_inj:
+  "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 (y::string) \<Longrightarrow> x \<equiv>L\<^isub>1\<star>\<equiv> y"
+proof -
+  have "\<forall> x lang. (x = []) = (tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang})"
+  proof (rule_tac allI, rule_tac allI, rule_tac iffI)
+    fix x lang
+    show "x = [] \<Longrightarrow> tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang}" 
+      by (simp add:tag_str_STAR_def)
+  next    
+    fix x lang
+    show "tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang} \<Longrightarrow> x = []"
+      apply (simp add:tag_str_STAR_def)
+      apply (drule equalityD1)
+      apply (case_tac x)
+      apply simp
+      thm in_mono
+      apply (drule_tac x = "\<lbrakk>[a]\<rbrakk>lang" in in_mono)
+      apply simp
+      apply auto
+      
+      apply (erule subsetCE)
+      
+      apply (case_tac y)
+      
+      sorry
+  next
+  qed
+    apply (simp add:tag_str_STAR_def equiv_class_def equiv_str_def)
+    apply (rule iffI)
+    
+    apply (auto simp:tag_str_STAR_def equiv_class_def equiv_str_def)
+  have "\<And> x y z xstr. xstr \<in> L\<^isub>1\<star> \<Longrightarrow> 
+                      xstr = x @ z \<and> tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y \<longrightarrow> y @ z \<in> L\<^isub>1\<star> "
+  proof (erule Star.induct)
+    fix x y z xstr
+    show "[] = x @ z \<and> tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y \<longrightarrow> y @ z \<in> L\<^isub>1\<star>"
+    apply (clarsimp simp add:tag_str_STAR_def equiv_str_def equiv_class_def)
+    apply (blast)
+apply (simp add:tag_str_STAR_def equiv_class_def QUOT_def)
+apply (simp add:equiv_str_def)
+apply (rule allI, rule_tac iffI)
+apply (erule_tac star.induct)
+apply blast
+
+sorry
+
+
+lemma quot_star:  
+  assumes finite1: "finite (QUOT L\<^isub>1)"
+  shows "finite (QUOT (L\<^isub>1\<star>))"
+proof (rule_tac f = "(op `) (tag_str_STAR L\<^isub>1)" in finite_imageD)
+  show "finite (op ` (tag_str_STAR L\<^isub>1) ` QUOT (L\<^isub>1\<star>))"
+    using finite_tag_image tag_str_star_range_finite finite1
+    by auto
+next
+  show "inj_on (op ` (tag_str_STAR L\<^isub>1)) (QUOT (L\<^isub>1\<star>))"
+    apply (rule_tac str_inj_imps)
+    by (erule_tac tag_str_star_inj)
+qed
+
+lemma other_direction:
+  "Lang = L (r::rexp) \<Longrightarrow> finite (QUOT Lang)"
+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)  
+
+
+
+
 end
\ No newline at end of file