[isabelle] Question about functions with equal names defined in different theories
We have some theory A, that defines, among others, the functions:
foldl, foldr, insert
Inside A, and inside theories extending A, these names make perfectly
sense, and we do not want to change them to, say, "A_foldl".
However, some theories based on A are now to be used a bigger context,
where the details of A (including foldl, etc.) are no longer important.
Nevertheless, the constants remain defined and overwrite the standard
constants from List.thy and Set.thy, which is embarrassing.
What's the right solution to this problem?
I know the hide_const (open) construct, however, its annoying to
explicitly having to list all constants of the theory again (and perhaps
Moreover, if the constants are hidden "too early", its impossible to use
them by unqualified names in theories extending A.
Alternatively, I thought of defining a locale:
locale A_loc begin
definition foldl, foldr, insert, ...
interpretation A: A_loc .
And proving extensions to A inside the locale.
The interpretation is required for code generation, as the code generator
seems not to generate code for "A_loc.foldl", etc.
Am I on the right track? Is there a simpler solution?
This archive was generated by a fusion of
Pipermail (Mailman edition) and