# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259922838 -3600
# Node ID ebfd747b47ab07605d1881ae19348e4bd1222e0d
# Parent  14f68c1f4d12e691d347cf4ebce0274f864384d9
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.

diff -r 14f68c1f4d12 -r ebfd747b47ab QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 11:06:43 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 11:33:58 2009 +0100
@@ -136,16 +136,6 @@
 
 end
 
-(* EQUALS_RSP is stronger *)
-lemma equiv_trans2:
-  assumes e: "EQUIV R"
-  and     ac: "R a c"
-  and     bd: "R b d"
-  shows "R a b = R c d"
-using ac bd e
-unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def
-by (blast)
-
 section {* type definition for the quotient type *}
 
 (* the auxiliary data for the quotient types *)
@@ -1343,7 +1333,8 @@
       val rthm' = atomize_thm rthm
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
-      val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
+      val quotients = quotient_rules_get lthy
+      val trans2 = map (fn x => @{thm EQUALS_RSP} OF [x]) quotients
       val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
     in
       EVERY1
diff -r 14f68c1f4d12 -r ebfd747b47ab QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 11:06:43 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 11:33:58 2009 +0100
@@ -268,8 +268,8 @@
 
 lemma EQUALS_RSP:
   assumes q: "QUOTIENT R Abs Rep"
-  and     a: "R x1 x2" "R y1 y2"
-  shows "R x1 y1 = R x2 y2"
+  and     a: "R xa xb" "R ya yb"
+  shows "R xa ya = R xb yb"
 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def
 using a by blast