equal
deleted
inserted
replaced
484 shows "\<And>f g. (R ===> (op =)) f g ==> |
484 shows "\<And>f g. (R ===> (op =)) f g ==> |
485 (Bex (Respects R) f = Bex (Respects R) g)" |
485 (Bex (Respects R) f = Bex (Respects R) g)" |
486 apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS) |
486 apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS) |
487 done |
487 done |
488 |
488 |
489 (* TODO: |
489 |
490 - [FORALL_PRS, EXISTS_PRS, COND_PRS]; |
|
491 > val it = |
|
492 [|- !R abs rep. |
|
493 QUOTIENT R abs rep ==> |
|
494 !f. $! f <=> RES_FORALL (respects R) ((abs --> I) f), |
|
495 |- !R abs rep. |
|
496 QUOTIENT R abs rep ==> |
|
497 !f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f), |
|
498 *) |
|
499 lemma FORALL_PRS: |
490 lemma FORALL_PRS: |
500 assumes a: "QUOTIENT R absf repf" |
491 assumes a: "QUOTIENT R absf repf" |
501 shows "All f = Ball (Respects R) ((absf ---> id) f)" |
492 shows "All f = Ball (Respects R) ((absf ---> id) f)" |
502 using a |
493 using a |
503 unfolding QUOTIENT_def |
494 unfolding QUOTIENT_def |
511 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def) |
502 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def) |
512 |
503 |
513 lemma COND_PRS: |
504 lemma COND_PRS: |
514 assumes a: "QUOTIENT R absf repf" |
505 assumes a: "QUOTIENT R absf repf" |
515 shows "(if a then b else c) = absf (if a then repf b else repf c)" |
506 shows "(if a then b else c) = absf (if a then repf b else repf c)" |
516 using a |
507 using a unfolding QUOTIENT_def by auto |
517 unfolding QUOTIENT_def |
|
518 sorry |
|
519 |
508 |
520 (* These are the fixed versions, general ones need to be proved. *) |
509 (* These are the fixed versions, general ones need to be proved. *) |
521 lemma ho_all_prs: |
510 lemma ho_all_prs: |
522 shows "op = ===> op = ===> op = All All" |
511 shows "op = ===> op = ===> op = All All" |
523 by auto |
512 by auto |