--- a/MyhillNerode.thy	Sat Nov 06 23:31:53 2010 +0000
+++ b/MyhillNerode.thy	Mon Nov 08 01:13:09 2010 +0000
@@ -1512,25 +1512,13 @@
 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))"
-apply(rule finite_subset)
-apply(rule QUOT_union)
-apply(simp add: finite1 finite2)
-done
-
+(*
 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)
@@ -1540,8 +1528,7 @@
 lemma test: 
   "UNIV Quo Lang = QUOT Lang"
 by (auto simp add: quot_def QUOT_def)
-
-
+*)
 
 
 (* by chunhan *)
@@ -1552,9 +1539,12 @@
 apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset)
 by (auto simp add:image_def Pow_def)
 
+term image
+term "(op `) tag"
+
 lemma str_inj_imps:
   assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<equiv>lang\<equiv> n"
-  shows "inj_on ((op `) tag) (QUOT lang)"
+  shows "inj_on (image tag) (QUOT lang)"
 proof (clarsimp simp add:inj_on_def QUOT_def)
   fix x y
   assume eq_tag: "tag ` \<lbrakk>x\<rbrakk>lang = tag ` \<lbrakk>y\<rbrakk>lang"
@@ -1573,17 +1563,24 @@
   qed
 qed
 
-definition tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
+definition 
+  tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
 where
   "tag_str_ALT L\<^isub>1 L\<^isub>2 x \<equiv> (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)"
 
+lemma
+  "{(\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2) | x. True} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"
+unfolding QUOT_def
+by (auto)
+
 lemma tag_str_alt_range_finite:
   assumes finite1: "finite (QUOT L\<^isub>1)"
   and finite2: "finite (QUOT L\<^isub>2)"
   shows "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))"
 proof -
   have "{y. \<exists>x. y = (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"
-    by (auto simp:QUOT_def)
+    unfolding QUOT_def
+    by auto
   thus ?thesis using finite1 finite2
     by (auto simp: image_def tag_str_ALT_def UNION_def 
             intro: finite_subset[where B = "(QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"])
@@ -1598,16 +1595,111 @@
   assumes finite1: "finite (QUOT L\<^isub>1)"
   and finite2: "finite (QUOT L\<^isub>2)"
   shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
-proof (rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD)
-  show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+proof -
+  have "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))"
     using finite_tag_image tag_str_alt_range_finite finite1 finite2
     by auto
-next
-  show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+  moreover 
+  have "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
     apply (rule_tac str_inj_imps)
     by (erule_tac tag_str_alt_inj)
+  ultimately 
+  show "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
 qed
 
+
+(*by cu *)
+
+
+definition
+  str_eq ("_ \<approx>_ _")
+where
+  "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
+
+definition
+  str_eq_rel ("\<approx>_")
+where
+  "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"
+
+lemma [simp]:
+  "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
+by simp
+
+lemma inj_image_lang:
+  fixes f::"string \<Rightarrow> 'a"
+  assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y"
+  shows "inj_on (image f) (UNIV // (\<approx>Lang))"
+proof - 
+  { fix x y::string
+    assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}"
+    moreover
+    have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto
+    ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast
+    then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto
+    then have "x \<approx>Lang y" unfolding str_eq_def by simp 
+    then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp
+  }
+  then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y"
+    unfolding quotient_def Image_def str_eq_rel_def by simp
+  then show "inj_on (image f) (UNIV // (\<approx>Lang))"
+    unfolding inj_on_def by simp
+qed
+
+
+lemma finite_range_image: 
+  assumes fin: "finite (range f)"
+  shows "finite ((image f) ` X)"
+proof -
+  from fin have "finite (Pow (f ` UNIV))" by auto
+  moreover
+  have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto
+  ultimately show "finite ((image f) ` X)" using finite_subset by auto
+qed
+
+definition 
+  tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
+where
+  "tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
+
+lemma tag1_range_finite:
+  assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)"
+  and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
+  shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
+proof -
+  have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto
+  moreover
+  have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)"
+    unfolding tag1_def quotient_def by auto
+  ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))" 
+    using finite_subset by blast
+qed
+
+lemma tag1_inj:
+  "tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
+unfolding tag1_def Image_def str_eq_rel_def str_eq_def
+by auto
+
+lemma quot_alt_cu:
+  fixes L\<^isub>1 L\<^isub>2::"string set"
+  assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)"
+  and fin2: "finite (UNIV // \<approx>L\<^isub>2)"
+  shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
+proof -
+  have "finite (range (tag1 L\<^isub>1 L\<^isub>2))" 
+    using fin1 fin2 tag1_range_finite by simp
+  then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))" 
+    using finite_range_image by blast
+  moreover 
+  have "\<And>x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y" 
+    using tag1_inj by simp
+  then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" 
+    using inj_image_lang by blast
+  ultimately 
+  show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
+qed
+
+(* by chunhan *)
+
 (* list_diff:: list substract, once different return tailer *)
 fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)
 where