equal
deleted
inserted
replaced
254 assumes a: "equivp R2" |
254 assumes a: "equivp R2" |
255 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))" |
255 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))" |
256 apply(rule iffI) |
256 apply(rule iffI) |
257 apply(rule allI) |
257 apply(rule allI) |
258 apply(drule_tac x="\<lambda>y. f x" in bspec) |
258 apply(drule_tac x="\<lambda>y. f x" in bspec) |
259 apply(simp add: Respects_def in_respects) |
259 apply(simp add: in_respects) |
260 apply(rule impI) |
260 apply(rule impI) |
261 using a equivp_reflp_symp_transp[of "R2"] |
261 using a equivp_reflp_symp_transp[of "R2"] |
262 apply(simp add: reflp_def) |
262 apply(simp add: reflp_def) |
263 apply(simp) |
263 apply(simp) |
264 apply(simp) |
264 apply(simp) |
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 (* needed for regularising? *) |
|
342 lemma babs_reg_eqv: |
|
343 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
|
344 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
|
345 |
|
346 |
341 (* 2 lemmas needed for cleaning of quantifiers *) |
347 (* 2 lemmas needed for cleaning of quantifiers *) |
342 lemma all_prs: |
348 lemma all_prs: |
343 assumes a: "Quotient R absf repf" |
349 assumes a: "Quotient R absf repf" |
344 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
350 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
345 using a unfolding Quotient_def |
351 using a unfolding Quotient_def |