Re: [isabelle] Variable sharing



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

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,
>        Florian
>
> --
>
> Home:
> http://www.in.tum.de/~haftmann
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>





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