[isabelle-dev] Order of sublocale declarations
amine at chaieb.org
Thu Jan 31 15:38:11 CET 2013
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.
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.
> 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?
>> 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.
More information about the isabelle-dev