Email Gateway (Aug 22 2022 at 10:45): Email Gateway (Aug 22 2022 at 10:45):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear locale experts,
Suppose the locale l1 defines one of its parameter using "defines". When another locale l2
imports l1 and tries to instantiate the defined parameter in the locale expression,
Isabelle2015 complains about bad left-hand sides and existing constants. Here is the
minimal (silly) example:
locale l1 =
fixes x y :: nat
defines "y == x"
locale l2 = l1 2 "Suc 1" (* error: Bad head of lhs: existing constant Suc *)
What is the right way to instantiate defined parameters in locale expressions?
Here is some background on my use case. I want to abstract over a monad in some
definitions, so I have a locale for monads (I need the monad operation only on a single
type, so this works). As every monad is also a functor, I can define the map operation
canonically in terms of bind and return. Later, I want to specialise the monad to concrete
instances such as 'a option, which I thought could be done by instantiating the locale
parameters in the locale expression. Of course, I also want to replace all instances of
the canonical map with map_option in all theorems.
If I define the map in the locale for monad as a constant, the replacement has to be done
at every interpretation or sublocale command using a where clause (and a corresponding
proof of equality of definitions). Unfortunately, I have not found a way to do the
replacement during locale imports. Therefore, I tried to use the defines element and move
the definition to the locale declaration itself. But this causes trouble, too.
Andreas
Email Gateway (Aug 22 2022 at 11:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
after having a look of the code (Local_Defs.cert_def in closeup in
expression.ML) I come to the conclusion that the whole machinery assumes
that a »defines« element remains a »defines« element after input -- with
all required syntactic restrictions.
Looks to me that the idea »defines« requires further rethinking here.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 11:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
Thanks for looking into this. Meanwhile, I have found out that instantiating a "defines"
element in a sublocale declaration works. What is the difference between locale
expressions in locale declarations and sublocale commands?
At the moment, I work around this problem as follows:
I refrain from using constants or syntax declared in the locale and refer to the
foundational constants if necessary (just like in times long ago).
After the declaration, I issue a sublocale command to resurrect the input.
Best,
Andreas
Last updated: Apr 26 2024 at 04:17 UTC