equal
deleted
inserted
replaced
500 and b: "Respects (R1 ===> R2) g" |
500 and b: "Respects (R1 ===> R2) g" |
501 shows "Respects (R1 ===> R3) (f o g)" |
501 shows "Respects (R1 ===> R3) (f o g)" |
502 using a b unfolding Respects_def |
502 using a b unfolding Respects_def |
503 by simp |
503 by simp |
504 |
504 |
|
505 lemma abs_o_rep: |
|
506 assumes a: "Quotient r absf repf" |
|
507 shows "absf o repf = id" |
|
508 apply(rule ext) |
|
509 apply(simp add: Quotient_abs_rep[OF a]) |
|
510 done |
|
511 |
505 lemma fun_rel_eq_rel: |
512 lemma fun_rel_eq_rel: |
506 assumes q1: "Quotient R1 Abs1 Rep1" |
513 assumes q1: "Quotient R1 Abs1 Rep1" |
507 and q2: "Quotient R2 Abs2 Rep2" |
514 and q2: "Quotient R2 Abs2 Rep2" |
508 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
515 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
509 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
516 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |