author  haftmann 
Mon, 29 Nov 2010 22:32:06 +0100  
changeset 40816  19c492929756 
parent 40815  6e2d17cc0d1d 
child 40817  781da1e8808c 
permissions  rwrr 
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 HigherOrder 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 

40815  16 
lemma equivI: 
17 
"refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r" 

18 
by (simp add: equiv_def) 

19 

20 
lemma equivE: 

21 
assumes "equiv A r" 

22 
obtains "refl_on A r" and "sym r" and "trans r" 

23 
using assms by (simp add: equiv_def) 

24 

15300  25 
text {* 
26 
Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O 

27 
r = r"}. 

28 

29 
First half: @{text "equiv A r ==> r\<inverse> O r = r"}. 

30 
*} 

31 

32 
lemma sym_trans_comp_subset: 

33 
"sym r ==> trans r ==> r\<inverse> O r \<subseteq> r" 

34 
by (unfold trans_def sym_def converse_def) blast 

35 

30198  36 
lemma refl_on_comp_subset: "refl_on A r ==> r \<subseteq> r\<inverse> O r" 
37 
by (unfold refl_on_def) blast 

15300  38 

39 
lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r" 

40 
apply (unfold equiv_def) 

41 
apply clarify 

42 
apply (rule equalityI) 

30198  43 
apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+ 
15300  44 
done 
45 

46 
text {* Second half. *} 

47 

48 
lemma comp_equivI: 

49 
"r\<inverse> O r = r ==> Domain r = A ==> equiv A r" 

30198  50 
apply (unfold equiv_def refl_on_def sym_def trans_def) 
15300  51 
apply (erule equalityE) 
52 
apply (subgoal_tac "\<forall>x y. (x, y) \<in> r > (y, x) \<in> r") 

53 
apply fast 

54 
apply fast 

55 
done 

56 

57 

58 
subsection {* Equivalence classes *} 

59 

60 
lemma equiv_class_subset: 

61 
"equiv A r ==> (a, b) \<in> r ==> r``{a} \<subseteq> r``{b}" 

62 
 {* lemma for the next result *} 

63 
by (unfold equiv_def trans_def sym_def) blast 

64 

65 
theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}" 

66 
apply (assumption  rule equalityI equiv_class_subset)+ 

67 
apply (unfold equiv_def sym_def) 

68 
apply blast 

69 
done 

70 

71 
lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r``{a}" 

30198  72 
by (unfold equiv_def refl_on_def) blast 
15300  73 

74 
lemma subset_equiv_class: 

75 
"equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r" 

76 
 {* lemma for the next result *} 

30198  77 
by (unfold equiv_def refl_on_def) blast 
15300  78 

79 
lemma eq_equiv_class: 

80 
"r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r" 

17589  81 
by (iprover intro: equalityD2 subset_equiv_class) 
15300  82 

83 
lemma equiv_class_nondisjoint: 

84 
"equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r" 

85 
by (unfold equiv_def trans_def sym_def) blast 

86 

87 
lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A" 

30198  88 
by (unfold equiv_def refl_on_def) blast 
15300  89 

90 
theorem equiv_class_eq_iff: 

91 
"equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)" 

92 
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) 

93 

94 
theorem eq_equiv_class_iff: 

95 
"equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)" 

96 
by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) 

97 

98 

99 
subsection {* Quotients *} 

100 

28229  101 
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where 
37767  102 
"A//r = (\<Union>x \<in> A. {r``{x}})"  {* set of equiv classes *} 
15300  103 

104 
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r" 

105 
by (unfold quotient_def) blast 

106 

107 
lemma quotientE: 

108 
"X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P" 

109 
by (unfold quotient_def) blast 

110 

111 
lemma Union_quotient: "equiv A r ==> Union (A//r) = A" 

30198  112 
by (unfold equiv_def refl_on_def quotient_def) blast 
15300  113 

114 
lemma quotient_disj: 

115 
"equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y  (X \<inter> Y = {})" 

