Re: [isabelle] Properties on intervals
On Tuesday 06 February 2007 14:31, 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.
beware that your lemma might not quite capture what you had in mind. From
ALL u. (u::real) <= 0 & ~ leaking (u + t)
you can show e.g.
(1::real) <= 0,
so your first premise already entails "False", not using the fact that
"leaking t" (or the "leaking" predicate at all).
Maybe you want to replace "&" (conjunction) by "-->" (implication) above, but
that's just a quick guess.
This archive was generated by a fusion of
Pipermail (Mailman edition) and