equal
deleted
inserted
replaced
28 by (metis equivp_reflp_symp_transp symp_def) |
28 by (metis equivp_reflp_symp_transp symp_def) |
29 |
29 |
30 lemma equivp_transp: |
30 lemma equivp_transp: |
31 shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)" |
31 shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)" |
32 by (metis equivp_reflp_symp_transp transp_def) |
32 by (metis equivp_reflp_symp_transp transp_def) |
|
33 |
|
34 lemma equivpI: |
|
35 assumes "reflp R" "symp R" "transp R" |
|
36 shows "equivp R" |
|
37 using assms by (simp add: equivp_reflp_symp_transp) |
33 |
38 |
34 definition |
39 definition |
35 "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
40 "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
36 |
41 |
37 lemma equivp_IMP_part_equivp: |
42 lemma equivp_IMP_part_equivp: |