equal
deleted
inserted
replaced
499 QUOTIENT 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)] : |
500 !a b c. (if a then b else c) = abs (if a then rep b else rep c)] : |
501 *) |
501 *) |
502 lemma FORALL_PRS: |
502 lemma FORALL_PRS: |
503 assumes a: "QUOTIENT R absf repf" |
503 assumes a: "QUOTIENT R absf repf" |
504 shows "!f. All f = Ball (Respects R) ((absf ---> id) f)" |
504 shows "All f = Ball (Respects R) ((absf ---> id) f)" |
505 sorry |
505 using a |
|
506 unfolding QUOTIENT_def |
|
507 by (metis IN_RESPECTS fun_map.simps id_apply) |
506 |
508 |
507 lemma EXISTS_PRS: |
509 lemma EXISTS_PRS: |
508 assumes a: "QUOTIENT R absf repf" |
510 assumes a: "QUOTIENT R absf repf" |
509 shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)" |
511 shows "Ex f = Bex (Respects R) ((absf ---> id) f)" |
510 sorry |
512 using a |
511 |
513 unfolding QUOTIENT_def |
512 lemma ho_all_prs: "op = ===> op = ===> op = All All" |
514 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def) |
513 apply (auto) |
515 |
514 done |
516 lemma ho_all_prs: |
515 |
517 shows "op = ===> op = ===> op = All All" |
516 lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex" |
518 by auto |
517 apply (auto) |
519 |
518 done |
520 lemma ho_ex_prs: |
|
521 shows "op = ===> op = ===> op = Ex Ex" |
|
522 by auto |
519 |
523 |
520 end |
524 end |
521 |
525 |