kaliszyk@44413: (* Title: HOL/Library/Quotient_Set.thy kaliszyk@44413: Author: Cezary Kaliszyk and Christian Urban kaliszyk@44413: *) kaliszyk@44413: kaliszyk@44413: header {* Quotient infrastructure for the set type *} kaliszyk@44413: kaliszyk@44413: theory Quotient_Set kaliszyk@44413: imports Main Quotient_Syntax kaliszyk@44413: begin kaliszyk@44413: kaliszyk@44413: lemma set_quotient [quot_thm]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)" kaliszyk@44413: proof (rule QuotientI) kaliszyk@44413: from assms have "\x. Abs (Rep x) = x" by (rule Quotient_abs_rep) kaliszyk@44413: then show "\xs. Rep -` (Abs -` xs) = xs" kaliszyk@44413: unfolding vimage_def by auto kaliszyk@44413: next kaliszyk@44413: show "\xs. set_rel R (Abs -` xs) (Abs -` xs)" kaliszyk@44413: unfolding set_rel_def vimage_def kaliszyk@44413: by auto (metis Quotient_rel_abs[OF assms])+ kaliszyk@44413: next kaliszyk@44413: fix r s kaliszyk@44413: show "set_rel R r s = (set_rel R r r \ set_rel R s s \ Rep -` r = Rep -` s)" kaliszyk@44413: unfolding set_rel_def vimage_def set_eq_iff kaliszyk@44413: by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+ kaliszyk@44413: qed kaliszyk@44413: kaliszyk@44413: lemma empty_set_rsp[quot_respect]: kaliszyk@44413: "set_rel R {} {}" kaliszyk@44413: unfolding set_rel_def by simp kaliszyk@44413: kaliszyk@44413: lemma collect_rsp[quot_respect]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "((R ===> op =) ===> set_rel R) Collect Collect" kaliszyk@44413: by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def) kaliszyk@44413: kaliszyk@44413: lemma collect_prs[quot_preserve]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "((Abs ---> id) ---> op -` Rep) Collect = Collect" kaliszyk@44413: unfolding fun_eq_iff kaliszyk@44413: by (simp add: Quotient_abs_rep[OF assms]) kaliszyk@44413: kaliszyk@44413: lemma union_rsp[quot_respect]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "(set_rel R ===> set_rel R ===> set_rel R) op \ op \" kaliszyk@44413: by (intro fun_relI) (auto simp add: set_rel_def) kaliszyk@44413: kaliszyk@44413: lemma union_prs[quot_preserve]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \ = op \" kaliszyk@44413: unfolding fun_eq_iff kaliszyk@44413: by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) kaliszyk@44413: kaliszyk@44413: lemma diff_rsp[quot_respect]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -" kaliszyk@44413: by (intro fun_relI) (auto simp add: set_rel_def) kaliszyk@44413: kaliszyk@44413: lemma diff_prs[quot_preserve]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -" kaliszyk@44413: unfolding fun_eq_iff kaliszyk@44413: by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff) kaliszyk@44413: kaliszyk@44413: lemma inter_rsp[quot_respect]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "(set_rel R ===> set_rel R ===> set_rel R) op \ op \" kaliszyk@44413: by (intro fun_relI) (auto simp add: set_rel_def) kaliszyk@44413: kaliszyk@44413: lemma inter_prs[quot_preserve]: kaliszyk@44413: assumes "Quotient R Abs Rep" kaliszyk@44413: shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \ = op \" kaliszyk@44413: unfolding fun_eq_iff kaliszyk@44413: by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) kaliszyk@44413: kaliszyk@44413: end