1 (* Title: HOL/Library/Quotient.thy |
|
2 Author: Markus Wenzel, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Quotient types *} |
|
6 |
|
7 theory Quotient |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 text {* |
|
12 We introduce the notion of quotient types over equivalence relations |
|
13 via type classes. |
|
14 *} |
|
15 |
|
16 subsection {* Equivalence relations and quotient types *} |
|
17 |
|
18 text {* |
|
19 \medskip Type class @{text equiv} models equivalence relations @{text |
|
20 "\<sim> :: 'a => 'a => bool"}. |
|
21 *} |
|
22 |
|
23 class eqv = |
|
24 fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) |
|
25 |
|
26 class equiv = eqv + |
|
27 assumes equiv_refl [intro]: "x \<sim> x" |
|
28 assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z" |
|
29 assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x" |
|
30 |
|
31 lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))" |
|
32 proof - |
|
33 assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)" |
|
34 by (rule contrapos_nn) (rule equiv_sym) |
|
35 qed |
|
36 |
|
37 lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))" |
|
38 proof - |
|
39 assume "\<not> (x \<sim> y)" and "y \<sim> z" |
|
40 show "\<not> (x \<sim> z)" |
|
41 proof |
|
42 assume "x \<sim> z" |
|
43 also from `y \<sim> z` have "z \<sim> y" .. |
|
44 finally have "x \<sim> y" . |
|
45 with `\<not> (x \<sim> y)` show False by contradiction |
|
46 qed |
|
47 qed |
|
48 |
|
49 lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))" |
|
50 proof - |
|
51 assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" .. |
|
52 also assume "x \<sim> y" then have "y \<sim> x" .. |
|
53 finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" .. |
|
54 qed |
|
55 |
|
56 text {* |
|
57 \medskip The quotient type @{text "'a quot"} consists of all |
|
58 \emph{equivalence classes} over elements of the base type @{typ 'a}. |
|
59 *} |
|
60 |
|
61 typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}" |
|
62 by blast |
|
63 |
|
64 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
|
65 unfolding quot_def by blast |
|
66 |
|
67 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" |
|
68 unfolding quot_def by blast |
|
69 |
|
70 text {* |
|
71 \medskip Abstracted equivalence classes are the canonical |
|
72 representation of elements of a quotient type. |
|
73 *} |
|
74 |
|
75 definition |
|
76 "class" :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") where |
|
77 "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" |
|
78 |
|
79 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" |
|
80 proof (cases A) |
|
81 fix R assume R: "A = Abs_quot R" |
|
82 assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast |
|
83 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
|
84 then show ?thesis unfolding class_def . |
|
85 qed |
|
86 |
|
87 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" |
|
88 using quot_exhaust by blast |
|
89 |
|
90 |
|
91 subsection {* Equality on quotients *} |
|
92 |
|
93 text {* |
|
94 Equality of canonical quotient elements coincides with the original |
|
95 relation. |
|
96 *} |
|
97 |
|
98 theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" |
|
99 proof |
|
100 assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
|
101 show "a \<sim> b" |
|
102 proof - |
|
103 from eq have "{x. a \<sim> x} = {x. b \<sim> x}" |
|
104 by (simp only: class_def Abs_quot_inject quotI) |
|
105 moreover have "a \<sim> a" .. |
|
106 ultimately have "a \<in> {x. b \<sim> x}" by blast |
|
107 then have "b \<sim> a" by blast |
|
108 then show ?thesis .. |
|
109 qed |
|
110 next |
|
111 assume ab: "a \<sim> b" |
|
112 show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
|
113 proof - |
|
114 have "{x. a \<sim> x} = {x. b \<sim> x}" |
|
115 proof (rule Collect_cong) |
|
116 fix x show "(a \<sim> x) = (b \<sim> x)" |
|
117 proof |
|
118 from ab have "b \<sim> a" .. |
|
119 also assume "a \<sim> x" |
|
120 finally show "b \<sim> x" . |
|
121 next |
|
122 note ab |
|
123 also assume "b \<sim> x" |
|
124 finally show "a \<sim> x" . |
|
125 qed |
|
126 qed |
|
127 then show ?thesis by (simp only: class_def) |
|
128 qed |
|
129 qed |
|
130 |
|
131 |
|
132 subsection {* Picking representing elements *} |
|
133 |
|
134 definition |
|
135 pick :: "'a::equiv quot => 'a" where |
|
136 "pick A = (SOME a. A = \<lfloor>a\<rfloor>)" |
|
137 |
|
138 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" |
|
139 proof (unfold pick_def) |
|
140 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
|
141 proof (rule someI2) |
|
142 show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. |
|
143 fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" |
|
144 then have "a \<sim> x" .. then show "x \<sim> a" .. |
|
145 qed |
|
146 qed |
|
147 |
|
148 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A" |
|
149 proof (cases A) |
|
150 fix a assume a: "A = \<lfloor>a\<rfloor>" |
|
151 then have "pick A \<sim> a" by (simp only: pick_equiv) |
|
152 then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. |
|
153 with a show ?thesis by simp |
|
154 qed |
|
155 |
|
156 text {* |
|
157 \medskip The following rules support canonical function definitions |
|
158 on quotient types (with up to two arguments). Note that the |
|
159 stripped-down version without additional conditions is sufficient |
|
160 most of the time. |
|
161 *} |
|
162 |
|
163 theorem quot_cond_function: |
|
164 assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)" |
|
165 and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> |
|
166 ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'" |
|
167 and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" |
|
168 shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
|
169 proof - |
|
170 from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) |
|
171 also have "... = g a b" |
|
172 proof (rule cong) |
|
173 show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. |
|
174 moreover |
|
175 show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" .. |
|
176 moreover |
|
177 show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P) |
|
178 ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:) |
|
179 qed |
|
180 finally show ?thesis . |
|
181 qed |
|
182 |
|
183 theorem quot_function: |
|
184 assumes "!!X Y. f X Y == g (pick X) (pick Y)" |
|
185 and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'" |
|
186 shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
|
187 using assms and TrueI |
|
188 by (rule quot_cond_function) |
|
189 |
|
190 theorem quot_function': |
|
191 "(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
|
192 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==> |
|
193 f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
|
194 by (rule quot_function) (simp_all only: quot_equality) |
|
195 |
|
196 end |
|