23146

1 
(* Title: ZF/EquivClass.thy


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1994 University of Cambridge


4 
*)


5 


6 
header{*Equivalence Relations*}


7 


8 
theory EquivClass imports Trancl Perm begin


9 

24893

10 
definition


11 
quotient :: "[i,i]=>i" (infixl "'/'/" 90) (*set of equiv classes*) where

46953

12 
"A//r == {r``{x} . x \<in> A}"

23146

13 

24893

14 
definition


15 
congruent :: "[i,i=>i]=>o" where

46820

16 
"congruent(r,b) == \<forall>y z. <y,z>:r \<longrightarrow> b(y)=b(z)"

23146

17 

24893

18 
definition


19 
congruent2 :: "[i,i,[i,i]=>i]=>o" where

46820

20 
"congruent2(r1,r2,b) == \<forall>y1 z1 y2 z2.


21 
<y1,z1>:r1 \<longrightarrow> <y2,z2>:r2 \<longrightarrow> b(y1,y2) = b(z1,z2)"

23146

22 

24892

23 
abbreviation


24 
RESPECTS ::"[i=>i, i] => o" (infixr "respects" 80) where


25 
"f respects r == congruent(r,f)"


26 


27 
abbreviation


28 
RESPECTS2 ::"[i=>i=>i, i] => o" (infixr "respects2 " 80) where


29 
"f respects2 r == congruent2(r,r,f)"

23146

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


31 


32 


33 
subsection{*Suppes, Theorem 70:


34 
@{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}


35 


36 
(** first half: equiv(A,r) ==> converse(r) O r = r **)


37 


38 
lemma sym_trans_comp_subset:

46820

39 
"[ sym(r); trans(r) ] ==> converse(r) O r \<subseteq> r"

23146

40 
by (unfold trans_def sym_def, blast)


41 


42 
lemma refl_comp_subset:

46820

43 
"[ refl(A,r); r \<subseteq> A*A ] ==> r \<subseteq> converse(r) O r"

23146

44 
by (unfold refl_def, blast)


45 


46 
lemma equiv_comp_eq:


47 
"equiv(A,r) ==> converse(r) O r = r"


48 
apply (unfold equiv_def)


49 
apply (blast del: subsetI intro!: sym_trans_comp_subset refl_comp_subset)


50 
done


51 


52 
(*second half*)


53 
lemma comp_equivI:


54 
"[ converse(r) O r = r; domain(r) = A ] ==> equiv(A,r)"


55 
apply (unfold equiv_def refl_def sym_def trans_def)


56 
apply (erule equalityE)

46820

57 
apply (subgoal_tac "\<forall>x y. <x,y> \<in> r \<longrightarrow> <y,x> \<in> r", blast+)

23146

58 
done


59 


60 
(** Equivalence classes **)


61 


62 
(*Lemma for the next result*)


63 
lemma equiv_class_subset:

46820

64 
"[ sym(r); trans(r); <a,b>: r ] ==> r``{a} \<subseteq> r``{b}"

23146

65 
by (unfold trans_def sym_def, blast)


66 


67 
lemma equiv_class_eq:


68 
"[ equiv(A,r); <a,b>: r ] ==> r``{a} = r``{b}"


69 
apply (unfold equiv_def)


70 
apply (safe del: subsetI intro!: equalityI equiv_class_subset)


71 
apply (unfold sym_def, blast)


72 
done


73 


74 
lemma equiv_class_self:

46953

75 
"[ equiv(A,r); a \<in> A ] ==> a \<in> r``{a}"

23146

76 
by (unfold equiv_def refl_def, blast)


77 


78 
(*Lemma for the next result*)


79 
lemma subset_equiv_class:

46953

80 
"[ equiv(A,r); r``{b} \<subseteq> r``{a}; b \<in> A ] ==> <a,b>: r"

23146

81 
by (unfold equiv_def refl_def, blast)


82 

46953

83 
lemma eq_equiv_class: "[ r``{a} = r``{b}; equiv(A,r); b \<in> A ] ==> <a,b>: r"

23146

84 
by (assumption  rule equalityD2 subset_equiv_class)+


85 


86 
(*thus r``{a} = r``{b} as well*)


87 
lemma equiv_class_nondisjoint:

46820

88 
"[ equiv(A,r); x: (r``{a} \<inter> r``{b}) ] ==> <a,b>: r"

23146

89 
by (unfold equiv_def trans_def sym_def, blast)


90 

46820

91 
lemma equiv_type: "equiv(A,r) ==> r \<subseteq> A*A"

23146

92 
by (unfold equiv_def, blast)


93 


94 
lemma equiv_class_eq_iff:

46953

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

23146

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


97 


98 
lemma eq_equiv_class_iff:

46953

99 
"[ equiv(A,r); x \<in> A; y \<in> A ] ==> r``{x} = r``{y} \<longleftrightarrow> <x,y>: r"

23146

100 
by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)


