src/HOL/Quotient.thy
```     1.1 --- a/src/HOL/Quotient.thy	Wed Apr 04 17:51:12 2012 +0200
1.2 +++ b/src/HOL/Quotient.thy	Wed Apr 04 19:20:52 2012 +0200
1.3 @@ -772,6 +772,32 @@
1.4  using assms
1.5  by (rule OOO_quotient3) auto
1.6
1.7 +subsection {* Quotient3 to Quotient *}
1.8 +
1.9 +lemma Quotient3_to_Quotient:
1.10 +assumes "Quotient3 R Abs Rep"
1.11 +and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
1.12 +shows "Quotient R Abs Rep T"
1.13 +using assms unfolding Quotient3_def by (intro QuotientI) blast+
1.14 +
1.15 +lemma Quotient3_to_Quotient_equivp:
1.16 +assumes q: "Quotient3 R Abs Rep"
1.17 +and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
1.18 +and eR: "equivp R"
1.19 +shows "Quotient R Abs Rep T"
1.20 +proof (intro QuotientI)
1.21 +  fix a
1.22 +  show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep)
1.23 +next
1.24 +  fix a
1.25 +  show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp)
1.26 +next
1.27 +  fix r s
1.28 +  show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric])
1.29 +next
1.30 +  show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp
1.31 +qed
1.32 +
1.33  subsection {* ML setup *}
1.34
1.35  text {* Auxiliary data for the quotient package *}
```