equal
deleted
inserted
replaced
387 |
387 |
388 |
388 |
389 (******************************************) |
389 (******************************************) |
390 (* REST OF THE FILE IS UNUSED (until now) *) |
390 (* REST OF THE FILE IS UNUSED (until now) *) |
391 (******************************************) |
391 (******************************************) |
|
392 |
|
393 (* Always safe to apply, but not too helpful *) |
|
394 lemma app_prs2: |
|
395 assumes q1: "Quotient R1 abs1 rep1" |
|
396 and q2: "Quotient R2 abs2 rep2" |
|
397 shows "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)" |
|
398 unfolding expand_fun_eq |
|
399 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
|
400 by simp |
|
401 |
392 lemma Quotient_rel_abs: |
402 lemma Quotient_rel_abs: |
393 assumes a: "Quotient E Abs Rep" |
403 assumes a: "Quotient E Abs Rep" |
394 shows "E r s \<Longrightarrow> Abs r = Abs s" |
404 shows "E r s \<Longrightarrow> Abs r = Abs s" |
395 using a unfolding Quotient_def |
405 using a unfolding Quotient_def |
396 by blast |
406 by blast |