src/HOL/Quotient.thy
changeset 47362 b1f099bdfbba
parent 47361 87c0eaf04bad
child 47436 d8fad618a67a
     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 *}