On 18 Dec 2013, at 04:21, Michael Norrish wrote:
> On 18/12/13 14:56, Bill Richter wrote:
>> I tried something like this when you first posted, but I didn't think to use
>> dest_comb. Do you have any general tips on how to recognize a term as say a
>> combination (which worked here) on an abstraction (not here)?
>
> Try using a match-expression:
>
> match tm with
> Var(_,_) -> "it's a var"
> | Const(_,_) -> "it's a const"
> | Comb(_,_) -> "it's an application"
> | Abs(_,_) -> "it's an abstraction"
>
> You can also use the helper functions is_comb, is_abs, is_const, and is_var.
>
That is of course the right approach if you are actually programming rather
than just
playing around interactively. If you are looking at the pretty-printed term
that you
want to destroy, then you should be able to see at a glance what to do (assuming
HOL4 and HOL Light are like ProofPower-HOL}, since in ProofPower-HOL, at least,
lambda-abstractions are never pretty-printed as anything other than
lambda-abstractions.
lambda-abstractions where the "bound variable" is actually several variables
combined
with a comma (like \(x, y).x + y) are actually applications (\(x, y). x + y is
really Uncurry(\x y. x + y)).
So, if you are just interactively picking terms apart then the rule is use
dest_comb
(actually called dest_app in ProofPower) unless the thing pretty--prints as a
single
variable or constant or as "\v ..." where v is a plain variable.
Regards,
Rob.
------------------------------------------------------------------------------
Rapidly troubleshoot problems before they affect your business. Most IT
organizations don't have a clear picture of how application performance
affects their revenue. With AppDynamics, you get 100% visibility into your
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
