regexp: comparison MyhillNerode.thy

equal deleted inserted replaced

-:0792821035b6
+:e31b733ace44
 theory MyhillNerode
-imports "Main"
+imports "Main" "List_Prefix"
 begin
 text {* sequential composition of languages *}
 definition
 definition
 quot :: "string set \<Rightarrow> string set \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100)
 where
 "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}"
 lemma lang_eqs_union_of_eqcls:
-"Lang = (\<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)})"
+"Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}"
 proof
 show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}"
 proof
 fix x
 assume "x \<in> Lang"
 next
 show "\<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang} \<subseteq> Lang"
 by auto
 qed
 lemma empty_notin_CS: "{} \<notin> UNIV Quo Lang"
 apply (clarsimp simp:quot_def equiv_class_def)
 by (rule_tac x = x in exI, auto simp:equiv_str_def)
 lemma no_two_cls_inters:
 text {* equiv_class transition *}
 definition
 CT :: "string set \<Rightarrow> char \<Rightarrow> string set \<Rightarrow> bool" ("_-_\<rightarrow>_" [99,99]99)
 where
-"X-c\<rightarrow>Y \<equiv> ( X; {[c]} \<subseteq> Y)"
+"X-c\<rightarrow>Y \<equiv> ((X;{[c]}) \<subseteq> Y)"
 types t_equa_rhs = "(string set \<times> rexp) set"
 types t_equa = "(string set \<times> t_equa_rhs)"
 definition
 equation_rhs :: "(string set) set \<Rightarrow> string set \<Rightarrow> t_equa_rhs"
 where
 "equation_rhs CS X \<equiv> if (X = {[]}) then {({[]}, EMPTY)}
 else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X"
 definition
 equations :: "(string set) set \<Rightarrow> t_equas"
 where
 "equations CS \<equiv> {(X, equation_rhs CS X) | X. X \<in> CS}"
 qed
 qed
 qed
 text {*
-merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} =
+merge_rhs {(x1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} =
 {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \<dots>} *}
 definition
 merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs"
 where
 "merge_rhs rhs rhs' \<equiv> {(X, r). (\<exists> r1 r2. ((X,r1) \<in> rhs \<and> (X, r2) \<in> rhs') \<and> r = ALT r1 r2)  \<or>
 (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or>
 (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2)    }"
 text {* rhs_subst rhs X=xrhs r: substitude all occurence of X in rhs((X,r) \<in> rhs) with xrhs *}
 definition
 rhs_subst :: "t_equa_rhs \<Rightarrow> string set \<Rightarrow> t_equa_rhs \<Rightarrow> rexp \<Rightarrow> t_equa_rhs"
 Inv: Invairance of the equation-system, during the decrease of the equation-system, Inv holds.
 *}
 definition Inv :: "string set \<Rightarrow> t_equas \<Rightarrow> bool"
 where
 "Inv X ES \<equiv> finite ES \<and> (\<exists> rhs. (X, rhs) \<in> ES) \<and> distinct_equas ES \<and>
-(\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs
+(\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls ES))"
-\<subseteq> insert {[]} (left_eq_cls ES))"
 text {*
 TCon: Termination Condition of the equation-system decreasion.
 *}
 definition TCon:: "'a set \<Rightarrow> bool"
 "TCon ES \<equiv> card ES = 1"
 text {*
 The following is a iteration principle, and is the main framework for the proof:
+1: We can form the initial equation-system using "equations" defined above, and prove it has invariance Inv by lemma "init_ES_satisfy_Inv";
+2: We can decrease the number of the equation-system using ardens_lemma_revised and substitution ("equas_subst", defined above),
+and prove it holds the property "step" in "wf_iter" by lemma "iteration_step"
+and finally using property Inv and TCon to prove the myhill-nerode theorem
-1: We can form the initial equation-system using "equations" defined above,
-and prove it has invariance Inv by lemma "init_ES_satisfy_Inv";
-2: We can decrease the number of the equation-system using ardens_lemma_revised
-and substitution ("equas_subst", defined above),
-and prove it holds the property "step" in "wf_iter" by lemma "iteration_step"
-and finally using property Inv and TCon to prove the myhill-nerode theorem
 *}
 lemma wf_iter [rule_format]:
 fixes f
 assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and>  (f(e'), f(e)) \<in> less_than)"
 shows pe:     "P e \<longrightarrow> (\<exists> e'. P e' \<and>  Q e')"
 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}",
+apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+
-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 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}"
+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'")
-(is "\<exists> yrhs'. ?P yrhs'")
 proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)")
 case True
 thus ?thesis
 proof
 fix reg
 qed
 text {* tests by Christian *}
-lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)"
+(* Alternative definition for Quo *)
-by(auto intro:set_eqI)
-fun
-MNRel
-where
-"MNRel Lang (x, y) = (x \<equiv>Lang\<equiv> y)"
-lemma
-"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
-"(MNRel Lang)``{x} = \<lbrakk>x\<rbrakk>Lang"
-unfolding equiv_class_def Image_def mem_def
-by (simp)
-lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp
-lemma
-"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(rule UN_mono)
-apply(simp)
-apply(simp)
-unfolding Image_def
-unfolding mem_def
-unfolding MNRel.simps
-apply(simp)
-oops
-text {* Alternative definition for Quo *}
 definition
 QUOT :: "string set \<Rightarrow> (string set) set"
 where
 "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})"
-lemma test_01:
+lemma test:
-"Lang \<subseteq> (\<Union> QUOT Lang)"
+"UNIV Quo Lang = QUOT Lang"
-unfolding QUOT_def equiv_class_def equiv_str_def
+by (auto simp add: quot_def QUOT_def)
-by (blast)
+lemma test1:
+assumes finite_CS: "finite (QUOT Lang)"
-(* by chunhan *)
+shows "reg Lang"
+using finite_CS
+unfolding test[symmetric]
+by (auto dest: myhill_nerode)
+lemma cons_one: "x @ y \<in> {z} \<Longrightarrow> x @ y = z"
+by simp
 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"
 proof
 show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}"
 proof
 fix x
 by (auto simp add:equiv_str_def)
 moreover have "xa = [c] \<Longrightarrow> x = {[c]}"
 proof -
 have "xa = [c] \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = {[c]}" using in_eqiv
 apply (simp add:equiv_str_def)
-apply (rule temp_set_ext, rule iffI, simp)
+apply (rule set_ext, rule iffI, simp)
 apply (drule_tac x = "[]" in spec, auto)
 done
 thus "xa = [c] \<Longrightarrow> x = {[c]}" using in_eqiv by simp
 qed
 moreover have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}"
 proof -
 have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = UNIV - {[],[c]}"
 apply (clarsimp simp add:equiv_str_def)
-apply (rule temp_set_ext, rule iffI, simp)
+apply (rule set_ext, rule iffI, simp)
 apply (rule conjI)
 apply (drule_tac x = "[c]" in spec, simp)
 apply (drule_tac x = "[]" in spec, simp)
 by (auto dest:quot_single_aux)
 thus "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}" using in_eqiv by simp
 apply (simp add:QUOT_def equiv_class_def equiv_str_def)
 by (rule_tac x = "[]" in exI, auto)
 moreover have "x = {[c]} \<Longrightarrow> x \<in> QUOT {[c]}"
 apply (simp add:QUOT_def equiv_class_def equiv_str_def)
 apply (rule_tac x = "[c]" in exI, simp)
-apply (rule temp_set_ext, rule iffI, simp+)
+apply (rule set_ext, rule iffI, simp+)
 by (drule_tac x = "[]" in spec, simp)
 moreover have "x = UNIV - {[],[c]} \<Longrightarrow> x \<in> QUOT {[c]}"
 using exist_another
 apply (clarsimp simp add:QUOT_def equiv_class_def equiv_str_def)
 apply (rule_tac x = "[a]" in exI, simp)
-apply (rule temp_set_ext, rule iffI, simp)
+apply (rule set_ext, rule iffI, simp)
 apply (clarsimp simp:quot_single_aux, simp)
 apply (rule conjI)
 apply (drule_tac x = "[c]" in spec, simp)
 by (drule_tac x = "[]" in spec, simp)
 ultimately show ?thesis using in_res by blast
 qed
 qed
 qed
 qed
