Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question about locales

Email Gateway (Aug 18 2022 at 12:25):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,

I have defined a locale

locale concept1 = fixes a b assumes ...

and another locale

locale L =
fixes x
begin
definition aa where ...
definition bb where ...
end

Now, aa and bb in L model concept1. However, writing

context L
begin
interpretation concept1[aa bb]
end

does not work. Neither does:
interpretation L \<subseteq> concept1[aa bb]
the latter one does not bind the aa and bb to their definitions in L,
but introduces them as fresh variables.

How can I achieve to make available all stuff proven in concept1 in
locale L for aa and bb ?

Regards,
Peter

Email Gateway (Aug 18 2022 at 12:26):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi Peter,

context L
begin
interpretation concept1[aa bb]
end

does not work. Neither does:
interpretation L \<subseteq> concept1[aa bb]

Neither of these, although desirable, are supported by the current
implementation. In particular, note that on the rhs of \<subseteq>
you may only have a locale expression. Square brackets are not
supported.

I quote from an earlier message on this list, which explains how to
deal with such a sitution.

Here is an example. Assume that you have a locale for rings (for
simplicity, all operations of the ring are bundled in a singe
parameter R):

locale ring = fixes R assumes ...

and a constructor for polynomials Poly, which takes R to its
polynomial ring. You cannot have

interpretation ring < ring "Poly R"

since the right side is not a locale expression. Instead the
comment suggests the following: extend ring

locale poly_ring = ring + fixes P defines "P == Poly R"

and now you can make the interpretation

interpretation poly_ring < ring P

Clemens

Last updated: May 03 2024 at 12:27 UTC