(* Authors: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) header {* Equivalence Relations in Higher-Order Set Theory *} theory Equiv_Relations imports Big_Operators Relation Plain begin subsection {* Equivalence relations -- set version *} definition equiv :: "'a set \ ('a \ 'a) set \ bool" where "equiv A r \ refl_on A r \ sym r \ trans r" lemma equivI: "refl_on A r \ sym r \ trans r \ equiv A r" by (simp add: equiv_def) lemma equivE: assumes "equiv A r" obtains "refl_on A r" and "sym r" and "trans r" using assms by (simp add: equiv_def) text {* Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\ O r = r"}. First half: @{text "equiv A r ==> r\ O r = r"}. *} lemma sym_trans_comp_subset: "sym r ==> trans r ==> r\ O r \ r" by (unfold trans_def sym_def converse_def) blast lemma refl_on_comp_subset: "refl_on A r ==> r \ r\ O r" by (unfold refl_on_def) blast lemma equiv_comp_eq: "equiv A r ==> r\ O r = r" apply (unfold equiv_def) apply clarify apply (rule equalityI) apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+ done text {* Second half. *} lemma comp_equivI: "r\ O r = r ==> Domain r = A ==> equiv A r" apply (unfold equiv_def refl_on_def sym_def trans_def) apply (erule equalityE) apply (subgoal_tac "\x y. (x, y) \ r --> (y, x) \ r") apply fast apply fast done subsection {* Equivalence classes *} lemma equiv_class_subset: "equiv A r ==> (a, b) \ r ==> r``{a} \ r``{b}" -- {* lemma for the next result *} by (unfold equiv_def trans_def sym_def) blast theorem equiv_class_eq: "equiv A r ==> (a, b) \ r ==> r``{a} = r``{b}" apply (assumption | rule equalityI equiv_class_subset)+ apply (unfold equiv_def sym_def) apply blast done lemma equiv_class_self: "equiv A r ==> a \ A ==> a \ r``{a}" by (unfold equiv_def refl_on_def) blast lemma subset_equiv_class: "equiv A r ==> r``{b} \ r``{a} ==> b \ A ==> (a,b) \ r" -- {* lemma for the next result *} by (unfold equiv_def refl_on_def) blast lemma eq_equiv_class: "r``{a} = r``{b} ==> equiv A r ==> b \ A ==> (a, b) \ r" by (iprover intro: equalityD2 subset_equiv_class) lemma equiv_class_nondisjoint: "equiv A r ==> x \ (r``{a} \ r``{b}) ==> (a, b) \ r" by (unfold equiv_def trans_def sym_def) blast lemma equiv_type: "equiv A r ==> r \ A \ A" by (unfold equiv_def refl_on_def) blast theorem equiv_class_eq_iff: "equiv A r ==> ((x, y) \ r) = (r``{x} = r``{y} & x \ A & y \ A)" by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) theorem eq_equiv_class_iff: "equiv A r ==> x \ A ==> y \ A ==> (r``{x} = r``{y}) = ((x, y) \ r)" by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) subsection {* Quotients *} definition quotient :: "'a set \ ('a \ 'a) set \ 'a set set" (infixl "'/'/" 90) where "A//r = (\x \ A. {r``{x}})" -- {* set of equiv classes *} lemma quotientI: "x \ A ==> r``{x} \ A//r" by (unfold quotient_def) blast lemma quotientE: "X \ A//r ==> (!!x. X = r``{x} ==> x \ A ==> P) ==> P" by (unfold quotient_def) blast lemma Union_quotient: "equiv A r ==> Union (A//r) = A" by (unfold equiv_def refl_on_def quotient_def) blast lemma quotient_disj: "equiv A r ==> X \ A//r ==> Y \ A//r ==> X = Y | (X \ Y = {})" apply (unfold quotient_def) apply clarify apply (rule equiv_class_eq) apply assumption apply (unfold equiv_def trans_def sym_def) apply blast done lemma quotient_eqI: "[|equiv A r; X \ A//r; Y \ A//r; x \ X; y \ Y; (x,y) \ r|] ==> X = Y" apply (clarify elim!: quotientE) apply (rule equiv_class_eq, assumption) apply (unfold equiv_def sym_def trans_def, blast) done lemma quotient_eq_iff: "[|equiv A r; X \ A//r; Y \ A//r; x \ X; y \ Y|] ==> (X = Y) = ((x,y) \ r)" apply (rule iffI) prefer 2 apply (blast del: equalityI intro: quotient_eqI) apply (clarify elim!: quotientE) apply (unfold equiv_def sym_def trans_def, blast) done lemma eq_equiv_class_iff2: "\ equiv A r; x \ A; y \ A \ \ ({x}//r = {y}//r) = ((x,y) : r)" by(simp add:quotient_def eq_equiv_class_iff) lemma quotient_empty [simp]: "{}//r = {}" by(simp add: quotient_def) lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})" by(simp add: quotient_def) lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})" by(simp add: quotient_def) lemma singleton_quotient: "{x}//r = {r `` {x}}" by(simp add:quotient_def) lemma quotient_diff1: "\ inj_on (%a. {a}//r) A; a \ A \ \ (A - {a})//r = A//r - {a}//r" apply(simp add:quotient_def inj_on_def) apply blast done subsection {* Defining unary operations upon equivalence classes *} text{*A congruence-preserving function*} definition congruent where "congruent r f \ (\y z. (y, z) \ r \ f y = f z)" lemma congruentI: "(\y z. (y, z) \ r \ f y = f z) \ congruent r f" by (simp add: congruent_def) lemma congruentD: "congruent r f \ (y, z) \ r \ f y = f z" by (simp add: congruent_def) abbreviation RESPECTS :: "('a => 'b) => ('a * 'a) set => bool" (infixr "respects" 80) where "f respects r == congruent r f" lemma UN_constant_eq: "a \ A ==> \y \ A. f y = c ==> (\y \ A. f(y))=c" -- {* lemma required to prove @{text UN_equiv_class} *} by auto lemma UN_equiv_class: "equiv A r ==> f respects r ==> a \ A ==> (\x \ r``{a}. f x) = f a" -- {* Conversion rule *} apply (rule equiv_class_self [THEN UN_constant_eq], assumption+) apply (unfold equiv_def congruent_def sym_def) apply (blast del: equalityI) done lemma UN_equiv_class_type: "equiv A r ==> f respects r ==> X \ A//r ==> (!!x. x \ A ==> f x \ B) ==> (\x \ X. f x) \ B" apply (unfold quotient_def) apply clarify apply (subst UN_equiv_class) apply auto done text {* Sufficient conditions for injectiveness. Could weaken premises! major premise could be an inclusion; bcong could be @{text "!!y. y \ A ==> f y \ B"}. *} lemma UN_equiv_class_inject: "equiv A r ==> f respects r ==> (\x \ X. f x) = (\y \ Y. f y) ==> X \ A//r ==> Y \ A//r ==> (!!x y. x \ A ==> y \ A ==> f x = f y ==> (x, y) \ r) ==> X = Y" apply (unfold quotient_def) apply clarify apply (rule equiv_class_eq) apply assumption apply (subgoal_tac "f x = f xa") apply blast apply (erule box_equals) apply (assumption | rule UN_equiv_class)+ done subsection {* Defining binary operations upon equivalence classes *} text{*A congruence-preserving function of two arguments*} locale congruent2 = fixes r1 and r2 and f assumes congruent2: "(y1,z1) \ r1 ==> (y2,z2) \ r2 ==> f y1 y2 = f z1 z2" text{*Abbreviation for the common case where the relations are identical*} abbreviation RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool" (infixr "respects2" 80) where "f respects2 r == congruent2 r r f" lemma congruent2_implies_congruent: "equiv A r1 ==> congruent2 r1 r2 f ==> a \ A ==> congruent r2 (f a)" by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast lemma congruent2_implies_congruent_UN: "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \ A2 ==> congruent r1 (\x1. \x2 \ r2``{a}. f x1 x2)" apply (unfold congruent_def) apply clarify apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+) apply (simp add: UN_equiv_class congruent2_implies_congruent) apply (unfold congruent2_def equiv_def refl_on_def) apply (blast del: equalityI) done lemma UN_equiv_class2: "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \ A1 ==> a2 \ A2 ==> (\x1 \ r1``{a1}. \x2 \ r2``{a2}. f x1 x2) = f a1 a2" by (simp add: UN_equiv_class congruent2_implies_congruent congruent2_implies_congruent_UN) lemma UN_equiv_class_type2: "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> X1 \ A1//r1 ==> X2 \ A2//r2 ==> (!!x1 x2. x1 \ A1 ==> x2 \ A2 ==> f x1 x2 \ B) ==> (\x1 \ X1. \x2 \ X2. f x1 x2) \ B" apply (unfold quotient_def) apply clarify apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN congruent2_implies_congruent quotientI) done lemma UN_UN_split_split_eq: "(\(x1, x2) \ X. \(y1, y2) \ Y. A x1 x2 y1 y2) = (\x \ X. \y \ Y. (\(x1, x2). (\(y1, y2). A x1 x2 y1 y2) y) x)" -- {* Allows a natural expression of binary operators, *} -- {* without explicit calls to @{text split} *} by auto lemma congruent2I: "equiv A1 r1 ==> equiv A2 r2 ==> (!!y z w. w \ A2 ==> (y,z) \ r1 ==> f y w = f z w) ==> (!!y z w. w \ A1 ==> (y,z) \ r2 ==> f w y = f w z) ==> congruent2 r1 r2 f" -- {* Suggested by John Harrison -- the two subproofs may be *} -- {* \emph{much} simpler than the direct proof. *} apply (unfold congruent2_def equiv_def refl_on_def) apply clarify apply (blast intro: trans) done lemma congruent2_commuteI: assumes equivA: "equiv A r" and commute: "!!y z. y \ A ==> z \ A ==> f y z = f z y" and congt: "!!y z w. w \ A ==> (y,z) \ r ==> f w y = f w z" shows "f respects2 r" apply (rule congruent2I [OF equivA equivA]) apply (rule commute [THEN trans]) apply (rule_tac [3] commute [THEN trans, symmetric]) apply (rule_tac [5] sym) apply (rule congt | assumption | erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ done subsection {* Quotients and finiteness *} text {*Suggested by Florian Kammüller*} lemma finite_quotient: "finite A ==> r \ A \ A ==> finite (A//r)" -- {* recall @{thm equiv_type} *} apply (rule finite_subset) apply (erule_tac [2] finite_Pow_iff [THEN iffD2]) apply (unfold quotient_def) apply blast done lemma finite_equiv_class: "finite A ==> r \ A \ A ==> X \ A//r ==> finite X" apply (unfold quotient_def) apply (rule finite_subset) prefer 2 apply assumption apply blast done lemma equiv_imp_dvd_card: "finite A ==> equiv A r ==> \X \ A//r. k dvd card X ==> k dvd card A" apply (rule Union_quotient [THEN subst [where P="\A. k dvd card A"]]) apply assumption apply (rule dvd_partition) prefer 3 apply (blast dest: quotient_disj) apply (simp_all add: Union_quotient equiv_type) done lemma card_quotient_disjoint: "\ finite A; inj_on (\x. {x} // r) A \ \ card(A//r) = card A" apply(simp add:quotient_def) apply(subst card_UN_disjoint) apply assumption apply simp apply(fastsimp simp add:inj_on_def) apply simp done subsection {* Equivalence relations -- predicate version *} text {* Partial equivalences *} definition part_equivp :: "('a \ 'a \ bool) \ bool" where "part_equivp R \ (\x. R x x) \ (\x y. R x y \ R x x \ R y y \ R x = R y)" -- {* John-Harrison-style characterization *} lemma part_equivpI: "(\x. R x x) \ symp R \ transp R \ part_equivp R" by (auto simp add: part_equivp_def mem_def) (auto elim: sympE transpE) lemma part_equivpE: assumes "part_equivp R" obtains x where "R x x" and "symp R" and "transp R" proof - from assms have 1: "\x. R x x" and 2: "\x y. R x y \ R x x \ R y y \ R x = R y" by (unfold part_equivp_def) blast+ from 1 obtain x where "R x x" .. moreover have "symp R" proof (rule sympI) fix x y assume "R x y" with 2 [of x y] show "R y x" by auto qed moreover have "transp R" proof (rule transpI) fix x y z assume "R x y" and "R y z" with 2 [of x y] 2 [of y z] show "R x z" by auto qed ultimately show thesis by (rule that) qed lemma part_equivp_refl_symp_transp: "part_equivp R \ (\x. R x x) \ symp R \ transp R" by (auto intro: part_equivpI elim: part_equivpE) lemma part_equivp_symp: "part_equivp R \ R x y \ R y x" by (erule part_equivpE, erule sympE) lemma part_equivp_transp: "part_equivp R \ R x y \ R y z \ R x z" by (erule part_equivpE, erule transpE) lemma part_equivp_typedef: "part_equivp R \ \d. d \ (\c. \x. R x x \ c = R x)" by (auto elim: part_equivpE simp add: mem_def) text {* Total equivalences *} definition equivp :: "('a \ 'a \ bool) \ bool" where "equivp R \ (\x y. R x y = (R x = R y))" -- {* John-Harrison-style characterization *} lemma equivpI: "reflp R \ symp R \ transp R \ equivp R" by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def) lemma equivpE: assumes "equivp R" obtains "reflp R" and "symp R" and "transp R" using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def) lemma equivp_implies_part_equivp: "equivp R \ part_equivp R" by (auto intro: part_equivpI elim: equivpE reflpE) lemma equivp_equiv: "equiv UNIV A \ equivp (\x y. (x, y) \ A)" by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def) lemma equivp_reflp_symp_transp: shows "equivp R \ reflp R \ symp R \ transp R" by (auto intro: equivpI elim: equivpE) lemma identity_equivp: "equivp (op =)" by (auto intro: equivpI reflpI sympI transpI) lemma equivp_reflp: "equivp R \ R x x" by (erule equivpE, erule reflpE) lemma equivp_symp: "equivp R \ R x y \ R y x" by (erule equivpE, erule sympE) lemma equivp_transp: "equivp R \ R x y \ R y z \ R x z" by (erule equivpE, erule transpE) end