src/HOL/Quotient.thy
 changeset 40031 2671cce4d25d parent 39956 132b79985660 child 40466 c6587375088e
```     1.1 --- a/src/HOL/Quotient.thy	Mon Oct 18 14:25:15 2010 +0100
1.2 +++ b/src/HOL/Quotient.thy	Tue Oct 19 11:44:42 2010 +0900
1.3 @@ -88,6 +88,32 @@
1.4    apply (rule refl)
1.5    done
1.6
1.7 +lemma part_equivp_refl_symp_transp:
1.8 +  shows "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> symp E \<and> transp E)"
1.9 +proof
1.10 +  assume "part_equivp E"
1.11 +  then show "(\<exists>x. E x x) \<and> symp E \<and> transp E"
1.12 +  unfolding part_equivp_def symp_def transp_def
1.13 +  by metis
1.14 +next
1.15 +  assume a: "(\<exists>x. E x x) \<and> symp E \<and> transp E"
1.16 +  then have b: "(\<forall>x y. E x y \<longrightarrow> E y x)" and c: "(\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
1.17 +    unfolding symp_def transp_def by (metis, metis)
1.18 +  have "(\<forall>x y. E x y = (E x x \<and> E y y \<and> E x = E y))"
1.19 +  proof (intro allI iffI conjI)
1.20 +    fix x y
1.21 +    assume d: "E x y"
1.22 +    then show "E x x" using b c by metis
1.23 +    show "E y y" using b c d by metis
1.24 +    show "E x = E y" unfolding fun_eq_iff using b c d by metis
1.25 +  next
1.26 +    fix x y
1.27 +    assume "E x x \<and> E y y \<and> E x = E y"
1.28 +    then show "E x y" using b c by metis
1.29 +  qed
1.30 +  then show "part_equivp E" unfolding part_equivp_def using a by metis
1.31 +qed
1.32 +
1.33  text {* Composition of Relations *}
1.34
1.35  abbreviation
```