Email Gateway (Aug 18 2022 at 14:55): Email Gateway (Aug 18 2022 at 14:55):From: munddr@googlemail.com
Hi,
If I have two locales:
locale loc1 =
fixes x::real
assumes "x < 2"
locale loc2 =
fixes y::real
assumes "y < 3"
is there a way to define a proof goal for showing EX x. x < 2 in loc1 and
EX x. x < y in loc2 (as one proof goal)? Does this require some form of
variable sharing?
Thanks
John
Email Gateway (Aug 18 2022 at 14:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
there is no facility to simultaneously prove things in different
locales. If you need such a simultaneous proof, I guess that both
locales are interwoven in a way that one can be interpreted into the
other by means of sublocale.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:55):From: Clemens Ballarin <ballarin@in.tum.de>
Hi John,
You need to define a context (ie locale) that inherits from both.
This can be achieved with locale expressions. I recommend reading the
tutorial (http://isabelle.in.tum.de/dist/Isabelle/doc/locales.pdf),
Section 6. Sharing is achieved by providing suitable locale
instances. In your example, there is no sharing (Parameters x and y
remain distinct.)
Cheers,
Clemens
Email Gateway (Aug 18 2022 at 14:55):From: John Munroe <munddr@googlemail.com>
Hi,
If I have two locales:
locale loc1 =
fixes x::real
assumes "x < 2"
locale loc2 =
fixes y::real
assumes "y < 3"
is there a way to define a proof goal for showing EX x. x < 2 in loc1
and EX x. x < y in loc2 (as one proof goal)? Does this require some
form of variable sharing?
Thanks
John
Email Gateway (Aug 18 2022 at 14:56):From: John Munroe <munddr@googlemail.com>
Thanks.
But what if I have two locales that contradict with each other, i.e.
consts
c::real
locale loc1 =
assumes "c < 2"
locale loc2 =
assumes "c > 2"
If I want to show that there exists a real value such that it is < 2
in loc1 and >2 in loc2, does changing the locale hierarchy with
sublocale enable this type of simultaneous proof? More specifically,
can I specify I want to proof one goal in one locale and another goal
in another, but the two goals are related in some way?
Thanks
John
Last updated: Apr 25 2024 at 04:18 UTC