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)`