327 |
327 |
328 (* Not used *) |
328 (* Not used *) |
329 lemma REP_ABS_RSP_LEFT: |
329 lemma REP_ABS_RSP_LEFT: |
330 assumes q: "QUOTIENT R Abs Rep" |
330 assumes q: "QUOTIENT R Abs Rep" |
331 and a: "R x1 x2" |
331 and a: "R x1 x2" |
332 and "R (Rep (Abs x1)) x2" |
|
333 shows "R x1 (Rep (Abs x2))" |
332 shows "R x1 (Rep (Abs x2))" |
334 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q]) |
333 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) |
335 |
334 |
336 (* ----------------------------------------------------- *) |
335 (* ----------------------------------------------------- *) |
337 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
336 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
338 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
337 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
339 (* ----------------------------------------------------- *) |
338 (* ----------------------------------------------------- *) |
380 and q2: "QUOTIENT R2 Abs2 Rep2" |
379 and q2: "QUOTIENT R2 Abs2 Rep2" |
381 shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))" |
380 shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))" |
382 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto |
381 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto |
383 |
382 |
384 (* ask peter: no use of q1 q2 *) |
383 (* ask peter: no use of q1 q2 *) |
|
384 (* Cez: I can answer, |
|
385 In the following theorem R2 can be instantiated with anything, |
|
386 but we know some of the types of the Rep and Abs functions; |
|
387 so by solving QUOTIENT assumptions we can get a unique R2 that |
|
388 will be provable; which is why we need to use APPLY_RSP1 *) |
385 lemma APPLY_RSP: |
389 lemma APPLY_RSP: |
386 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
390 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
387 and q2: "QUOTIENT R2 Abs2 Rep2" |
391 and q2: "QUOTIENT R2 Abs2 Rep2" |
388 and a: "(R1 ===> R2) f g" "R1 x y" |
392 and a: "(R1 ===> R2) f g" "R1 x y" |
389 shows "R2 (f x) (g y)" |
393 shows "R2 (f x) (g y)" |
|
394 using a by (rule FUN_REL_IMP) |
|
395 |
|
396 lemma APPLY_RSP1: |
|
397 assumes q: "QUOTIENT R1 Abs1 Rep1" |
|
398 and a: "(R1 ===> R2) f g" "R1 x y" |
|
399 shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)" |
390 using a by (rule FUN_REL_IMP) |
400 using a by (rule FUN_REL_IMP) |
391 |
401 |
392 lemma APPLY_RSP2: |
402 lemma APPLY_RSP2: |
393 assumes a: "(R1 ===> R2) f g" "R1 x y" |
403 assumes a: "(R1 ===> R2) f g" "R1 x y" |
394 shows "R2 (f x) (g y)" |
404 shows "R2 (f x) (g y)" |