Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Definition in locales and interpretation acros...

Email Gateway (Aug 18 2022 at 11:21):

From: Andreas Lochbihler <lochbihl@infosun.fim.uni-passau.de>
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

Email Gateway (Aug 18 2022 at 11:22):

From: Clemens Ballarin <ballarin@in.tum.de>
Dear Andreas,

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.

due to the operational nature of locales, this does not work. I
agree, though, that it would be desireable to have such a form of
behaviour in the future.

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?

You cannot change an ancestor theory, and TestD only sees one locale
"loc". You can either move the interpretation to TestA or TestD, or
declare the missing interpreted theorems from TestB in TestD manually.

Clemens

Last updated: May 03 2024 at 04:19 UTC