equal
deleted
inserted
replaced
480 using a |
480 using a |
481 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
481 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
482 done |
482 done |
483 |
483 |
484 lemma LEFT_RES_EXISTS_REGULAR: |
484 lemma LEFT_RES_EXISTS_REGULAR: |
485 assumes a: "!x :: 'a. (R x --> Q x --> P x)" |
485 assumes a: "!x :: 'a. (R x \<Longrightarrow> Q x \<longrightarrow> P x)" |
486 shows "Bex R Q ==> Ex P" |
486 shows "Bex R Q \<longrightarrow> Ex P" |
487 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
487 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
488 |
488 |
489 lemma RIGHT_RES_EXISTS_REGULAR: |
489 lemma RIGHT_RES_EXISTS_REGULAR: |
490 assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))" |
490 assumes a: "!x :: 'a. (R x \<and> (P x \<longrightarrow> Q x))" |
491 shows "Ex P \<Longrightarrow> Bex R Q" |
491 shows "Ex P \<longrightarrow> Bex R Q" |
492 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
492 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
493 |
493 |
494 (* TODO: Add similar *) |
494 (* TODO: Add similar *) |
495 lemma RES_FORALL_RSP: |
495 lemma RES_FORALL_RSP: |
496 shows "\<And>f g. (R ===> (op =)) f g ==> |
496 shows "\<And>f g. (R ===> (op =)) f g ==> |