equal
deleted
inserted
replaced
333 assumes a: "Quotient R absf repf" |
333 assumes a: "Quotient R absf repf" |
334 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
334 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
335 using a unfolding Quotient_def |
335 using a unfolding Quotient_def |
336 by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) |
336 by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) |
337 |
337 |
|
338 lemma fun_rel_id: |
|
339 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
|
340 shows "(R1 ===> R2) f g" |
|
341 using a by simp |
|
342 |
|
343 lemma quot_rel_rsp: |
|
344 assumes a: "Quotient R Abs Rep" |
|
345 shows "(R ===> R ===> op =) R R" |
|
346 apply(rule fun_rel_id)+ |
|
347 apply(rule equals_rsp[OF a]) |
|
348 apply(assumption)+ |
|
349 done |
|
350 |
338 |
351 |
339 |
352 |
340 |
353 |
341 |
354 |
342 |
355 |