Re: [isabelle] Sublocales

Dear Holden,

Locales and records are independent, so your setting is not well-specified. However, I suspect that your situation resembles the following.

record 'a a = a_object :: 'a
record ('a, 'b) ab = "'a a" + b_object :: 'b
locale a = fixes r_a :: "'a a"
locale ab = fixes r_b :: "('a, 'b) ab" begin
sublocale a r_b .

Here, the sublocale command fails because r_b has type "(_, _) ab" which is incompatible with type "_ a" as required by locale a. The reason is that the locales use the closed record types "_ a" and "(_, _) ab" instead of the extensible record schemes that the record package uses internally. If you generalise your locales to schemes, it works in this setting:

locale a = fixes r_a :: "('a, 'more) a_scheme"
locale ab = fixes r_b :: "('a, 'b, 'more) ab_scheme" begin
sublocale a r_b .

What happens here is the following: The type parameter 'more from locale a gets instantiated with the extension type ('b, 'more) ab_ext which implements the extension of record type ab over record type a.

Hope this helps,

On 20/08/14 10:49, Holden Lee wrote:

I'm wondering whether it is possible to declare a sublocale when the one of
the records is an extension of the other. Suppose I first define

locale ab_locale

which is based off the record (a_object::'a, b_object::'b), and later
decide it would be useful to have a more general

locale a_locale

which is based off the record (a_object::'a). Could I make ab_object a
sublocale of a_object (here I would just want to set the a_object's equal)?


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