Hi Michael, Thanks for your help! I wasn't subscribed to the mailing list so I only saw your response in the mail archive. I have since properly signed up for the list.
I have a question on pattern matching on the assumptions: what is meant by a pattern and where is it defined? Does `!x. P` match all forall binders? Is only top level term matched or does it go into subterms? I am hoping to avoid copying all the assumptions I want into the proof. With regard to pattern matching I have a related question on exists unique quantifiers, which I will ask in a new thread. Thanks! Haitao On Mon, Feb 25, 2019 at 11:09 AM Haitao Zhang <zhtp...@gmail.com> wrote: > 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
