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