[isabelle] Definition in locales and interpretation across multiple theories



Hi all,

I have encountered the following problem with locales and
interpretation. Normally, I would expect that theorems and definitions
which are added to some locale are also immediately available in their
interpretations. However, this does not seem to be the case in the
following example.

Theory TestA defines some locale loc:

theory TestA imports Main begin
locale loc = fixes r :: "'a => bool" begin
end
end

Theory TestB extends TestA and adds a definition to loc:

theory TestB imports TestA begin
definition (in loc) bar :: nat where "bar == 0"
end

Theory TestC extends TestA interprets this locale:

theory TestC imports TestA begin
interpretation foo: loc["%x. True"] .
end

Theory TestD joins TestB and TestC and queries the definition of bar in
the interpretation:

theory TestD imports TestB TestC begin
thm foo.bar_def

which gives that foo.bar_def is an unknown theorem, although
print_locale loc does show it being part of the locale.
Probably, this is due to the diamond inheritance structure with the
theories. But: Is there some way to tell Isabelle in TestD to add
definitions to the locale loc in TestB to the definitions from TestC
except changing the theory dependencies?

Thanks,
Andreas





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