(* Title: HOL/Library/Quotient_Set.thy
Author: Cezary Kaliszyk and Christian Urban
*)
section \<open>Quotient infrastructure for the set type\<close>
theory Quotient_Set
imports Quotient_Syntax
begin
subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close>
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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
