equal
deleted
inserted
replaced
17 lemma equivp_reflp_symp_transp: |
17 lemma equivp_reflp_symp_transp: |
18 shows "equivp E = (reflp E \<and> symp E \<and> transp E)" |
18 shows "equivp E = (reflp E \<and> symp E \<and> transp E)" |
19 unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq |
19 unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq |
20 by (blast) |
20 by (blast) |
21 |
21 |
22 lemma equivp_refl: |
|
23 shows "equivp R \<Longrightarrow> (\<And>x. R x x)" |
|
24 by (simp add: equivp_reflp_symp_transp reflp_def) |
|
25 |
|
26 lemma equivp_reflp: |
22 lemma equivp_reflp: |
27 shows "equivp E \<Longrightarrow> (\<And>x. E x x)" |
23 shows "equivp E \<Longrightarrow> (\<And>x. E x x)" |
28 by (simp add: equivp_reflp_symp_transp reflp_def) |
24 by (simp only: equivp_reflp_symp_transp reflp_def) |
|
25 |
|
26 lemma equivp_symp: |
|
27 shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)" |
|
28 by (metis equivp_reflp_symp_transp symp_def) |
|
29 |
|
30 lemma equivp_transp: |
|
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) |
29 |
33 |
30 definition |
34 definition |
31 "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)))" |
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)))" |
32 |
36 |
33 lemma equivp_IMP_part_equivp: |
37 lemma equivp_IMP_part_equivp: |
91 lemma Quotient_transp: |
95 lemma Quotient_transp: |
92 assumes a: "Quotient E Abs Rep" |
96 assumes a: "Quotient E Abs Rep" |
93 shows "transp E" |
97 shows "transp E" |
94 using a unfolding Quotient_def transp_def |
98 using a unfolding Quotient_def transp_def |
95 by metis |
99 by metis |
96 |
|
97 fun |
|
98 prod_rel |
|
99 where |
|
100 "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)" |
|
101 |
100 |
102 fun |
101 fun |
103 fun_map |
102 fun_map |
104 where |
103 where |
105 "fun_map f g h x = g (h (f x))" |
104 "fun_map f g h x = g (h (f x))" |