equal
deleted
inserted
replaced
515 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
515 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
516 and b: "Bex R P" |
516 and b: "Bex R P" |
517 shows "Bex R Q" |
517 shows "Bex R Q" |
518 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
518 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
519 |
519 |
|
520 lemma ball_all_comm: |
|
521 "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
|
522 by auto |
|
523 |
|
524 lemma bex_ex_comm: |
|
525 "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
|
526 by auto |
520 |
527 |
521 |
528 |
522 |
529 |
523 (* TODO: Add similar *) |
530 (* TODO: Add similar *) |
524 lemma RES_FORALL_RSP: |
531 lemma RES_FORALL_RSP: |