author | paulson |
Wed, 01 Sep 2004 15:04:01 +0200 | |
changeset 15169 | 2b5da07a0b89 |
parent 15140 | 322485b816ac |
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 |
||
15131 | 9 |
theory Equiv |
15140 | 10 |
imports Relation Finite_Set |
15131 | 11 |
begin |
13482 | 12 |
|
14658 | 13 |
subsection {* Equivalence relations *} |
13482 | 14 |
|
15 |
locale equiv = |
|
16 |
fixes A and r |
|
17 |
assumes refl: "refl A r" |
|
18 |
and sym: "sym r" |
|
19 |
and trans: "trans r" |
|
20 |
||
21 |
text {* |
|
22 |
Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O |
|
23 |
r = r"}. |
|
24 |
||
25 |
First half: @{text "equiv A r ==> r\<inverse> O r = r"}. |
|
26 |
*} |
|
27 |
||
28 |
lemma sym_trans_comp_subset: |
|
29 |
"sym r ==> trans r ==> r\<inverse> O r \<subseteq> r" |
|
30 |
by (unfold trans_def sym_def converse_def) blast |
|
31 |
||
32 |
lemma refl_comp_subset: "refl A r ==> r \<subseteq> r\<inverse> O r" |
|
33 |
by (unfold refl_def) blast |
|
34 |
||
35 |
lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r" |
|
36 |
apply (unfold equiv_def) |
|
37 |
apply clarify |
|
38 |
apply (rule equalityI) |
|
39 |
apply (rules intro: sym_trans_comp_subset refl_comp_subset)+ |
|
40 |
done |
|
41 |
||
14658 | 42 |
text {* Second half. *} |
13482 | 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 |
||
14512 | 90 |
theorem 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 |
|
15108 | 137 |
lemma quotient_empty [simp]: "{}//r = {}" |
138 |
by(simp add: quotient_def) |
|
139 |
||
140 |
lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})" |
|
141 |
by(simp add: quotient_def) |
|
142 |
||
143 |
lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})" |
|
144 |
by(simp add: quotient_def) |
|
145 |
||
146 |
||
13482 | 147 |
subsection {* Defining unary operations upon equivalence classes *} |
148 |
||
14658 | 149 |
text{*A congruence-preserving function*} |
13482 | 150 |
locale congruent = |
14512 | 151 |
fixes r and f |
14658 | 152 |
assumes congruent: "(y,z) \<in> r ==> f y = f z" |
13482 | 153 |
|
15169 | 154 |
syntax |
155 |
RESPECTS ::"['a => 'b, ('a * 'a) set] => bool" (infixr "respects" 80) |
|
156 |
||
157 |
translations |
|
158 |
"f respects r" == "congruent r f" |
|
159 |
||
160 |
||
14512 | 161 |
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c" |
13482 | 162 |
-- {* lemma required to prove @{text UN_equiv_class} *} |
163 |
by auto |
|
164 |
||
165 |
lemma UN_equiv_class: |
|
15169 | 166 |
"equiv A r ==> f respects r ==> a \<in> A |
14512 | 167 |
==> (\<Union>x \<in> r``{a}. f x) = f a" |
13482 | 168 |
-- {* Conversion rule *} |
169 |
apply (rule equiv_class_self [THEN UN_constant_eq], assumption+) |
|
170 |
apply (unfold equiv_def congruent_def sym_def) |
|
171 |
apply (blast del: equalityI) |
|
172 |
done |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
173 |
|
13482 | 174 |
lemma UN_equiv_class_type: |
15169 | 175 |
"equiv A r ==> f respects r ==> X \<in> A//r ==> |
14512 | 176 |
(!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B" |
13482 | 177 |
apply (unfold quotient_def) |
178 |
apply clarify |
|
179 |
apply (subst UN_equiv_class) |
|
180 |
apply auto |
|
181 |
done |
|
182 |
||
183 |
text {* |
|
184 |
Sufficient conditions for injectiveness. Could weaken premises! |
|
185 |
major premise could be an inclusion; bcong could be @{text "!!y. y \<in> |
|
14512 | 186 |
A ==> f y \<in> B"}. |
13482 | 187 |
*} |
188 |
||
189 |
lemma UN_equiv_class_inject: |
|
15169 | 190 |
"equiv A r ==> f respects r ==> |
14512 | 191 |
(\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r |
192 |
==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r) |
|
13482 | 193 |
==> X = Y" |
194 |
apply (unfold quotient_def) |
|
195 |
apply clarify |
|
196 |
apply (rule equiv_class_eq) |
|
197 |
apply assumption |
|
14512 | 198 |
apply (subgoal_tac "f x = f xa") |
13482 | 199 |
apply blast |
200 |
apply (erule box_equals) |
|
201 |
apply (assumption | rule UN_equiv_class)+ |
|
202 |
done |
|
203 |
||
204 |
||
205 |
subsection {* Defining binary operations upon equivalence classes *} |
|
206 |
||
14658 | 207 |
text{*A congruence-preserving function of two arguments*} |
13482 | 208 |
locale congruent2 = |
14658 | 209 |
fixes r1 and r2 and f |
13482 | 210 |
assumes congruent2: |
14658 | 211 |
"(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2" |
13482 | 212 |
|
15169 | 213 |
text{*Abbreviation for the common case where the relations are identical*} |
214 |
syntax |
|
215 |
RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool" (infixr "respects2 " 80) |
|
216 |
||
217 |
translations |
|
218 |
"f respects2 r" => "congruent2 r r f" |
|
219 |
||
13482 | 220 |
lemma congruent2_implies_congruent: |
14658 | 221 |
"equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)" |
13482 | 222 |
by (unfold congruent_def congruent2_def equiv_def refl_def) blast |
223 |
||
224 |
lemma congruent2_implies_congruent_UN: |
|
14658 | 225 |
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==> |
226 |
congruent r1 (\<lambda>x1. \<Union>x2 \<in> r2``{a}. f x1 x2)" |
|
13482 | 227 |
apply (unfold congruent_def) |
228 |
apply clarify |
|
229 |
apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+) |
|
230 |
apply (simp add: UN_equiv_class congruent2_implies_congruent) |
|
231 |
apply (unfold congruent2_def equiv_def refl_def) |
|
232 |
apply (blast del: equalityI) |
|
233 |
done |
|
234 |
||
235 |
lemma UN_equiv_class2: |
|
14658 | 236 |
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \<in> A1 ==> a2 \<in> A2 |
237 |
==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. f x1 x2) = f a1 a2" |
|
13482 | 238 |
by (simp add: UN_equiv_class congruent2_implies_congruent |
239 |
congruent2_implies_congruent_UN) |
|
9392 | 240 |
|
13482 | 241 |
lemma UN_equiv_class_type2: |
14658 | 242 |
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f |
243 |
==> X1 \<in> A1//r1 ==> X2 \<in> A2//r2 |
|
244 |
==> (!!x1 x2. x1 \<in> A1 ==> x2 \<in> A2 ==> f x1 x2 \<in> B) |
|
14512 | 245 |
==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B" |
13482 | 246 |
apply (unfold quotient_def) |
247 |
apply clarify |
|
248 |
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN |
|
249 |
congruent2_implies_congruent quotientI) |
|
250 |
done |
|
251 |
||
252 |
lemma UN_UN_split_split_eq: |
|
253 |
"(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) = |
|
254 |
(\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)" |
|
255 |
-- {* Allows a natural expression of binary operators, *} |
|
256 |
-- {* without explicit calls to @{text split} *} |
|
257 |
by auto |
|
258 |
||
259 |
lemma congruent2I: |
|
14658 | 260 |
"equiv A1 r1 ==> equiv A2 r2 |
261 |
==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w) |
|
262 |
==> (!!y z w. w \<in> A1 ==> (y,z) \<in> r2 ==> f w y = f w z) |
|
263 |
==> congruent2 r1 r2 f" |
|
13482 | 264 |
-- {* Suggested by John Harrison -- the two subproofs may be *} |
265 |
-- {* \emph{much} simpler than the direct proof. *} |
|
266 |
apply (unfold congruent2_def equiv_def refl_def) |
|
267 |
apply clarify |
|
268 |
apply (blast intro: trans) |
|
269 |
done |
|
270 |
||
271 |
lemma congruent2_commuteI: |
|
272 |
assumes equivA: "equiv A r" |
|
14512 | 273 |
and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y" |
14658 | 274 |
and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z" |
15169 | 275 |
shows "f respects2 r" |
14658 | 276 |
apply (rule congruent2I [OF equivA equivA]) |
13482 | 277 |
apply (rule commute [THEN trans]) |
278 |
apply (rule_tac [3] commute [THEN trans, symmetric]) |
|
279 |
apply (rule_tac [5] sym) |
|
280 |
apply (assumption | rule congt | |
|
281 |
erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ |
|
282 |
done |
|
283 |
||
284 |
||
285 |
subsection {* Cardinality results *} |
|
286 |
||
15169 | 287 |
text {*Suggested by Florian Kammüller*} |
13482 | 288 |
|
289 |
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)" |
|
290 |
-- {* recall @{thm equiv_type} *} |
|
291 |
apply (rule finite_subset) |
|
292 |
apply (erule_tac [2] finite_Pow_iff [THEN iffD2]) |
|
293 |
apply (unfold quotient_def) |
|
294 |
apply blast |
|
295 |
done |
|
296 |
||
297 |
lemma finite_equiv_class: |
|
298 |
"finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X" |
|
299 |
apply (unfold quotient_def) |
|
300 |
apply (rule finite_subset) |
|
301 |
prefer 2 apply assumption |
|
302 |
apply blast |
|
303 |
done |
|
304 |
||
305 |
lemma equiv_imp_dvd_card: |
|
306 |
"finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X |
|
307 |
==> k dvd card A" |
|
308 |
apply (rule Union_quotient [THEN subst]) |
|
309 |
apply assumption |
|
310 |
apply (rule dvd_partition) |
|
311 |
prefer 4 apply (blast dest: quotient_disj) |
|
312 |
apply (simp_all add: Union_quotient equiv_type finite_quotient) |
|
313 |
done |
|
314 |
||
14259 | 315 |
ML |
316 |
{* |
|
317 |
val UN_UN_split_split_eq = thm "UN_UN_split_split_eq"; |
|
318 |
val UN_constant_eq = thm "UN_constant_eq"; |
|
319 |
val UN_equiv_class = thm "UN_equiv_class"; |
|
320 |
val UN_equiv_class2 = thm "UN_equiv_class2"; |
|
321 |
val UN_equiv_class_inject = thm "UN_equiv_class_inject"; |
|
322 |
val UN_equiv_class_type = thm "UN_equiv_class_type"; |
|
323 |
val UN_equiv_class_type2 = thm "UN_equiv_class_type2"; |
|
324 |
val Union_quotient = thm "Union_quotient"; |
|
325 |
val comp_equivI = thm "comp_equivI"; |
|
326 |
val congruent2I = thm "congruent2I"; |
|
327 |
val congruent2_commuteI = thm "congruent2_commuteI"; |
|
328 |
val congruent2_def = thm "congruent2_def"; |
|
329 |
val congruent2_implies_congruent = thm "congruent2_implies_congruent"; |
|
330 |
val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN"; |
|
331 |
val congruent_def = thm "congruent_def"; |
|
332 |
val eq_equiv_class = thm "eq_equiv_class"; |
|
333 |
val eq_equiv_class_iff = thm "eq_equiv_class_iff"; |
|
334 |
val equiv_class_eq = thm "equiv_class_eq"; |
|
335 |
val equiv_class_eq_iff = thm "equiv_class_eq_iff"; |
|
336 |
val equiv_class_nondisjoint = thm "equiv_class_nondisjoint"; |
|
337 |
val equiv_class_self = thm "equiv_class_self"; |
|
338 |
val equiv_comp_eq = thm "equiv_comp_eq"; |
|
339 |
val equiv_def = thm "equiv_def"; |
|
340 |
val equiv_imp_dvd_card = thm "equiv_imp_dvd_card"; |
|
341 |
val equiv_type = thm "equiv_type"; |
|
342 |
val finite_equiv_class = thm "finite_equiv_class"; |
|
343 |
val finite_quotient = thm "finite_quotient"; |
|
344 |
val quotientE = thm "quotientE"; |
|
345 |
val quotientI = thm "quotientI"; |
|
346 |
val quotient_def = thm "quotient_def"; |
|
347 |
val quotient_disj = thm "quotient_disj"; |
|
348 |
val refl_comp_subset = thm "refl_comp_subset"; |
|
349 |
val subset_equiv_class = thm "subset_equiv_class"; |
|
350 |
val sym_trans_comp_subset = thm "sym_trans_comp_subset"; |
|
351 |
*} |
|
352 |
||
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
353 |
end |