|
1 (* Title: HOL/Library/Quotient_Set.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 *) |
|
4 |
|
5 header {* Quotient infrastructure for the set type *} |
|
6 |
|
7 theory Quotient_Set |
|
8 imports Main Quotient_Syntax |
|
9 begin |
|
10 |
|
11 lemma set_quotient [quot_thm]: |
|
12 assumes "Quotient R Abs Rep" |
|
13 shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)" |
|
14 proof (rule QuotientI) |
|
15 from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep) |
|
16 then show "\<And>xs. Rep -` (Abs -` xs) = xs" |
|
17 unfolding vimage_def by auto |
|
18 next |
|
19 show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)" |
|
20 unfolding set_rel_def vimage_def |
|
21 by auto (metis Quotient_rel_abs[OF assms])+ |
|
22 next |
|
23 fix r s |
|
24 show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)" |
|
25 unfolding set_rel_def vimage_def set_eq_iff |
|
26 by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+ |
|
27 qed |
|
28 |
|
29 lemma empty_set_rsp[quot_respect]: |
|
30 "set_rel R {} {}" |
|
31 unfolding set_rel_def by simp |
|
32 |
|
33 lemma collect_rsp[quot_respect]: |
|
34 assumes "Quotient R Abs Rep" |
|
35 shows "((R ===> op =) ===> set_rel R) Collect Collect" |
|
36 by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def) |
|
37 |
|
38 lemma collect_prs[quot_preserve]: |
|
39 assumes "Quotient R Abs Rep" |
|
40 shows "((Abs ---> id) ---> op -` Rep) Collect = Collect" |
|
41 unfolding fun_eq_iff |
|
42 by (simp add: Quotient_abs_rep[OF assms]) |
|
43 |
|
44 lemma union_rsp[quot_respect]: |
|
45 assumes "Quotient R Abs Rep" |
|
46 shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>" |
|
47 by (intro fun_relI) (auto simp add: set_rel_def) |
|
48 |
|
49 lemma union_prs[quot_preserve]: |
|
50 assumes "Quotient R Abs Rep" |
|
51 shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>" |
|
52 unfolding fun_eq_iff |
|
53 by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) |
|
54 |
|
55 lemma diff_rsp[quot_respect]: |
|
56 assumes "Quotient R Abs Rep" |
|
57 shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -" |
|
58 by (intro fun_relI) (auto simp add: set_rel_def) |
|
59 |
|
60 lemma diff_prs[quot_preserve]: |
|
61 assumes "Quotient R Abs Rep" |
|
62 shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -" |
|
63 unfolding fun_eq_iff |
|
64 by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff) |
|
65 |
|
66 lemma inter_rsp[quot_respect]: |
|
67 assumes "Quotient R Abs Rep" |
|
68 shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>" |
|
69 by (intro fun_relI) (auto simp add: set_rel_def) |
|
70 |
|
71 lemma inter_prs[quot_preserve]: |
|
72 assumes "Quotient R Abs Rep" |
|
73 shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>" |
|
74 unfolding fun_eq_iff |
|
75 by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]]) |
|
76 |
|
77 end |