equal
deleted
inserted
replaced
41 (\<forall>a. E (Rep a) (Rep a)) \<and> |
41 (\<forall>a. E (Rep a) (Rep a)) \<and> |
42 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
42 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
43 |
43 |
44 lemma Quotient_abs_rep: |
44 lemma Quotient_abs_rep: |
45 assumes a: "Quotient E Abs Rep" |
45 assumes a: "Quotient E Abs Rep" |
46 shows "Abs (Rep a) = a" |
46 shows "Abs (Rep a) \<equiv> a" |
47 using a unfolding Quotient_def |
47 using a unfolding Quotient_def |
48 by simp |
48 by simp |
49 |
49 |
50 lemma Quotient_rep_reflp: |
50 lemma Quotient_rep_reflp: |
51 assumes a: "Quotient E Abs Rep" |
51 assumes a: "Quotient E Abs Rep" |