471 lemma RIGHT_RES_EXISTS_REGULAR: |
471 lemma RIGHT_RES_EXISTS_REGULAR: |
472 assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))" |
472 assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))" |
473 shows "Ex P \<Longrightarrow> Bex R Q" |
473 shows "Ex P \<Longrightarrow> Bex R Q" |
474 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
474 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
475 |
475 |
|
476 (* TODO: Add similar *) |
476 lemma RES_FORALL_RSP: |
477 lemma RES_FORALL_RSP: |
477 shows "\<And>f g. (R ===> (op =)) f g ==> |
478 shows "\<And>f g. (R ===> (op =)) f g ==> |
478 (Ball (Respects R) f = Ball (Respects R) g)" |
479 (Ball (Respects R) f = Ball (Respects R) g)" |
479 apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS) |
480 apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS) |
480 done |
481 done |
481 |
482 |
|
483 (* TODO: |
|
484 - [FORALL_PRS, EXISTS_PRS, COND_PRS]; |
|
485 > val it = |
|
486 [|- !R abs rep. |
|
487 QUOTIENT R abs rep ==> |
|
488 !f. $! f <=> RES_FORALL (respects R) ((abs --> I) f), |
|
489 |- !R abs rep. |
|
490 QUOTIENT R abs rep ==> |
|
491 !f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f), |
|
492 |- !R abs rep. |
|
493 QUOTIENT R abs rep ==> |
|
494 !a b c. (if a then b else c) = abs (if a then rep b else rep c)] : |
|
495 *) |
|
496 lemma FORALL_PRS: |
|
497 assumes a: "QUOTIENT R absf repf" |
|
498 shows "!f. All f = Ball (Respects R) ((absf ---> id) f)" |
|
499 sorry |
|
500 |
|
501 |
482 end |
502 end |
483 |
503 |