src/HOL/Library/Quotient_Set.thy
 changeset 47626 f7b1034cb9ce parent 47455 26315a545e26 child 47647 ec29cc09599d
1.1 --- a/src/HOL/Library/Quotient_Set.thy	Fri Apr 20 15:30:13 2012 +0200
1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Fri Apr 20 15:34:33 2012 +0200
1.3 @@ -8,6 +8,21 @@
1.4  imports Main Quotient_Syntax
1.5  begin
1.7 +subsection {* set map (vimage) and set relation *}
1.8 +
1.9 +definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
1.10 +
1.11 +lemma set_rel_eq [id_simps]:
1.12 +  "set_rel op = = op ="
1.13 +  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
1.14 +
1.15 +lemma set_rel_equivp:
1.16 +  assumes e: "equivp R"
1.17 +  shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
1.18 +  unfolding set_rel_def
1.19 +  using equivp_reflp[OF e]
1.20 +  by auto (metis, metis equivp_symp[OF e])
1.21 +
1.22  lemma set_quotient [quot_thm]:
1.23    assumes "Quotient3 R Abs Rep"
1.24    shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"