equal
deleted
inserted
replaced
15 (*Easier to apply than someI if witness ?a comes from an EX-formula*) |
15 (*Easier to apply than someI if witness ?a comes from an EX-formula*) |
16 Goal "EX x. P x ==> P (SOME x. P x)"; |
16 Goal "EX x. P x ==> P (SOME x. P x)"; |
17 by (etac exE 1); |
17 by (etac exE 1); |
18 by (etac someI 1); |
18 by (etac someI 1); |
19 qed "someI_ex"; |
19 qed "someI_ex"; |
20 AddXEs [someI_ex]; |
|
21 |
20 |
22 (*Easier to apply than someI: conclusion has only one occurrence of P*) |
21 (*Easier to apply than someI: conclusion has only one occurrence of P*) |
23 val prems = Goal "[| P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"; |
22 val prems = Goal "[| P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"; |
24 by (resolve_tac prems 1); |
23 by (resolve_tac prems 1); |
25 by (rtac someI 1); |
24 by (rtac someI 1); |