[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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and