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.
Haitao On Wed, Mar 6, 2019 at 4:16 PM Haitao Zhang <zhtp...@gmail.com> 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
