wenzelm@47455: (*  Title:      HOL/Library/Quotient_Set.thy
kaliszyk@44413:     Author:     Cezary Kaliszyk and Christian Urban
kaliszyk@44413: *)
kaliszyk@44413: 
wenzelm@58881: section {* Quotient infrastructure for the set type *}
kaliszyk@44413: 
kaliszyk@44413: theory Quotient_Set
kaliszyk@44413: imports Main Quotient_Syntax
kaliszyk@44413: begin
kaliszyk@44413: 
kuncar@53012: subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *}
huffman@47626: 
blanchet@55940: definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
huffman@47626: 
blanchet@55940: lemma rel_vset_eq [id_simps]:
blanchet@55940:   "rel_vset op = = op ="
blanchet@55940:   by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff rel_vset_def)
huffman@47626: 
blanchet@55940: lemma rel_vset_equivp:
huffman@47626:   assumes e: "equivp R"
blanchet@55940:   shows "rel_vset R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
blanchet@55940:   unfolding rel_vset_def
huffman@47626:   using equivp_reflp[OF e]
huffman@47626:   by auto (metis, metis equivp_symp[OF e])
huffman@47626: 
kaliszyk@44413: lemma set_quotient [quot_thm]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
blanchet@55940:   shows "Quotient3 (rel_vset R) (vimage Rep) (vimage Abs)"
kuncar@47308: proof (rule Quotient3I)
kuncar@47308:   from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
kaliszyk@44413:   then show "\<And>xs. Rep -` (Abs -` xs) = xs"
kaliszyk@44413:     unfolding vimage_def by auto
kaliszyk@44413: next
blanchet@55940:   show "\<And>xs. rel_vset R (Abs -` xs) (Abs -` xs)"
blanchet@55940:     unfolding rel_vset_def vimage_def
kuncar@47308:     by auto (metis Quotient3_rel_abs[OF assms])+
kaliszyk@44413: next
kaliszyk@44413:   fix r s
blanchet@55940:   show "rel_vset R r s = (rel_vset R r r \<and> rel_vset R s s \<and> Rep -` r = Rep -` s)"
blanchet@55940:     unfolding rel_vset_def vimage_def set_eq_iff
kuncar@47308:     by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
kaliszyk@44413: qed
kaliszyk@44413: 
blanchet@55940: declare [[mapQ3 set = (rel_vset, set_quotient)]]
kuncar@47094: 
kaliszyk@44413: lemma empty_set_rsp[quot_respect]:
blanchet@55940:   "rel_vset R {} {}"
blanchet@55940:   unfolding rel_vset_def by simp
kaliszyk@44413: 
kaliszyk@44413: lemma collect_rsp[quot_respect]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
blanchet@55940:   shows "((R ===> op =) ===> rel_vset R) Collect Collect"
blanchet@55945:   by (intro rel_funI) (simp add: rel_fun_def rel_vset_def)
kaliszyk@44413: 
kaliszyk@44413: lemma collect_prs[quot_preserve]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
kaliszyk@44413:   shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
kaliszyk@44413:   unfolding fun_eq_iff
kuncar@47308:   by (simp add: Quotient3_abs_rep[OF assms])
kaliszyk@44413: 
kaliszyk@44413: lemma union_rsp[quot_respect]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
blanchet@55940:   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
blanchet@55945:   by (intro rel_funI) (simp add: rel_vset_def)
kaliszyk@44413: 
kaliszyk@44413: lemma union_prs[quot_preserve]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
kaliszyk@44413:   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
kaliszyk@44413:   unfolding fun_eq_iff
kuncar@47308:   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
kaliszyk@44413: 
kaliszyk@44413: lemma diff_rsp[quot_respect]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
blanchet@55940:   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
blanchet@55945:   by (intro rel_funI) (simp add: rel_vset_def)
kaliszyk@44413: 
kaliszyk@44413: lemma diff_prs[quot_preserve]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
kaliszyk@44413:   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
kaliszyk@44413:   unfolding fun_eq_iff
kuncar@47308:   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
kaliszyk@44413: 
kaliszyk@44413: lemma inter_rsp[quot_respect]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
blanchet@55940:   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
blanchet@55945:   by (intro rel_funI) (auto simp add: rel_vset_def)
kaliszyk@44413: 
kaliszyk@44413: lemma inter_prs[quot_preserve]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
kaliszyk@44413:   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
kaliszyk@44413:   unfolding fun_eq_iff
kuncar@47308:   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
kaliszyk@44413: 
kaliszyk@44459: lemma mem_prs[quot_preserve]:
kuncar@47308:   assumes "Quotient3 R Abs Rep"
kaliszyk@44459:   shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
kuncar@47308:   by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
kaliszyk@44459: 
haftmann@45970: lemma mem_rsp[quot_respect]:
blanchet@55940:   shows "(R ===> rel_vset R ===> op =) op \<in> op \<in>"
blanchet@55945:   by (intro rel_funI) (simp add: rel_vset_def)
kaliszyk@44459: 
kaliszyk@44413: end