[isabelle-dev] Order of sublocale declarations

[Andreas Lochbihler]

Hi Amine,

let's look at what happens:

A defines the constant local.fpower as "A.fpower f"
AB inherits it from A, i.e., we have "local.fpower == A.fpower f" (1)
B < A "d g" produces "local.fpower == A.fpower (d g)"
AB < B "d f" inherits this as "local.fpower == A.fpower (d (d f))" (2)

As the locale infrastructure does not know about "d (d f) = f", it 
considers two different declarations of local.fpower from (1) and (2) as 
not being the same and therefore tries to declare both of them - which 
the local context infrastructure rejects.

You can either use prefixes to disambiguate local.fpower like in 
sublocale AB < b!: B "d f"
This gives you (1) and "local.b.fpower == A.fpower (d (d f))".
Or, tell the locale infrastructure to rewrite "d (d f) = f":

sublocale AB < B "d f" where "d (d f) == f"

The second approach only works if you order the sublocale declarations 
like in your second case. I do not know why, but I believe it has 
technical reasons; Clemens might be able to tell you more.

Andreas

On 01/31/2013 02:56 PM, Amine Chaieb wrote:
> Thanks Andreas. Does this mean that this sublocale scenario is
> prohibited? And if so, is it due to technical reasons or is there a
> fundamental problem here?
>
> Amine.
>
> On 01/31/2013 02:04 PM, Andreas Lochbihler wrote:
>> Hi Amine,
>>
>> the error message in the second case is only delayed: You get it, once
>> you open the AB context again (context AB begin). In the first case,
>> it shows up immediately, because the sublocale command already
>> constructs the context AB enriched with B.
>>
>> Best,
>> Andreas
>