author | haftmann |
Mon, 29 Nov 2010 12:14:43 +0100 | |
changeset 40812 | ff16e22e8776 |
parent 37767 | a2b7a20d6ea3 |
child 40815 | 6e2d17cc0d1d |
permissions | -rw-r--r-- |
29655
ac31940cfb69
Plain, Main form meeting points in import hierarchy
haftmann
parents:
28562
diff
changeset
|
1 |
(* Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
15300 | 2 |
Copyright 1996 University of Cambridge |
3 |
*) |
|
4 |
||
5 |
header {* Equivalence Relations in Higher-Order Set Theory *} |
|
6 |
||
7 |
theory Equiv_Relations |
|
35725
4d7e3cc9c52c
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
haftmann
parents:
35216
diff
changeset
|
8 |
imports Big_Operators Relation Plain |
15300 | 9 |
begin |
10 |
||
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
11 |
subsection {* Equivalence relations -- set version *} |
15300 | 12 |
|
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
13 |
definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
14 |
"equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r" |
15300 | 15 |
|
16 |
text {* |
|
17 |
Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O |
|
18 |
r = r"}. |
|
19 |
||
20 |
First half: @{text "equiv A r ==> r\<inverse> O r = r"}. |
|
21 |
*} |
|
22 |
||
23 |
lemma sym_trans_comp_subset: |
|
24 |
"sym r ==> trans r ==> r\<inverse> O r \<subseteq> r" |
|
25 |
by (unfold trans_def sym_def converse_def) blast |
|
26 |
||
30198 | 27 |
lemma refl_on_comp_subset: "refl_on A r ==> r \<subseteq> r\<inverse> O r" |
28 |
by (unfold refl_on_def) blast |
|
15300 | 29 |
|
30 |
lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r" |
|
31 |
apply (unfold equiv_def) |
|
32 |
apply clarify |
|
33 |
apply (rule equalityI) |
|
30198 | 34 |
apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+ |
15300 | 35 |
done |
36 |
||
37 |
text {* Second half. *} |
|
38 |
||
39 |
lemma comp_equivI: |
|
40 |
"r\<inverse> O r = r ==> Domain r = A ==> equiv A r" |
|
30198 | 41 |
apply (unfold equiv_def refl_on_def sym_def trans_def) |
15300 | 42 |
apply (erule equalityE) |
43 |
apply (subgoal_tac "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> r") |
|
44 |
apply fast |
|
45 |
apply fast |
|
46 |
done |
|
47 |
||
48 |
||
49 |
subsection {* Equivalence classes *} |
|
50 |
||
51 |
lemma equiv_class_subset: |
|
52 |
"equiv A r ==> (a, b) \<in> r ==> r``{a} \<subseteq> r``{b}" |
|
53 |
-- {* lemma for the next result *} |
|
54 |
by (unfold equiv_def trans_def sym_def) blast |
|
55 |
||
56 |
theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}" |
|
57 |
apply (assumption | rule equalityI equiv_class_subset)+ |
|
58 |
apply (unfold equiv_def sym_def) |
|
59 |
apply blast |
|
60 |
done |
|
61 |
||
62 |
lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r``{a}" |
|
30198 | 63 |
by (unfold equiv_def refl_on_def) blast |
15300 | 64 |
|
65 |
lemma subset_equiv_class: |
|
66 |
"equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r" |
|
67 |
-- {* lemma for the next result *} |
|
30198 | 68 |
by (unfold equiv_def refl_on_def) blast |
15300 | 69 |
|
70 |
lemma eq_equiv_class: |
|
71 |
"r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r" |
|
17589 | 72 |
by (iprover intro: equalityD2 subset_equiv_class) |
15300 | 73 |
|
74 |
lemma equiv_class_nondisjoint: |
|
75 |
"equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r" |
|
76 |
by (unfold equiv_def trans_def sym_def) blast |
|
77 |
||
78 |
lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A" |
|
30198 | 79 |
by (unfold equiv_def refl_on_def) blast |
15300 | 80 |
|
81 |
theorem equiv_class_eq_iff: |
|
82 |
"equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)" |
|
83 |
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) |
|
84 |
||
85 |
theorem eq_equiv_class_iff: |
|
86 |
"equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)" |
|
87 |
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) |
|
88 |
||
89 |
||
90 |
subsection {* Quotients *} |
|
91 |
||
28229 | 92 |
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where |
37767 | 93 |
"A//r = (\<Union>x \<in> A. {r``{x}})" -- {* set of equiv classes *} |
15300 | 94 |
|
95 |
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r" |
|
96 |
by (unfold quotient_def) blast |
|
97 |
||
98 |
lemma quotientE: |
|
99 |
"X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P" |
|
100 |
by (unfold quotient_def) blast |
|
101 |
||
102 |
lemma Union_quotient: "equiv A r ==> Union (A//r) = A" |
|
30198 | 103 |
by (unfold equiv_def refl_on_def quotient_def) blast |
15300 | 104 |
|
105 |
lemma quotient_disj: |
|
106 |
"equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> Y = {})" |
|
107 |
apply (unfold quotient_def) |
|
108 |
apply clarify |
|
109 |
apply (rule equiv_class_eq) |
|
110 |
apply assumption |
|
111 |
apply (unfold equiv_def trans_def sym_def) |
|
112 |
apply blast |
|
113 |
done |
|
114 |
||
115 |
lemma quotient_eqI: |
|
116 |
"[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y; (x,y) \<in> r|] ==> X = Y" |
|
117 |
apply (clarify elim!: quotientE) |
|
118 |
apply (rule equiv_class_eq, assumption) |
|
119 |
apply (unfold equiv_def sym_def trans_def, blast) |
|
120 |
done |
|
121 |
||
122 |
lemma quotient_eq_iff: |
|
123 |
"[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y|] ==> (X = Y) = ((x,y) \<in> r)" |
|
124 |
apply (rule iffI) |
|
125 |
prefer 2 apply (blast del: equalityI intro: quotient_eqI) |
|
126 |
apply (clarify elim!: quotientE) |
|
127 |
apply (unfold equiv_def sym_def trans_def, blast) |
|
128 |
done |
|
129 |
||
18493 | 130 |
lemma eq_equiv_class_iff2: |
131 |
"\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)" |
|
132 |
by(simp add:quotient_def eq_equiv_class_iff) |
|
133 |
||
15300 | 134 |
|
135 |
lemma quotient_empty [simp]: "{}//r = {}" |
|
136 |
by(simp add: quotient_def) |
|
137 |
||
138 |
lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})" |
|
139 |
by(simp add: quotient_def) |
|
140 |
||
141 |
lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})" |
|
142 |
by(simp add: quotient_def) |
|
143 |
||
144 |
||
15302 | 145 |
lemma singleton_quotient: "{x}//r = {r `` {x}}" |
146 |
by(simp add:quotient_def) |
|
147 |
||
148 |
lemma quotient_diff1: |
|
149 |
"\<lbrakk> inj_on (%a. {a}//r) A; a \<in> A \<rbrakk> \<Longrightarrow> (A - {a})//r = A//r - {a}//r" |
|
150 |
apply(simp add:quotient_def inj_on_def) |
|
151 |
apply blast |
|
152 |
done |
|
153 |
||
15300 | 154 |
subsection {* Defining unary operations upon equivalence classes *} |
155 |
||
156 |
text{*A congruence-preserving function*} |
|
157 |
locale congruent = |
|
158 |
fixes r and f |
|
159 |
assumes congruent: "(y,z) \<in> r ==> f y = f z" |
|
160 |
||
19363 | 161 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19979
diff
changeset
|
162 |
RESPECTS :: "('a => 'b) => ('a * 'a) set => bool" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19979
diff
changeset
|
163 |
(infixr "respects" 80) where |
19363 | 164 |
"f respects r == congruent r f" |
15300 | 165 |
|
166 |
||
167 |
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c" |
|
168 |
-- {* lemma required to prove @{text UN_equiv_class} *} |
|
169 |
by auto |
|
170 |
||
171 |
lemma UN_equiv_class: |
|
172 |
"equiv A r ==> f respects r ==> a \<in> A |
|
173 |
==> (\<Union>x \<in> r``{a}. f x) = f a" |
|
174 |
-- {* Conversion rule *} |
|
175 |
apply (rule equiv_class_self [THEN UN_constant_eq], assumption+) |
|
176 |
apply (unfold equiv_def congruent_def sym_def) |
|
177 |
apply (blast del: equalityI) |
|
178 |
done |
|
179 |
||
180 |
lemma UN_equiv_class_type: |
|
181 |
"equiv A r ==> f respects r ==> X \<in> A//r ==> |
|
182 |
(!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B" |
|
183 |
apply (unfold quotient_def) |
|
184 |
apply clarify |
|
185 |
apply (subst UN_equiv_class) |
|
186 |
apply auto |
|
187 |
done |
|
188 |
||
189 |
text {* |
|
190 |
Sufficient conditions for injectiveness. Could weaken premises! |
|
191 |
major premise could be an inclusion; bcong could be @{text "!!y. y \<in> |
|
192 |
A ==> f y \<in> B"}. |
|
193 |
*} |
|
194 |
||
195 |
lemma UN_equiv_class_inject: |
|
196 |
"equiv A r ==> f respects r ==> |
|
197 |
(\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r |
|
198 |
==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r) |
|
199 |
==> X = Y" |
|
200 |
apply (unfold quotient_def) |
|
201 |
apply clarify |
|
202 |
apply (rule equiv_class_eq) |
|
203 |
apply assumption |
|
204 |
apply (subgoal_tac "f x = f xa") |
|
205 |
apply blast |
|
206 |
apply (erule box_equals) |
|
207 |
apply (assumption | rule UN_equiv_class)+ |
|
208 |
done |
|
209 |
||
210 |
||
211 |
subsection {* Defining binary operations upon equivalence classes *} |
|
212 |
||
213 |
text{*A congruence-preserving function of two arguments*} |
|
214 |
locale congruent2 = |
|
215 |
fixes r1 and r2 and f |
|
216 |
assumes congruent2: |
|
217 |
"(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2" |
|
218 |
||
219 |
text{*Abbreviation for the common case where the relations are identical*} |
|
19979 | 220 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19979
diff
changeset
|
221 |
RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool" |
21749 | 222 |
(infixr "respects2" 80) where |
19979 | 223 |
"f respects2 r == congruent2 r r f" |
224 |
||
15300 | 225 |
|
226 |
lemma congruent2_implies_congruent: |
|
227 |
"equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)" |
|
30198 | 228 |
by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast |
15300 | 229 |
|
230 |
lemma congruent2_implies_congruent_UN: |
|
231 |
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==> |
|
232 |
congruent r1 (\<lambda>x1. \<Union>x2 \<in> r2``{a}. f x1 x2)" |
|
233 |
apply (unfold congruent_def) |
|
234 |
apply clarify |
|
235 |
apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+) |
|
236 |
apply (simp add: UN_equiv_class congruent2_implies_congruent) |
|
30198 | 237 |
apply (unfold congruent2_def equiv_def refl_on_def) |
15300 | 238 |
apply (blast del: equalityI) |
239 |
done |
|
240 |
||
241 |
lemma UN_equiv_class2: |
|
242 |
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \<in> A1 ==> a2 \<in> A2 |
|
243 |
==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. f x1 x2) = f a1 a2" |
|
244 |
by (simp add: UN_equiv_class congruent2_implies_congruent |
|
245 |
congruent2_implies_congruent_UN) |
|
246 |
||
247 |
lemma UN_equiv_class_type2: |
|
248 |
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f |
|
249 |
==> X1 \<in> A1//r1 ==> X2 \<in> A2//r2 |
|
250 |
==> (!!x1 x2. x1 \<in> A1 ==> x2 \<in> A2 ==> f x1 x2 \<in> B) |
|
251 |
==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B" |
|
252 |
apply (unfold quotient_def) |
|
253 |
apply clarify |
|
254 |
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN |
|
255 |
congruent2_implies_congruent quotientI) |
|
256 |
done |
|
257 |
||
258 |
lemma UN_UN_split_split_eq: |
|
259 |
"(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) = |
|
260 |
(\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)" |
|
261 |
-- {* Allows a natural expression of binary operators, *} |
|
262 |
-- {* without explicit calls to @{text split} *} |
|
263 |
by auto |
|
264 |
||
265 |
lemma congruent2I: |
|
266 |
"equiv A1 r1 ==> equiv A2 r2 |
|
267 |
==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w) |
|
268 |
==> (!!y z w. w \<in> A1 ==> (y,z) \<in> r2 ==> f w y = f w z) |
|
269 |
==> congruent2 r1 r2 f" |
|
270 |
-- {* Suggested by John Harrison -- the two subproofs may be *} |
|
271 |
-- {* \emph{much} simpler than the direct proof. *} |
|
30198 | 272 |
apply (unfold congruent2_def equiv_def refl_on_def) |
15300 | 273 |
apply clarify |
274 |
apply (blast intro: trans) |
|
275 |
done |
|
276 |
||
277 |
lemma congruent2_commuteI: |
|
278 |
assumes equivA: "equiv A r" |
|
279 |
and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y" |
|
280 |
and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z" |
|
281 |
shows "f respects2 r" |
|
282 |
apply (rule congruent2I [OF equivA equivA]) |
|
283 |
apply (rule commute [THEN trans]) |
|
284 |
apply (rule_tac [3] commute [THEN trans, symmetric]) |
|
285 |
apply (rule_tac [5] sym) |
|
25482 | 286 |
apply (rule congt | assumption | |
15300 | 287 |
erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ |
288 |
done |
|
289 |
||
24728 | 290 |
|
291 |
subsection {* Quotients and finiteness *} |
|
292 |
||
293 |
text {*Suggested by Florian Kammüller*} |
|
294 |
||
295 |
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)" |
|
296 |
-- {* recall @{thm equiv_type} *} |
|
297 |
apply (rule finite_subset) |
|
298 |
apply (erule_tac [2] finite_Pow_iff [THEN iffD2]) |
|
299 |
apply (unfold quotient_def) |
|
300 |
apply blast |
|
301 |
done |
|
302 |
||
303 |
lemma finite_equiv_class: |
|
304 |
"finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X" |
|
305 |
apply (unfold quotient_def) |
|
306 |
apply (rule finite_subset) |
|
307 |
prefer 2 apply assumption |
|
308 |
apply blast |
|
309 |
done |
|
310 |
||
311 |
lemma equiv_imp_dvd_card: |
|
312 |
"finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X |
|
313 |
==> k dvd card A" |
|
26791
3581a9c71909
Instantiated subst rule to avoid problems with HO unification.
berghofe
parents:
25482
diff
changeset
|
314 |
apply (rule Union_quotient [THEN subst [where P="\<lambda>A. k dvd card A"]]) |
24728 | 315 |
apply assumption |
316 |
apply (rule dvd_partition) |
|
317 |
prefer 3 apply (blast dest: quotient_disj) |
|
318 |
apply (simp_all add: Union_quotient equiv_type) |
|
319 |
done |
|
320 |
||
321 |
lemma card_quotient_disjoint: |
|
322 |
"\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A" |
|
323 |
apply(simp add:quotient_def) |
|
324 |
apply(subst card_UN_disjoint) |
|
325 |
apply assumption |
|
326 |
apply simp |
|
327 |
apply(fastsimp simp add:inj_on_def) |
|
35216 | 328 |
apply simp |
24728 | 329 |
done |
330 |
||
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
331 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
332 |
subsection {* Equivalence relations -- predicate version *} |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
333 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
334 |
text {* Partial equivalences *} |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
335 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
336 |
definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
337 |
"part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> (\<forall>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y)" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
338 |
-- {* John-Harrison-style characterization *} |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
339 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
340 |
lemma part_equivpI: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
341 |
"(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
342 |
by (auto simp add: part_equivp_def mem_def) (auto elim: sympE transpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
343 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
344 |
lemma part_equivpE: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
345 |
assumes "part_equivp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
346 |
obtains x where "R x x" and "symp R" and "transp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
347 |
proof - |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
348 |
from assms have 1: "\<exists>x. R x x" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
349 |
and 2: "\<And>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
350 |
by (unfold part_equivp_def) blast+ |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
351 |
from 1 obtain x where "R x x" .. |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
352 |
moreover have "symp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
353 |
proof (rule sympI) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
354 |
fix x y |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
355 |
assume "R x y" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
356 |
with 2 [of x y] show "R y x" by auto |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
357 |
qed |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
358 |
moreover have "transp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
359 |
proof (rule transpI) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
360 |
fix x y z |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
361 |
assume "R x y" and "R y z" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
362 |
with 2 [of x y] 2 [of y z] show "R x z" by auto |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
363 |
qed |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
364 |
ultimately show thesis by (rule that) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
365 |
qed |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
366 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
367 |
lemma part_equivp_refl_symp_transp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
368 |
"part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> symp R \<and> transp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
369 |
by (auto intro: part_equivpI elim: part_equivpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
370 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
371 |
lemma part_equivp_symp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
372 |
"part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
373 |
by (erule part_equivpE, erule sympE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
374 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
375 |
lemma part_equivp_transp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
376 |
"part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
377 |
by (erule part_equivpE, erule transpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
378 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
379 |
lemma part_equivp_typedef: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
380 |
"part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
381 |
by (auto elim: part_equivpE simp add: mem_def) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
382 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
383 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
384 |
text {* Total equivalences *} |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
385 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
386 |
definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
387 |
"equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" -- {* John-Harrison-style characterization *} |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
388 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
389 |
lemma equivpI: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
390 |
"reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
391 |
by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
392 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
393 |
lemma equivpE: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
394 |
assumes "equivp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
395 |
obtains "reflp R" and "symp R" and "transp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
396 |
using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
397 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
398 |
lemma equivp_implies_part_equivp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
399 |
"equivp R \<Longrightarrow> part_equivp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
400 |
by (auto intro: part_equivpI elim: equivpE reflpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
401 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
402 |
lemma equivp_equiv: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
403 |
"equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
404 |
by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
405 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
406 |
lemma equivp_reflp_symp_transp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
407 |
shows "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
408 |
by (auto intro: equivpI elim: equivpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
409 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
410 |
lemma identity_equivp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
411 |
"equivp (op =)" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
412 |
by (auto intro: equivpI reflpI sympI transpI) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
413 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
414 |
lemma equivp_reflp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
415 |
"equivp R \<Longrightarrow> R x x" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
416 |
by (erule equivpE, erule reflpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
417 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
418 |
lemma equivp_symp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
419 |
"equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
420 |
by (erule equivpE, erule sympE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
421 |
|
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
422 |
lemma equivp_transp: |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
423 |
"equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
424 |
by (erule equivpE, erule transpE) |
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset
|
425 |
|
15300 | 426 |
end |