The behaviour of PAT_ASSUM is described in the REFERENCE manual. In short, it uses higher order pattern matching to do the match. The pattern can be as detailed as you like and all variables that aren’t already “local constants” in the goal can be instantiated.
Michael From: Haitao Zhang <zhtp...@gmail.com> Date: Wednesday, 27 February 2019 at 15:23 To: hol-info <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] Working with assumptions 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<mailto: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
