If you really need to instantiate a theorem by hand, using Q.SPEC_THEN and
Q.ISPEC_THEN is usually better. The first is also available under the name
qspec_then.
E.g., you can do
qspec_then `a` mp_tac mytheorem
If you need to do lots of specialisations you can use the list forms:
qspecl_
I think I really like how drule and drule_all work, but is there something
that walks the middle road? I mean drule only discharges one condition; and
drule_all needs all conditions to be discharged. It would be nice to have a
drule that discharges as many as possible and leave the rest as implican
Thanks qspecl_then and friends are great! Sometimes it is easier to be more
specific.
Haitao
On Wed, Mar 6, 2019 at 1:46 AM wrote:
> If you really need to instantiate a theorem by hand, using Q.SPEC_THEN and
> Q.ISPEC_THEN is usually better. The first is also available under the name
> qspec_t
Another thing I noticed about drule* and I believe irule as well is that
they treat free variables as universally quantified so they don't conserve
prior specialization. The idiom I found to work around it is to qspecl_then
[list of specialization] mp_tac thm to get new goal as thm ==> old goal,
an
