--- a/Quot/QuotScript.thy	Thu Jan 21 09:02:04 2010 +0100
+++ b/Quot/QuotScript.thy	Thu Jan 21 09:55:05 2010 +0100
@@ -350,6 +350,11 @@
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
+definition
+  Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+where
+  "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
+
 (* 3 lemmas needed for proving repabs_inj *)
 lemma ball_rsp:
   assumes a: "(R ===> (op =)) f g"
@@ -361,6 +366,12 @@
   shows "(Bex (Respects R) f = Bex (Respects R) g)"
   using a by (simp add: Bex_def in_respects)
 
+lemma bex1_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)"
+  using a 
+by (simp add: Ex1_def Bex1_def in_respects) auto
+
 lemma babs_rsp:
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g"
@@ -415,6 +426,42 @@
   using a unfolding Quotient_def
   by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply)
 
+lemma ex1_prs:
+  assumes a: "Quotient R absf repf"
+  shows "Bexeq R ((absf ---> id) f) = Ex1 f"
+apply (subst Bexeq_def)
+apply (subst Bex_def)
+apply (subst Ex1_def)
+apply simp
+apply rule
+ apply (erule conjE)+
+ apply (erule_tac exE)
+ apply (erule conjE)
+ apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
+  apply (rule_tac x="absf x" in exI)
+  apply (thin_tac "\<forall>x\<in>Respects R. \<forall>y\<in>Respects R. f (absf x) \<and> f (absf y) \<longrightarrow> R x y")
+  apply (simp)
+  apply rule+
+  using a unfolding Quotient_def
+  apply metis
+ apply rule+
+ apply (erule_tac x="x" in ballE)
+  apply (erule_tac x="y" in ballE)
+   apply simp
+  apply (simp add: in_respects)
+ apply (simp add: in_respects)
+apply (erule_tac exE)
+ apply rule
+ apply (rule_tac x="repf x" in exI)
+ apply (simp only: in_respects)
+  apply rule
+ apply (metis Quotient_rel_rep[OF a])
+using a unfolding Quotient_def apply (simp)
+apply rule+
+using a unfolding Quotient_def in_respects
+apply metis
+done
+
 lemma fun_rel_id:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   shows "(R1 ===> R2) f g"