# Theory Equiv_Relations

Up to index of Isabelle/HOL

theory Equiv_Relations
imports Big_Operators
(*  Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1996  University of Cambridge*)header {* Equivalence Relations in Higher-Order Set Theory *}theory Equiv_Relationsimports Big_Operators Relation Plainbeginsubsection {* 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_unfold) blastlemma refl_on_comp_subset: "refl_on A r ==> r ⊆ r¯ O r"  by (unfold refl_on_def) blastlemma 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)+  donetext {* 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  donesubsection {* 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) blasttheorem 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  donelemma equiv_class_self: "equiv A r ==> a ∈ A ==> a ∈ r{a}"  by (unfold equiv_def refl_on_def) blastlemma 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) blastlemma 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) blastlemma equiv_type: "equiv A r ==> r ⊆ A × A"  by (unfold equiv_def refl_on_def) blasttheorem 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 = (\<Union>x ∈ A. {r{x}})"  -- {* set of equiv classes *}lemma quotientI: "x ∈ A ==> r{x} ∈ A//r"  by (unfold quotient_def) blastlemma quotientE:  "X ∈ A//r ==> (!!x. X = r{x} ==> x ∈ A ==> P) ==> P"  by (unfold quotient_def) blastlemma Union_quotient: "equiv A r ==> Union (A//r) = A"  by (unfold equiv_def refl_on_def quotient_def) blastlemma 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  donelemma 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)  donelemma 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)  donelemma 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 blastdonesubsection {* Defining unary operations upon equivalence classes *}text{*A congruence-preserving function*}definition congruent :: "('a × 'a) set => ('a => 'b) => bool"  where  "congruent r f <-> (∀(y, z) ∈ r. f y = f z)"lemma congruentI:  "(!!y z. (y, z) ∈ r ==> f y = f z) ==> congruent r f"  by (auto simp add: congruent_def)lemma congruentD:  "congruent r f ==> (y, z) ∈ r ==> f y = f z"  by (auto 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 ==> (\<Union>y ∈ A. f(y))=c"  -- {* lemma required to prove @{text UN_equiv_class} *}  by autolemma UN_equiv_class:  "equiv A r ==> f respects r ==> a ∈ A    ==> (\<Union>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)  donelemma UN_equiv_class_type:  "equiv A r ==> f respects r ==> X ∈ A//r ==>    (!!x. x ∈ A ==> f x ∈ B) ==> (\<Union>x ∈ X. f x) ∈ B"  apply (unfold quotient_def)  apply clarify  apply (subst UN_equiv_class)     apply auto  donetext {*  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 ==>    (\<Union>x ∈ X. f x) = (\<Union>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)+  donesubsection {* Defining binary operations upon equivalence classes *}text{*A congruence-preserving function of two arguments*}definition congruent2 :: "('a × 'a) set => ('b × 'b) set => ('a => 'b => 'c) => bool" where  "congruent2 r1 r2 f <-> (∀(y1, z1) ∈ r1. ∀(y2, z2) ∈ r2. f y1 y2 = f z1 z2)"lemma congruent2I':  assumes "!!y1 z1 y2 z2. (y1, z1) ∈ r1 ==> (y2, z2) ∈ r2 ==> f y1 y2 = f z1 z2"  shows "congruent2 r1 r2 f"  using assms by (auto simp add: congruent2_def)lemma congruent2D:  "congruent2 r1 r2 f ==> (y1, z1) ∈ r1 ==> (y2, z2) ∈ r2 ==> f y1 y2 = f z1 z2"  using assms by (auto simp add: congruent2_def)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) blastlemma congruent2_implies_congruent_UN:  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a ∈ A2 ==>    congruent r1 (λx1. \<Union>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)  donelemma UN_equiv_class2:  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 ∈ A1 ==> a2 ∈ A2    ==> (\<Union>x1 ∈ r1{a1}. \<Union>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)    ==> (\<Union>x1 ∈ X1. \<Union>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)  donelemma UN_UN_split_split_eq:  "(\<Union>(x1, x2) ∈ X. \<Union>(y1, y2) ∈ Y. A x1 x2 y1 y2) =    (\<Union>x ∈ X. \<Union>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 autolemma 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)  donelemma 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])+  donesubsection {* 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  donelemma 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  donelemma 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)  donelemma 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(fastforce simp add:inj_on_def)apply simpdonesubsection {* 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) (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)qedlemma 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 = Collect (R x)}"  by (auto elim: part_equivpE)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)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!: equivI equivpI [to_set] elim!: equivE equivpE [to_set])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