--- a/MyhillNerode.thy Sat Oct 23 12:51:38 2010 +0000
+++ b/MyhillNerode.thy Sun Oct 24 01:17:44 2010 +0000
@@ -281,9 +281,8 @@
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
@@ -305,6 +304,7 @@
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"
@@ -505,7 +505,7 @@
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,7 +631,8 @@
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.
@@ -643,11 +644,14 @@
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
@@ -802,7 +806,8 @@
"(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:
@@ -889,7 +894,8 @@
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
@@ -1306,12 +1312,58 @@
text {* tests by Christian *}
-(* Alternative definition for Quo *)
+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 *}
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)
+
+
(* by chunhan *)
lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"
proof
@@ -1394,7 +1446,7 @@
proof -
have "xa = [c] \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = {[c]}" using in_eqiv
apply (simp add:equiv_str_def)
- apply (rule set_ext, rule iffI, simp)
+ apply (rule temp_set_ext, rule iffI, simp)
apply (drule_tac x = "[]" in spec, auto)
done
thus "xa = [c] \<Longrightarrow> x = {[c]}" using in_eqiv by simp
@@ -1403,7 +1455,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 set_ext, rule iffI, simp)
+ apply (rule temp_set_ext, rule iffI, simp)
apply (rule conjI)
apply (drule_tac x = "[c]" in spec, simp)
apply (drule_tac x = "[]" in spec, simp)
@@ -1429,13 +1481,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 set_ext, rule iffI, simp+)
+ apply (rule temp_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 set_ext, rule iffI, simp)
+ apply (rule temp_set_ext, rule iffI, simp)
apply (clarsimp simp:quot_single_aux, simp)
apply (rule conjI)
apply (drule_tac x = "[c]" in spec, simp)
@@ -1453,11 +1505,26 @@
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_union:
+ "(QUOT (L1 \<union> L2)) \<subseteq> ((QUOT L1) \<union> (QUOT L2))"
+sorry
+
+
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))"
-sorry
+apply(rule finite_subset)
+apply(rule QUOT_union)
+apply(simp add: finite1 finite2)
+done
lemma quot_star:
assumes finite1: "finite (QUOT L\<^isub>1)"
@@ -1470,67 +1537,10 @@
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)
-lemma test1:
- assumes finite_CS: "finite (QUOT Lang)"
- shows "reg Lang"
-using finite_CS
-unfolding test[symmetric]
-by (auto dest: myhill_nerode)
-
-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)
-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