diff -r 10cfaf771687 -r f7b1034cb9ce src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Fri Apr 20 15:30:13 2012 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Fri Apr 20 15:34:33 2012 +0200 @@ -8,6 +8,21 @@ imports Main Quotient_Syntax begin +subsection {* set map (vimage) and set relation *} + +definition "set_rel R xs ys \ \x y. R x y \ x \ xs \ y \ ys" + +lemma set_rel_eq [id_simps]: + "set_rel op = = op =" + by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def) + +lemma set_rel_equivp: + assumes e: "equivp R" + shows "set_rel R xs ys \ xs = ys \ (\x y. x \ xs \ R x y \ y \ xs)" + unfolding set_rel_def + using equivp_reflp[OF e] + by auto (metis, metis equivp_symp[OF e]) + lemma set_quotient [quot_thm]: assumes "Quotient3 R Abs Rep" shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"