--- a/QuotScript.thy	Mon Dec 07 11:14:21 2009 +0100
+++ b/QuotScript.thy	Mon Dec 07 12:14:25 2009 +0100
@@ -310,7 +310,13 @@
   "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
 by auto
 
-(* 2 lemmas needed for proving repabs_inj *)
+(* Bounded abstraction *)
+definition
+  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+
+(* 3 lemmas needed for proving repabs_inj *)
 lemma ball_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "Ball (Respects R) f = Ball (Respects R) g"
@@ -321,6 +327,17 @@
   shows "(Bex (Respects R) f = Bex (Respects R) g)"
   using a by (simp add: Bex_def in_respects)
 
+lemma babs_rsp:
+  assumes q: "Quotient R1 Abs1 Rep1"
+  and     a: "(R1 ===> R2) f g"
+  shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
+  apply (auto simp add: Babs_def)
+  apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+  using a apply (simp add: Babs_def)
+  apply (simp add: in_respects)
+  using Quotient_rel[OF q]
+  by metis
+
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"