equal
deleted
inserted
replaced
336 using a apply (simp add: Babs_def) |
336 using a apply (simp add: Babs_def) |
337 apply (simp add: in_respects) |
337 apply (simp add: in_respects) |
338 using Quotient_rel[OF q] |
338 using Quotient_rel[OF q] |
339 by metis |
339 by metis |
340 |
340 |
|
341 lemma babs_prs: |
|
342 assumes q1: "Quotient R1 Abs1 Rep1" |
|
343 and q2: "Quotient R2 Abs2 Rep2" |
|
344 shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f" |
|
345 apply(rule eq_reflection) |
|
346 apply(rule ext) |
|
347 apply simp |
|
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]) |
|
350 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
|
351 done |
|
352 |
341 (* needed for regularising? *) |
353 (* needed for regularising? *) |
342 lemma babs_reg_eqv: |
354 lemma babs_reg_eqv: |
343 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
355 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
344 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
356 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
345 |
|
346 |
357 |
347 (* 2 lemmas needed for cleaning of quantifiers *) |
358 (* 2 lemmas needed for cleaning of quantifiers *) |
348 lemma all_prs: |
359 lemma all_prs: |
349 assumes a: "Quotient R absf repf" |
360 assumes a: "Quotient R absf repf" |
350 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
361 shows "Ball (Respects R) ((absf ---> id) f) = All f" |