--- a/MyhillNerode.thy	Sun Oct 24 01:17:44 2010 +0000
+++ b/MyhillNerode.thy	Tue Oct 26 13:01:22 2010 +0000
@@ -1312,42 +1312,120 @@
 
 text {* tests by Christian *}
 
+(* compatibility with stable Isabelle *)
 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)"
-by(auto intro:set_eqI)
+  by(auto intro:set_eqI)
+
+abbreviation
+  str_eq ("_ \<approx>_ _")
+where
+  "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
+
+abbreviation
+  lang_eq ("\<approx>_")
+where
+  "\<approx>Lang \<equiv> (\<lambda>(x, y). x \<approx>Lang y)"
 
-fun
-  MNRel
-where
-  "MNRel Lang (x, y) = (x \<equiv>Lang\<equiv> y)"
+lemma lang_eq_is_equiv:
+  "equiv UNIV (\<approx>Lang)"
+unfolding equiv_def
+unfolding refl_on_def sym_def trans_def
+by (simp add: mem_def equiv_str_def)
+
+text {*
+  equivalence classes of x can be written
+
+    (\<approx>Lang)``{x}
+
+  the language quotient can be written
+
+    UNIV // (\<approx>Lang)
+*}
+
+lemma
+  "(\<approx>Lang)``{x} = \<lbrakk>x\<rbrakk>Lang"
+unfolding equiv_class_def equiv_str_def Image_def mem_def
+by (simp)
 
 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)
+  "UNIV // (\<approx>Lang) = UNIV Quo Lang"
+unfolding quotient_def quot_def 
+unfolding equiv_class_def equiv_str_def
+unfolding Image_def mem_def
+by auto
+
+lemma
+  "{} \<notin> UNIV // (\<approx>Lang)"
+unfolding quotient_def 
+unfolding Image_def 
+apply(auto)
+apply(rule_tac x="x" in exI)
+unfolding mem_def
+apply(simp)
+done
+
+definition
+  transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
+where
+  "X \<Turnstile>\<Rightarrow> Y \<equiv> {CHAR c | c. X ; {[c]} \<subseteq> Y}"
+
+definition
+  "rhs CS X \<equiv> { (Y, X \<Turnstile>\<Rightarrow>Y) | Y. Y \<in> CS }"
+
+definition
+  "rhs_sem CS X \<equiv> { (Y; L (folds ALT NULL (X \<Turnstile>\<Rightarrow>Y))) | Y. Y \<in> CS }"
+
+definition
+  "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})"
+
+lemma finite_rhs:
+  assumes fin: "finite CS"
+  shows "finite (rhs CS X)"
+  using fin unfolding rhs_def by (auto)
+
+lemma finite_eqs:
+  assumes fin: "finite CS"
+  shows "finite (eqs CS)"
+unfolding eqs_def
+apply(rule finite_UN_I)
+apply(rule fin)
+apply(simp add: eq_def)
 done
 
 lemma
-  "(MNRel Lang)``{x} = \<lbrakk>x\<rbrakk>Lang"
-unfolding equiv_class_def Image_def mem_def
-by (simp)
+  shows "X ; L (folds ALT NULL X \<Turnstile>\<Rightarrow> Y) \<subseteq> Y" 
+by (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs)
+
+lemma
+  assumes a: "X \<in> (UNIV // (\<approx>Lang))"
+  shows "X \<subseteq> \<Union> (rhs_sem (UNIV // (\<approx>Lang)) X)"
+unfolding rhs_sem_def 
+apply (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs)
+apply(rule_tac x="X" in exI)
+apply(simp)
+apply(simp add: quotient_def Image_def)
+apply(subst (4) mem_def)
+apply(simp)
+using a
+apply(simp add: quotient_def Image_def)
+apply(subst (asm) (2) mem_def)
+apply(simp)
+apply(rule_tac x="X" in exI)
+apply(simp)
+apply(erule exE)
+apply(simp)
+apply(rule temp_set_ext)
+apply(simp)
+apply(rule iffI)
+apply(rule_tac x="x" in exI)
+apply(simp)
+oops
 
 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)
+  "UNIV//(\<approx>(L1 \<union> L2)) \<subseteq> (UNIV//(\<approx>L1)) \<union> (UNIV//(\<approx>L2))"
+unfolding quotient_def Image_def
 oops
 
 
@@ -1358,13 +1436,13 @@
 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 *)
+text{* by chunhan *}
 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"
 proof 
   show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}"