equal
deleted
inserted
replaced
258 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" |
258 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" |
259 -- {* Normally the best argument order: @{prop "P x"} constrains the |
259 -- {* Normally the best argument order: @{prop "P x"} constrains the |
260 choice of @{prop "x:A"}. *} |
260 choice of @{prop "x:A"}. *} |
261 by (unfold Bex_def) blast |
261 by (unfold Bex_def) blast |
262 |
262 |
263 lemma rev_bexI: "x:A ==> P x ==> EX x:A. P x" |
263 lemma rev_bexI [intro?]: "x:A ==> P x ==> EX x:A. P x" |
264 -- {* The best argument order when there is only one @{prop "x:A"}. *} |
264 -- {* The best argument order when there is only one @{prop "x:A"}. *} |
265 by (unfold Bex_def) blast |
265 by (unfold Bex_def) blast |
266 |
266 |
267 lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x" |
267 lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x" |
268 by (unfold Bex_def) blast |
268 by (unfold Bex_def) blast |