
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 "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
kaliszyk@44413:   then show "\<And>xs. Rep -` (Abs -` xs) = xs"
kaliszyk@44413:     unfolding vimage_def by auto
kaliszyk@44413: next
kaliszyk@44413:   show "\<And>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 \<and> set_rel R s s \<and> 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 \<union> op \<union>"
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 \<union> = op \<union>"
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 \<inter> op \<inter>"
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 \<inter> = op \<inter>"
kaliszyk@44413:   unfolding fun_eq_iff
kaliszyk@44413:   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
kaliszyk@44413: 
kaliszyk@44413: end




