equal
deleted
inserted
replaced
393 by metis |
393 by metis |
394 |
394 |
395 lemma babs_prs: |
395 lemma babs_prs: |
396 assumes q1: "Quotient R1 Abs1 Rep1" |
396 assumes q1: "Quotient R1 Abs1 Rep1" |
397 and q2: "Quotient R2 Abs2 Rep2" |
397 and q2: "Quotient R2 Abs2 Rep2" |
398 shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f" |
398 shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" |
399 apply(rule eq_reflection) |
399 apply (rule ext) |
400 apply(rule ext) |
400 apply (simp) |
401 apply simp |
|
402 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
401 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
403 apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
402 apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
404 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
403 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
405 done |
404 done |
406 |
405 |