POP_ASSUM is working the same.
I'd say the choice between FIRST_X_ASSUM or POP_ASSUM highly depends on
the context: POP_ASSUM is simpler but does not always work of course.
V.
On 14.02.2014 14:29, Ramana Kumar wrote:
You are right, Bill. Thank you. FIRST_X_ASSUM rather than FIRST_ASSUM,
defi
On 14.02.2014 04:39, Bill Richter wrote:
> I guess I understood that REWRITE_TAC used a complicated algorithm in order
> to avoid infinite looping. So I think I didn't express my question very
> well. I tend to think that it's not good coding on my part to rely on
> features that I don't even
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 wrote:
> Ramana, I think it's better to say that the one time
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
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.
On Thu, Feb 13, 2014 at 4:03 AM, Adnan Rashid
[~~ Please disseminate widely within your teams & contacts ~~]
Dear Colleagues,
PERSYVAL-Lab and NASA-JPL are organizing the second edition of the CPS Summer
School. The broad objective of the CPS Summer School is to explore the manifold
relationship between networked embedded systems
Dear all,
I am working in HOL-Light. Can I find any tactics which can be used to delete
the assumptions which are generated during the proof. These assumptions are
used once, and of no need in future.
--
Regards
Adnan---
On 14.02.2014 01:42, Michael Norrish wrote:
> On 13/02/14 04:46, Vincent Aravantinos wrote:
>
>> Then considering leaving the goal unchanged, well it is a matter of taste...
>> I
>> know it is the standard to leave the goal unchanged. But I personally met
>> many
>> buggy situations that I hardly