-lemma quot_seq:
+lemma eq_class_imp_eq_str:
-assumes finite1: "finite (QUOT L\<^isub>1)"
+"\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang \<Longrightarrow> x \<equiv>lang\<equiv> y"
-and finite2: "finite (QUOT L\<^isub>2)"
+by (auto simp:equiv_class_def equiv_str_def)
-shows "finite (QUOT (L\<^isub>1;L\<^isub>2))"
-apply (simp add:QUOT_def equiv_class_def equiv_str_def)
-sorry
-lemma a:
-"\<lbrakk>x \<equiv>L1\<equiv> y \<and> x \<equiv>L2\<equiv> y\<rbrakk> \<Longrightarrow> x \<equiv>(L1 \<union> L2)\<equiv> y"
-apply(simp add: equiv_str_def)
-done
-(*
-lemma quot_star:
-assumes finite1: "finite (QUOT L\<^isub>1)"
-shows "finite (QUOT (L\<^isub>1\<star>))"
-sorry
-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)
-lemma test:
-"UNIV Quo Lang = QUOT Lang"
-by (auto simp add: quot_def QUOT_def)
-*)
-(* 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)
-term image
-term "(op `) tag"
 lemma str_inj_imps:
 assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<equiv>lang\<equiv> n"
-shows "inj_on (image tag) (QUOT lang)"
+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 -
 apply (drule_tac str_inj, (drule_tac aux1)+)
 by (simp add:equiv_str_def equiv_class_def)
 qed
 qed
-definition
+definition tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
-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
-"{(\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2) | x. True} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"
-unfolding QUOT_def
-by (auto)
 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)"
-unfolding QUOT_def
+by (auto simp:QUOT_def)
-by auto
 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 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 -
+proof (rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD)
-have "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+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
-moreover
+next
-have "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+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)
-ultimately
+qed
-show "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
-qed
-(*by cu *)
-definition
-str_eq ("_ \<approx>_ _")
-where
-"x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
-definition
-str_eq_rel ("\<approx>_")
-where
-"\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"
-lemma [simp]:
-"(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
-by simp
-lemma inj_image_lang:
-fixes f::"string \<Rightarrow> 'a"
-assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y"
-shows "inj_on (image f) (UNIV // (\<approx>Lang))"
-proof -
-{ fix x y::string
-assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}"
-moreover
-have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto
-ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast
-then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto
-then have "x \<approx>Lang y" unfolding str_eq_def by simp
-then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp
-}
-then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y"
-unfolding quotient_def Image_def str_eq_rel_def by simp
-then show "inj_on (image f) (UNIV // (\<approx>Lang))"
-unfolding inj_on_def by simp
-qed
-lemma finite_range_image:
-assumes fin: "finite (range f)"
-shows "finite ((image f) ` X)"
-proof -
-from fin have "finite (Pow (f ` UNIV))" by auto
-moreover
-have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto
-ultimately show "finite ((image f) ` X)" using finite_subset by auto
-qed
-definition
-tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
-where
-"tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
-lemma tag1_range_finite:
-assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)"
-and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
-shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
-proof -
-have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto
-moreover
-have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)"
-unfolding tag1_def quotient_def by auto
-ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
-using finite_subset by blast
-qed
-lemma tag1_inj:
-"tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
-unfolding tag1_def Image_def str_eq_rel_def str_eq_def
-by auto
-lemma quot_alt_cu:
-fixes L\<^isub>1 L\<^isub>2::"string set"
-assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)"
-and fin2: "finite (UNIV // \<approx>L\<^isub>2)"
-shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
-proof -
-have "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
-using fin1 fin2 tag1_range_finite by simp
-then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))"
-using finite_range_image by blast
-moreover
-have "\<And>x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
-using tag1_inj by simp
-then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
-using inj_image_lang by blast
-ultimately
-show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
-qed
-(* by chunhan *)
 (* 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"
+lemma [simp]: "(x @ y) - x = y"
-where
+apply (induct x)
-"tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> if (\<exists> y. y \<le> x \<and> y \<in> L\<^isub>1)
+by (case_tac y, simp+)
-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 [simp]: "x - x = []"
+by (induct x, auto)
+lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y "
+by (induct x, auto)
+lemma [simp]: "x - [] = x"
+by (induct x, auto)
+lemma [simp]: "xa \<le> x \<Longrightarrow> (x @ y) - xa = (x - xa) @ y"
+by (auto elim:prefixE)
+definition tag_str_SEQ:: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set set)"
+where
+"tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> if (\<exists> xa \<le> x. xa \<in> L\<^isub>1)
+then (\<lbrakk>x\<rbrakk>L\<^isub>1, {\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 | xa.  xa \<le> x \<and> xa \<in> L\<^isub>1})
+else (\<lbrakk>x\<rbrakk>L\<^isub>1, {})"
+lemma tag_seq_eq_E:
+"tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y \<Longrightarrow>
+((\<exists> xa \<le> x. xa \<in> L\<^isub>1) \<and> \<lbrakk>x\<rbrakk>L\<^isub>1 = \<lbrakk>y\<rbrakk>L\<^isub>1 \<and>
+{\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 | xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = {\<lbrakk>(y - ya)\<rbrakk>L\<^isub>2 | ya. ya \<le> y \<and> ya \<in> L\<^isub>1} ) \<or>
+((\<forall> xa \<le> x. xa \<notin> L\<^isub>1) \<and> \<lbrakk>x\<rbrakk>L\<^isub>1 = \<lbrakk>y\<rbrakk>L\<^isub>1)"
+by (simp add:tag_str_SEQ_def split:if_splits, blast)
 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))"
