Theory HOL-Library.Quotient_Set

(*  Title:      HOL/Library/Quotient_Set.thy
    Author:     Cezary Kaliszyk and Christian Urban
*)

section ‹Quotient infrastructure for the set type›

theory Quotient_Set
imports Quotient_Syntax
begin

subsection ‹Contravariant set map (vimage) and set relator, rules for the Quotient package›

definition "rel_vset R xs ys ≡ ∀x y. R x y ⟶ x ∈ xs ⟷ y ∈ ys"

lemma rel_vset_eq [id_simps]:
  "rel_vset (=) = (=)"
  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff rel_vset_def)

lemma rel_vset_equivp:
  assumes e: "equivp R"
  shows "rel_vset R xs ys ⟷ xs = ys ∧ (∀x y. x ∈ xs ⟶ R x y ⟶ y ∈ xs)"
  unfolding rel_vset_def
  using equivp_reflp[OF e]
  by auto (metis, metis equivp_symp[OF e])

lemma set_quotient [quot_thm]:
  assumes "Quotient3 R Abs Rep"
  shows "Quotient3 (rel_vset R) (vimage Rep) (vimage Abs)"
proof (rule Quotient3I)
  from assms have "⋀x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
  then show "⋀xs. Rep -` (Abs -` xs) = xs"
    unfolding vimage_def by auto
next
  show "⋀xs. rel_vset R (Abs -` xs) (Abs -` xs)"
    unfolding rel_vset_def vimage_def
    by auto (metis Quotient3_rel_abs[OF assms])+
next
  fix r s
  show "rel_vset R r s = (rel_vset R r r ∧ rel_vset R s s ∧ Rep -` r = Rep -` s)"
    unfolding rel_vset_def vimage_def set_eq_iff
    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
qed

declare [[mapQ3 set = (rel_vset, set_quotient)]]

lemma empty_set_rsp[quot_respect]:
  "rel_vset R {} {}"
  unfolding rel_vset_def by simp

lemma collect_rsp[quot_respect]:
  assumes "Quotient3 R Abs Rep"
  shows "((R ===> (=)) ===> rel_vset R) Collect Collect"
  by (intro rel_funI) (simp add: rel_fun_def rel_vset_def)

lemma collect_prs[quot_preserve]:
  assumes "Quotient3 R Abs Rep"
  shows "((Abs ---> id) ---> (-`) Rep) Collect = Collect"
  unfolding fun_eq_iff
  by (simp add: Quotient3_abs_rep[OF assms])

lemma union_rsp[quot_respect]:
  assumes "Quotient3 R Abs Rep"
  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (∪) (∪)"
  by (intro rel_funI) (simp add: rel_vset_def)

lemma union_prs[quot_preserve]:
  assumes "Quotient3 R Abs Rep"
  shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (∪) = (∪)"
  unfolding fun_eq_iff
  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])

lemma diff_rsp[quot_respect]:
  assumes "Quotient3 R Abs Rep"
  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (-) (-)"
  by (intro rel_funI) (simp add: rel_vset_def)

lemma diff_prs[quot_preserve]:
  assumes "Quotient3 R Abs Rep"
  shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (-) = (-)"
  unfolding fun_eq_iff
  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)

lemma inter_rsp[quot_respect]:
  assumes "Quotient3 R Abs Rep"
  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (∩) (∩)"
  by (intro rel_funI) (auto simp add: rel_vset_def)

lemma inter_prs[quot_preserve]:
  assumes "Quotient3 R Abs Rep"
  shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (∩) = (∩)"
  unfolding fun_eq_iff
  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])

lemma mem_prs[quot_preserve]:
  assumes "Quotient3 R Abs Rep"
  shows "(Rep ---> (-`) Abs ---> id) (∈) = (∈)"
  by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])

lemma mem_rsp[quot_respect]:
  shows "(R ===> rel_vset R ===> (=)) (∈) (∈)"
  by (intro rel_funI) (simp add: rel_vset_def)

end