[isabelle] Definition in locales and interpretation across multiple theories
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
Theory TestA defines some locale loc:
theory TestA imports Main begin
locale loc = fixes r :: "'a => bool" begin
Theory TestB extends TestA and adds a definition to loc:
theory TestB imports TestA begin
definition (in loc) bar :: nat where "bar == 0"
Theory TestC extends TestA interprets this locale:
theory TestC imports TestA begin
interpretation foo: loc["%x. True"] .
Theory TestD joins TestB and TestC and queries the definition of bar in
theory TestD imports TestB TestC begin
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and