[isabelle] Question about functions with equal names defined in different theories



Hi all.

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 forgetting one). 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, ...
 end
 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?


Best,
 Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.