# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260217283 -3600
# Node ID a8c3fa5c4015eb9e7485b946b9cede487eee901c
# Parent  38aa6b67a80b66942d461d396e2a10bd92fea91f
babs_prs

diff -r 38aa6b67a80b -r a8c3fa5c4015 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/QuotScript.thy	Mon Dec 07 21:21:23 2009 +0100
@@ -338,12 +338,23 @@
   using Quotient_rel[OF q]
   by metis
 
+lemma babs_prs:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f"
+  apply(rule eq_reflection)
+  apply(rule ext)
+  apply simp
+  apply (subgoal_tac "Rep1 x \<in> Respects R1")
+  apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+  apply (simp add: in_respects Quotient_rel_rep[OF q1])
+  done
+
 (* needed for regularising? *)
 lemma babs_reg_eqv:
   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
 
-
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"