Re: [isabelle] Properties on intervals

It appears you need to provide the instantiation by hand using rule allE. Please consult the tutorial (section 5.9) on how to deal with quantifiers by hand.


Antonio D'Ettole wrote:
I'm trying to show that since a property holds for all values of a
real interval, it has to hold for a particular value in that interval.
Specifically my goal is:

[| ALL u. u <= 0 & ~ leaking (u + t); leaking t |] ==> False

it should follow that since ALL u. u <= 0 & ~ leaking (u + t), it has
to be particularly ~leaking(0+t) and since leaking(t) is in the
assumption, False should entail.
Unfortunately the auto method does not prove this automatically.
I've tried to take a look at the theory files in HOL-Complex but I
couldn't find a suitable theorem.
Does anybody know how to prove this?
Thank you
Antonio D'Ettole

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.