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

Hi Peter,

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.
This sounds like the theory A and some of its descendents form some kind of module, so I would suggest to set up a theory file of its own which specifies the canonical entry point. Inside this "interface" theory, you can hide all "internal" constants as with hide_const (open). If you want to access the constants unqualified, you just have to do this in a theory whose imports bypass the interface theory. However, this does not solve the problem of having to explicitly hide every internal constant.

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.
Note that the interpretation is executed only once, i.e. if you later add definitions/code equations to locale A, they will not be carried through the interpretation automatically. And, AFAIK, there is no way to force a re-interpretation of A. If you want to go that way, I recommend that you do your code generator setup manually by declaring all necessary equations OUTSIDE the locale context as [code].

Am I on the right track? Is there a simpler solution?
If the constant that gets hidden is not visible at the point where the other constant of the same name is defined, you could exploit the order of theory merges. But this can make your developments very fragile and possibly hard to maintain. Here is an example:

theory Foo imports Plain begin
definition foldl :: "nat" where "foldl = 0"

theory Bar imports Main Foo begin
-- "foldl now refers to Foo.foldl"

theory Bar2 imports Foo Main begin
-- "foldl now refers to List.foldl"

Another option is to abuse notation, which also allows to unhide the constant again:

theory Foo imports Main begin
definition foldl :: "nat" where "foldl = 0"

notation List.foldl ("foldl")
term "foldl" -- "List.foldl"

no_notation List.fold ("foldl")
term "foldl" -- "Foo.foldl"


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Gebäude 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-8352
Fax: +49 721 608-8457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft

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