# Re: [isabelle] interpretation of a locale in a locale

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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.