author  haftmann 
Thu, 11 Mar 2010 14:39:58 +0100  
changeset 35725  4d7e3cc9c52c 
parent 35216  7641e8d831d2 
child 37767  a2b7a20d6ea3 
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 

11 
subsection {* Equivalence relations *} 

12 

13 
locale equiv = 

14 
fixes A and r 

30198  15 
assumes refl_on: "refl_on A r" 
15300  16 
and sym: "sym r" 
17 
and trans: "trans r" 

18 

19 
text {* 

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

21 
r = r"}. 

22 

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

24 
*} 

25 

26 
lemma sym_trans_comp_subset: 

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

28 
by (unfold trans_def sym_def converse_def) blast 

29 

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

15300  32 

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

34 
apply (unfold equiv_def) 

35 
apply clarify 

36 
apply (rule equalityI) 

30198  37 
apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+ 
15300  38 
done 
39 

40 
text {* Second half. *} 

41 

42 
lemma comp_equivI: 

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

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

47 
apply fast 

48 
apply fast 

49 
done 

50 

51 

52 
subsection {* Equivalence classes *} 

53 

54 
lemma equiv_class_subset: 

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

56 
 {* lemma for the next result *} 

57 
by (unfold equiv_def trans_def sym_def) blast 

58 

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

60 
apply (assumption  rule equalityI equiv_class_subset)+ 

61 
apply (unfold equiv_def sym_def) 

62 
apply blast 

63 
done 

64 

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

30198  66 
by (unfold equiv_def refl_on_def) blast 
15300  67 

68 
lemma subset_equiv_class: 

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

70 
 {* lemma for the next result *} 

30198  71 
by (unfold equiv_def refl_on_def) blast 
15300  72 

73 
lemma eq_equiv_class: 

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

17589  75 
by (iprover intro: equalityD2 subset_equiv_class) 
15300  76 

77 
lemma equiv_class_nondisjoint: 

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

79 
by (unfold equiv_def trans_def sym_def) blast 

80 

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

30198  82 
by (unfold equiv_def refl_on_def) blast 
15300  83 

84 
theorem equiv_class_eq_iff: 

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

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

87 

88 
theorem eq_equiv_class_iff: 

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

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

91 

92 

93 
subsection {* Quotients *} 

94 

