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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
