Email Gateway (Aug 22 2022 at 16:36): Email Gateway (Aug 22 2022 at 16:36):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
In the attached (minimized) theory, I have the following setup:
there are two locales, "infinite" and "permutation_type"; the latter
defines a constant "eqvt".
"permutation_type" is a sublocale of "infinite" in two different
ways; the corresponding sublocales are named "atom_pt" and "bool_pt".
Everything works fine so far; the locale "permutation_type" is
instantiated twice, and both "atom_pt.eqvt" and "bool_pt.eqvt" are
available.
However, when leaving the context and entering it again, only
"atom_pt.eqvt" is restored; "bool_pt.eqvt" is no longer accessible.
Is this behavior expected? It doesn't fit into my mental model of how
sublocales are supposed to work.
I've observed this with Isabelle 2017, but a7de81d847b0 does the same.
Cheers,
Bertram
Background: This example is based on the "Renaming" theory in IsaFoR,
which is itself an adaptation of notions from HOL-Nominal2. In its
current version, the fact that there are infinitely atoms is modelled
by a type class (called "infinite"). The problem I described above
arose in an attempt to change the type class into a locale; in order
for this to work, a number of top-level interpretations that use a kind
constraint "'a :: infinite" (including "atom_pt" and "bool_pt") would
have to become sublocales of "infinite".
R.thy
Email Gateway (Aug 22 2022 at 16:36):From: Clemens Ballarin <ballarin@in.tum.de>
You are bitten by cyclic dependencies between infinite and
permutation_type. This is the sublocale graph:
infinite --> permutation_type
permutation_type --> infinite (qualifier atom_pt)
permutation_type --> infinite (qualifier bool_pt)
Activation of infinite yields these locale instances:
atom_pt.bool_pt : permutation_type "permute_bool"
atom_pt : infinite "()"
atom_pt : permutation_type "permute_atom"
infinite "bar"
and you will see that
term "atom_pt.bool_pt.eqvt"
is defined; perhaps not the way you want it, though.
You probably want to make a clone of one of the involved locales, say
locale meaningful_name = infinite
to break the cycles.
Clemens
Last updated: May 06 2024 at 20:16 UTC