--- a/Closures.thy	Mon Aug 22 12:49:27 2011 +0000
+++ b/Closures.thy	Tue Aug 23 00:24:10 2011 +0000
@@ -164,6 +164,7 @@
   then show "regular (Deriv_lang B A)" by auto
 qed
 
+
 subsection {* Finite and co-finite sets are regular *}
 
 lemma singleton_regular:
@@ -243,4 +244,31 @@
 qed
 
 
+
+(* tests *)
+definition
+  "quot A B \<equiv> {x. \<exists>y \<in> B. x @ y \<in> A}"
+
+definition
+  "quot1 A B \<equiv> {x. \<exists>y \<in> B. y @ x \<in> A}"
+
+lemma
+  "quot1 A B \<subseteq> Deriv_lang B A"
+unfolding quot1_def Derivs_def
+apply(auto)
+done
+
+lemma  
+  "rev ` quot1 A B \<subseteq> quot (rev ` A) (rev ` B)"
+unfolding quot_def quot1_def
+apply(auto)
+unfolding image_def
+apply(auto)
+apply(rule_tac x="y" in bexI)
+apply(rule_tac x="y @ xa" in bexI)
+apply(auto)
+done
+
+
+
 end
\ No newline at end of file