116 
apply (unfold quotient_def) 

117 
apply clarify 

118 
apply (rule equiv_class_eq) 

119 
apply assumption 

120 
apply (unfold equiv_def trans_def sym_def) 

121 
apply blast 

122 
done 

123 

124 
lemma quotient_eqI: 

125 
"[equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y; (x,y) \<in> r] ==> X = Y" 

126 
apply (clarify elim!: quotientE) 

127 
apply (rule equiv_class_eq, assumption) 

128 
apply (unfold equiv_def sym_def trans_def, blast) 

129 
done 

130 

131 
lemma quotient_eq_iff: 

132 
"[equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y] ==> (X = Y) = ((x,y) \<in> r)" 

133 
apply (rule iffI) 

134 
prefer 2 apply (blast del: equalityI intro: quotient_eqI) 

135 
apply (clarify elim!: quotientE) 

136 
apply (unfold equiv_def sym_def trans_def, blast) 

137 
done 

138 

18493  139 
lemma eq_equiv_class_iff2: 
140 
"\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)" 

141 
by(simp add:quotient_def eq_equiv_class_iff) 

142 

15300  143 

144 
lemma quotient_empty [simp]: "{}//r = {}" 

145 
by(simp add: quotient_def) 

146 

147 
lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})" 

148 
by(simp add: quotient_def) 

149 

150 
lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})" 

151 
by(simp add: quotient_def) 

152 

153 

15302  154 
lemma singleton_quotient: "{x}//r = {r `` {x}}" 
155 
by(simp add:quotient_def) 

156 

157 
lemma quotient_diff1: 

158 
"\<lbrakk> inj_on (%a. {a}//r) A; a \<in> A \<rbrakk> \<Longrightarrow> (A  {a})//r = A//r  {a}//r" 

159 
apply(simp add:quotient_def inj_on_def) 

160 
apply blast 

161 
done 

162 

15300  163 
subsection {* Defining unary operations upon equivalence classes *} 
164 

165 
text{*A congruencepreserving function*} 

40816
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

166 

19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

167 
definition congruent where 
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

168 
"congruent r f \<longleftrightarrow> (\<forall>y z. (y, z) \<in> r \<longrightarrow> f y = f z)" 
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

169 

19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

170 
lemma congruentI: 
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

171 
"(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f" 
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

172 
by (simp add: congruent_def) 
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

173 

19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

174 
lemma congruentD: 
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

175 
"congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z" 
19c492929756
replaced slightly odd locale congruent by plain definition
haftmann
parents:
40815
diff
changeset

176 
by (simp add: congruent_def) 
15300  177 

19363  178 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19979
diff
changeset

179 
RESPECTS :: "('a => 'b) => ('a * 'a) set => bool" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19979
diff
changeset

180 
(infixr "respects" 80) where 
19363  181 
"f respects r == congruent r f" 
15300  182 

183 

184 
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c" 

185 
 {* lemma required to prove @{text UN_equiv_class} *} 

186 
by auto 

187 

188 
lemma UN_equiv_class: 

189 
"equiv A r ==> f respects r ==> a \<in> A 

190 
==> (\<Union>x \<in> r``{a}. f x) = f a" 

191 
 {* Conversion rule *} 

192 
apply (rule equiv_class_self [THEN UN_constant_eq], assumption+) 

193 
apply (unfold equiv_def congruent_def sym_def) 

194 
apply (blast del: equalityI) 

195 
done 

196 

197 
lemma UN_equiv_class_type: 

198 
"equiv A r ==> f respects r ==> X \<in> A//r ==> 

