--- a/MyhillNerode.thy Fri Oct 22 10:45:01 2010 +0000
+++ b/MyhillNerode.thy Fri Oct 22 19:43:56 2010 +0000
@@ -38,16 +38,6 @@
apply(metis)
by (metis append_assoc)
-lemma lang_seq_minus:
- shows "(L1; L2) - {[]} =
- (if [] \<in> L1 then L2 - {[]} else {}) \<union>
- (if [] \<in> L2 then L1 - {[]} else {}) \<union> ((L1 - {[]}); (L2 - {[]}))"
-apply(auto simp add: lang_seq_def)
-apply(metis mem_def self_append_conv)
-apply(metis mem_def self_append_conv2)
-apply(metis mem_def self_append_conv2)
-apply(metis mem_def self_append_conv)
-done
section {* Kleene star for languages defined as least fixed point *}
@@ -270,6 +260,8 @@
from f1 f2 show "X = B; A\<star>" by auto
qed
+
+
section {* equiv class' definition *}
definition
@@ -290,9 +282,6 @@
"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)}"
proof
@@ -468,7 +457,11 @@
qed
text {*
- arden_variate_valid: proves variation from "X = X;r + Y;ry + \<dots>" to "X = Y;(SEQ ry (STAR r)) + \<dots>" holds the law of "language of left equiv language of right"
+ arden_variate_valid: proves variation from
+
+ "X = X;r + Y;ry + \<dots>" to "X = Y;(SEQ ry (STAR r)) + \<dots>"
+
+ holds the law of "language of left equiv language of right"
*}
lemma arden_variate_valid:
assumes X_not_empty: "X \<noteq> {[]}"
@@ -504,7 +497,9 @@
qed
qed
-text {* 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>} *}
+text {*
+ 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
@@ -682,7 +677,7 @@
qed
-(* ********************************* BEGIN: proving the initial equation-system satisfies Inv **************************************** *)
+text {* ******BEGIN: proving the initial equation-system satisfies Inv ****** *}
lemma distinct_rhs_equations:
"(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs"
@@ -762,7 +757,8 @@
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})"
+ 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"
@@ -775,8 +771,10 @@
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
+ 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
@@ -798,15 +796,13 @@
qed
qed
-lemma finite_CT_chars:
- "finite {CHAR c |c. Xa-c\<rightarrow>X}"
-by (auto)
+
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}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_CT_chars)+
+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:
@@ -837,10 +833,10 @@
qed
-(* ********************************* END: proving the initial equation-system satisfies Inv **************************************** *)
+text {* *********** END: proving the initial equation-system satisfies Inv ******* *}
-(* ***************************** BEGIN: proving every equation-system's iteration step satisfies Inv ******************************* *)
+text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}
lemma not_T_aux: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk>
\<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> insert a A "
@@ -1147,8 +1143,10 @@
thus ?thesis by blast
next
case False
- --"in this situation, we pick a equation and using ardenable to get a rhs without itself in it, then use equas_subst to form a new equation-system"
- hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" using subst Inv_ES
+ --"in this situation, we pick a equation and using ardenable to get a
+ rhs without itself in it, then use equas_subst to form a new equation-system"
+ hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}"
+ using subst Inv_ES
by (auto intro:ardenable_prop simp add:Inv_def simp del:L_rhs.simps)
then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'"
and dist_Y': "distinct_rhs yrhs'"
@@ -1183,7 +1181,7 @@
qed
qed
-(* ****************************** END: proving every equation-system's iteration step satisfies Inv ******************************* *)
+text {* ***** END: proving every equation-system's iteration step satisfies Inv ************** *}
lemma iteration_conc:
assumes history: "Inv X ES"
@@ -1265,6 +1263,13 @@
qed
qed
+text {* definition of a regular language *}
+
+abbreviation
+ reg :: "string set => bool"
+where
+ "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)"
+
theorem myhill_nerode:
assumes finite_CS: "finite (UNIV Quo Lang)"
shows "\<exists> (reg::rexp). Lang = L reg" (is "\<exists> r. ?P r")
@@ -1301,29 +1306,68 @@
text {* tests by Christian *}
-abbreviation
- reg :: "string set => bool"
+(* Alternative definition for Quo *)
+definition
+ QUOT :: "string set \<Rightarrow> (string set) set"
where
- "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)"
+ "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})"
+
+lemma test:
+ "UNIV Quo Lang = QUOT Lang"
+by (auto simp add: quot_def QUOT_def)
lemma test1:
- assumes finite_CS: "finite (UNIV Quo Lang)"
+ assumes finite_CS: "finite (QUOT Lang)"
shows "reg Lang"
using finite_CS
+unfolding test[symmetric]
by (auto dest: myhill_nerode)
-lemma t1: "(UNIV Quo {}) = {UNIV}"
-apply(simp only: quot_def equiv_class_def equiv_str_def)
+lemma t1: "(QUOT {}) = {UNIV}"
+apply(simp only: QUOT_def equiv_class_def equiv_str_def)
apply(simp)
done
+lemma t2: "{[]} \<in> (QUOT {[]})"
+apply(simp only: QUOT_def equiv_class_def equiv_str_def)
+apply(simp)
+apply(simp add: set_eq_iff)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+by (metis eq_commute)
+
+
+lemma t2': "X \<in> (QUOT {[]})"
+apply(simp only: QUOT_def equiv_class_def equiv_str_def)
+apply(simp)
+apply(simp add: set_eq_iff)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+apply(rule allI)
+
+by (metis eq_commute)
+
+oops
+
+lemma
+ fixes r :: "rexp"
+ shows "finite (QUOT (L r))"
+apply(induct r)
+apply(simp add: t1)
+apply(simp add: QUOT_def)
+apply(simp add: equiv_class_def equiv_str_def)
+apply(rule finite_UN_I)
+oops
+
lemma
fixes r :: "rexp"
shows "finite (UNIV Quo (L r))"
apply(induct r)
-apply(simp add: t1)
-oops
-
+prefer 2
+apply(simp add: quot_def)
+apply(simp add: equiv_class_def equiv_str_def)
+apply(rule finite_UN_I)
+apply(simp)
end
\ No newline at end of file