author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46752  e9e7209eb375 
child 51112  da97167e03f7 
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" 

46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45969
diff
changeset

34 
by (unfold trans_def sym_def converse_unfold) blast 
15300  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 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
44204
diff
changeset

167 
definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where 
40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

168 
"congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)" 
40816
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" 
40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

172 
by (auto simp add: congruent_def) 
40816
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" 
40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

176 
by (auto 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*} 

40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

231 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
44204
diff
changeset

232 
definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" where 
40817
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

233 
"congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)" 
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

234 

781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

235 
lemma congruent2I': 
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

236 
assumes "\<And>y1 z1 y2 z2. (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2" 
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

237 
shows "congruent2 r1 r2 f" 
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

238 
using assms by (auto simp add: congruent2_def) 
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

239 

781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

240 
lemma congruent2D: 
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

241 
"congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2" 
781da1e8808c
replaced slightly odd locale congruent2 by plain definition
haftmann
parents:
40816
diff
changeset

242 
using assms by (auto simp add: congruent2_def) 
15300  243 

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

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

246 
RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool" 
21749  247 
(infixr "respects2" 80) where 
19979  248 
"f respects2 r == congruent2 r r f" 
249 

15300  250 

251 
lemma congruent2_implies_congruent: 

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

30198  253 
by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast 
15300  254 

255 
lemma congruent2_implies_congruent_UN: 

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

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

258 
apply (unfold congruent_def) 

259 
apply clarify 

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

261 
apply (simp add: UN_equiv_class congruent2_implies_congruent) 

30198  262 
apply (unfold congruent2_def equiv_def refl_on_def) 
15300  263 
apply (blast del: equalityI) 
264 
done 

265 

266 
lemma UN_equiv_class2: 

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

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

269 
by (simp add: UN_equiv_class congruent2_implies_congruent 

270 
congruent2_implies_congruent_UN) 

271 

272 
lemma UN_equiv_class_type2: 

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

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

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

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

277 
apply (unfold quotient_def) 

278 
apply clarify 

279 
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 

280 
congruent2_implies_congruent quotientI) 

281 
done 

282 

283 
lemma UN_UN_split_split_eq: 

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

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

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

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

288 
by auto 

289 

290 
lemma congruent2I: 

291 
"equiv A1 r1 ==> equiv A2 r2 

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

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

294 
==> congruent2 r1 r2 f" 

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

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

30198  297 
apply (unfold congruent2_def equiv_def refl_on_def) 
15300  298 
apply clarify 
299 
apply (blast intro: trans) 

300 
done 

301 

302 
lemma congruent2_commuteI: 

303 
assumes equivA: "equiv A r" 

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

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

306 
shows "f respects2 r" 

307 
apply (rule congruent2I [OF equivA equivA]) 

308 
apply (rule commute [THEN trans]) 

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

310 
apply (rule_tac [5] sym) 

25482  311 
apply (rule congt  assumption  
15300  312 
erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ 
313 
done 

314 

24728  315 

316 
subsection {* Quotients and finiteness *} 

317 

40945  318 
text {*Suggested by Florian KammÃ¼ller*} 
24728  319 

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

321 
 {* recall @{thm equiv_type} *} 

322 
apply (rule finite_subset) 

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

324 
apply (unfold quotient_def) 

325 
apply blast 

326 
done 

327 

328 
lemma finite_equiv_class: 

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

330 
apply (unfold quotient_def) 

331 
apply (rule finite_subset) 

332 
prefer 2 apply assumption 

333 
apply blast 

334 
done 

335 

336 
lemma equiv_imp_dvd_card: 

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

338 
==> k dvd card A" 

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

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

342 
prefer 3 apply (blast dest: quotient_disj) 

343 
apply (simp_all add: Union_quotient equiv_type) 

344 
done 

345 

346 
lemma card_quotient_disjoint: 

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

348 
apply(simp add:quotient_def) 

349 
apply(subst card_UN_disjoint) 

350 
apply assumption 

351 
apply simp 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44279
diff
changeset

352 
apply(fastforce simp add:inj_on_def) 
35216  353 
apply simp 
24728  354 
done 
355 

40812
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 
subsection {* Equivalence relations  predicate version *} 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

358 

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

359 
text {* Partial equivalences *} 
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 
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

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

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

364 

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

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

366 
"(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R" 
45969  367 
by (auto simp add: part_equivp_def) (auto elim: sympE transpE) 
40812
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

368 

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

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

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

371 
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

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

373 
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

374 
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

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

376 
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

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

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

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

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

381 
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

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

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

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

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

386 
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

387 
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

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

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

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

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

394 
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

395 

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

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

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

398 
by (erule part_equivpE, erule sympE) 
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 
lemma part_equivp_transp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

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

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

403 

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

404 
lemma part_equivp_typedef: 
44204
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40945
diff
changeset

405 
"part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}" 
3cdc4176638c
Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
40945
diff
changeset

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

407 

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

408 

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

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

410 

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

411 
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

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

413 

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

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

415 
"reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R" 
45969  416 
by (auto elim: reflpE sympE transpE simp add: equivp_def) 
40812
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 equivpE: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

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

420 
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

421 
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

422 

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

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

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

425 
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

426 

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

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

428 
"equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)" 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45969
diff
changeset

429 
by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set]) 
40812
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_symp_transp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

432 
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

433 
by (auto intro: equivpI elim: equivpE) 
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 identity_equivp: 
ff16e22e8776
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents:
37767
diff
changeset

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

437 
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

438 

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

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

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

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

442 

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

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

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

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

446 

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

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

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

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

450 

15300  451 
end 
46752
e9e7209eb375
more fundamental predtoset conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
45969
diff
changeset

452 