+have "(range (tag_str_SEQ L\<^isub>1 L\<^isub>2)) \<subseteq> (QUOT L\<^isub>1) \<times> (Pow (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)
+by (rule_tac B = "(QUOT L\<^isub>1) \<times> (Pow (QUOT L\<^isub>2))" in finite_subset, auto)
 qed
+lemma app_in_seq_decom[rule_format]:
+"\<forall> x. x @ z \<in> L\<^isub>1 ; L\<^isub>2 \<longrightarrow> (\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or>
+(\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)"
+apply (induct z)
+apply (simp, rule allI, rule impI, rule disjI1)
+apply (clarsimp simp add:lang_seq_def)
+apply (rule_tac x = s1 in exI, simp)
+apply (rule allI | rule impI)+
+apply (drule_tac x = "x @ [a]" in spec, simp)
+apply (erule exE | erule conjE | erule disjE)+
+apply (rule disjI2, rule_tac x = "[a]" in exI, simp)
+apply (rule disjI1, rule_tac x = xa in exI, simp)
+apply (erule exE | erule conjE)+
+apply (rule disjI2, rule_tac x = "a # za" in exI, simp)
+done
 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")
+proof -
-have equiv_str_sym: "\<And> x y lang. (x::string) \<equiv>lang\<equiv> y \<Longrightarrow> y \<equiv>lang\<equiv> x"
+have aux: "\<And> x y z. \<lbrakk>tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y; x @ z \<in> L\<^isub>1 ; L\<^isub>2\<rbrakk>
-by (auto simp:equiv_str_def)
+\<Longrightarrow> y @ z \<in> L\<^isub>1 ; L\<^isub>2"
-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
+proof (drule app_in_seq_decom, erule disjE)
-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"
+fix x y z
-by (drule set_equ_D, auto simp:equiv_str_def)
+assume tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
-assume  x_left_l1: "\<exists>xa\<le>x. xa \<in> L\<^isub>1"
+and x_gets_l2: "\<exists>xa\<le>x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2"
-show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+from x_gets_l2 have "\<exists> xa \<le> x. xa \<in> L\<^isub>1" by blast
-proof (cases "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1")
+hence xy_l2:"{\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 | xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = {\<lbrakk>(y - ya)\<rbrakk>L\<^isub>2 | ya. ya \<le> y \<and> ya \<in> L\<^isub>1}"
-assume y_left_l1: "\<exists>ya\<le>y. ya \<in> L\<^isub>1"
+using tag_eq tag_seq_eq_E by blast
-with tag_eq x_left_l1
+from x_gets_l2 obtain xa where xa_le_x: "xa \<le> x"
-show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+and xa_in_l1: "xa \<in> L\<^isub>1"
-apply (simp add:tag_str_SEQ_def)
+and rest_in_l2: "(x - xa) @ z \<in> L\<^isub>2" by blast
-apply (drule set_equ_D)
+hence "\<exists> ya. \<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 = \<lbrakk>(y - ya)\<rbrakk>L\<^isub>2 \<and> ya \<le> y \<and> ya \<in> L\<^isub>1" using xy_l2 by auto
-apply (auto simp:equiv_class_def equiv_str_def)[1]
+then obtain ya where ya_le_x: "ya \<le> y"
-apply (clarsimp simp:equiv_str_def)
+and ya_in_l1: "ya \<in> L\<^isub>1"
-apply (rule iffI)
+and rest_eq: "\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 = \<lbrakk>(y - ya)\<rbrakk>L\<^isub>2" by blast
-apply
+from rest_eq rest_in_l2 have "(y - ya) @ z \<in> L\<^isub>2"
-apply (
+by (auto simp:equiv_class_def equiv_str_def)
+hence "ya @ ((y - ya) @ z) \<in> L\<^isub>1 ; L\<^isub>2" using ya_in_l1
+by (auto simp:lang_seq_def)
+thus "y @ z \<in> L\<^isub>1 ; L\<^isub>2" using ya_le_x
+by (erule_tac prefixE, simp)
 next
-assume y_in_l1: "\<not> (\<exists>ya\<le>y. ya \<in> L\<^isub>1)"
+fix x y z
-show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+assume tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
-sorry
+and x_gets_l1: "\<exists>za\<le>z. x @ za \<in> L\<^isub>1 \<and> z - za \<in> L\<^isub>2"
+from tag_eq tag_seq_eq_E have x_y_eq: "\<lbrakk>x\<rbrakk>L\<^isub>1 = \<lbrakk>y\<rbrakk>L\<^isub>1" by blast
+from x_gets_l1 obtain za where za_le_z: "za \<le> z"
+and x_za_in_l1: "(x @ za) \<in> L\<^isub>1"
+and rest_in_l2: "z - za \<in> L\<^isub>2" by blast
+from x_y_eq x_za_in_l1 have y_za_in_l1: "y @ za \<in> L\<^isub>1"
+by (auto simp:equiv_class_def equiv_str_def)
+hence "(y @ za) @ (z - za) \<in> L\<^isub>1 ; L\<^isub>2" using rest_in_l2
+apply (simp add:lang_seq_def)
+by (rule_tac x = "y @ za" in exI, rule_tac x = "z - za" in exI, simp)
+thus "y @ z \<in> L\<^isub>1 ; L\<^isub>2" using za_le_z
+by (erule_tac prefixE, simp)
 qed
-next
+show ?thesis using tag_eq
-assume x_in_l1: "\<not> (\<exists>xa\<le>x. xa \<in> L\<^isub>1)"
+apply (simp add:equiv_str_def)
-show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
+by (auto intro:aux)
-proof (cases "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1")
+qed
-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))"
 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"
+(****************** the STAR case ************************)
-where
-"tag_str_STAR L\<^isub>1 x = {\<lbrakk>y\<rbrakk>L\<^isub>1 | y. y \<le> x}"
+lemma app_eq_elim[rule_format]:
+"\<And> a. \<forall> b x y. a @ b = x @ y \<longrightarrow> (\<exists> aa ab. a = aa @ ab \<and> x = aa \<and> y = ab @ b) \<or>
+(\<exists> ba bb. b = ba @ bb \<and> x = a @ ba \<and> y = bb \<and> ba \<noteq> [])"
+apply (induct_tac a rule:List.induct, simp)
+apply (rule allI | rule impI)+
+by (case_tac x, auto)
+definition tag_str_STAR:: "string set \<Rightarrow> string \<Rightarrow> string set set"
+where
+"tag_str_STAR L\<^isub>1 x \<equiv> if (x = [])
+then {}
+else {\<lbrakk>x\<^isub>2\<rbrakk>L\<^isub>1 | x\<^isub>1 x\<^isub>2. x =  x\<^isub>1 @ x\<^isub>2 \<and> x\<^isub>1 \<in> L\<^isub>1\<star> \<and> x\<^isub>2 \<noteq> []}"
 lemma tag_str_star_range_finite:
 assumes finite1: "finite (QUOT L\<^isub>1)"
 shows "finite (range (tag_str_STAR L\<^isub>1))"
 proof -
 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 star_prop[rule_format]: "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>"
