# HG changeset patch
# User wu
# Date 1287838298 0
# Node ID 440a01d100ebe1bb24e9661c801374e59f51de7a
# Parent  475dd40cd73440d55c7f13189b50ffd7596f1ab8
add some proofs about the other direction
1: the NULL case
2: the EMPTY case
3: the atomic CHAR c case

diff -r 475dd40cd734 -r 440a01d100eb MyhillNerode.thy
--- 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)