equal
deleted
inserted
replaced
16 |
16 |
17 lemma EQUIV_REFL_SYM_TRANS: |
17 lemma EQUIV_REFL_SYM_TRANS: |
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 |
|
22 lemma EQUIV_REFL: |
|
23 shows "EQUIV E ==> REFL E" |
|
24 by (simp add: EQUIV_REFL_SYM_TRANS) |
21 |
25 |
22 definition |
26 definition |
23 "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)))" |
24 |
28 |
25 lemma EQUIV_IMP_PART_EQUIV: |
29 lemma EQUIV_IMP_PART_EQUIV: |