--- a/MyhillNerode.thy Wed Nov 03 21:42:44 2010 +0000
+++ b/MyhillNerode.thy Wed Nov 03 22:08:50 2010 +0000
@@ -740,8 +740,12 @@
shows "X = L xrhs"
proof (cases "X = {[]}")
case True
- thus ?thesis using X_in_equas
- by (simp add:equations_def equation_rhs_def lang_seq_def)
+ 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
next
case False
show ?thesis
@@ -754,33 +758,32 @@
proof (cases "x = []")
assume empty: "x = []"
hence "x \<in> L (empty_rhs X)" using "(1)"
- by (auto simp:empty_rhs_def lang_seq_def)
+ unfolding empty_rhs_def
+ by (simp add: 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})"
+ 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})"
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"
+ assume Y_CT_X: "Y-c\<rightarrow>X"
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 \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast
+ "Xa \<in> UNIV Quo Lang" "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
@@ -791,11 +794,14 @@
assume "(2)": "x \<in> L xrhs"
have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"
using finite_charset_rS
- by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)
+ unfolding CT_def
+ by (simp add: lang_seq_def fold_alt_null_eqs) (auto)
have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"
- by (simp add:empty_rhs_def split:if_splits)
- show "x \<in> X" using X_in_equas False "(2)"
- by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def)
+ 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)
qed
qed
qed
@@ -1316,6 +1322,24 @@
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
+
+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
@@ -1335,7 +1359,7 @@
text {*
equivalence classes of x can be written
- (\<approx>Lang)``{x}
+ UNIV // (\<approx>Lang)``{x}
the language quotient can be written
@@ -1367,17 +1391,79 @@
definition
transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
where
- "X \<Turnstile>\<Rightarrow> Y \<equiv> {CHAR c | c. X ; {[c]} \<subseteq> Y}"
+ "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ; {[c]} \<subseteq> X}"
definition
- "rhs CS X \<equiv> { (Y, X \<Turnstile>\<Rightarrow>Y) | Y. Y \<in> CS }"
+ 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_sem CS X \<equiv> { (Y; L (folds ALT NULL (X \<Turnstile>\<Rightarrow>Y))) | Y. Y \<in> CS }"
+ "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)"
@@ -1393,8 +1479,25 @@
done
lemma
- shows "X ; L (folds ALT NULL X \<Turnstile>\<Rightarrow> Y) \<subseteq> Y"
-by (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs)
+ 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
+
+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
assumes a: "X \<in> (UNIV // (\<approx>Lang))"
@@ -1405,27 +1508,62 @@
apply(simp)
apply(simp add: quotient_def Image_def)
apply(subst (4) mem_def)
-apply(simp)
-using a
-apply(simp add: quotient_def Image_def)
-apply(subst (asm) (2) mem_def)
-apply(simp)
-apply(rule_tac x="X" in exI)
-apply(simp)
-apply(erule exE)
-apply(simp)
-apply(rule temp_set_ext)
-apply(simp)
-apply(rule iffI)
-apply(rule_tac x="x" in exI)
-apply(simp)
oops
-lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp
+
+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}"
+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
+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
- "UNIV//(\<approx>(L1 \<union> L2)) \<subseteq> (UNIV//(\<approx>L1)) \<union> (UNIV//(\<approx>L2))"
-unfolding quotient_def Image_def
+ 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