equal
deleted
inserted
replaced
493 QUOTIENT R abs rep ==> |
493 QUOTIENT R abs rep ==> |
494 !f. $! f <=> RES_FORALL (respects R) ((abs --> I) f), |
494 !f. $! f <=> RES_FORALL (respects R) ((abs --> I) f), |
495 |- !R abs rep. |
495 |- !R abs rep. |
496 QUOTIENT R abs rep ==> |
496 QUOTIENT R abs rep ==> |
497 !f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f), |
497 !f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f), |
498 |- !R abs rep. |
|
499 QUOTIENT R abs rep ==> |
|
500 !a b c. (if a then b else c) = abs (if a then rep b else rep c)] : |
|
501 *) |
498 *) |
502 lemma FORALL_PRS: |
499 lemma FORALL_PRS: |
503 assumes a: "QUOTIENT R absf repf" |
500 assumes a: "QUOTIENT R absf repf" |
504 shows "All f = Ball (Respects R) ((absf ---> id) f)" |
501 shows "All f = Ball (Respects R) ((absf ---> id) f)" |
505 using a |
502 using a |
510 assumes a: "QUOTIENT R absf repf" |
507 assumes a: "QUOTIENT R absf repf" |
511 shows "Ex f = Bex (Respects R) ((absf ---> id) f)" |
508 shows "Ex f = Bex (Respects R) ((absf ---> id) f)" |
512 using a |
509 using a |
513 unfolding QUOTIENT_def |
510 unfolding QUOTIENT_def |
514 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def) |
511 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def) |
515 |
512 |
516 lemma ho_all_prs: |
513 lemma COND_PRS: |
|
514 assumes a: "QUOTIENT R absf repf" |
|
515 shows "(if a then b else c) = absf (if a then repf b else repf c)" |
|
516 using a |
|
517 unfolding QUOTIENT_def |
|
518 sorry |
|
519 |
|
520 (* These are the fixed versions, general ones need to be proved. *) |
|
521 lemma ho_all_prs: |
517 shows "op = ===> op = ===> op = All All" |
522 shows "op = ===> op = ===> op = All All" |
518 by auto |
523 by auto |
519 |
524 |
520 lemma ho_ex_prs: |
525 lemma ho_ex_prs: |
521 shows "op = ===> op = ===> op = Ex Ex" |
526 shows "op = ===> op = ===> op = Ex Ex" |