equal
deleted
inserted
replaced
18 shows "EQUIV E = (REFL E \<and> SYM E \<and> TRANS E)" |
18 shows "EQUIV E = (REFL E \<and> SYM E \<and> TRANS E)" |
19 unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq |
19 unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq |
20 by (blast) |
20 by (blast) |
21 |
21 |
22 lemma EQUIV_REFL: |
22 lemma EQUIV_REFL: |
23 shows "EQUIV E ==> REFL E" |
23 shows "EQUIV E \<Longrightarrow> (\<And>x. E x x)" |
24 by (simp add: EQUIV_REFL_SYM_TRANS) |
24 by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) |
25 |
25 |
26 definition |
26 definition |
27 "PART_EQUIV 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)))" |
27 "PART_EQUIV 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)))" |
28 |
28 |
29 lemma EQUIV_IMP_PART_EQUIV: |
29 lemma EQUIV_IMP_PART_EQUIV: |