# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260440374 -3600
# Node ID fd718dde1d61e5aaabe491a7a8521dd0eced7e4c
# Parent  2eba169533b560d3f5b976a4c1bc6edf42651d92
Simplification of Babses for regularize; will probably become injection

diff -r 2eba169533b5 -r fd718dde1d61 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Thu Dec 10 10:54:45 2009 +0100
+++ b/Quot/QuotScript.thy	Thu Dec 10 11:19:34 2009 +0100
@@ -350,6 +350,19 @@
   apply (simp add: in_respects Quotient_rel_rep[OF q1])
   done
 
+lemma babs_simp:
+  assumes q: "Quotient R1 Abs Rep"
+  shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
+apply(rule iffI)
+apply(simp_all only: babs_rsp[OF q])
+apply(auto simp add: Babs_def)
+apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+apply(metis Babs_def)
+apply (simp add: in_respects)
+using Quotient_rel[OF q]
+by metis
+
+
 (* needed for regularising? *)
 lemma babs_reg_eqv:
   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"