Hi Haitao, I’m glad you figured out sg and metis_tac as a solution to this, but of course, you’re right that this can be tedious. One of the most precise way of attacking this is to use a tactic like drule, and to select assumptions with the various _assum combinators (first_assum, last_assum, qpat_x_assum, etc). See the section on tactics for manipulating assumptions in the DESCRIPTION manual, and also the REFERENCE manual.
If I had exactly your situation, I might try something like first_assum drule This looks for the first assumption that can be successfully passed to drule, and then applies the effect of drule when applied to that assumption. In turn, drule th looks for the first assumption that can be combined (using MATCH_MP) with th. The result is then passed to mp_tac. If you want a different continuation, you can use drule_then. I hope this is helpful. Best wishes, Michael From: Haitao Zhang <zhtp...@gmail.com> Date: Tuesday, 26 February 2019 at 09:12 To: hol-info <hol-info@lists.sourceforge.net> Subject: [Hol-info] Working with assumptions Hi, I just started HOL and am really enjoying it quite a bit. One difficulty I find during interactive tactic proof sessions is to get hold of and manipulate assumptions. Right now I find myself using sg to write new subgoals and then metis_tac[] to prove the baby steps that could be easily proved with MP if I know how to select an assumption to apply to another. Is this difficulty by design? Should I be writing sml code instead of going with existing tactics? Concrete example: if assumption #n1 says a -> b and assumption #n2 says a how can I add b to the assumptions? Of course it may be a little more complicated as #n1 may be !x. a -> c /\ d /\ b and I may only want b. Thanks, Haitao Zhang
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
