[isabelle-dev] Order of sublocale declarations
andreas.lochbihler at inf.ethz.ch
Thu Jan 31 15:21:03 CET 2013
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