10250
|
1 |
(* Title: HOL/Library/Quotient.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {*
|
|
7 |
\title{Quotients}
|
|
8 |
\author{Gertrud Bauer and Markus Wenzel}
|
|
9 |
*}
|
|
10 |
|
|
11 |
theory Quotient = Main:
|
|
12 |
|
|
13 |
text {*
|
|
14 |
Higher-order quotients are defined over partial equivalence relations
|
|
15 |
(PERs) instead of total ones. We provide axiomatic type classes
|
|
16 |
@{text "equiv < partial_equiv"} and a type constructor
|
|
17 |
@{text "'a quot"} with basic operations. Note that conventional
|
|
18 |
quotient constructions emerge as a special case. This development is
|
|
19 |
loosely based on \cite{Slotosch:1997}.
|
|
20 |
*}
|
|
21 |
|
|
22 |
|
|
23 |
subsection {* Equivalence relations *}
|
|
24 |
|
|
25 |
subsubsection {* Partial equivalence *}
|
|
26 |
|
|
27 |
text {*
|
|
28 |
Type class @{text partial_equiv} models partial equivalence relations
|
|
29 |
(PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
|
|
30 |
which is required to be symmetric and transitive, but not necessarily
|
|
31 |
reflexive.
|
|
32 |
*}
|
|
33 |
|
|
34 |
consts
|
|
35 |
eqv :: "'a => 'a => bool" (infixl "\<sim>" 50)
|
|
36 |
|
|
37 |
axclass partial_equiv < "term"
|
|
38 |
eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
|
|
39 |
eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
|
|
40 |
|
|
41 |
text {*
|
|
42 |
\medskip The domain of a partial equivalence relation is the set of
|
|
43 |
reflexive elements. Due to symmetry and transitivity this
|
|
44 |
characterizes exactly those elements that are connected with
|
|
45 |
\emph{any} other one.
|
|
46 |
*}
|
|
47 |
|
|
48 |
constdefs
|
|
49 |
domain :: "'a::partial_equiv set"
|
|
50 |
"domain == {x. x \<sim> x}"
|
|
51 |
|
|
52 |
lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"
|
|
53 |
by (unfold domain_def) blast
|
|
54 |
|
|
55 |
lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"
|
|
56 |
by (unfold domain_def) blast
|
|
57 |
|
|
58 |
theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"
|
|
59 |
proof
|
|
60 |
assume xy: "x \<sim> y"
|
|
61 |
also from xy have "y \<sim> x" ..
|
|
62 |
finally show "x \<sim> x" .
|
|
63 |
qed
|
|
64 |
|
|
65 |
|
|
66 |
subsubsection {* Equivalence on function spaces *}
|
|
67 |
|
|
68 |
text {*
|
|
69 |
The @{text \<sim>} relation is lifted to function spaces. It is
|
|
70 |
important to note that this is \emph{not} the direct product, but a
|
|
71 |
structural one corresponding to the congruence property.
|
|
72 |
*}
|
|
73 |
|
|
74 |
defs (overloaded)
|
|
75 |
eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
|
|
76 |
|
|
77 |
lemma partial_equiv_funI [intro?]:
|
|
78 |
"(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"
|
|
79 |
by (unfold eqv_fun_def) blast
|
|
80 |
|
|
81 |
lemma partial_equiv_funD [dest?]:
|
|
82 |
"f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
|
|
83 |
by (unfold eqv_fun_def) blast
|
|
84 |
|
|
85 |
text {*
|
|
86 |
The class of partial equivalence relations is closed under function
|
|
87 |
spaces (in \emph{both} argument positions).
|
|
88 |
*}
|
|
89 |
|
|
90 |
instance fun :: (partial_equiv, partial_equiv) partial_equiv
|
|
91 |
proof intro_classes
|
|
92 |
fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
|
|
93 |
assume fg: "f \<sim> g"
|
|
94 |
show "g \<sim> f"
|
|
95 |
proof
|
|
96 |
fix x y :: 'a
|
|
97 |
assume x: "x \<in> domain" and y: "y \<in> domain"
|
|
98 |
assume "x \<sim> y" hence "y \<sim> x" ..
|
|
99 |
with fg y x have "f y \<sim> g x" ..
|
|
100 |
thus "g x \<sim> f y" ..
|
|
101 |
qed
|
|
102 |
assume gh: "g \<sim> h"
|
|
103 |
show "f \<sim> h"
|
|
104 |
proof
|
|
105 |
fix x y :: 'a
|
|
106 |
assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y"
|
|
107 |
with fg have "f x \<sim> g y" ..
|
|
108 |
also from y have "y \<sim> y" ..
|
|
109 |
with gh y y have "g y \<sim> h y" ..
|
|
110 |
finally show "f x \<sim> h y" .
|
|
111 |
qed
|
|
112 |
qed
|
|
113 |
|
|
114 |
|
|
115 |
subsubsection {* Total equivalence *}
|
|
116 |
|
|
117 |
text {*
|
|
118 |
The class of total equivalence relations on top of PERs. It
|
|
119 |
coincides with the standard notion of equivalence, i.e.\
|
|
120 |
@{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
|
|
121 |
and symmetric.
|
|
122 |
*}
|
|
123 |
|
|
124 |
axclass equiv < partial_equiv
|
|
125 |
eqv_refl [intro]: "x \<sim> x"
|
|
126 |
|
|
127 |
text {*
|
|
128 |
On total equivalences all elements are reflexive, and congruence
|
|
129 |
holds unconditionally.
|
|
130 |
*}
|
|
131 |
|
|
132 |
theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
|
|
133 |
proof
|
|
134 |
show "x \<sim> x" ..
|
|
135 |
qed
|
|
136 |
|
|
137 |
theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"
|
|
138 |
proof -
|
|
139 |
assume "f \<sim> g"
|
|
140 |
moreover have "x \<in> domain" ..
|
|
141 |
moreover have "y \<in> domain" ..
|
|
142 |
moreover assume "x \<sim> y"
|
|
143 |
ultimately show ?thesis ..
|
|
144 |
qed
|
|
145 |
|
|
146 |
|
|
147 |
subsection {* Quotient types *}
|
|
148 |
|
|
149 |
subsubsection {* General quotients and equivalence classes *}
|
|
150 |
|
|
151 |
text {*
|
|
152 |
The quotient type @{text "'a quot"} consists of all \emph{equivalence
|
|
153 |
classes} over elements of the base type @{typ 'a}.
|
|
154 |
*}
|
|
155 |
|
|
156 |
typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
|
|
157 |
by blast
|
|
158 |
|
|
159 |
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
|
|
160 |
by (unfold quot_def) blast
|
|
161 |
|
|
162 |
lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
|
|
163 |
by (unfold quot_def) blast
|
|
164 |
|
|
165 |
text {*
|
|
166 |
\medskip Abstracted equivalence classes are the canonical
|
|
167 |
representation of elements of a quotient type.
|
|
168 |
*}
|
|
169 |
|
|
170 |
constdefs
|
|
171 |
eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>")
|
|
172 |
"\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
|
|
173 |
|
|
174 |
theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"
|
10278
|
175 |
proof (cases A)
|
|
176 |
fix R assume R: "A = Abs_quot R"
|
|
177 |
assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
|
|
178 |
with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
|
|
179 |
thus ?thesis by (unfold eqv_class_def)
|
10250
|
180 |
qed
|
|
181 |
|
|
182 |
lemma quot_cases [case_names rep, cases type: quot]:
|
|
183 |
"(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
|
|
184 |
by (insert quot_rep) blast
|
|
185 |
|
|
186 |
|
|
187 |
subsubsection {* Equality on quotients *}
|
|
188 |
|
|
189 |
text {*
|
|
190 |
Equality of canonical quotient elements corresponds to the original
|
|
191 |
relation as follows.
|
|
192 |
*}
|
|
193 |
|
|
194 |
theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
|
|
195 |
proof -
|
|
196 |
assume ab: "a \<sim> b"
|
|
197 |
have "{x. a \<sim> x} = {x. b \<sim> x}"
|
|
198 |
proof (rule Collect_cong)
|
|
199 |
fix x show "(a \<sim> x) = (b \<sim> x)"
|
|
200 |
proof
|
|
201 |
from ab have "b \<sim> a" ..
|
|
202 |
also assume "a \<sim> x"
|
|
203 |
finally show "b \<sim> x" .
|
|
204 |
next
|
|
205 |
note ab
|
|
206 |
also assume "b \<sim> x"
|
|
207 |
finally show "a \<sim> x" .
|
|
208 |
qed
|
|
209 |
qed
|
|
210 |
thus ?thesis by (simp only: eqv_class_def)
|
|
211 |
qed
|
|
212 |
|
|
213 |
theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b" (* FIXME [dest] would cause trouble with blast due to overloading *)
|
|
214 |
proof (unfold eqv_class_def)
|
|
215 |
assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"
|
|
216 |
hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)
|
|
217 |
moreover assume "a \<in> domain" hence "a \<sim> a" ..
|
|
218 |
ultimately have "a \<in> {x. b \<sim> x}" by blast
|
|
219 |
hence "b \<sim> a" by blast
|
|
220 |
thus "a \<sim> b" ..
|
|
221 |
qed
|
|
222 |
|
|
223 |
theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)" (* FIXME [dest] would cause trouble with blast due to overloading *)
|
|
224 |
proof (rule eqv_class_eqD')
|
|
225 |
show "a \<in> domain" ..
|
|
226 |
qed
|
|
227 |
|
|
228 |
lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
|
|
229 |
by (insert eqv_class_eqI eqv_class_eqD') blast
|
|
230 |
|
|
231 |
lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
|
|
232 |
by (insert eqv_class_eqI eqv_class_eqD) blast
|
|
233 |
|
|
234 |
|
|
235 |
subsubsection {* Picking representing elements *}
|
|
236 |
|
|
237 |
constdefs
|
|
238 |
pick :: "'a::partial_equiv quot => 'a"
|
|
239 |
"pick A == SOME a. A = \<lfloor>a\<rfloor>"
|
|
240 |
|
|
241 |
theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" (* FIXME [intro] !? *)
|
|
242 |
proof (unfold pick_def)
|
|
243 |
assume a: "a \<in> domain"
|
|
244 |
show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
|
|
245 |
proof (rule someI2)
|
|
246 |
show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
|
|
247 |
fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
|
|
248 |
hence "a \<sim> x" ..
|
|
249 |
thus "x \<sim> a" ..
|
|
250 |
qed
|
|
251 |
qed
|
|
252 |
|
|
253 |
theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)"
|
|
254 |
proof (rule pick_eqv')
|
|
255 |
show "a \<in> domain" ..
|
|
256 |
qed
|
|
257 |
|
10278
|
258 |
theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)"
|
10250
|
259 |
proof (cases A)
|
|
260 |
fix a assume a: "A = \<lfloor>a\<rfloor>"
|
10278
|
261 |
hence "pick A \<sim> a" by simp
|
10250
|
262 |
hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp
|
|
263 |
with a show ?thesis by simp
|
|
264 |
qed
|
|
265 |
|
|
266 |
end
|