I have used the tactics POP_ASSUM (K ALL_TAC).
It has deleted thevery last assumption from the assumption list, which I was
required.
The other tactical are also useful in their own context for me which are
provided by Romana and mentioned by Bill as well.
Many thanks Bill & Romana...
--
Regards
Adnan
On Friday, February 14, 2014 6:12 PM, Bill Richter
<[email protected]> 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
------------------------------------------------------------------------------
Managing the Performance of Cloud-Based Applications
Take advantage of what the Cloud has to offer - Avoid Common Pitfalls.
Read the Whitepaper.
http://pubads.g.doubleclick.net/gampad/clk?id=121054471&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
