(*  Title:      HOL/Library/Quotient_Set.thy

     Author:     Cezary Kaliszyk and Christian Urban

 *)

 header {* Quotient infrastructure for the set type *}

 theory Quotient_Set

 imports Main Quotient_Syntax

 begin

 lemma set_quotient [quot_thm]:

   assumes "Quotient R Abs Rep"

   shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"

 proof (rule QuotientI)

   from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)

   then show "\<And>xs. Rep -` (Abs -` xs) = xs"

     unfolding vimage_def by auto

 next

   show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"

     unfolding set_rel_def vimage_def

     by auto (metis Quotient_rel_abs[OF assms])+

 next

   fix r s

   show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"

     unfolding set_rel_def vimage_def set_eq_iff

     by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+

 qed

 lemma empty_set_rsp[quot_respect]:

   "set_rel R {} {}"

   unfolding set_rel_def by simp

 lemma collect_rsp[quot_respect]:

   assumes "Quotient R Abs Rep"

   shows "((R ===> op =) ===> set_rel R) Collect Collect"

   by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def)

 lemma collect_prs[quot_preserve]:

   assumes "Quotient R Abs Rep"

   shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"

   unfolding fun_eq_iff

   by (simp add: Quotient_abs_rep[OF assms])

 lemma union_rsp[quot_respect]:

   assumes "Quotient R Abs Rep"

   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"

   by (intro fun_relI) (auto simp add: set_rel_def)

 lemma union_prs[quot_preserve]:

   assumes "Quotient R Abs Rep"

   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"

   unfolding fun_eq_iff

   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])

 lemma diff_rsp[quot_respect]:

   assumes "Quotient R Abs Rep"

   shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"

   by (intro fun_relI) (auto simp add: set_rel_def)

 lemma diff_prs[quot_preserve]:

   assumes "Quotient R Abs Rep"

   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"

   unfolding fun_eq_iff

   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)

 lemma inter_rsp[quot_respect]:

   assumes "Quotient R Abs Rep"

   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"

   by (intro fun_relI) (auto simp add: set_rel_def)

 lemma inter_prs[quot_preserve]:

   assumes "Quotient R Abs Rep"

   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"

   unfolding fun_eq_iff

   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])

 end