--- a/src/HOL/Quotient.thy Wed Apr 04 17:51:12 2012 +0200
+++ b/src/HOL/Quotient.thy Wed Apr 04 19:20:52 2012 +0200
@@ -772,6 +772,32 @@
using assms
by (rule OOO_quotient3) auto
+subsection {* Quotient3 to Quotient *}
+
+lemma Quotient3_to_Quotient:
+assumes "Quotient3 R Abs Rep"
+and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
+shows "Quotient R Abs Rep T"
+using assms unfolding Quotient3_def by (intro QuotientI) blast+
+
+lemma Quotient3_to_Quotient_equivp:
+assumes q: "Quotient3 R Abs Rep"
+and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
+and eR: "equivp R"
+shows "Quotient R Abs Rep T"
+proof (intro QuotientI)
+ fix a
+ show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep)
+next
+ fix a
+ show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp)
+next
+ fix r s
+ show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric])
+next
+ show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp
+qed
+
subsection {* ML setup *}
text {* Auxiliary data for the quotient package *}