# HG changeset patch # User Cezary Kaliszyk # Date 1287456282 -32400 # Node ID 2671cce4d25d4a872efa8348186276067db15656 # Parent 9f8dcf6ef563270e4c06d3373acd7576c98bed0d Quotient package: partial equivalence introduction diff -r 9f8dcf6ef563 -r 2671cce4d25d src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Mon Oct 18 14:25:15 2010 +0100 +++ b/src/HOL/Quotient.thy Tue Oct 19 11:44:42 2010 +0900 @@ -88,6 +88,32 @@ apply (rule refl) done +lemma part_equivp_refl_symp_transp: + shows "part_equivp E \ ((\x. E x x) \ symp E \ transp E)" +proof + assume "part_equivp E" + then show "(\x. E x x) \ symp E \ transp E" + unfolding part_equivp_def symp_def transp_def + by metis +next + assume a: "(\x. E x x) \ symp E \ transp E" + then have b: "(\x y. E x y \ E y x)" and c: "(\x y z. E x y \ E y z \ E x z)" + unfolding symp_def transp_def by (metis, metis) + have "(\x y. E x y = (E x x \ E y y \ E x = E y))" + proof (intro allI iffI conjI) + fix x y + assume d: "E x y" + then show "E x x" using b c by metis + show "E y y" using b c d by metis + show "E x = E y" unfolding fun_eq_iff using b c d by metis + next + fix x y + assume "E x x \ E y y \ E x = E y" + then show "E x y" using b c by metis + qed + then show "part_equivp E" unfolding part_equivp_def using a by metis +qed + text {* Composition of Relations *} abbreviation