199 
(!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B" 

200 
apply (unfold quotient_def) 

201 
apply clarify 

202 
apply (subst UN_equiv_class) 

203 
apply auto 

204 
done 

205 

206 
text {* 

207 
Sufficient conditions for injectiveness. Could weaken premises! 

208 
major premise could be an inclusion; bcong could be @{text "!!y. y \<in> 

209 
A ==> f y \<in> B"}. 

210 
*} 

211 

212 
lemma UN_equiv_class_inject: 

213 
"equiv A r ==> f respects r ==> 

214 
(\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r 

215 
==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r) 

216 
==> X = Y" 

217 
apply (unfold quotient_def) 

218 
apply clarify 

219 
apply (rule equiv_class_eq) 

220 
apply assumption 

221 
apply (subgoal_tac "f x = f xa") 

222 
apply blast 

223 
apply (erule box_equals) 

224 
apply (assumption  rule UN_equiv_class)+ 

225 
done 

226 

227 

228 
subsection {* Defining binary operations upon equivalence classes *} 

229 

230 
text{*A congruencepreserving function of two arguments*} 

231 
locale congruent2 = 

232 
fixes r1 and r2 and f 

233 
assumes congruent2: 

234 
"(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2" 

235 

236 
text{*Abbreviation for the common case where the relations are identical*} 

19979  237 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19979
diff
changeset

238 
RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool" 
21749  239 
(infixr "respects2" 80) where 
19979  240 
"f respects2 r == congruent2 r r f" 
241 

15300  242 

243 
lemma congruent2_implies_congruent: 

244 
"equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)" 

30198  245 
by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast 
15300  246 

247 
lemma congruent2_implies_congruent_UN: 

248 
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==> 

249 
congruent r1 (\<lambda>x1. \<Union>x2 \<in> r2``{a}. f x1 x2)" 

250 
apply (unfold congruent_def) 

251 
apply clarify 

252 
apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+) 

253 
apply (simp add: UN_equiv_class congruent2_implies_congruent) 

30198  254 
apply (unfold congruent2_def equiv_def refl_on_def) 
15300  255 
apply (blast del: equalityI) 
256 
done 

257 

258 
lemma UN_equiv_class2: 

259 
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \<in> A1 ==> a2 \<in> A2 

260 
==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. f x1 x2) = f a1 a2" 

261 
by (simp add: UN_equiv_class congruent2_implies_congruent 

262 
congruent2_implies_congruent_UN) 

263 

264 
lemma UN_equiv_class_type2: 

265 
"equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f 

266 
==> X1 \<in> A1//r1 ==> X2 \<in> A2//r2 

267 
==> (!!x1 x2. x1 \<in> A1 ==> x2 \<in> A2 ==> f x1 x2 \<in> B) 

268 
==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B" 

269 
apply (unfold quotient_def) 

270 
apply clarify 

271 
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 

272 
congruent2_implies_congruent quotientI) 

273 
done 

274 

275 
lemma UN_UN_split_split_eq: 

276 
"(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) = 

277 
(\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)" 

278 
 {* Allows a natural expression of binary operators, *} 

279 
 {* without explicit calls to @{text split} *} 

280 
by auto 

281 

282 
lemma congruent2I: 

283 
"equiv A1 r1 ==> equiv A2 r2 

284 
==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w) 

285 
==> (!!y z w. w \<in> A1 ==> (y,z) \<in> r2 ==> f w y = f w z) 

286 
==> congruent2 r1 r2 f" 

287 
 {* Suggested by John Harrison  the two subproofs may be *} 

288 
 {* \emph{much} simpler than the direct proof. *} 

30198  289 
apply (unfold congruent2_def equiv_def refl_on_def) 
15300  290 
apply clarify 
291 
apply (blast intro: trans) 

292 
done 

293 

294 
lemma congruent2_commuteI: 

295 
assumes equivA: "equiv A r" 

296 
and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y" 

297 
and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z" 

298 
shows "f respects2 r" 

299 
apply (rule congruent2I [OF equivA equivA]) 

300 
apply (rule commute [THEN trans]) 

301 
apply (rule_tac [3] commute [THEN trans, symmetric]) 

302 
apply (rule_tac [5] sym) 

25482  303 
apply (rule congt  assumption  
15300  304 
erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ 
305 
done 

306 

24728  307 

308 
subsection {* Quotients and finiteness *} 

309 

310 
text {*Suggested by Florian Kammüller*} 

311 

312 
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)" 

