Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] interpretation of a locale in a locale

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

From: Clemens Ballarin <ballarin@in.tum.de>
On 12 Sep 2008, at 0:44, David Streader wrote:

I have read the isabelle/isar reference manual

Good. We appreciate that ;-)

but thing are are still not clear. What does sentence:
"Using defined parameters in {\it name} one may achieve an
effect similar to instantiation, though"
, in second paragraph on interpretation, mean?

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

Hope this helps,

Clemens

Last updated: May 03 2024 at 08:18 UTC