equal
deleted
inserted
replaced
507 shows "absf o repf = id" |
507 shows "absf o repf = id" |
508 apply(rule ext) |
508 apply(rule ext) |
509 apply(simp add: Quotient_abs_rep[OF a]) |
509 apply(simp add: Quotient_abs_rep[OF a]) |
510 done |
510 done |
511 |
511 |
|
512 lemma eq_comp_r: "op = OO R OO op = \<equiv> R" |
|
513 apply (rule eq_reflection) |
|
514 apply (rule ext)+ |
|
515 apply auto |
|
516 done |
|
517 |
512 lemma fun_rel_eq_rel: |
518 lemma fun_rel_eq_rel: |
513 assumes q1: "Quotient R1 Abs1 Rep1" |
519 assumes q1: "Quotient R1 Abs1 Rep1" |
514 and q2: "Quotient R2 Abs2 Rep2" |
520 and q2: "Quotient R2 Abs2 Rep2" |
515 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
521 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
516 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
522 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |