author  blanchet 
Thu, 16 Jan 2014 18:52:50 +0100  
changeset 55022  eeba3ba73486 
parent 54744  1e7f2d296e19 
child 55024  05cc0dbf3a50 
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 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
51112
diff
changeset

8 
imports Groups_Big Relation 
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 

55022
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

163 

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

166 
text{*A congruencepreserving function*} 

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

167 

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

168 
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

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

170 

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

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

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

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

174 

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

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

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

177 
by (auto simp add: congruent_def) 
15300  178 

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

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

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

184 

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

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

187 
by auto 

188 

189 
lemma UN_equiv_class: 

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

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

192 
 {* Conversion rule *} 

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

194 
apply (unfold equiv_def congruent_def sym_def) 

195 
apply (blast del: equalityI) 

196 
done 

197 

198 
lemma UN_equiv_class_type: 

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

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

201 
apply (unfold quotient_def) 

202 
apply clarify 

203 
apply (subst UN_equiv_class) 

204 
apply auto 

205 
done 

206 

207 
text {* 

208 
Sufficient conditions for injectiveness. Could weaken premises! 

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

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

211 
*} 

212 

213 
lemma UN_equiv_class_inject: 

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

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

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

217 
==> X = Y" 

218 
apply (unfold quotient_def) 

219 
apply clarify 

220 
apply (rule equiv_class_eq) 

221 
apply assumption 

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

223 
apply blast 

224 
apply (erule box_equals) 

225 
apply (assumption  rule UN_equiv_class)+ 

226 
done 

227 

228 

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

230 

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

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

232 

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

233 
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

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

235 

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

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

237 
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

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

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

240 

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

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

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

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

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

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

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

15300  251 

252 
lemma congruent2_implies_congruent: 

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

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

256 
lemma congruent2_implies_congruent_UN: 

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

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

259 
apply (unfold congruent_def) 

260 
apply clarify 

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

262 
apply (simp add: UN_equiv_class congruent2_implies_congruent) 

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

266 

267 
lemma UN_equiv_class2: 

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

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

270 
by (simp add: UN_equiv_class congruent2_implies_congruent 

271 
congruent2_implies_congruent_UN) 

272 

273 
lemma UN_equiv_class_type2: 

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

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

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

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

278 
apply (unfold quotient_def) 

279 
apply clarify 

280 
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 

281 
congruent2_implies_congruent quotientI) 

282 
done 

283 

284 
lemma UN_UN_split_split_eq: 

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

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

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

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

289 
by auto 

290 

291 
lemma congruent2I: 

292 
"equiv A1 r1 ==> equiv A2 r2 

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

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

295 
==> congruent2 r1 r2 f" 

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

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

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

301 
done 

302 

303 
lemma congruent2_commuteI: 

304 
assumes equivA: "equiv A r" 

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

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

307 
shows "f respects2 r" 

308 
apply (rule congruent2I [OF equivA equivA]) 

309 
apply (rule commute [THEN trans]) 

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

311 
apply (rule_tac [5] sym) 

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

315 

24728  316 

317 
subsection {* Quotients and finiteness *} 

318 

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

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

322 
 {* recall @{thm equiv_type} *} 

323 
apply (rule finite_subset) 

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

325 
apply (unfold quotient_def) 

326 
apply blast 

327 
done 

328 

329 
lemma finite_equiv_class: 

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

331 
apply (unfold quotient_def) 

332 
apply (rule finite_subset) 

333 
prefer 2 apply assumption 

334 
apply blast 

335 
done 

336 

337 
lemma equiv_imp_dvd_card: 

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

339 
==> k dvd card A" 

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

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

343 
prefer 3 apply (blast dest: quotient_disj) 

344 
apply (simp_all add: Union_quotient equiv_type) 

345 
done 

346 

347 
lemma card_quotient_disjoint: 

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

349 
apply(simp add:quotient_def) 

350 
apply(subst card_UN_disjoint) 

351 
apply assumption 

352 
apply simp 

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

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

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

357 

55022
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

358 
subsection {* Projection *} 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

359 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

360 
definition proj where "proj r x = r `` {x}" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

361 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

362 
lemma proj_preserves: 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

363 
"x \<in> A \<Longrightarrow> proj r x \<in> A//r" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

364 
unfolding proj_def by (rule quotientI) 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

365 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

366 
lemma proj_in_iff: 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

367 
assumes "equiv A r" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

368 
shows "(proj r x \<in> A//r) = (x \<in> A)" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

369 
apply(rule iffI, auto simp add: proj_preserves) 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

370 
unfolding proj_def quotient_def proof clarsimp 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

371 
fix y assume y: "y \<in> A" and "r `` {x} = r `` {y}" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

372 
moreover have "y \<in> r `` {y}" using assms y unfolding equiv_def refl_on_def by blast 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

373 
ultimately have "(x,y) \<in> r" by blast 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

374 
thus "x \<in> A" using assms unfolding equiv_def refl_on_def by blast 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

375 
qed 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

376 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

377 
lemma proj_iff: 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

378 
"\<lbrakk>equiv A r; {x,y} \<subseteq> A\<rbrakk> \<Longrightarrow> (proj r x = proj r y) = ((x,y) \<in> r)" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

379 
by (simp add: proj_def eq_equiv_class_iff) 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

380 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

381 
(* 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

382 
lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

383 
unfolding proj_def equiv_def refl_on_def by blast 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

384 
*) 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

385 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

386 
lemma proj_image: "(proj r) ` A = A//r" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

387 
unfolding proj_def[abs_def] quotient_def by blast 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

388 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

389 
lemma in_quotient_imp_non_empty: 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

390 
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<noteq> {}" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

391 
unfolding quotient_def using equiv_class_self by fast 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

392 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

393 
lemma in_quotient_imp_in_rel: 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

394 
"\<lbrakk>equiv A r; X \<in> A//r; {x,y} \<subseteq> X\<rbrakk> \<Longrightarrow> (x,y) \<in> r" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

395 
using quotient_eq_iff[THEN iffD1] by fastforce 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

396 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

397 
lemma in_quotient_imp_closed: 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

398 
"\<lbrakk>equiv A r; X \<in> A//r; x \<in> X; (x,y) \<in> r\<rbrakk> \<Longrightarrow> y \<in> X" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

399 
unfolding quotient_def equiv_def trans_def by blast 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

400 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

401 
lemma in_quotient_imp_subset: 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

402 
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A" 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

403 
using assms in_quotient_imp_in_rel equiv_type by fastforce 
eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

404 

eeba3ba73486
liquidated 'Equiv_Relations_More'  distinguished between choicedependent parts and choiceindependent parts
blanchet
parents:
54744
diff
changeset

405 

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

406 
subsection {* Equivalence relations  predicate version *} 
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 
text {* Partial equivalences *} 
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 
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

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

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

415 
"(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R" 
45969  416 
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

417 

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

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

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

420 
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

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

422 
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

423 
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

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

425 
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

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

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

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

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

430 
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

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

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

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

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

435 
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

436 
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

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

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

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

440 

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

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

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

443 
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

444 

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

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

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

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

448 

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

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

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

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

452 

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

453 
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

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

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

456 

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

457 

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

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

459 

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

460 
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

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

462 

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

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

464 
"reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R" 
45969  465 
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

466 

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

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

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

469 
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

470 
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

471 

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

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

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

474 
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

475 

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

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

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

478 
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

479 

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

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

481 
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

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

483 

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

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

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

486 
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

487 

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

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

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

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

491 

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

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

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

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

495 

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

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

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

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

499 

15300  500 
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

501 