author | paulson |
Tue, 30 Mar 2004 11:18:12 +0200 | |
changeset 14496 | aba569f1b1e0 |
parent 14365 | 3d4df8c166ae |
child 14512 | e516d7cfa249 |
permissions | -rw-r--r-- |
13482 | 1 |
(* Title: HOL/Integ/Equiv.thy |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2215 | 3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 |
Copyright 1996 University of Cambridge |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
6 |
|
13482 | 7 |
header {* Equivalence relations in Higher-Order Set Theory *} |
8 |
||
9 |
theory Equiv = Relation + Finite_Set: |
|
10 |
||
11 |
subsection {* Equiv relations *} |
|
12 |
||
13 |
locale equiv = |
|
14 |
fixes A and r |
|
15 |
assumes refl: "refl A r" |
|
16 |
and sym: "sym r" |
|
17 |
and trans: "trans r" |
|
18 |
||
19 |
text {* |
|
20 |
Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O |
|
21 |
r = r"}. |
|
22 |
||
23 |
First half: @{text "equiv A r ==> r\<inverse> O r = r"}. |
|
24 |
*} |
|
25 |
||
26 |
lemma sym_trans_comp_subset: |
|
27 |
"sym r ==> trans r ==> r\<inverse> O r \<subseteq> r" |
|
28 |
by (unfold trans_def sym_def converse_def) blast |
|
29 |
||
30 |
lemma refl_comp_subset: "refl A r ==> r \<subseteq> r\<inverse> O r" |
|
31 |
by (unfold refl_def) blast |
|
32 |
||
33 |
lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r" |
|
34 |
apply (unfold equiv_def) |
|
35 |
apply clarify |
|
36 |
apply (rule equalityI) |
|
37 |
apply (rules intro: sym_trans_comp_subset refl_comp_subset)+ |
|
38 |
done |
|
39 |
||
40 |
text {* |
|
41 |
Second half. |
|
42 |
*} |
|
43 |
||
44 |
lemma comp_equivI: |
|
45 |
"r\<inverse> O r = r ==> Domain r = A ==> equiv A r" |
|
46 |
apply (unfold equiv_def refl_def sym_def trans_def) |
|
47 |
apply (erule equalityE) |
|
48 |
apply (subgoal_tac "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> r") |
|
49 |
apply fast |
|
50 |
apply fast |
|
51 |
done |
|
52 |
||
53 |
||
54 |
subsection {* Equivalence classes *} |
|
55 |
||
56 |
lemma equiv_class_subset: |
|
57 |
"equiv A r ==> (a, b) \<in> r ==> r``{a} \<subseteq> r``{b}" |
|
58 |
-- {* lemma for the next result *} |
|
59 |
by (unfold equiv_def trans_def sym_def) blast |
|
60 |
||
14496 | 61 |
theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}" |
13482 | 62 |
apply (assumption | rule equalityI equiv_class_subset)+ |
63 |
apply (unfold equiv_def sym_def) |
|
64 |
apply blast |
|
65 |
done |
|
66 |
||
67 |
lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r``{a}" |
|
68 |
by (unfold equiv_def refl_def) blast |
|
69 |
||
70 |
lemma subset_equiv_class: |
|
71 |
"equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r" |
|
72 |
-- {* lemma for the next result *} |
|
73 |
by (unfold equiv_def refl_def) blast |
|
74 |
||
75 |
lemma eq_equiv_class: |
|
76 |
"r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r" |
|
77 |
by (rules intro: equalityD2 subset_equiv_class) |
|
78 |
||
79 |
lemma equiv_class_nondisjoint: |
|
80 |
"equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r" |
|
81 |
by (unfold equiv_def trans_def sym_def) blast |
|
82 |
||
83 |
lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A" |
|
84 |
by (unfold equiv_def refl_def) blast |
|
85 |
||
14496 | 86 |
theorem equiv_class_eq_iff: |
13482 | 87 |
"equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)" |
88 |
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) |
|
89 |
||
14496 | 90 |
corollary eq_equiv_class_iff: |
13482 | 91 |
"equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)" |
92 |
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) |
|
93 |
||
94 |
||
95 |
subsection {* Quotients *} |
|
96 |
||
9392 | 97 |
constdefs |
13482 | 98 |
quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90) |
99 |
"A//r == \<Union>x \<in> A. {r``{x}}" -- {* set of equiv classes *} |
|
100 |
||
101 |
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r" |
|
102 |
by (unfold quotient_def) blast |
|
103 |
||
104 |
lemma quotientE: |
|
105 |
"X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P" |
|
106 |
by (unfold quotient_def) blast |
|
107 |
||
108 |
lemma Union_quotient: "equiv A r ==> Union (A//r) = A" |
|
109 |
by (unfold equiv_def refl_def quotient_def) blast |
|
9392 | 110 |
|
13482 | 111 |
lemma quotient_disj: |
112 |
"equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> Y = {})" |
|
113 |
apply (unfold quotient_def) |
|
114 |
apply clarify |
|
115 |
apply (rule equiv_class_eq) |
|
116 |
apply assumption |
|
117 |
apply (unfold equiv_def trans_def sym_def) |
|
118 |
apply blast |
|
119 |
done |
|
120 |
||
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
121 |
lemma quotient_eqI: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
122 |
"[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y; (x,y) \<in> r|] ==> X = Y" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
123 |
apply (clarify elim!: quotientE) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
124 |
apply (rule equiv_class_eq, assumption) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
125 |
apply (unfold equiv_def sym_def trans_def, blast) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
126 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
127 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
128 |
lemma quotient_eq_iff: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
129 |
"[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y|] ==> (X = Y) = ((x,y) \<in> r)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
130 |
apply (rule iffI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
131 |
prefer 2 apply (blast del: equalityI intro: quotient_eqI) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
132 |
apply (clarify elim!: quotientE) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
133 |
apply (unfold equiv_def sym_def trans_def, blast) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
134 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14259
diff
changeset
|
135 |
|
13482 | 136 |
|
137 |
subsection {* Defining unary operations upon equivalence classes *} |
|
138 |
||
139 |
locale congruent = |
|
140 |
fixes r and b |
|
141 |
assumes congruent: "(y, z) \<in> r ==> b y = b z" |
|
142 |
||
143 |
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. b y = c ==> (\<Union>y \<in> A. b(y))=c" |
|
144 |
-- {* lemma required to prove @{text UN_equiv_class} *} |
|
145 |
by auto |
|
146 |
||
147 |
lemma UN_equiv_class: |
|
148 |
"equiv A r ==> congruent r b ==> a \<in> A |
|
149 |
==> (\<Union>x \<in> r``{a}. b x) = b a" |
|
150 |
-- {* Conversion rule *} |
|
151 |
apply (rule equiv_class_self [THEN UN_constant_eq], assumption+) |
|
152 |
apply (unfold equiv_def congruent_def sym_def) |
|
153 |
apply (blast del: equalityI) |
|
154 |
done |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
155 |
|
13482 | 156 |
lemma UN_equiv_class_type: |
157 |
"equiv A r ==> congruent r b ==> X \<in> A//r ==> |
|
158 |
(!!x. x \<in> A ==> b x : B) ==> (\<Union>x \<in> X. b x) : B" |
|
159 |
apply (unfold quotient_def) |
|
160 |
apply clarify |
|
161 |
apply (subst UN_equiv_class) |
|
162 |
apply auto |
|
163 |
done |
|
164 |
||
165 |
text {* |
|
166 |
Sufficient conditions for injectiveness. Could weaken premises! |
|
167 |
major premise could be an inclusion; bcong could be @{text "!!y. y \<in> |
|
168 |
A ==> b y \<in> B"}. |
|
169 |
*} |
|
170 |
||
171 |
lemma UN_equiv_class_inject: |
|
172 |
"equiv A r ==> congruent r b ==> |
|
173 |
(\<Union>x \<in> X. b x) = (\<Union>y \<in> Y. b y) ==> X \<in> A//r ==> Y \<in> A//r |
|
174 |
==> (!!x y. x \<in> A ==> y \<in> A ==> b x = b y ==> (x, y) \<in> r) |
|
175 |
==> X = Y" |
|
176 |
apply (unfold quotient_def) |
|
177 |
apply clarify |
|
178 |
apply (rule equiv_class_eq) |
|
179 |
apply assumption |
|
180 |
apply (subgoal_tac "b x = b xa") |
|
181 |
apply blast |
|
182 |
apply (erule box_equals) |
|
183 |
apply (assumption | rule UN_equiv_class)+ |
|
184 |
done |
|
185 |
||
186 |
||
187 |
subsection {* Defining binary operations upon equivalence classes *} |
|
188 |
||
189 |
locale congruent2 = |
|
190 |
fixes r and b |
|
191 |
assumes congruent2: |
|
192 |
"(y1, z1) \<in> r ==> (y2, z2) \<in> r ==> b y1 y2 = b z1 z2" |
|
193 |
||
194 |
lemma congruent2_implies_congruent: |
|
195 |
"equiv A r ==> congruent2 r b ==> a \<in> A ==> congruent r (b a)" |
|
196 |
by (unfold congruent_def congruent2_def equiv_def refl_def) blast |
|
197 |
||
198 |
lemma congruent2_implies_congruent_UN: |
|
199 |
"equiv A r ==> congruent2 r b ==> a \<in> A ==> |
|
200 |
congruent r (\<lambda>x1. \<Union>x2 \<in> r``{a}. b x1 x2)" |
|
201 |
apply (unfold congruent_def) |
|
202 |
apply clarify |
|
203 |
apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+) |
|
204 |
apply (simp add: UN_equiv_class congruent2_implies_congruent) |
|
205 |
apply (unfold congruent2_def equiv_def refl_def) |
|
206 |
apply (blast del: equalityI) |
|
207 |
done |
|
208 |
||
209 |
lemma UN_equiv_class2: |
|
210 |
"equiv A r ==> congruent2 r b ==> a1 \<in> A ==> a2 \<in> A |
|
211 |
==> (\<Union>x1 \<in> r``{a1}. \<Union>x2 \<in> r``{a2}. b x1 x2) = b a1 a2" |
|
212 |
by (simp add: UN_equiv_class congruent2_implies_congruent |
|
213 |
congruent2_implies_congruent_UN) |
|
9392 | 214 |
|
13482 | 215 |
lemma UN_equiv_class_type2: |
216 |
"equiv A r ==> congruent2 r b ==> X1 \<in> A//r ==> X2 \<in> A//r |
|
217 |
==> (!!x1 x2. x1 \<in> A ==> x2 \<in> A ==> b x1 x2 \<in> B) |
|
218 |
==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. b x1 x2) \<in> B" |
|
219 |
apply (unfold quotient_def) |
|
220 |
apply clarify |
|
221 |
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN |
|
222 |
congruent2_implies_congruent quotientI) |
|
223 |
done |
|
224 |
||
225 |
lemma UN_UN_split_split_eq: |
|
226 |
"(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) = |
|
227 |
(\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)" |
|
228 |
-- {* Allows a natural expression of binary operators, *} |
|
229 |
-- {* without explicit calls to @{text split} *} |
|
230 |
by auto |
|
231 |
||
232 |
lemma congruent2I: |
|
233 |
"equiv A r |
|
234 |
==> (!!y z w. w \<in> A ==> (y, z) \<in> r ==> b y w = b z w) |
|
235 |
==> (!!y z w. w \<in> A ==> (y, z) \<in> r ==> b w y = b w z) |
|
236 |
==> congruent2 r b" |
|
237 |
-- {* Suggested by John Harrison -- the two subproofs may be *} |
|
238 |
-- {* \emph{much} simpler than the direct proof. *} |
|
239 |
apply (unfold congruent2_def equiv_def refl_def) |
|
240 |
apply clarify |
|
241 |
apply (blast intro: trans) |
|
242 |
done |
|
243 |
||
244 |
lemma congruent2_commuteI: |
|
245 |
assumes equivA: "equiv A r" |
|
246 |
and commute: "!!y z. y \<in> A ==> z \<in> A ==> b y z = b z y" |
|
247 |
and congt: "!!y z w. w \<in> A ==> (y, z) \<in> r ==> b w y = b w z" |
|
248 |
shows "congruent2 r b" |
|
249 |
apply (rule equivA [THEN congruent2I]) |
|
250 |
apply (rule commute [THEN trans]) |
|
251 |
apply (rule_tac [3] commute [THEN trans, symmetric]) |
|
252 |
apply (rule_tac [5] sym) |
|
253 |
apply (assumption | rule congt | |
|
254 |
erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ |
|
255 |
done |
|
256 |
||
257 |
||
258 |
subsection {* Cardinality results *} |
|
259 |
||
260 |
text {* (suggested by Florian Kammüller) *} |
|
261 |
||
262 |
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)" |
|
263 |
-- {* recall @{thm equiv_type} *} |
|
264 |
apply (rule finite_subset) |
|
265 |
apply (erule_tac [2] finite_Pow_iff [THEN iffD2]) |
|
266 |
apply (unfold quotient_def) |
|
267 |
apply blast |
|
268 |
done |
|
269 |
||
270 |
lemma finite_equiv_class: |
|
271 |
"finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X" |
|
272 |
apply (unfold quotient_def) |
|
273 |
apply (rule finite_subset) |
|
274 |
prefer 2 apply assumption |
|
275 |
apply blast |
|
276 |
done |
|
277 |
||
278 |
lemma equiv_imp_dvd_card: |
|
279 |
"finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X |
|
280 |
==> k dvd card A" |
|
281 |
apply (rule Union_quotient [THEN subst]) |
|
282 |
apply assumption |
|
283 |
apply (rule dvd_partition) |
|
284 |
prefer 4 apply (blast dest: quotient_disj) |
|
285 |
apply (simp_all add: Union_quotient equiv_type finite_quotient) |
|
286 |
done |
|
287 |
||
14259 | 288 |
ML |
289 |
{* |
|
290 |
||
291 |
(* legacy ML bindings *) |
|
292 |
||
293 |
val UN_UN_split_split_eq = thm "UN_UN_split_split_eq"; |
|
294 |
val UN_constant_eq = thm "UN_constant_eq"; |
|
295 |
val UN_equiv_class = thm "UN_equiv_class"; |
|
296 |
val UN_equiv_class2 = thm "UN_equiv_class2"; |
|
297 |
val UN_equiv_class_inject = thm "UN_equiv_class_inject"; |
|
298 |
val UN_equiv_class_type = thm "UN_equiv_class_type"; |
|
299 |
val UN_equiv_class_type2 = thm "UN_equiv_class_type2"; |
|
300 |
val Union_quotient = thm "Union_quotient"; |
|
301 |
val comp_equivI = thm "comp_equivI"; |
|
302 |
val congruent2I = thm "congruent2I"; |
|
303 |
val congruent2_commuteI = thm "congruent2_commuteI"; |
|
304 |
val congruent2_def = thm "congruent2_def"; |
|
305 |
val congruent2_implies_congruent = thm "congruent2_implies_congruent"; |
|
306 |
val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN"; |
|
307 |
val congruent_def = thm "congruent_def"; |
|
308 |
val eq_equiv_class = thm "eq_equiv_class"; |
|
309 |
val eq_equiv_class_iff = thm "eq_equiv_class_iff"; |
|
310 |
val equiv_class_eq = thm "equiv_class_eq"; |
|
311 |
val equiv_class_eq_iff = thm "equiv_class_eq_iff"; |
|
312 |
val equiv_class_nondisjoint = thm "equiv_class_nondisjoint"; |
|
313 |
val equiv_class_self = thm "equiv_class_self"; |
|
314 |
val equiv_comp_eq = thm "equiv_comp_eq"; |
|
315 |
val equiv_def = thm "equiv_def"; |
|
316 |
val equiv_imp_dvd_card = thm "equiv_imp_dvd_card"; |
|
317 |
val equiv_type = thm "equiv_type"; |
|
318 |
val finite_equiv_class = thm "finite_equiv_class"; |
|
319 |
val finite_quotient = thm "finite_quotient"; |
|
320 |
val quotientE = thm "quotientE"; |
|
321 |
val quotientI = thm "quotientI"; |
|
322 |
val quotient_def = thm "quotient_def"; |
|
323 |
val quotient_disj = thm "quotient_disj"; |
|
324 |
val refl_comp_subset = thm "refl_comp_subset"; |
|
325 |
val subset_equiv_class = thm "subset_equiv_class"; |
|
326 |
val sym_trans_comp_subset = thm "sym_trans_comp_subset"; |
|
327 |
*} |
|
328 |
||
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
329 |
end |