equal
deleted
inserted
replaced
478 shows "\<And>f g. (R ===> (op =)) f g ==> |
478 shows "\<And>f g. (R ===> (op =)) f g ==> |
479 (Ball (Respects R) f = Ball (Respects R) g)" |
479 (Ball (Respects R) f = Ball (Respects R) g)" |
480 apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS) |
480 apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS) |
481 done |
481 done |
482 |
482 |
|
483 lemma RES_EXISTS_RSP: |
|
484 shows "\<And>f g. (R ===> (op =)) f g ==> |
|
485 (Bex (Respects R) f = Bex (Respects R) g)" |
|
486 apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS) |
|
487 done |
|
488 |
483 (* TODO: |
489 (* TODO: |
484 - [FORALL_PRS, EXISTS_PRS, COND_PRS]; |
490 - [FORALL_PRS, EXISTS_PRS, COND_PRS]; |
485 > val it = |
491 > val it = |
486 [|- !R abs rep. |
492 [|- !R abs rep. |
487 QUOTIENT R abs rep ==> |
493 QUOTIENT R abs rep ==> |
496 lemma FORALL_PRS: |
502 lemma FORALL_PRS: |
497 assumes a: "QUOTIENT R absf repf" |
503 assumes a: "QUOTIENT R absf repf" |
498 shows "!f. All f = Ball (Respects R) ((absf ---> id) f)" |
504 shows "!f. All f = Ball (Respects R) ((absf ---> id) f)" |
499 sorry |
505 sorry |
500 |
506 |
|
507 lemma EXISTS_PRS: |
|
508 assumes a: "QUOTIENT R absf repf" |
|
509 shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)" |
|
510 sorry |
|
511 |
501 lemma ho_all_prs: "op = ===> op = ===> op = All All" |
512 lemma ho_all_prs: "op = ===> op = ===> op = All All" |
502 apply (auto) |
513 apply (auto) |
503 done |
514 done |
504 |
515 |
|
516 lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex" |
|
517 apply (auto) |
|
518 done |
|
519 |
505 end |
520 end |
506 |
521 |