equal
deleted
inserted
replaced
348 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
348 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
349 apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
349 apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
350 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
350 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
351 done |
351 done |
352 |
352 |
|
353 lemma babs_simp: |
|
354 assumes q: "Quotient R1 Abs Rep" |
|
355 shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" |
|
356 apply(rule iffI) |
|
357 apply(simp_all only: babs_rsp[OF q]) |
|
358 apply(auto simp add: Babs_def) |
|
359 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
|
360 apply(metis Babs_def) |
|
361 apply (simp add: in_respects) |
|
362 using Quotient_rel[OF q] |
|
363 by metis |
|
364 |
|
365 |
353 (* needed for regularising? *) |
366 (* needed for regularising? *) |
354 lemma babs_reg_eqv: |
367 lemma babs_reg_eqv: |
355 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
368 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
356 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
369 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
357 |
370 |