+by (erule Star.induct, auto)
+lemma star_prop2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>"
+by (drule step[of y lang "[]"], auto simp:start)
+lemma star_prop3[rule_format]: "x \<in> lang\<star> \<Longrightarrow> \<forall>y . y \<in> lang \<longrightarrow> x @ y \<in> lang\<star>"
+by (erule Star.induct, auto intro:star_prop2)
+lemma postfix_prop: "y >>= (x @ y) \<Longrightarrow> x = []"
+by (erule postfixE, induct x arbitrary:y, auto)
+lemma inj_aux:
+"\<lbrakk>(m @ z) \<in> L\<^isub>1\<star>; m \<equiv>L\<^isub>1\<equiv> yb; xa @ m = x; xa \<in> L\<^isub>1\<star>; m \<noteq> [];
+\<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= m\<rbrakk>
+\<Longrightarrow> (yb @ z) \<in> L\<^isub>1\<star>"
+proof-
+have "\<And>s. s \<in> L\<^isub>1\<star> \<Longrightarrow> \<forall> m z yb. (s = m @ z \<and> m \<equiv>L\<^isub>1\<equiv> yb \<and> x = xa @ m \<and> xa \<in> L\<^isub>1\<star> \<and> m \<noteq> [] \<and>
+(\<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= m) \<longrightarrow> (yb @ z) \<in> L\<^isub>1\<star>)"
+apply (erule Star.induct, simp)
+apply (rule allI | rule impI | erule conjE)+
+apply (drule app_eq_elim)
+apply (erule disjE | erule exE | erule conjE)+
+apply simp
+apply (simp (no_asm) only:append_assoc[THEN sym])
+apply (rule step)
+apply (simp add:equiv_str_def)
+apply simp
+apply (erule exE | erule conjE)+
+apply (rotate_tac 3)
+apply (frule_tac x = "xa @ s1" in spec)
+apply (rotate_tac 12)
+apply (drule_tac x = ba in spec)
+apply (erule impE)
+apply ( simp add:star_prop3)
+apply (simp)
+apply (drule postfix_prop)
+apply simp
+done
+thus "\<lbrakk>(m @ z) \<in> L\<^isub>1\<star>; m \<equiv>L\<^isub>1\<equiv> yb; xa @ m = x; xa \<in> L\<^isub>1\<star>; m \<noteq> [];
+\<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= m\<rbrakk>
+\<Longrightarrow> (yb @ z) \<in> L\<^isub>1\<star>" by blast
+qed
+lemma min_postfix_exists[rule_format]:
+"finite A \<Longrightarrow> A \<noteq> {} \<and> (\<forall> a \<in> A. \<forall> b \<in> A. ((b >>= a) \<or> (a >>= b)))
+\<longrightarrow> (\<exists> min. (min \<in> A \<and> (\<forall> a \<in> A. a >>= min)))"
+apply (erule finite.induct)
+apply simp
+apply simp
+apply (case_tac "A = {}")
+apply simp
+apply clarsimp
+apply (case_tac "a >>= min")
+apply (rule_tac x = min in exI, simp)
+apply (rule_tac x = a in exI, simp)
+apply clarify
+apply (rotate_tac 5)
+apply (erule_tac x = aa in ballE) defer apply simp
+apply (erule_tac ys = min in postfix_trans)
+apply (erule_tac x = min in ballE)
+by simp+
 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})"
