src/HOL/Library/Quotient_Set.thy
 changeset 47626 f7b1034cb9ce parent 47455 26315a545e26 child 47647 ec29cc09599d
equal inserted replaced
47625:10cfaf771687 47626:f7b1034cb9ce
5 header {* Quotient infrastructure for the set type *}
5 header {* Quotient infrastructure for the set type *}
6
6
7 theory Quotient_Set
7 theory Quotient_Set
8 imports Main Quotient_Syntax
8 imports Main Quotient_Syntax
9 begin
9 begin

10

11 subsection {* set map (vimage) and set relation *}

12

13 definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"

14

15 lemma set_rel_eq [id_simps]:

16   "set_rel op = = op ="

17   by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)

18

19 lemma set_rel_equivp:

20   assumes e: "equivp R"

21   shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"

22   unfolding set_rel_def

23   using equivp_reflp[OF e]

24   by auto (metis, metis equivp_symp[OF e])
10
25
11 lemma set_quotient [quot_thm]:
26 lemma set_quotient [quot_thm]:
12   assumes "Quotient3 R Abs Rep"
27   assumes "Quotient3 R Abs Rep"
13   shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
28   shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
14 proof (rule Quotient3I)
29 proof (rule Quotient3I)