equal
deleted
inserted
replaced
305 |
305 |
306 lemma REP_ABS_RSP: |
306 lemma REP_ABS_RSP: |
307 assumes q: "QUOTIENT R Abs Rep" |
307 assumes q: "QUOTIENT R Abs Rep" |
308 and a: "R x1 x2" |
308 and a: "R x1 x2" |
309 shows "R x1 (Rep (Abs x2))" |
309 shows "R x1 (Rep (Abs x2))" |
310 using a |
310 and "R (Rep (Abs x1)) x2" |
311 by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) |
311 proof - |
|
312 show "R x1 (Rep (Abs x2))" |
|
313 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) |
|
314 next |
|
315 show "R (Rep (Abs x1)) x2" |
|
316 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q]) |
|
317 qed |
312 |
318 |
313 (* ----------------------------------------------------- *) |
319 (* ----------------------------------------------------- *) |
314 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
320 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
315 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
321 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
316 (* ----------------------------------------------------- *) |
322 (* ----------------------------------------------------- *) |