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.