+have aux: "\<And> x y z. \<lbrakk>tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y; x @ z \<in> L\<^isub>1\<star>\<rbrakk> \<Longrightarrow> y @ z \<in> L\<^isub>1\<star>"
-proof (rule_tac allI, rule_tac allI, rule_tac iffI)
+proof-
-fix x lang
+fix x y z
-show "x = [] \<Longrightarrow> tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang}"
+assume tag_eq: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
-by (simp add:tag_str_STAR_def)
+and x_z: "x @ z \<in> L\<^isub>1\<star>"
-next
+show "y @ z \<in> L\<^isub>1\<star>"
-fix x lang
+proof (cases "x = []")
-show "tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang} \<Longrightarrow> x = []"
+case True
-apply (simp add:tag_str_STAR_def)
+with tag_eq have "y = []" by (simp add:tag_str_STAR_def split:if_splits, blast)
-apply (drule equalityD1)
+thus ?thesis using x_z True by simp
-apply (case_tac x)
+next
-apply simp
+case False
-thm in_mono
+hence not_empty: "{xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>} \<noteq> {}" using x_z
-apply (drule_tac x = "\<lbrakk>[a]\<rbrakk>lang" in in_mono)
+by (simp, rule_tac x = x in exI, rule_tac x = "[]" in exI, simp add:start)
-apply simp
+have finite_set: "finite {xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>}"
-apply auto
+apply (rule_tac B = "{xb. \<exists> xa. x = xa @ xb}" in finite_subset)
+apply auto
-apply (erule subsetCE)
+apply (induct x, simp)
+apply (subgoal_tac "{xb. \<exists>xa. a # x = xa @ xb} = insert (a # x) {xb. \<exists>xa. x = xa @ xb}")
-apply (case_tac y)
+apply auto
+by (case_tac xaa, simp+)
-sorry
+have comparable: "\<forall> a \<in> {xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>}.
-next
+\<forall> b \<in> {xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>}.
+((b >>= a) \<or> (a >>= b))"
+by (auto simp:postfix_def, drule app_eq_elim, blast)
+hence "\<exists> min. min \<in> {xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>}
+\<and> (\<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= min)"
+using finite_set not_empty comparable
+apply (drule_tac min_postfix_exists, simp)
+by (erule exE, rule_tac x = min in exI, auto)
+then obtain min xa where x_decom: "x = xa @ min \<and> xa \<in> L\<^isub>1\<star>"
+and min_not_empty: "min \<noteq> []"
+and min_z_in_star: "min @ z \<in> L\<^isub>1\<star>"
+and is_min: "\<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= min"  by blast
+from x_decom min_not_empty have "\<lbrakk>min\<rbrakk>L\<^isub>1 \<in> tag_str_STAR L\<^isub>1 x"  by (auto simp:tag_str_STAR_def)
+hence "\<exists> yb. \<lbrakk>yb\<rbrakk>L\<^isub>1 \<in> tag_str_STAR L\<^isub>1 y \<and> \<lbrakk>min\<rbrakk>L\<^isub>1 = \<lbrakk>yb\<rbrakk>L\<^isub>1" using tag_eq by auto
+hence "\<exists> ya yb. y = ya @ yb \<and> ya \<in> L\<^isub>1\<star> \<and> min \<equiv>L\<^isub>1\<equiv> yb \<and> yb \<noteq> [] "
+by (simp add:tag_str_STAR_def equiv_class_def equiv_str_def split:if_splits, blast)
+then obtain ya yb where y_decom: "y = ya @ yb"
+and ya_in_star: "ya \<in> L\<^isub>1\<star>"
+and yb_not_empty: "yb \<noteq> []"
+and min_yb_eq: "min \<equiv>L\<^isub>1\<equiv> yb"  by blast
+from min_z_in_star min_yb_eq min_not_empty is_min x_decom
+have "yb @ z \<in> L\<^isub>1\<star>"
+by (rule_tac x = x and xa = xa in inj_aux, simp+)
+thus ?thesis using ya_in_star y_decom
+by (auto dest:star_prop)
+qed
 qed
-apply (simp add:tag_str_STAR_def equiv_class_def equiv_str_def)
+show "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 (y::string) \<Longrightarrow> x \<equiv>L\<^isub>1\<star>\<equiv> y"
-apply (rule iffI)
+by (auto intro:aux simp:equiv_str_def)
+qed
-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)
 "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
-end

changeset 23	e31b733ace44
parent 19	48744a7f2661