src/HOL/Library/Quotient_Set.thy
 author nipkow Wed Jan 10 15:25:09 2018 +0100 (21 months ago) changeset 67399 eab6ce8368fa parent 62954 c5d0fdc260fa permissions -rw-r--r--
ran isabelle update_op on all sources
1 (*  Title:      HOL/Library/Quotient_Set.thy
2     Author:     Cezary Kaliszyk and Christian Urban
3 *)
5 section \<open>Quotient infrastructure for the set type\<close>
7 theory Quotient_Set
8 imports Quotient_Syntax
9 begin
11 subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close>
13 definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
15 lemma rel_vset_eq [id_simps]:
16   "rel_vset (=) = (=)"
17   by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff rel_vset_def)
19 lemma rel_vset_equivp:
20   assumes e: "equivp R"
21   shows "rel_vset R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
22   unfolding rel_vset_def
23   using equivp_reflp[OF e]
24   by auto (metis, metis equivp_symp[OF e])
26 lemma set_quotient [quot_thm]:
27   assumes "Quotient3 R Abs Rep"
28   shows "Quotient3 (rel_vset R) (vimage Rep) (vimage Abs)"
29 proof (rule Quotient3I)
30   from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
31   then show "\<And>xs. Rep -` (Abs -` xs) = xs"
32     unfolding vimage_def by auto
33 next
34   show "\<And>xs. rel_vset R (Abs -` xs) (Abs -` xs)"
35     unfolding rel_vset_def vimage_def
36     by auto (metis Quotient3_rel_abs[OF assms])+
37 next
38   fix r s
39   show "rel_vset R r s = (rel_vset R r r \<and> rel_vset R s s \<and> Rep -` r = Rep -` s)"
40     unfolding rel_vset_def vimage_def set_eq_iff
41     by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
42 qed
44 declare [[mapQ3 set = (rel_vset, set_quotient)]]
46 lemma empty_set_rsp[quot_respect]:
47   "rel_vset R {} {}"
48   unfolding rel_vset_def by simp
50 lemma collect_rsp[quot_respect]:
51   assumes "Quotient3 R Abs Rep"
52   shows "((R ===> (=)) ===> rel_vset R) Collect Collect"
53   by (intro rel_funI) (simp add: rel_fun_def rel_vset_def)
55 lemma collect_prs[quot_preserve]:
56   assumes "Quotient3 R Abs Rep"
57   shows "((Abs ---> id) ---> (-`) Rep) Collect = Collect"
58   unfolding fun_eq_iff
59   by (simp add: Quotient3_abs_rep[OF assms])
61 lemma union_rsp[quot_respect]:
62   assumes "Quotient3 R Abs Rep"
63   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (\<union>) (\<union>)"
64   by (intro rel_funI) (simp add: rel_vset_def)
66 lemma union_prs[quot_preserve]:
67   assumes "Quotient3 R Abs Rep"
68   shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (\<union>) = (\<union>)"
69   unfolding fun_eq_iff
70   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
72 lemma diff_rsp[quot_respect]:
73   assumes "Quotient3 R Abs Rep"
74   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (-) (-)"
75   by (intro rel_funI) (simp add: rel_vset_def)
77 lemma diff_prs[quot_preserve]:
78   assumes "Quotient3 R Abs Rep"
79   shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (-) = (-)"
80   unfolding fun_eq_iff
81   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
83 lemma inter_rsp[quot_respect]:
84   assumes "Quotient3 R Abs Rep"
85   shows "(rel_vset R ===> rel_vset R ===> rel_vset R) (\<inter>) (\<inter>)"
86   by (intro rel_funI) (auto simp add: rel_vset_def)
88 lemma inter_prs[quot_preserve]:
89   assumes "Quotient3 R Abs Rep"
90   shows "((-`) Abs ---> (-`) Abs ---> (-`) Rep) (\<inter>) = (\<inter>)"
91   unfolding fun_eq_iff
92   by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
94 lemma mem_prs[quot_preserve]:
95   assumes "Quotient3 R Abs Rep"
96   shows "(Rep ---> (-`) Abs ---> id) (\<in>) = (\<in>)"
97   by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
99 lemma mem_rsp[quot_respect]:
100   shows "(R ===> rel_vset R ===> (=)) (\<in>) (\<in>)"
101   by (intro rel_funI) (simp add: rel_vset_def)
103 end