You are right, Bill. Thank you. FIRST_X_ASSUM rather than FIRST_ASSUM,
definitely. In HOL4 POP_ASSUM deletes the assumption, but I'm not sure if
it's the same in HOL Light - perhaps not.
On Fri, Feb 14, 2014 at 1:12 PM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> Ramana, I think it's better to say that the one time you use the
> assumption you should use it with FIRST_X_ASSUM or REMOVE_THEN. You can
> grep through the hol-light sources to get many examples, e.g.
> (poisson)hol_light> grep REMOVE_THEN Multivariate/*
> Let's get on-line help with
>
> # help "FIRST_X_ASSUM";;
> -------------------------------------------------------------------
>
> FIRST_X_ASSUM : thm_tactic -> tactic
>
> SYNOPSIS
>
> Applies theorem-tactic to first assumption possible, extracting assumption.
> [...]
>
> # help "REMOVE_THEN";;
> -------------------------------------------------------------------
>
> REMOVE_THEN : string -> thm_tactic -> tactic
>
> SYNOPSIS
>
> Apply a theorem tactic to named assumption, removing the assumption.
> [...]
>
> # help "LABEL_TAC";;
> gives an example using USE_THEN, which is the same as REMOVE_THEN, except
> that it does not remove the assumption.
>
> You could use some tactical that pulls out an assumption
> (POP_ASSUM, FIND_ASSUM, FIRST_ASSUM, USE_THEN, REMOVE_THEN, etc.)
> and give it a trivial thm_tactic like (K ALL_TAC) to essentially
> ignore (and hence discard) the assumption and do nothing else.
>
> I think this is partly wrong, in that POP_ASSUM, FIRST_ASSUM and USE_THEN
> do not delete assumptions, as Adnan wanted.
>
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> Android apps run on BlackBerry 10
> Introducing the new BlackBerry 10.2.1 Runtime for Android apps.
> Now with support for Jelly Bean, Bluetooth, Mapview and more.
> Get your Android app in front of a whole new audience. Start now.
>
> http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Android apps run on BlackBerry 10
Introducing the new BlackBerry 10.2.1 Runtime for Android apps.
Now with support for Jelly Bean, Bluetooth, Mapview and more.
Get your Android app in front of a whole new audience. Start now.
http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
