1(* Title: HOL/Equiv_Relations.thy 2 Author: Lawrence C Paulson, 1996 Cambridge University Computer Laboratory 3*) 4 5section \<open>Equivalence Relations in Higher-Order Set Theory\<close> 6 7theory Equiv_Relations 8 imports Groups_Big 9begin 10 11subsection \<open>Equivalence relations -- set version\<close> 12 13definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" 14 where "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r" 15 16lemma equivI: "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r" 17 by (simp add: equiv_def) 18 19lemma equivE: 20 assumes "equiv A r" 21 obtains "refl_on A r" and "sym r" and "trans r" 22 using assms by (simp add: equiv_def) 23 24text \<open> 25 Suppes, Theorem 70: \<open>r\<close> is an equiv relation iff \<open>r\<inverse> O r = r\<close>. 26 27 First half: \<open>equiv A r \<Longrightarrow> r\<inverse> O r = r\<close>. 28\<close> 29 30lemma sym_trans_comp_subset: "sym r \<Longrightarrow> trans r \<Longrightarrow> r\<inverse> O r \<subseteq> r" 31 unfolding trans_def sym_def converse_unfold by blast 32 33lemma refl_on_comp_subset: "refl_on A r \<Longrightarrow> r \<subseteq> r\<inverse> O r" 34 unfolding refl_on_def by blast 35 36lemma equiv_comp_eq: "equiv A r \<Longrightarrow> r\<inverse> O r = r" 37 apply (unfold equiv_def) 38 apply clarify 39 apply (rule equalityI) 40 apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+ 41 done 42 43text \<open>Second half.\<close> 44 45lemma comp_equivI: "r\<inverse> O r = r \<Longrightarrow> Domain r = A \<Longrightarrow> equiv A r" 46 apply (unfold equiv_def refl_on_def sym_def trans_def) 47 apply (erule equalityE) 48 apply (subgoal_tac "\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r") 49 apply fast 50 apply fast 51 done 52 53 54subsection \<open>Equivalence classes\<close> 55 56lemma equiv_class_subset: "equiv A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> r``{a} \<subseteq> r``{b}" 57 \<comment> \<open>lemma for the next result\<close> 58 unfolding equiv_def trans_def sym_def by blast 59 60theorem equiv_class_eq: "equiv A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> r``{a} = r``{b}" 61 apply (assumption | rule equalityI equiv_class_subset)+ 62 apply (unfold equiv_def sym_def) 63 apply blast 64 done 65 66lemma equiv_class_self: "equiv A r \<Longrightarrow> a \<in> A \<Longrightarrow> a \<in> r``{a}" 67 unfolding equiv_def refl_on_def by blast 68 69lemma subset_equiv_class: "equiv A r \<Longrightarrow> r``{b} \<subseteq> r``{a} \<Longrightarrow> b \<in> A \<Longrightarrow> (a, b) \<in> r" 70 \<comment> \<open>lemma for the next result\<close> 71 unfolding equiv_def refl_on_def by blast 72 73lemma eq_equiv_class: "r``{a} = r``{b} \<Longrightarrow> equiv A r \<Longrightarrow> b \<in> A \<Longrightarrow> (a, b) \<in> r" 74 by (iprover intro: equalityD2 subset_equiv_class) 75 76lemma equiv_class_nondisjoint: "equiv A r \<Longrightarrow> x \<in> (r``{a} \<inter> r``{b}) \<Longrightarrow> (a, b) \<in> r" 77 unfolding equiv_def trans_def sym_def by blast 78 79lemma equiv_type: "equiv A r \<Longrightarrow> r \<subseteq> A \<times> A" 80 unfolding equiv_def refl_on_def by blast 81 82lemma equiv_class_eq_iff: "equiv A r \<Longrightarrow> (x, y) \<in> r \<longleftrightarrow> r``{x} = r``{y} \<and> x \<in> A \<and> y \<in> A" 83 by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) 84 85lemma eq_equiv_class_iff: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> r``{x} = r``{y} \<longleftrightarrow> (x, y) \<in> r" 86 by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) 87 88 89subsection \<open>Quotients\<close> 90 91definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90) 92 where "A//r = (\<Union>x \<in> A. {r``{x}})" \<comment> \<open>set of equiv classes\<close> 93 94lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r" 95 unfolding quotient_def by blast 96 97lemma quotientE: "X \<in> A//r \<Longrightarrow> (\<And>x. X = r``{x} \<Longrightarrow> x \<in> A \<Longrightarrow> P) \<Longrightarrow> P" 98 unfolding quotient_def by blast 99 100lemma Union_quotient: "equiv A r \<Longrightarrow> \<Union>(A//r) = A" 101 unfolding equiv_def refl_on_def quotient_def by blast 102 103lemma quotient_disj: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> X = Y \<or> X \<inter> Y = {}" 104 apply (unfold quotient_def) 105 apply clarify 106 apply (rule equiv_class_eq) 107 apply assumption 108 apply (unfold equiv_def trans_def sym_def) 109 apply blast 110 done 111 112lemma quotient_eqI: 113 "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> X = Y" 114 apply (clarify elim!: quotientE) 115 apply (rule equiv_class_eq) 116 apply assumption 117 apply (unfold equiv_def sym_def trans_def) 118 apply blast 119 done 120 121lemma quotient_eq_iff: 122 "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> X = Y \<longleftrightarrow> (x, y) \<in> r" 123 apply (rule iffI) 124 prefer 2 125 apply (blast del: equalityI intro: quotient_eqI) 126 apply (clarify elim!: quotientE) 127 apply (unfold equiv_def sym_def trans_def) 128 apply blast 129 done 130 131lemma eq_equiv_class_iff2: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> {x}//r = {y}//r \<longleftrightarrow> (x, y) \<in> r" 132 by (simp add: quotient_def eq_equiv_class_iff) 133 134lemma quotient_empty [simp]: "{}//r = {}" 135 by (simp add: quotient_def) 136 137lemma quotient_is_empty [iff]: "A//r = {} \<longleftrightarrow> A = {}" 138 by (simp add: quotient_def) 139 140lemma quotient_is_empty2 [iff]: "{} = A//r \<longleftrightarrow> A = {}" 141 by (simp add: quotient_def) 142 143lemma singleton_quotient: "{x}//r = {r `` {x}}" 144 by (simp add: quotient_def) 145 146lemma quotient_diff1: "inj_on (\<lambda>a. {a}//r) A \<Longrightarrow> a \<in> A \<Longrightarrow> (A - {a})//r = A//r - {a}//r" 147 unfolding quotient_def inj_on_def by blast 148 149 150subsection \<open>Refinement of one equivalence relation WRT another\<close> 151 152lemma refines_equiv_class_eq: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> R``(S``{a}) = S``{a}" 153 by (auto simp: equiv_class_eq_iff) 154 155lemma refines_equiv_class_eq2: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> S``(R``{a}) = S``{a}" 156 by (auto simp: equiv_class_eq_iff) 157 158lemma refines_equiv_image_eq: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> (\<lambda>X. S``X) ` (A//R) = A//S" 159 by (auto simp: quotient_def image_UN refines_equiv_class_eq2) 160 161lemma finite_refines_finite: 162 "finite (A//R) \<Longrightarrow> R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> finite (A//S)" 163 by (erule finite_surj [where f = "\<lambda>X. S``X"]) (simp add: refines_equiv_image_eq) 164 165lemma finite_refines_card_le: 166 "finite (A//R) \<Longrightarrow> R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> card (A//S) \<le> card (A//R)" 167 by (subst refines_equiv_image_eq [of R S A, symmetric]) 168 (auto simp: card_image_le [where f = "\<lambda>X. S``X"]) 169 170 171subsection \<open>Defining unary operations upon equivalence classes\<close> 172 173text \<open>A congruence-preserving function.\<close> 174 175definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" 176 where "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)" 177 178lemma congruentI: "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f" 179 by (auto simp add: congruent_def) 180 181lemma congruentD: "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z" 182 by (auto simp add: congruent_def) 183 184abbreviation RESPECTS :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infixr "respects" 80) 185 where "f respects r \<equiv> congruent r f" 186 187 188lemma UN_constant_eq: "a \<in> A \<Longrightarrow> \<forall>y \<in> A. f y = c \<Longrightarrow> (\<Union>y \<in> A. f y) = c" 189 \<comment> \<open>lemma required to prove \<open>UN_equiv_class\<close>\<close> 190 by auto 191 192lemma UN_equiv_class: "equiv A r \<Longrightarrow> f respects r \<Longrightarrow> a \<in> A \<Longrightarrow> (\<Union>x \<in> r``{a}. f x) = f a" 193 \<comment> \<open>Conversion rule\<close> 194 apply (rule equiv_class_self [THEN UN_constant_eq]) 195 apply assumption 196 apply assumption 197 apply (unfold equiv_def congruent_def sym_def) 198 apply (blast del: equalityI) 199 done 200 201lemma UN_equiv_class_type: 202 "equiv A r \<Longrightarrow> f respects r \<Longrightarrow> X \<in> A//r \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<Union>x \<in> X. f x) \<in> B" 203 apply (unfold quotient_def) 204 apply clarify 205 apply (subst UN_equiv_class) 206 apply auto 207 done 208 209text \<open> 210 Sufficient conditions for injectiveness. Could weaken premises! 211 major premise could be an inclusion; \<open>bcong\<close> could be 212 \<open>\<And>y. y \<in> A \<Longrightarrow> f y \<in> B\<close>. 213\<close> 214 215lemma UN_equiv_class_inject: 216 "equiv A r \<Longrightarrow> f respects r \<Longrightarrow> 217 (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) \<Longrightarrow> X \<in> A//r ==> Y \<in> A//r 218 \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<Longrightarrow> (x, y) \<in> r) 219 \<Longrightarrow> X = Y" 220 apply (unfold quotient_def) 221 apply clarify 222 apply (rule equiv_class_eq) 223 apply assumption 224 apply (subgoal_tac "f x = f xa") 225 apply blast 226 apply (erule box_equals) 227 apply (assumption | rule UN_equiv_class)+ 228 done 229 230 231subsection \<open>Defining binary operations upon equivalence classes\<close> 232 233text \<open>A congruence-preserving function of two arguments.\<close> 234 235definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool" 236 where "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)" 237 238lemma congruent2I': 239 assumes "\<And>y1 z1 y2 z2. (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2" 240 shows "congruent2 r1 r2 f" 241 using assms by (auto simp add: congruent2_def) 242 243lemma congruent2D: "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2" 244 by (auto simp add: congruent2_def) 245 246text \<open>Abbreviation for the common case where the relations are identical.\<close> 247abbreviation RESPECTS2:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infixr "respects2" 80) 248 where "f respects2 r \<equiv> congruent2 r r f" 249 250 251lemma congruent2_implies_congruent: 252 "equiv A r1 \<Longrightarrow> congruent2 r1 r2 f \<Longrightarrow> a \<in> A \<Longrightarrow> congruent r2 (f a)" 253 unfolding congruent_def congruent2_def equiv_def refl_on_def by blast 254 255lemma congruent2_implies_congruent_UN: 256 "equiv A1 r1 \<Longrightarrow> equiv A2 r2 \<Longrightarrow> congruent2 r1 r2 f \<Longrightarrow> a \<in> A2 \<Longrightarrow> 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) 262 apply (unfold congruent2_def equiv_def refl_on_def) 263 apply (blast del: equalityI) 264 done 265 266lemma UN_equiv_class2: 267 "equiv A1 r1 \<Longrightarrow> equiv A2 r2 \<Longrightarrow> congruent2 r1 r2 f \<Longrightarrow> a1 \<in> A1 \<Longrightarrow> a2 \<in> A2 \<Longrightarrow> 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 congruent2_implies_congruent_UN) 270 271lemma UN_equiv_class_type2: 272 "equiv A1 r1 \<Longrightarrow> equiv A2 r2 \<Longrightarrow> congruent2 r1 r2 f 273 \<Longrightarrow> X1 \<in> A1//r1 \<Longrightarrow> X2 \<in> A2//r2 274 \<Longrightarrow> (\<And>x1 x2. x1 \<in> A1 \<Longrightarrow> x2 \<in> A2 \<Longrightarrow> f x1 x2 \<in> B) 275 \<Longrightarrow> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B" 276 apply (unfold quotient_def) 277 apply clarify 278 apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 279 congruent2_implies_congruent quotientI) 280 done 281 282lemma UN_UN_split_split_eq: 283 "(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) = 284 (\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)" 285 \<comment> \<open>Allows a natural expression of binary operators,\<close> 286 \<comment> \<open>without explicit calls to \<open>split\<close>\<close> 287 by auto 288 289lemma congruent2I: 290 "equiv A1 r1 \<Longrightarrow> equiv A2 r2 291 \<Longrightarrow> (\<And>y z w. w \<in> A2 \<Longrightarrow> (y,z) \<in> r1 \<Longrightarrow> f y w = f z w) 292 \<Longrightarrow> (\<And>y z w. w \<in> A1 \<Longrightarrow> (y,z) \<in> r2 \<Longrightarrow> f w y = f w z) 293 \<Longrightarrow> congruent2 r1 r2 f" 294 \<comment> \<open>Suggested by John Harrison -- the two subproofs may be\<close> 295 \<comment> \<open>\<^emph>\<open>much\<close> simpler than the direct proof.\<close> 296 apply (unfold congruent2_def equiv_def refl_on_def) 297 apply clarify 298 apply (blast intro: trans) 299 done 300 301lemma congruent2_commuteI: 302 assumes equivA: "equiv A r" 303 and commute: "\<And>y z. y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> f y z = f z y" 304 and congt: "\<And>y z w. w \<in> A \<Longrightarrow> (y,z) \<in> r \<Longrightarrow> f w y = f w z" 305 shows "f respects2 r" 306 apply (rule congruent2I [OF equivA equivA]) 307 apply (rule commute [THEN trans]) 308 apply (rule_tac [3] commute [THEN trans, symmetric]) 309 apply (rule_tac [5] sym) 310 apply (rule congt | assumption | 311 erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ 312 done 313 314 315subsection \<open>Quotients and finiteness\<close> 316 317text \<open>Suggested by Florian Kamm��ller\<close> 318 319lemma finite_quotient: "finite A \<Longrightarrow> r \<subseteq> A \<times> A \<Longrightarrow> finite (A//r)" 320 \<comment> \<open>recall @{thm equiv_type}\<close> 321 apply (rule finite_subset) 322 apply (erule_tac [2] finite_Pow_iff [THEN iffD2]) 323 apply (unfold quotient_def) 324 apply blast 325 done 326 327lemma finite_equiv_class: "finite A \<Longrightarrow> r \<subseteq> A \<times> A \<Longrightarrow> X \<in> A//r \<Longrightarrow> finite X" 328 apply (unfold quotient_def) 329 apply (rule finite_subset) 330 prefer 2 apply assumption 331 apply blast 332 done 333 334lemma equiv_imp_dvd_card: "finite A \<Longrightarrow> equiv A r \<Longrightarrow> \<forall>X \<in> A//r. k dvd card X \<Longrightarrow> k dvd card A" 335 apply (rule Union_quotient [THEN subst [where P="\<lambda>A. k dvd card A"]]) 336 apply assumption 337 apply (rule dvd_partition) 338 prefer 3 apply (blast dest: quotient_disj) 339 apply (simp_all add: Union_quotient equiv_type) 340 done 341 342lemma card_quotient_disjoint: "finite A \<Longrightarrow> inj_on (\<lambda>x. {x} // r) A \<Longrightarrow> card (A//r) = card A" 343 apply (simp add:quotient_def) 344 apply (subst card_UN_disjoint) 345 apply assumption 346 apply simp 347 apply (fastforce simp add:inj_on_def) 348 apply simp 349 done 350 351 352subsection \<open>Projection\<close> 353 354definition proj :: "('b \<times> 'a) set \<Rightarrow> 'b \<Rightarrow> 'a set" 355 where "proj r x = r `` {x}" 356 357lemma proj_preserves: "x \<in> A \<Longrightarrow> proj r x \<in> A//r" 358 unfolding proj_def by (rule quotientI) 359 360lemma proj_in_iff: 361 assumes "equiv A r" 362 shows "proj r x \<in> A//r \<longleftrightarrow> x \<in> A" 363 (is "?lhs \<longleftrightarrow> ?rhs") 364proof 365 assume ?rhs 366 then show ?lhs by (simp add: proj_preserves) 367next 368 assume ?lhs 369 then show ?rhs 370 unfolding proj_def quotient_def 371 proof clarsimp 372 fix y 373 assume y: "y \<in> A" and "r `` {x} = r `` {y}" 374 moreover have "y \<in> r `` {y}" 375 using assms y unfolding equiv_def refl_on_def by blast 376 ultimately have "(x, y) \<in> r" by blast 377 then show "x \<in> A" 378 using assms unfolding equiv_def refl_on_def by blast 379 qed 380qed 381 382lemma proj_iff: "equiv A r \<Longrightarrow> {x, y} \<subseteq> A \<Longrightarrow> proj r x = proj r y \<longleftrightarrow> (x, y) \<in> r" 383 by (simp add: proj_def eq_equiv_class_iff) 384 385(* 386lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x" 387unfolding proj_def equiv_def refl_on_def by blast 388*) 389 390lemma proj_image: "proj r ` A = A//r" 391 unfolding proj_def[abs_def] quotient_def by blast 392 393lemma in_quotient_imp_non_empty: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> X \<noteq> {}" 394 unfolding quotient_def using equiv_class_self by fast 395 396lemma in_quotient_imp_in_rel: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> {x, y} \<subseteq> X \<Longrightarrow> (x, y) \<in> r" 397 using quotient_eq_iff[THEN iffD1] by fastforce 398 399lemma in_quotient_imp_closed: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> x \<in> X \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> X" 400 unfolding quotient_def equiv_def trans_def by blast 401 402lemma in_quotient_imp_subset: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> X \<subseteq> A" 403 using in_quotient_imp_in_rel equiv_type by fastforce 404 405 406subsection \<open>Equivalence relations -- predicate version\<close> 407 408text \<open>Partial equivalences.\<close> 409 410definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 411 where "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)" 412 \<comment> \<open>John-Harrison-style characterization\<close> 413 414lemma part_equivpI: "\<exists>x. R x x \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R" 415 by (auto simp add: part_equivp_def) (auto elim: sympE transpE) 416 417lemma part_equivpE: 418 assumes "part_equivp R" 419 obtains x where "R x x" and "symp R" and "transp R" 420proof - 421 from assms have 1: "\<exists>x. R x x" 422 and 2: "\<And>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y" 423 unfolding part_equivp_def by blast+ 424 from 1 obtain x where "R x x" .. 425 moreover have "symp R" 426 proof (rule sympI) 427 fix x y 428 assume "R x y" 429 with 2 [of x y] show "R y x" by auto 430 qed 431 moreover have "transp R" 432 proof (rule transpI) 433 fix x y z 434 assume "R x y" and "R y z" 435 with 2 [of x y] 2 [of y z] show "R x z" by auto 436 qed 437 ultimately show thesis by (rule that) 438qed 439 440lemma part_equivp_refl_symp_transp: "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> symp R \<and> transp R" 441 by (auto intro: part_equivpI elim: part_equivpE) 442 443lemma part_equivp_symp: "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x" 444 by (erule part_equivpE, erule sympE) 445 446lemma part_equivp_transp: "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" 447 by (erule part_equivpE, erule transpE) 448 449lemma part_equivp_typedef: "part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}" 450 by (auto elim: part_equivpE) 451 452 453text \<open>Total equivalences.\<close> 454 455definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 456 where "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" \<comment> \<open>John-Harrison-style characterization\<close> 457 458lemma equivpI: "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R" 459 by (auto elim: reflpE sympE transpE simp add: equivp_def) 460 461lemma equivpE: 462 assumes "equivp R" 463 obtains "reflp R" and "symp R" and "transp R" 464 using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def) 465 466lemma equivp_implies_part_equivp: "equivp R \<Longrightarrow> part_equivp R" 467 by (auto intro: part_equivpI elim: equivpE reflpE) 468 469lemma equivp_equiv: "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)" 470 by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set]) 471 472lemma equivp_reflp_symp_transp: "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R" 473 by (auto intro: equivpI elim: equivpE) 474 475lemma identity_equivp: "equivp (=)" 476 by (auto intro: equivpI reflpI sympI transpI) 477 478lemma equivp_reflp: "equivp R \<Longrightarrow> R x x" 479 by (erule equivpE, erule reflpE) 480 481lemma equivp_symp: "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x" 482 by (erule equivpE, erule sympE) 483 484lemma equivp_transp: "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" 485 by (erule equivpE, erule transpE) 486 487hide_const (open) proj 488 489end 490