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,
and then use simp_tac bool_ss [] to strip away the conditions that are
dischargable. This is useful when a theorem is used multiple times and
there are multiple assumptions that can be used to instantiate the theorem.


On Wed, Mar 6, 2019 at 4:16 PM Haitao Zhang <> wrote:

> 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 implicants.
> Also it appears that drule_all does not check if the theorem is proved and
> leaves ``P ==> P`` as a goal.
> Haitao
hol-info mailing list

Reply via email to