Re: [isabelle] Properties on intervals



Antonio,

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.

Best,
Tjark





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