# HG changeset patch # User haftmann # Date 1291029283 -3600 # Node ID ff16e22e8776b5ba09baa18ef3b68bf242c0cb09 # Parent 330eb65c9469f06c51fa40cb886e4f388fd75914 moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; more natural deduction rules; replaced slightly odd locale equiv by plain definition diff -r 330eb65c9469 -r ff16e22e8776 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Sun Nov 28 21:07:28 2010 +0100 +++ b/src/HOL/Equiv_Relations.thy Mon Nov 29 12:14:43 2010 +0100 @@ -8,13 +8,10 @@ imports Big_Operators Relation Plain begin -subsection {* Equivalence relations *} +subsection {* Equivalence relations -- set version *} -locale equiv = - fixes A and r - assumes refl_on: "refl_on A r" - and sym: "sym r" - and trans: "trans r" +definition equiv :: "'a set \ ('a \ 'a) set \ bool" where + "equiv A r \ refl_on A r \ sym r \ trans r" text {* Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\ O @@ -331,4 +328,99 @@ 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