Email Gateway (Aug 18 2022 at 10:08): Email Gateway (Aug 18 2022 at 10:08):From: Antonio D'Ettole <codazzo@gmail.com>
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
Email Gateway (Aug 18 2022 at 10:08):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
Antonio D'Ettole wrote:
Email Gateway (Aug 18 2022 at 10:08):From: Michael Nedzelsky <MichaelNedzelsky@yandex.ru>
It works:
consts
leaking :: "real ==> bool"
theorem " [| ALL u. u <= 0 & ~ leaking(u + t); leaking t |] ==> False"
proof -
assume A1: "ALL (u::real). u <= 0 & ~ leaking(u + t)"
assume A2: "leaking t"
from A1 have "~leaking (0 + t)" by (blast)
then have L: "~leaking t" by (simp add: real_add_zero_left)
from A2 L show ?thesis by (blast)
qed
Regards,
Michael Nedzelsky
Email Gateway (Aug 18 2022 at 10:09):From: Tjark Weber <tjark.weber@gmx.de>
Antonio,
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
Last updated: May 03 2024 at 12:27 UTC