101 


102 
(*** Quotients ***)


103 


104 
(** Introduction/elimination rules  needed? **)


105 

46953

106 
lemma quotientI [TC]: "x \<in> A ==> r``{x}: A//r"

23146

107 
apply (unfold quotient_def)


108 
apply (erule RepFunI)


109 
done


110 


111 
lemma quotientE:

46953

112 
"[ X \<in> A//r; !!x. [ X = r``{x}; x \<in> A ] ==> P ] ==> P"

23146

113 
by (unfold quotient_def, blast)


114 


115 
lemma Union_quotient:

46820

116 
"equiv(A,r) ==> \<Union>(A//r) = A"

23146

117 
by (unfold equiv_def refl_def quotient_def, blast)


118 


119 
lemma quotient_disj:

46953

120 
"[ equiv(A,r); X \<in> A//r; Y \<in> A//r ] ==> X=Y  (X \<inter> Y \<subseteq> 0)"

23146

121 
apply (unfold quotient_def)


122 
apply (safe intro!: equiv_class_eq, assumption)


123 
apply (unfold equiv_def trans_def sym_def, blast)


124 
done


125 


126 
subsection{*Defining Unary Operations upon Equivalence Classes*}


127 


128 
(** Could have a locale with the premises equiv(A,r) and congruent(r,b)


129 
**)


130 


131 
(*Conversion rule*)


132 
lemma UN_equiv_class:

46953

133 
"[ equiv(A,r); b respects r; a \<in> A ] ==> (\<Union>x\<in>r``{a}. b(x)) = b(a)"

46820

134 
apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)")

23146

135 
apply simp

46820

136 
apply (blast intro: equiv_class_self)

23146

137 
apply (unfold equiv_def sym_def congruent_def, blast)


138 
done


139 

46820

140 
(*type checking of @{term"\<Union>x\<in>r``{a}. b(x)"} *)

23146

141 
lemma UN_equiv_class_type:

46953

142 
"[ equiv(A,r); b respects r; X \<in> A//r; !!x. x \<in> A ==> b(x) \<in> B ]

46820

143 
==> (\<Union>x\<in>X. b(x)) \<in> B"

23146

144 
apply (unfold quotient_def, safe)


145 
apply (simp (no_asm_simp) add: UN_equiv_class)


146 
done


147 


148 
(*Sufficient conditions for injectiveness. Could weaken premises!

46953

149 
major premise could be an inclusion; bcong could be !!y. y \<in> A ==> b(y):B

23146

150 
*)


151 
lemma UN_equiv_class_inject:


152 
"[ equiv(A,r); b respects r;

46953

153 
(\<Union>x\<in>X. b(x))=(\<Union>y\<in>Y. b(y)); X \<in> A//r; Y \<in> A//r;


154 
!!x y. [ x \<in> A; y \<in> A; b(x)=b(y) ] ==> <x,y>:r ]

23146

155 
==> X=Y"


156 
apply (unfold quotient_def, safe)


157 
apply (rule equiv_class_eq, assumption)

46820

158 
apply (simp add: UN_equiv_class [of A r b])

23146

159 
done


160 


161 


162 
subsection{*Defining Binary Operations upon Equivalence Classes*}


