--- a/Myhill_1.thy	Thu Jul 28 17:52:36 2011 +0000
+++ b/Myhill_1.thy	Sun Jul 31 10:27:41 2011 +0000
@@ -11,11 +11,17 @@
 
 text {* Myhill-Nerode relation *}
 
+
 definition
-  str_eq_rel :: "'a lang \<Rightarrow> ('a list \<times> 'a list) set" ("\<approx>_" [100] 100)
+  str_eq :: "'a lang \<Rightarrow> ('a list \<times> 'a list) set" ("\<approx>_" [100] 100)
 where
   "\<approx>A \<equiv> {(x, y).  (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}"
 
+abbreviation
+  str_eq_applied :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>_ _")
+where
+  "x \<approx>A y \<equiv> (x, y) \<in> \<approx>A"
+
 definition 
   finals :: "'a lang \<Rightarrow> 'a lang set"
 where
@@ -25,7 +31,7 @@
   shows "A = \<Union> finals A"
 unfolding finals_def
 unfolding Image_def
-unfolding str_eq_rel_def
+unfolding str_eq_def
 by (auto) (metis append_Nil2)
 
 lemma finals_in_partitions:
@@ -247,7 +253,7 @@
   assumes "s \<in> X" "X \<in> UNIV // \<approx>A" 
   shows "X = \<approx>A `` {s}"
 using assms
-unfolding quotient_def Image_def str_eq_rel_def
+unfolding quotient_def Image_def str_eq_def 
 by auto
 
 lemma every_eqclass_has_transition:
@@ -263,11 +269,11 @@
     using has_str in_CS defined_by_str by blast
   then have "Y \<cdot> {[c]} \<subseteq> X" 
     unfolding Y_def Image_def conc_def
-    unfolding str_eq_rel_def
+    unfolding str_eq_def
     by clarsimp
   moreover
   have "s \<in> Y" unfolding Y_def 
-    unfolding Image_def str_eq_rel_def by simp
+    unfolding Image_def str_eq_def by simp
   ultimately show thesis using that by blast
 qed