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 absf repf" |
|
478 shows "\<And>f g. (R ===> (op =)) f g ==> |
477 shows "\<And>f g. (R ===> (op =)) f g ==> |
479 (Ball (Respects R) f = Ball (Respects R) g)" |
478 (Ball (Respects R) f = Ball (Respects R) g)" |
480 sorry |
479 apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS) |
|
480 done |
481 |
481 |
482 end |
482 end |
483 |
483 |