163 


164 
lemma congruent2_implies_congruent:

46953

165 
"[ equiv(A,r1); congruent2(r1,r2,b); a \<in> A ] ==> congruent(r2,b(a))"

23146

166 
by (unfold congruent_def congruent2_def equiv_def refl_def, blast)


167 


168 
lemma congruent2_implies_congruent_UN:

46953

169 
"[ equiv(A1,r1); equiv(A2,r2); congruent2(r1,r2,b); a \<in> A2 ] ==>

23146

170 
congruent(r1, %x1. \<Union>x2 \<in> r2``{a}. b(x1,x2))"


171 
apply (unfold congruent_def, safe)


172 
apply (frule equiv_type [THEN subsetD], assumption)

46820

173 
apply clarify

23146

174 
apply (simp add: UN_equiv_class congruent2_implies_congruent)


175 
apply (unfold congruent2_def equiv_def refl_def, blast)


176 
done


177 


178 
lemma UN_equiv_class2:


179 
"[ equiv(A1,r1); equiv(A2,r2); congruent2(r1,r2,b); a1: A1; a2: A2 ]


180 
==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. b(x1,x2)) = b(a1,a2)"


181 
by (simp add: UN_equiv_class congruent2_implies_congruent


182 
congruent2_implies_congruent_UN)


183 


184 
(*type checking*)


185 
lemma UN_equiv_class_type2:


186 
"[ equiv(A,r); b respects2 r;


187 
X1: A//r; X2: A//r;

46820

188 
!!x1 x2. [ x1: A; x2: A ] ==> b(x1,x2) \<in> B


189 
] ==> (\<Union>x1\<in>X1. \<Union>x2\<in>X2. b(x1,x2)) \<in> B"

23146

190 
apply (unfold quotient_def, safe)

46820

191 
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN

23146

192 
congruent2_implies_congruent quotientI)


193 
done


194 


195 


196 
(*Suggested by John Harrison  the two subproofs may be MUCH simpler


197 
than the direct proof*)


198 
lemma congruent2I:

46820

199 
"[ equiv(A1,r1); equiv(A2,r2);

23146

200 
!! y z w. [ w \<in> A2; <y,z> \<in> r1 ] ==> b(y,w) = b(z,w);


201 
!! y z w. [ w \<in> A1; <y,z> \<in> r2 ] ==> b(w,y) = b(w,z)


202 
] ==> congruent2(r1,r2,b)"


203 
apply (unfold congruent2_def equiv_def refl_def, safe)

46820

204 
apply (blast intro: trans)

23146

205 
done


206 


207 
lemma congruent2_commuteI:


208 
assumes equivA: "equiv(A,r)"

46953

209 
and commute: "!! y z. [ y \<in> A; z \<in> A ] ==> b(y,z) = b(z,y)"


210 
and congt: "!! y z w. [ w \<in> A; <y,z>: r ] ==> b(w,y) = b(w,z)"

23146

211 
shows "b respects2 r"

46820

212 
apply (insert equivA [THEN equiv_type, THEN subsetD])

23146

213 
apply (rule congruent2I [OF equivA equivA])


214 
apply (rule commute [THEN trans])


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

46820

216 
apply (rule_tac [5] sym)

23146

217 
apply (blast intro: congt)+


218 
done


219 


220 
(*Obsolete?*)


221 
lemma congruent_commuteI:

46953

222 
"[ equiv(A,r); Z \<in> A//r;


223 
!!w. [ w \<in> A ] ==> congruent(r, %z. b(w,z));


224 
!!x y. [ x \<in> A; y \<in> A ] ==> b(y,x) = b(x,y)

46820

225 
] ==> congruent(r, %w. \<Union>z\<in>Z. b(w,z))"

23146

226 
apply (simp (no_asm) add: congruent_def)


227 
apply (safe elim!: quotientE)


228 
apply (frule equiv_type [THEN subsetD], assumption)

46820

229 
apply (simp add: UN_equiv_class [of A r])


230 
apply (simp add: congruent_def)

23146

231 
done


232 


233 
end
