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