[isabelle] Properties on intervals



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.