Re: [isabelle] Variable sharing
But what if I have two locales that contradict with each other, i.e.
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?
On Thu, Mar 18, 2010 at 11:23 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi John,
>> 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?
> 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,
> PGP available:
This archive was generated by a fusion of
Pipermail (Mailman edition) and