--- a/MyhillNerode.thy Fri Oct 22 19:43:56 2010 +0000
+++ b/MyhillNerode.thy Sat Oct 23 12:51:38 2010 +0000
@@ -1312,6 +1312,169 @@
where
"QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})"
+(* by chunhan *)
+lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"
+proof
+ show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}"
+ proof
+ fix x
+ assume in_quot: "x \<in> QUOT {[]}"
+ show "x \<in> {{[]}, UNIV - {[]}}"
+ proof -
+ from in_quot
+ have "x = {[]} \<or> x = UNIV - {[]}"
+ unfolding QUOT_def equiv_class_def
+ proof
+ fix xa
+ assume in_univ: "xa \<in> UNIV"
+ and in_eqiv: "x \<in> {{y. xa \<equiv>{[]}\<equiv> y}}"
+ show "x = {[]} \<or> x = UNIV - {[]}"
+ proof(cases "xa = []")
+ case True
+ hence "{y. xa \<equiv>{[]}\<equiv> y} = {[]}" using in_eqiv
+ by (auto simp add:equiv_str_def)
+ thus ?thesis using in_eqiv by (rule_tac disjI1, simp)
+ next
+ case False
+ hence "{y. xa \<equiv>{[]}\<equiv> y} = UNIV - {[]}" using in_eqiv
+ by (auto simp:equiv_str_def)
+ thus ?thesis using in_eqiv by (rule_tac disjI2, simp)
+ qed
+ qed
+ thus ?thesis by simp
+ qed
+ qed
+next
+ show "{{[]}, UNIV - {[]}} \<subseteq> QUOT {[]}"
+ proof
+ fix x
+ assume in_res: "x \<in> {{[]}, (UNIV::string set) - {[]}}"
+ show "x \<in> (QUOT {[]})"
+ proof -
+ have "x = {[]} \<Longrightarrow> x \<in> QUOT {[]}"
+ apply (simp add:QUOT_def equiv_class_def equiv_str_def)
+ by (rule_tac x = "[]" in exI, auto)
+ moreover have "x = UNIV - {[]} \<Longrightarrow> x \<in> QUOT {[]}"
+ apply (simp add:QUOT_def equiv_class_def equiv_str_def)
+ by (rule_tac x = "''a''" in exI, auto)
+ ultimately show ?thesis using in_res by blast
+ qed
+ qed
+qed
+
+lemma quot_single_aux: "\<lbrakk>x \<noteq> []; x \<noteq> [c]\<rbrakk> \<Longrightarrow> x @ z \<noteq> [c]"
+by (induct x, auto)
+
+lemma quot_single: "\<And> (c::char). QUOT {[c]} = {{[]}, {[c]}, UNIV - {[], [c]}}"
+proof -
+ fix c::"char"
+ have exist_another: "\<exists> a. a \<noteq> c"
+ apply (case_tac "c = CHR ''a''")
+ apply (rule_tac x = "CHR ''b''" in exI, simp)
+ by (rule_tac x = "CHR ''a''" in exI, simp)
+ show "QUOT {[c]} = {{[]}, {[c]}, UNIV - {[], [c]}}"
+ proof
+ show "QUOT {[c]} \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
+ proof
+ fix x
+ assume in_quot: "x \<in> QUOT {[c]}"
+ show "x \<in> {{[]}, {[c]}, UNIV - {[],[c]}}"
+ proof -
+ from in_quot
+ have "x = {[]} \<or> x = {[c]} \<or> x = UNIV - {[],[c]}"
+ unfolding QUOT_def equiv_class_def
+ proof
+ fix xa
+ assume in_eqiv: "x \<in> {{y. xa \<equiv>{[c]}\<equiv> y}}"
+ show "x = {[]} \<or> x = {[c]} \<or> x = UNIV - {[], [c]}"
+ proof-
+ have "xa = [] \<Longrightarrow> x = {[]}" using in_eqiv
+ 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 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 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
+ qed
+ ultimately show ?thesis by blast
+ qed
+ qed
+ thus ?thesis by simp
+ qed
+ qed
+ next
+ show "{{[]}, {[c]}, UNIV - {[],[c]}} \<subseteq> QUOT {[c]}"
+ proof
+ fix x
+ assume in_res: "x \<in> {{[]},{[c]}, (UNIV::string set) - {[],[c]}}"
+ show "x \<in> (QUOT {[c]})"
+ proof -
+ have "x = {[]} \<Longrightarrow> x \<in> QUOT {[c]}"
+ 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 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 (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:
+ 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 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
+
+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)