Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Multiple locale instantiations with same argum...

Email Gateway (Aug 19 2022 at 11:52):

From: Joachim Breitner <mail@joachim-breitner.de>
Dear list,

my understanding of locales is still limited, but this seems fishy to me
(and if it is not I’m looking forward to improve my understanding of
locales).

In this theory, the line "term b.foo" says
Undeclared constant: "b.foo"
which I find surprising:

theory A imports Main begin

locale A =
fixes b :: bool
begin
definition "foo = b"
end

interpretation a: A True.
term a.foo

interpretation b: A True.
term b.foo

end

It must be related to the locale parameter, as it works for
interpretation b: A False.
and does not work if I remove the fixes from the definition of A.

Thanks,
Joachim
signature.asc

Email Gateway (Aug 19 2022 at 11:53):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Joachim,

You have stumbled across Clemens' round-up algorithm for locales described in [1].
Interpretations omits to generate declarations from a locale and parameter instantiation P
if the context already contains an interpretation with parameter instantiations Q that
subsume P. Subsumption means that there is a substitution S of free variables such that P
= S(Q). As the round-up algorithm ignores name prefixes, your second interpretation of A
does not register the constant foo under b.foo, because a.foo is already available.

The same happens if you generalise the first interpretation:

interpretation a!: A b for b .
term a.foo

interpretation b!: A True .
term b.foo (* b.foo does not exist *)

It does not happen if you reverse the order, because the first interpretation no longer
subsumes the second.

interpretation a!: A True .
term a.foo

interpretation b!: A b for b .
term b .foo

A related discussion has been on this list already in February 2013:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-February/msg00076.html

Best,
Andreas

[1] Clemens Ballarin: Locales: A Module System for Mathematical Theories. Journal of
Automated Reasoning, 2013. http://link.springer.com/article/10.1007%2Fs10817-013-9284-7

Last updated: Apr 23 2024 at 04:18 UTC