the ALT case is done;
the other two cases:
the relation is defined by not proved on inj part.
--- 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