313 
 {* recall @{thm equiv_type} *} 

314 
apply (rule finite_subset) 

315 
apply (erule_tac [2] finite_Pow_iff [THEN iffD2]) 

316 
apply (unfold quotient_def) 

317 
apply blast 

318 
done 

319 

320 
lemma finite_equiv_class: 

321 
"finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X" 

322 
apply (unfold quotient_def) 

323 
apply (rule finite_subset) 

324 
prefer 2 apply assumption 

325 
apply blast 

326 
done 

327 

328 
lemma equiv_imp_dvd_card: 

329 
"finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X 

330 
==> k dvd card A" 

26791
3581a9c71909
Instantiated subst rule to avoid problems with HO unification.
berghofe
parents:
25482
diff
changeset

331 
apply (rule Union_quotient [THEN subst [where P="\<lambda>A. k dvd card A"]]) 
24728  332 
apply assumption 
333 
apply (rule dvd_partition) 

334 
prefer 3 apply (blast dest: quotient_disj) 

335 
apply (simp_all add: Union_quotient equiv_type) 

336 
done 

337 

338 
lemma card_quotient_disjoint: 

339 
"\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A" 

340 
apply(simp add:quotient_def) 

341 
apply(subst card_UN_disjoint) 

342 
apply assumption 

343 
apply simp 

344 
apply(fastsimp simp add:inj_on_def) 

35216  345 
apply simp 
24728  346 
done 
347 

40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

348 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

349 
subsection {* Equivalence relations  predicate version *} 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

350 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

351 
text {* Partial equivalences *} 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

352 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

353 
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

354 
"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

355 
 {* JohnHarrisonstyle characterization *} 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

356 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

357 
lemma part_equivpI: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

358 
"(\<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

359 
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

360 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

361 
lemma part_equivpE: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

362 
assumes "part_equivp R" 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

363 
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

364 
proof  
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

365 
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

366 
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

367 
by (unfold part_equivp_def) blast+ 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

368 
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

369 
moreover have "symp R" 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

370 
proof (rule sympI) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

371 
fix x y 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

372 
assume "R x y" 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

373 
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

374 
qed 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

375 
moreover have "transp R" 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

376 
proof (rule transpI) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

377 
fix x y z 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

378 
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

379 
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

380 
qed 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

381 
ultimately show thesis by (rule that) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

382 
qed 
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 
lemma part_equivp_refl_symp_transp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

385 
"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

386 
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

387 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

388 
lemma part_equivp_symp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

389 
"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

390 
by (erule part_equivpE, erule sympE) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

391 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

392 
lemma part_equivp_transp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

393 
"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

394 
by (erule part_equivpE, erule transpE) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

395 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

396 
lemma part_equivp_typedef: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

397 
"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

398 
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

399 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

400 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

401 
text {* Total equivalences *} 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

402 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

403 
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

404 
"equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))"  {* JohnHarrisonstyle characterization *} 
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 equivpI: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

407 
"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

408 
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

409 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

410 
lemma equivpE: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

411 
assumes "equivp R" 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

412 
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

413 
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

414 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

415 
lemma equivp_implies_part_equivp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

416 
"equivp R \<Longrightarrow> part_equivp R" 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

417 
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

418 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

419 
lemma equivp_equiv: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

420 
"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

421 
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

422 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

423 
lemma equivp_reflp_symp_transp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

424 
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

425 
by (auto intro: equivpI elim: equivpE) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

426 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

427 
lemma identity_equivp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

428 
"equivp (op =)" 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

429 
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

430 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

431 
lemma equivp_reflp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

432 
"equivp R \<Longrightarrow> R x x" 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

433 
by (erule equivpE, erule reflpE) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

434 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

435 
lemma equivp_symp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

436 
"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

437 
by (erule equivpE, erule sympE) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

438 

ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

439 
lemma equivp_transp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

440 
"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

441 
by (erule equivpE, erule transpE) 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

442 

15300  443 
end 