--- a/MyhillNerode.thy Wed Nov 10 11:59:29 2010 +0000
+++ b/MyhillNerode.thy Thu Nov 18 11:39:17 2010 +0000
@@ -1,5 +1,5 @@
theory MyhillNerode
- imports "Main"
+ imports "Main" "List_Prefix"
begin
text {* sequential composition of languages *}
@@ -281,8 +281,9 @@
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
@@ -304,7 +305,6 @@
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)
@@ -317,7 +317,7 @@
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"
@@ -345,7 +345,7 @@
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"
+ 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"
@@ -498,14 +498,14 @@
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) }"
+ (\<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 *}
@@ -631,8 +631,7 @@
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
- \<subseteq> insert {[]} (left_eq_cls ES))"
+ (\<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))"
text {*
TCon: Termination Condition of the equation-system decreasion.
@@ -644,14 +643,11 @@
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
@@ -806,8 +802,7 @@
"(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)+
+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:
@@ -894,8 +889,7 @@
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'")
+ 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
@@ -1312,59 +1306,26 @@
text {* tests by Christian *}
-lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)"
-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 *}
+(* 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:
- "Lang \<subseteq> (\<Union> QUOT Lang)"
-unfolding QUOT_def equiv_class_def equiv_str_def
-by (blast)
+lemma test:
+ "UNIV Quo Lang = QUOT Lang"
+by (auto simp add: quot_def QUOT_def)
+lemma test1:
+ assumes finite_CS: "finite (QUOT Lang)"
+ shows "reg Lang"
+using finite_CS
+unfolding test[symmetric]
+by (auto dest: myhill_nerode)
-(* by chunhan *)
+lemma cons_one: "x @ y \<in> {z} \<Longrightarrow> x @ y = z"
+by simp
+
lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"
proof
show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}"
@@ -1446,7 +1407,7 @@
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
@@ -1455,7 +1416,7 @@
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)
@@ -1481,13 +1442,13 @@
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)
@@ -1498,53 +1459,18 @@
qed
qed
-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))"
-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 eq_class_imp_eq_str:
+ "\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang \<Longrightarrow> x \<equiv>lang\<equiv> y"
+by (auto simp:equiv_class_def equiv_str_def)
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"
@@ -1563,24 +1489,17 @@
qed
qed
-definition
- tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
+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
- "{(\<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
+ 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)"])
@@ -1595,111 +1514,16 @@
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 -
- have "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` 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
- moreover
- have "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+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)
- ultimately
- 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
@@ -1707,76 +1531,108 @@
"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"
+apply (induct x)
+by (case_tac y, simp+)
+
+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> 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 }"
+ "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")
- 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 (
+proof -
+ 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>
+ \<Longrightarrow> y @ z \<in> L\<^isub>1 ; L\<^isub>2"
+ proof (drule app_in_seq_decom, erule disjE)
+ fix x y z
+ assume tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
+ and x_gets_l2: "\<exists>xa\<le>x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2"
+ from x_gets_l2 have "\<exists> xa \<le> x. xa \<in> L\<^isub>1" by blast
+ 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}"
+ using tag_eq tag_seq_eq_E by blast
+ from x_gets_l2 obtain xa where xa_le_x: "xa \<le> x"
+ and xa_in_l1: "xa \<in> L\<^isub>1"
+ and rest_in_l2: "(x - xa) @ z \<in> L\<^isub>2" by blast
+ 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
+ then obtain ya where ya_le_x: "ya \<le> y"
+ and ya_in_l1: "ya \<in> L\<^isub>1"
+ and rest_eq: "\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 = \<lbrakk>(y - ya)\<rbrakk>L\<^isub>2" by blast
+ from rest_eq rest_in_l2 have "(y - ya) @ z \<in> L\<^isub>2"
+ 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)"
- show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
- sorry
+ fix x y z
+ assume tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
+ 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
- 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
+ show ?thesis using tag_eq
+ apply (simp add:equiv_str_def)
+ by (auto intro:aux)
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)"
@@ -1792,9 +1648,20 @@
by (erule_tac tag_str_seq_inj)
qed
-definition tag_str_STAR:: "string set \<Rightarrow> string \<Rightarrow> (string set) set"
+(****************** the STAR case ************************)
+
+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 = {\<lbrakk>y\<rbrakk>L\<^isub>1 | y. y \<le> x}"
+ "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)"
@@ -1806,52 +1673,126 @@
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})"
- 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
+ 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-
+ fix x y z
+ assume tag_eq: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
+ and x_z: "x @ z \<in> L\<^isub>1\<star>"
+ show "y @ z \<in> L\<^isub>1\<star>"
+ proof (cases "x = []")
+ case True
+ with tag_eq have "y = []" by (simp add:tag_str_STAR_def split:if_splits, blast)
+ thus ?thesis using x_z True by simp
+ next
+ case False
+ 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
+ by (simp, rule_tac x = x in exI, rule_tac x = "[]" in exI, simp add:start)
+ 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 (rule_tac B = "{xb. \<exists> xa. x = xa @ xb}" in finite_subset)
+ apply auto
+ apply (induct x, simp)
+ apply (subgoal_tac "{xb. \<exists>xa. a # x = xa @ xb} = insert (a # x) {xb. \<exists>xa. x = xa @ xb}")
+ apply auto
+ by (case_tac xaa, simp+)
+ 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>}.
+ \<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)
- 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
-
+ 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"
+ by (auto intro:aux simp:equiv_str_def)
+qed
lemma quot_star:
assumes finite1: "finite (QUOT L\<^isub>1)"
@@ -1872,7 +1813,4 @@
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
+end