equal
deleted
inserted
replaced
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 lemma RES_FORALL_RSP: |
|
477 assumes a: "QUOTIENT R abs rep" |
|
478 shows "\<And>f g. (R ===> (op =)) f g ==> |
|
479 (Ball (Respects R) f = Ball (Respects R) g)" |
|
480 sorry |
|
481 |
476 end |
482 end |
477 |
483 |