466 and b: "Bex R P" |
466 and b: "Bex R P" |
467 shows "Bex R Q" |
467 shows "Bex R Q" |
468 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
468 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
469 |
469 |
470 lemma LEFT_RES_FORALL_REGULAR: |
470 lemma LEFT_RES_FORALL_REGULAR: |
471 assumes a: "!x. (R x \<and> (Q x --> P x))" |
471 assumes a: "\<And>x. (R x \<and> (Q x \<longrightarrow> P x))" |
472 shows "Ball R Q --> All P" |
472 shows "Ball R Q \<longrightarrow> All P" |
473 using a |
473 using a |
474 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
474 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
475 done |
475 done |
476 |
476 |
477 lemma RIGHT_RES_FORALL_REGULAR: |
477 lemma RIGHT_RES_FORALL_REGULAR: |
478 assumes a: "\<And>x :: 'a. (R x \<Longrightarrow> P x \<longrightarrow> Q x)" |
478 assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x" |
479 shows "All P \<longrightarrow> Ball R Q" |
479 shows "All P \<longrightarrow> Ball R Q" |
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 \<Longrightarrow> Q x \<longrightarrow> P x)" |
485 assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x" |
486 shows "Bex R Q \<longrightarrow> 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 \<longrightarrow> Q x))" |
490 assumes a: "\<And>x. (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: |