[isabelle-dev] Order of sublocale declarations

[Amine Chaieb]

Hi Andreas, T

his is of great help. Thank you, especially for the rewriting hint. I 
was thinking modulo that equation.

This solves my concrete problem, but I am still intrigued by the 
behaviour and its reasons.

Amine.

On 01/31/2013 03:21 PM, Andreas Lochbihler wrote:
> 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
>>