28229  95 
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) where 
28562  96 
[code del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  {* set of equiv classes *} 
15300  97 

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

99 
by (unfold quotient_def) blast 

100 

101 
lemma quotientE: 

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

103 
by (unfold quotient_def) blast 

104 

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

30198  106 
by (unfold equiv_def refl_on_def quotient_def) blast 
15300  107 

108 
lemma quotient_disj: 

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

110 
apply (unfold quotient_def) 

111 
apply clarify 

112 
apply (rule equiv_class_eq) 

113 
apply assumption 

114 
apply (unfold equiv_def trans_def sym_def) 

115 
apply blast 

116 
done 

117 

118 
lemma quotient_eqI: 

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

120 
apply (clarify elim!: quotientE) 

121 
apply (rule equiv_class_eq, assumption) 

122 
apply (unfold equiv_def sym_def trans_def, blast) 

123 
done 

124 

125 
lemma quotient_eq_iff: 

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

127 
apply (rule iffI) 

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

129 
apply (clarify elim!: quotientE) 

130 
apply (unfold equiv_def sym_def trans_def, blast) 

131 
done 

132 

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

135 
by(simp add:quotient_def eq_equiv_class_iff) 

136 

15300  137 

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

139 
by(simp add: quotient_def) 

140 

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

142 
by(simp add: quotient_def) 

143 

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

145 
by(simp add: quotient_def) 

146 

147 

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

150 

151 
lemma quotient_diff1: 

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

153 
apply(simp add:quotient_def inj_on_def) 

154 
apply blast 

155 
done 

156 

15300  157 
subsection {* Defining unary operations upon equivalence classes *} 
158 

159 
text{*A congruencepreserving function*} 

160 
locale congruent = 

161 
fixes r and f 

162 
assumes congruent: "(y,z) \<in> r ==> f y = f z" 

163 

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

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

166 
(infixr "respects" 80) where 
19363  167 
"f respects r == congruent r f" 
15300  168 

169 

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

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

172 
by auto 

173 

174 
lemma UN_equiv_class: 

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

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

177 
 {* Conversion rule *} 

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

179 
apply (unfold equiv_def congruent_def sym_def) 

180 
apply (blast del: equalityI) 

181 
done 

182 

183 
lemma UN_equiv_class_type: 

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

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

186 
apply (unfold quotient_def) 

187 
apply clarify 

188 
apply (subst UN_equiv_class) 

189 
apply auto 

190 
done 

191 

192 
text {* 

193 
Sufficient conditions for injectiveness. Could weaken premises! 

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

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

196 
*} 

197 

198 
lemma UN_equiv_class_inject: 

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

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

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

202 
==> X = Y" 

203 
apply (unfold quotient_def) 

204 
apply clarify 

205 
apply (rule equiv_class_eq) 

206 
apply assumption 

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

208 
apply blast 

209 
apply (erule box_equals) 

210 
apply (assumption  rule UN_equiv_class)+ 

211 
done 

212 

213 

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

215 

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

217 
locale congruent2 = 

218 
fixes r1 and r2 and f 

219 
assumes congruent2: 

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

221 

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

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

224 
RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool" 
21749  225 
(infixr "respects2" 80) where 
19979  226 
"f respects2 r == congruent2 r r f" 
227 

15300  228 

229 
lemma congruent2_implies_congruent: 

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

30198  231 
by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast 
15300  232 

233 
lemma congruent2_implies_congruent_UN: 

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

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

236 
apply (unfold congruent_def) 

237 
apply clarify 

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

239 
apply (simp add: UN_equiv_class congruent2_implies_congruent) 

30198  240 
apply (unfold congruent2_def equiv_def refl_on_def) 
15300  241 
apply (blast del: equalityI) 
242 
done 

243 

244 
lemma UN_equiv_class2: 

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

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

247 
by (simp add: UN_equiv_class congruent2_implies_congruent 

248 
congruent2_implies_congruent_UN) 

249 

250 
lemma UN_equiv_class_type2: 

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

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

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

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

255 
apply (unfold quotient_def) 

256 
apply clarify 

257 
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 

258 
congruent2_implies_congruent quotientI) 

259 
done 

260 

261 
lemma UN_UN_split_split_eq: 

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

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

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

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

266 
by auto 

267 

268 
lemma congruent2I: 

269 
"equiv A1 r1 ==> equiv A2 r2 

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

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

272 
==> congruent2 r1 r2 f" 

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

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

30198  275 
apply (unfold congruent2_def equiv_def refl_on_def) 
15300  276 
apply clarify 
277 
apply (blast intro: trans) 

278 
done 

279 

280 
lemma congruent2_commuteI: 

281 
assumes equivA: "equiv A r" 

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

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

284 
shows "f respects2 r" 

285 
apply (rule congruent2I [OF equivA equivA]) 

286 
apply (rule commute [THEN trans]) 

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

288 
apply (rule_tac [5] sym) 

25482  289 
apply (rule congt  assumption  
15300  290 
erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ 
291 
done 

292 

24728  293 

294 
subsection {* Quotients and finiteness *} 

295 

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

297 

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

299 
 {* recall @{thm equiv_type} *} 

300 
apply (rule finite_subset) 

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

302 
apply (unfold quotient_def) 

303 
apply blast 

304 
done 

305 

306 
lemma finite_equiv_class: 

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

308 
apply (unfold quotient_def) 

309 
apply (rule finite_subset) 

310 
prefer 2 apply assumption 

311 
apply blast 

312 
done 

313 

314 
lemma equiv_imp_dvd_card: 

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

316 
==> k dvd card A" 

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

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

320 
prefer 3 apply (blast dest: quotient_disj) 

321 
apply (simp_all add: Union_quotient equiv_type) 

322 
done 

323 

324 
lemma card_quotient_disjoint: 

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

326 
apply(simp add:quotient_def) 

327 
apply(subst card_UN_disjoint) 

328 
apply assumption 

329 
apply simp 

330 
apply(fastsimp simp add:inj_on_def) 

35216  331 
apply simp 
24728  332 
done 
333 

15300  334 
end 